Extending preorderings to orderings

Let R be a commutative ring, and let P be a preordering on R. We prove that every preordering on R extends to an ordering on R, and characterise maximal orderings.

Main results

• Subsemiring.IsPreordering.exists_le_isOrdering: a preordering extends to an ordering.
• Subsemiring.maximal_isPreordering_iff_maximal_isOrdering: an ordering is maximal as an ordering if and only if it is maximal as a preordering.
• Subsemiring.maximal_isPreordering_iff_isOrdering: over a field, orderings are precisely maximal preorderings.

References

• An introduction to real algebra, by T.Y. Lam. Rocky Mountain J. Math. 14(4): 767-814 (1984). lam_1984

theorem Subsemiring.IsPreordering.closure_insert {R : Type u_1} [CommRing R] {P : Subsemiring R} {a : R} (hP : P.IsPreordering) (hx : -1 ∉ closure (insert a ↑P)) : (closure (insert a ↑P)).IsPreordering

theorem Subsemiring.IsPreordering.mem_closure_insert {R : Type u_1} [CommRing R] {P : Subsemiring R} {a : R} (hP : P.IsPreordering) {x : R} : x ∈ closure (insert a ↑P) ↔ ∃ y ∈ P, ∃ z ∈ P, x = y + a * z

theorem Subsemiring.IsPreordering.neg_one_notMem_closure_insert {R : Type u_1} [CommRing R] {P : Subsemiring R} (a : R) (hP : P.IsPreordering) (h : ∀ (x y : R), x ∈ P → y ∈ P → x + (1 + y) * a + 1 ≠ 0) : -1 ∉ closure (insert a ↑P)

theorem Subsemiring.IsPreordering.neg_one_notMem_closure_insert_or_of_neg_mul_mem {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) {x y : R} (h : -(x * y) ∈ P) : -1 ∉ closure (insert x ↑P) ∨ -1 ∉ closure (insert y ↑P)

theorem Subsemiring.IsPreordering.neg_one_notMem_closure_insert_of_neg_notMem {F : Type u_2} [Field F] {P : Subsemiring F} {a : F} (hP : P.IsPreordering) (ha : -a ∉ P) : -1 ∉ closure (insert a ↑P)

If F is a field, P is a preordering on F, and -a ∉ P, then -1 is not in the semiring generated by P and a.

theorem Subsemiring.IsPreordering.exists_le_and_mem_or_mem {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) (x y : R) (h : -(x * y) ∈ P) : ∃ Q ≥ P, Q.IsPreordering ∧ (x ∈ Q ∨ y ∈ Q)

theorem Subsemiring.IsOrdering.of_maximal_isPreordering {R : Type u_1} [CommRing R] {P : Subsemiring R} (max : Maximal IsPreordering P) : P.IsOrdering

theorem Subsemiring.IsPreordering.exists_le_isOrdering {R : Type u_1} [CommRing R] {P : Subsemiring R} (hP : P.IsPreordering) : ∃ O ≥ P, O.IsOrdering

theorem Subsemiring.IsPreordering.exists_le_isOrdering_and_mem {R : Type u_1} [CommRing R] {P : Subsemiring R} {a : R} (hP : P.IsPreordering) (h : -1 ∉ closure (insert a ↑P)) : ∃ O ≥ P, O.IsOrdering ∧ a ∈ O

theorem Subsemiring.IsPreordering.exists_le_isOrdering_and_mem_or_neg_mem {R : Type u_1} [CommRing R] {P : Subsemiring R} (a : R) (hP : P.IsPreordering) : ∃ Q ≥ P, Q.IsOrdering ∧ (a ∈ Q ∨ -a ∈ Q)

theorem Subsemiring.IsPreordering.exists_lt_isOrdering {R : Type u_1} [CommRing R] {P : Subsemiring R} {a : R} (hP : P.IsPreordering) (hp : a ∉ P) (hn : -a ∉ P) : ∃ Q > P, Q.IsOrdering

theorem Subsemiring.maximal_isOrdering_iff_maximal_isPreordering {R : Type u_1} [CommRing R] {O : Subsemiring R} : Maximal IsOrdering O ↔ Maximal IsPreordering O

theorem Subsemiring.maximal_isPreordering_iff_isOrdering {F : Type u_2} [Field F] {O : Subsemiring F} : Maximal IsPreordering O ↔ O.IsOrdering