Ring orderings

Let R be a commutative ring. A preordering on R is a subset closed under addition and multiplication that contains all squares, but not -1.

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

An ordering O on 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.

We define preorderings, supports and orderings.

A ring preordering can intuitively be viewed as a set of "non-negative" ring elements. Indeed, an ordering O with support p induces a linear order on R⧸p making it into an ordered ring, and vice versa.

References

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

Preorderings

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

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 RingPreordering.instSetLike (R : Type u_1) [CommRing R] : SetLike (RingPreordering R) R

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

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

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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]

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

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.

@[simp]

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]

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

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

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.

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

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

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

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

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

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.

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

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

@[simp]

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

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