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, T.Y. Lam][lam_1984]

structure 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

theorem Subsemiring.IsOrdering.isPrime_supportIdeal {R : Type u_1} [CommRing R] {S : Subsemiring R} (hS : S.IsOrdering) : (supportIdeal ⋯).IsPrime

theorem Subsemiring.IsOrdering.of_isPrime_supportIdeal {R : Type u_1} [CommRing R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) (hS₂ : (supportIdeal hS).IsPrime) : S.IsOrdering

structure 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

@[simp]

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

@[simp]

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

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

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

theorem Subsemiring.IsPreordering.of_sumSq_le {R : Type u_1} [CommRing R] {S : Subsemiring R} (hS : sumSq R ≤ S) (h : -1 ∉ S) : S.IsPreordering

theorem Subsemiring.IsPreordering.of_isSpanning {R : Type u_1} [CommRing R] {S : Subsemiring R} (hS : S.toAddSubmonoid.IsSpanning) (h : S ≠ ⊤) : S.IsPreordering

theorem Subsemiring.IsOrdering.isPreordering {R : Type u_1} [CommRing R] {S : Subsemiring R} (hS : S.IsOrdering) : S.IsPreordering

An ordering is a preordering.

@[deprecated Subsemiring.IsPreordering (since := "2026-10-28")]

structure RingPreordering (R : Type u_1) [CommRing R] extends Subsemiring R : Type u_1

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

• carrier : Set R
• mul_mem' {a b : R} : a ∈ (↑self).carrier → b ∈ (↑self).carrier → a * b ∈ (↑self).carrier
• one_mem' : 1 ∈ (↑self).carrier
• add_mem' {a b : R} : a ∈ (↑self).carrier → b ∈ (↑self).carrier → a + b ∈ (↑self).carrier
• zero_mem' : 0 ∈ (↑self).carrier
• mem_of_isSquare' {x : R} (hx : IsSquare x) : x ∈ (↑self).carrier
• neg_one_notMem' : -1 ∉ (↑self).carrier

