Ring orderings

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

References

• An introduction to real algebra, T.Y. Lam

Preorderings

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

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

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

Alias of the reverse direction of RingPreordering.toSubsemiring_le_toSubsemiring.

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

Alias of the reverse direction of RingPreordering.toSubsemiring_lt_toSubsemiring.

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

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

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

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

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

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]

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]

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

Supports

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

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

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

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

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

Constructor for IsOrdering that doesn't require ne_top'.

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

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

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

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

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

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

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

@[simp]

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

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

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