Ring orderings

Let R be a commutative ring. We define orderings and preorderings on R as predicates on Subsemiring R.

Definitions

• IsOrdering: an ordering is a subsemiring O such that O ∪ -O = R and the support O ∩ -O of O forms a prime ideal.
• IsPreordering: a preordering is a subsemiring that contains all squares, but not -1.

All orderings are preorderings.

References

• An introduction to real algebra, by T.Y. Lam. Rocky Mountain J. Math. 14(4): 767-814 (1984). lam_1984

class Subsemiring.IsOrdering {R : Type u_1} [CommRing R] (S : Subsemiring R) extends S.toAddSubmonoid.HasMemOrNegMem, S.toAddSubmonoid.support.IsPrime : Prop

An ordering O on a ring R is a subsemiring of R such that O ∪ -O = R and the support O ∩ -O of O forms a prime ideal.

• mem_or_neg_mem (a : R) : a ∈ S.toAddSubmonoid ∨ -a ∈ S.toAddSubmonoid
• ne_top' : S.toAddSubmonoid.support ≠ ⊤
• mem_or_mem' {x y : R} : x * y ∈ S.toAddSubmonoid.support → x ∈ S.toAddSubmonoid.support ∨ y ∈ S.toAddSubmonoid.support

class Subsemiring.IsPreordering {R : Type u_1} [CommRing R] (S : Subsemiring R) : Prop

A preordering on a ring R is a subsemiring of R that contains all squares, but not -1.

• mem_of_isSquare {x : R} (hx : IsSquare x) : x ∈ S
• neg_one_notMem : -1 ∉ S

theorem Subsemiring.mem_of_isSumSq {R : Type u_1} [CommRing R] (S : Subsemiring R) [S.IsPreordering] {x : R} (hx : IsSumSq x) : x ∈ S

theorem Subsemiring.sumSq_le {R : Type u_2} [CommRing R] (S : Subsemiring R) [S.IsPreordering] : sumSq R ≤ S

@[simp]

theorem Subsemiring.mul_self_mem {R : Type u_1} [CommRing R] (S : Subsemiring R) [S.IsPreordering] (x : R) : x * x ∈ S

@[simp]

theorem Subsemiring.pow_two_mem {R : Type u_1} [CommRing R] (S : Subsemiring R) [S.IsPreordering] (x : R) : x ^ 2 ∈ S

theorem Subsemiring.IsPreordering.of_support_neq_top {R : Type u_1} [CommRing R] {S : Subsemiring R} [S.toAddSubmonoid.HasMemOrNegMem] (h : S.toAddSubmonoid.support ≠ ⊤) : S.IsPreordering

instance Subsemiring.instIsPreorderingOfIsOrdering {R : Type u_1} [CommRing R] (S : Subsemiring R) [S.IsOrdering] : S.IsPreordering