Let R be a commutative ring, and let P be a preordering on R.

Main results

• Subsemiring.IsPreordering.exists_le: if a ∉ P, then P extends to a preordering containing either a or -a.
• Subsemiring.IsPreordering.exists_le_isOrdering: P 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} [P.IsPreordering] {a : R} (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} [P.IsPreordering] {a 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) [P.IsPreordering] (a : R) (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} [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} [P.IsPreordering] {a : F} (ha : -a ∉ P) : -1 ∉ closure (insert a ↑P)

If F is a field, P is a preordering on F, and a is an element of P such that -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) [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] {O : Subsemiring R} (max : Maximal IsPreordering O) : O.IsOrdering

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

theorem Subsemiring.IsPreordering.exists_le_isOrdering_and_mem {R : Type u_1} [CommRing R] {P : Subsemiring R} [P.IsPreordering] {a : R} (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) [P.IsPreordering] (a : R) : ∃ Q ≥ P, Q.IsOrdering ∧ (a ∈ Q ∨ -a ∈ Q)

theorem Subsemiring.IsPreordering.exists_lt_isOrdering {R : Type u_1} [CommRing R] (P : Subsemiring R) [P.IsPreordering] (a : R) (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