@[deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.ext_iff {R : Type u_1} {inst✝ : CommRing R} {x y : RingPreordering R} : x = y ↔ (↑x).carrier = (↑y).carrier

theorem RingPreordering.ext {R : Type u_1} {inst✝ : CommRing R} {x y : RingPreordering R} (carrier : (↑x).carrier = (↑y).carrier) : x = y

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance RingPreordering.instSetLike (R : Type u_1) [CommRing R] : SetLike (RingPreordering R) R

Equations

• RingPreordering.instSetLike R = { coe := fun (P : RingPreordering R) => (↑P).carrier, coe_injective := ⋯ }

@[instance_reducible, deprecated "no replacement" (since := "2026-10-28")]

instance RingPreordering.instPartialOrder (R : Type u_1) [CommRing R] : PartialOrder (RingPreordering R)

Equations

• RingPreordering.instPartialOrder R = PartialOrder.ofSetLike (RingPreordering R)

@[deprecated "no replacement" (since := "2026-10-28")]

instance RingPreordering.instSubsemiringClass (R : Type u_1) [CommRing R] : SubsemiringClass (RingPreordering R) R

@[deprecated Subsemiring.IsPreordering.mem_of_isSquare (since := "2026-10-28")]

theorem RingPreordering.mem_of_isSquare {R : Type u_1} [CommRing R] (P : RingPreordering R) {x : R} (hx : IsSquare x) : x ∈ P

@[simp, deprecated Subsemiring.IsPreordering.mul_self_mem (since := "2026-10-28")]

theorem RingPreordering.mul_self_mem {R : Type u_1} [CommRing R] (P : RingPreordering R) (x : R) : x * x ∈ P

@[simp, deprecated Subsemiring.IsPreordering.pow_two_mem (since := "2026-10-28")]

theorem RingPreordering.pow_two_mem {R : Type u_1} [CommRing R] (P : RingPreordering R) (x : R) : x ^ 2 ∈ P

@[deprecated Subsemiring.IsPreordering.neg_one_notMem (since := "2026-10-28")]

theorem RingPreordering.neg_one_notMem {R : Type u_1} [CommRing R] (P : RingPreordering R) : -1 ∉ P

@[deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.toSubsemiring_injective {R : Type u_1} [CommRing R] : Function.Injective toSubsemiring

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.toSubsemiring_inj {R : Type u_1} [CommRing R] {P₁ P₂ : RingPreordering R} : ↑P₁ = ↑P₂ ↔ P₁ = P₂

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.mem_toSubsemiring {R : Type u_1} [CommRing R] {P : RingPreordering R} {x : R} : x ∈ ↑P ↔ x ∈ P

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.coe_toSubsemiring {R : Type u_1} [CommRing R] (P : RingPreordering R) : ↑↑P = ↑P

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.mem_mk {R : Type u_1} [CommRing R] {toSubsemiring : Subsemiring R} (mem_of_isSquare : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) (neg_one_notMem : -1 ∉ toSubsemiring.carrier) {x : R} : x ∈ { toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare, neg_one_notMem' := neg_one_notMem } ↔ x ∈ toSubsemiring

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.coe_set_mk {R : Type u_1} [CommRing R] (toSubsemiring : Subsemiring R) (mem_of_isSquare : ∀ {x : R}, IsSquare x → x ∈ toSubsemiring.carrier) (neg_one_notMem : -1 ∉ toSubsemiring.carrier) : ↑{ toSubsemiring := toSubsemiring, mem_of_isSquare' := mem_of_isSquare, neg_one_notMem' := neg_one_notMem } = ↑toSubsemiring

@[deprecated "no replacement" (since := "2026-10-28")]

def RingPreordering.copy {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P) : RingPreordering R

Copy of a preordering with a new carrier equal to the old one. Useful to fix definitional equalities.

Equations

• P.copy S hS = { carrier := S, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, mem_of_isSquare' := ⋯, neg_one_notMem' := ⋯ }

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.coe_copy {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P) : ↑(P.copy S hS) = S

@[simp, deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.mem_copy {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P) {x : R} : x ∈ P.copy S hS ↔ x ∈ S

@[deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.copy_eq {R : Type u_1} [CommRing R] (P : RingPreordering R) (S : Set R) (hS : S = ↑P) : ↑(P.copy S hS) = S

Support

@[deprecated AddSubmonoid.support (since := "2026-10-28")]

def RingPreordering.supportAddSubgroup {R : Type u_1} [CommRing R] (P : RingPreordering R) : AddSubgroup R

The support of a ring preordering P in a commutative ring R is the set of elements x in R such that both x and -x lie in P.

Equations

• P.supportAddSubgroup = { carrier := ↑P ∩ -↑P, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }

@[deprecated AddSubmonoid.mem_support (since := "2026-10-28")]

theorem RingPreordering.mem_supportAddSubgroup {R : Type u_1} [CommRing R] {P : RingPreordering R} {x : R} : x ∈ P.supportAddSubgroup ↔ x ∈ P ∧ -x ∈ P

@[deprecated AddSubmonoid.coe_support (since := "2026-10-28")]

theorem RingPreordering.coe_supportAddSubgroup {R : Type u_1} [CommRing R] {P : RingPreordering R} : ↑P.supportAddSubgroup = ↑P ∩ -↑P

@[deprecated "no replacement" (since := "2026-10-28")]

class RingPreordering.HasIdealSupport {R : Type u_1} [CommRing R] (P : RingPreordering R) : Prop

Typeclass to track whether the support of a preordering forms an ideal.

• smul_mem_support (x : R) {a : R} (ha : a ∈ P.supportAddSubgroup) : x * a ∈ P.supportAddSubgroup

@[deprecated "no replacement" (since := "2026-10-28")]

theorem RingPreordering.hasIdealSupport_iff {R : Type u_1} [CommRing R] {P : RingPreordering R} : P.HasIdealSupport ↔ ∀ (x a : R), a ∈ P → -a ∈ P → x * a ∈ P ∧ -(x * a) ∈ P

@[deprecated Subsemiring.supportIdeal (since := "2026-10-28")]

instance RingPreordering.instHasIdealSupportOfHasMemOrNegMem {R : Type u_1} [CommRing R] {P : RingPreordering R} [HasMemOrNegMem P] : P.HasIdealSupport

@[deprecated Subsemiring.supportIdeal (since := "2026-10-28")]

def RingPreordering.support {R : Type u_1} [CommRing R] (P : RingPreordering R) [P.HasIdealSupport] : Ideal R

The support of a ring preordering P in a commutative ring R is the set of elements x in R such that both x and -x lie in P.

Equations

• P.support = { toAddSubmonoid := P.supportAddSubgroup.toAddSubmonoid, smul_mem' := ⋯ }

@[deprecated Subsemiring.mem_supportIdeal (since := "2026-10-28")]

theorem RingPreordering.mem_support {R : Type u_1} [CommRing R] {P : RingPreordering R} [P.HasIdealSupport] {x : R} : x ∈ P.support ↔ x ∈ P ∧ -x ∈ P

@[deprecated Subsemiring.coe_supportIdeal (since := "2026-10-28")]

theorem RingPreordering.coe_support {R : Type u_1} [CommRing R] {P : RingPreordering R} [P.HasIdealSupport] : ↑P.support = ↑P ∩ -↑P

@[simp, deprecated Subsemiring.supportIdeal_toAddSubgroup (since := "2026-10-28")]

theorem RingPreordering.supportAddSubgroup_eq {R : Type u_1} [CommRing R] {P : RingPreordering R} [P.HasIdealSupport] : P.supportAddSubgroup = Submodule.toAddSubgroup P.support

@[deprecated Subsemiring.IsOrdering (since := "2026-10-28")]

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

An ordering O on a ring R is a preordering such that

1. O contains either x or -x for each x in R and
2. the support of O is a prime ideal.

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