Extending field preorderings to orderings

A proper preordering on a field extends to a total ordering. The proof adjoins one element to a preordering and then applies Zorn's lemma. In particular, it preserves the prescribed positive elements, as required when ordering a field extension of an already ordered field.

References

This is the classical preordering extension argument; see Salma Kuhlmann, Real Algebraic Geometry, Lecture 3, Lemma 2.1 and Corollaries 3.2 and 3.4. The Lean construction uses Mathlib's RingPreordering and RingCone interfaces.

def RingPreordering.adjoin {K : Type u_1} [Field K] (P : RingPreordering K) (a : K) (ha : -a ∉ P) : RingPreordering K

Adjoin an element whose negative is absent from a field preordering.

Equations

• P.adjoin a ha = RingPreordering.mk' {x : K | ∃ u ∈ P, ∃ v ∈ P, x = u + a * v} ⋯ ⋯ ⋯ ⋯

@[simp]

theorem RingPreordering.mem_adjoin {K : Type u_1} [Field K] (P : RingPreordering K) (a : K) (ha : -a ∉ P) {x : K} : x ∈ P.adjoin a ha ↔ ∃ u ∈ P, ∃ v ∈ P, x = u + a * v

theorem RingPreordering.le_adjoin {K : Type u_1} [Field K] (P : RingPreordering K) (a : K) (ha : -a ∉ P) : P ≤ P.adjoin a ha

theorem RingPreordering.self_mem_adjoin {K : Type u_1} [Field K] (P : RingPreordering K) (a : K) (ha : -a ∉ P) : a ∈ P.adjoin a ha

theorem RingPreordering.adjoin_le {K : Type u_1} [Field K] {P Q : RingPreordering K} {a : K} {ha : -a ∉ P} (hPQ : P ≤ Q) (haQ : a ∈ Q) : P.adjoin a ha ≤ Q

The generated preordering is contained in every preordering containing its generators.

@[simp]

theorem RingPreordering.adjoin_le_iff {K : Type u_1} [Field K] {P Q : RingPreordering K} {a : K} {ha : -a ∉ P} : P.adjoin a ha ≤ Q ↔ P ≤ Q ∧ a ∈ Q

theorem RingPreordering.exists_le_isOrdering {K : Type u_1} [Field K] (P : RingPreordering K) : ∃ (Q : RingPreordering K), P ≤ Q ∧ Q.IsOrdering

A field preordering extends to an ordering, retaining every prescribed sign.

theorem RingPreordering.exists_le_isOrdering_mem {K : Type u_1} [Field K] (P : RingPreordering K) {a : K} (ha : -a ∉ P) : ∃ (Q : RingPreordering K), P ≤ Q ∧ Q.IsOrdering ∧ a ∈ Q

An element whose negative is absent can be made nonnegative in an extending ordering.

def RingPreordering.toRingCone {K : Type u_1} [Field K] (P : RingPreordering K) : RingCone K

A preordering on a field is a pointed ring cone.

Equations

• P.toRingCone = { toSubsemiring := ↑P, eq_zero_of_mem_of_neg_mem' := ⋯ }

@[simp]

theorem RingPreordering.mem_toRingCone {K : Type u_1} [Field K] (P : RingPreordering K) {x : K} : x ∈ P.toRingCone ↔ x ∈ P

instance RingPreordering.instHasMemOrNegMemRingConeToRingConeOfIsOrdering {K : Type u_1} [Field K] (P : RingPreordering K) [P.IsOrdering] : HasMemOrNegMem P.toRingCone

@[instance_reducible]

noncomputable def RingPreordering.linearOrder {K : Type u_1} [Field K] (P : RingPreordering K) [P.IsOrdering] : LinearOrder K

The linear order associated to a field ordering.

Equations

• P.linearOrder = LinearOrder.mkOfAddGroupCone P.toRingCone

theorem RingPreordering.isStrictOrderedRing {K : Type u_1} [Field K] (P : RingPreordering K) [P.IsOrdering] : IsStrictOrderedRing K

theorem RingPreordering.nonneg_iff {K : Type u_1} [Field K] (P : RingPreordering K) [P.IsOrdering] (x : K) : 0 ≤ x ↔ x ∈ P

theorem RingPreordering.exists_linearOrder {K : Type u_1} [Field K] (P : RingPreordering K) : ∃ (o : LinearOrder K), IsStrictOrderedRing K ∧ ∀ x ∈ P, 0 ≤ x

Order a field while respecting all signs in a specified preordering.