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) : 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.

• isSpanning : S.toAddSubmonoid.IsSpanning
• support_ne_top : S.toAddSubmonoid.support ≠ ⊤
• mem_support_or_mem_support {x y : R} : x * y ∈ S.toAddSubmonoid.support → x ∈ S.toAddSubmonoid.support ∨ y ∈ S.toAddSubmonoid.support

instance Subsemiring.instHasIdealSupportOfIsOrdering {R : Type u_1} [CommRing R] (S : Subsemiring R) [i : S.IsOrdering] : S.HasIdealSupport

instance Subsemiring.IsOrdering.support_isPrime {R : Type u_1} [CommRing R] (S : Subsemiring R) [i : S.IsOrdering] : S.support.IsPrime

theorem Subsemiring.IsOrdering.mk' {R : Type u_1} [CommRing R] {S : Subsemiring R} (hS₁ : S.toAddSubmonoid.IsSpanning) (hS₂ : have this := ⋯; S.support.IsPrime) : S.IsOrdering

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} (hS : S.toAddSubmonoid.IsSpanning) (h : have this := ⋯; S.support ≠ ⊤) : S.IsPreordering

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