Ring orderings

We prove basic properties of (pre)orderings on rings.

References

• [An introduction to real algebra, T.Y. Lam][lam_1984]

theorem Subsemiring.IsPreordering.unitsInv_mem {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) {a : Rˣ} (ha : ↑a ∈ P) : ↑a⁻¹ ∈ P

theorem Subsemiring.IsPreordering.one_notMem_support {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) : 1 ∉ P.toAddSubmonoid.support

theorem Subsemiring.IsPreordering.support_ne_top {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) : P.toAddSubmonoid.support ≠ ⊤

theorem Subsemiring.IsPreordering.isOrdering_iff {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) : P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P

theorem Subsemiring.IsPreordering.mul_mem_support_of_right {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) (h : IsUnit 2) (x : R) {a : R} (ha : a ∈ P.toAddSubmonoid.support) : x * a ∈ P.toAddSubmonoid.support

theorem Subsemiring.IsPreordering.mul_mem_support_of_left {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) (h : IsUnit 2) (x : R) {a : R} (ha : a ∈ P.toAddSubmonoid.support) : a * x ∈ P.toAddSubmonoid.support

theorem Subsemiring.IsPreordering.inv_mem {F : Type u_1} [Field F] {P : Subsemiring F} (hP : P.IsPreordering) {a : F} (ha : a ∈ P) : a⁻¹ ∈ P

theorem Subsemiring.IsPreordering.isPointed {F : Type u_1} [Field F] {P : Subsemiring F} (hP : P.IsPreordering) : P.toAddSubmonoid.IsPointed

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

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

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

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

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

theorem RingPreordering.toSubsemiring_mono {R : Type u_1} [CommRing R] : Monotone toSubsemiring

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

theorem RingPreordering.toSubsemiring_strictMono {R : Type u_1} [CommRing R] : StrictMono toSubsemiring

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

theorem RingPreordering.unitsInv_mem {R : Type u_1} [CommRing R] {P : RingPreordering R} {a : Rˣ} (ha : ↑a ∈ P) : ↑a⁻¹ ∈ P

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

theorem RingPreordering.inv_mem {F : Type u_2} [Field F] {P : RingPreordering F} {a : F} (ha : a ∈ P) : a⁻¹ ∈ P

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

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

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

def RingPreordering.mk' {R : Type u_3} [CommRing R] (P : Set R) (add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P) (mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P) (sq : ∀ (x : R), x * x ∈ P) (neg_one : -1 ∉ P) : RingPreordering R

Construct a preordering from a minimal set of axioms.

Equations

• RingPreordering.mk' P add mul sq neg_one = { carrier := P, mul_mem' := ⋯, one_mem' := ⋯, add_mem' := ⋯, zero_mem' := ⋯, mem_of_isSquare' := ⋯, neg_one_notMem' := ⋯ }

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

theorem RingPreordering.mem_mk' {R : Type u_2} [CommRing R] {P : Set R} {add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P} {mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P} {sq : ∀ (x : R), x * x ∈ P} {neg_one : -1 ∉ P} {x : R} : x ∈ mk' P add mul sq neg_one ↔ x ∈ P

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

theorem RingPreordering.coe_mk' {R : Type u_2} [CommRing R] {P : Set R} {add : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P} {mul : ∀ {x y : R}, x ∈ P → y ∈ P → x * y ∈ P} {sq : ∀ (x : R), x * x ∈ P} {neg_one : -1 ∉ P} : ↑(mk' P add mul sq neg_one) = P

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

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

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

theorem RingPreordering.one_notMem_support {R : Type u_1} [CommRing R] (P : RingPreordering R) [P.HasIdealSupport] : 1 ∉ P.support

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

theorem RingPreordering.supportAddSubgroup_ne_top {R : Type u_1} [CommRing R] (P : RingPreordering R) : P.supportAddSubgroup ≠ ⊤

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

theorem RingPreordering.support_ne_top {R : Type u_1} [CommRing R] (P : RingPreordering R) [P.HasIdealSupport] : P.support ≠ ⊤

@[deprecated "use the default constructor and `Subsemiring.IsPreordering.support_ne_top`" (since := "2026-10-28")]

theorem RingPreordering.IsOrdering.mk' {R : Type u_1} [CommRing R] (P : RingPreordering R) [HasMemOrNegMem P] (h : ∀ {x y : R}, x * y ∈ P.support → x ∈ P.support ∨ y ∈ P.support) : P.IsOrdering

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

theorem RingPreordering.HasIdealSupport.smul_mem {R : Type u_1} [CommRing R] (P : RingPreordering R) [P.HasIdealSupport] (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : x * a ∈ P

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

theorem RingPreordering.HasIdealSupport.neg_smul_mem {R : Type u_1} [CommRing R] (P : RingPreordering R) [P.HasIdealSupport] (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : -(x * a) ∈ P

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

theorem RingPreordering.hasIdealSupport_of_isUnit_two {R : Type u_1} [CommRing R] {P : RingPreordering R} (h : IsUnit 2) : P.HasIdealSupport

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

instance RingPreordering.instHasIdealSupportOfFactIsUnitOfNat {R : Type u_1} [CommRing R] (P : RingPreordering R) [h : Fact (IsUnit 2)] : P.HasIdealSupport

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

theorem RingPreordering.eq_zero_of_mem_of_neg_mem {F : Type u_2} [Field F] {P : RingPreordering F} {x : F} (h : x ∈ P) (h2 : -x ∈ P) : x = 0

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

theorem RingPreordering.supportAddSubgroup_eq_bot {F : Type u_2} [Field F] (P : RingPreordering F) : P.supportAddSubgroup = ⊥

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

instance RingPreordering.instHasIdealSupport {F : Type u_2} [Field F] (P : RingPreordering F) : P.HasIdealSupport

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

theorem RingPreordering.support_eq_bot {F : Type u_2} [Field F] (P : RingPreordering F) : P.support = ⊥

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

instance RingPreordering.instIsPrimeSupport {F : Type u_2} [Field F] (P : RingPreordering F) : P.support.IsPrime

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

theorem RingPreordering.isOrdering_iff {R : Type u_1} [CommRing R] {P : RingPreordering R} : P.IsOrdering ↔ ∀ (a b : R), -(a * b) ∈ P → a ∈ P ∨ b ∈ P