rewrite adjoin code to generalise

RealClosedField/RealClosedField/RingOrdering/Adjoin.lean

@@ -0,0 +1,160 @@
+/-
+Copyright (c) 2024 Florent Schaffhauser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Florent Schaffhauser, Artie Khovanov
+-/
+import RealClosedField.RealClosedField.RingOrdering.Basic
+
+import Mathlib.Order.Zorn
+
+/-
+## Adjoining an element to a preordering
+-/
+
+variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] (P : S) (a : R)
+
+namespace Subsemiring
+
+/-- An explicit form of the semiring generated by a preordering `P` and an element `a`. -/
+def ringPreordering_adjoin : Subsemiring R where
+  carrier := {z : R | ∃ x ∈ P, ∃ y ∈ P, z = x + a * y}
+  zero_mem' := ⟨0, by aesop, 0, by aesop, by simp⟩
+  one_mem' := ⟨1, by aesop, 0, by aesop, by simp⟩
+  add_mem' := by
+    intro a b ha hb
+    obtain ⟨x₁, hx₁, y₁, hy₁, rfl⟩ := ha
+    obtain ⟨x₂, hx₂, y₂, hy₂, rfl⟩ := hb
+    exact ⟨x₁ + x₂, by aesop, y₁ + y₂, by aesop, by ring⟩
+  mul_mem' := by
+    intro a b ha hb
+    obtain ⟨x₁, hx₁, y₁, hy₁, rfl⟩ := ha
+    obtain ⟨x₂, hx₂, y₂, hy₂, rfl⟩ := hb
+    exact ⟨x₁ * x₂ + (a * a) * (y₁ * y₂), by aesop, x₁ * y₂ + y₁ * x₂, by aesop, by ring⟩
+
+variable {P} in
+@[aesop unsafe 70% apply (rule_sets := [SetLike])]
+lemma subset_ringPreordering_adjoin {x : R} (hx : x ∈ P) :
+    x ∈ ringPreordering_adjoin P a := ⟨x, by aesop, 0, by aesop, by simp⟩
+
+@[aesop safe 0 apply (rule_sets := [SetLike])]
+lemma mem_ringPreordering_adjoin : a ∈ ringPreordering_adjoin P a :=
+  ⟨0, by aesop, 1, by aesop, by simp⟩
+
+@[aesop safe 0 apply (rule_sets := [SetLike])]
+lemma square_mem_ringPreordering_adjoin (x : R) : x * x ∈ ringPreordering_adjoin P a :=
+  by simpa using subset_ringPreordering_adjoin a (by aesop)
+
+theorem closure_insert_eq_ringPreordering_adjoin :
+    closure (insert a P) = ringPreordering_adjoin P a := by
+  refine closure_eq_of_le (fun x hx => ?_)
+                          (fun _ hz => ?_)
+  · rcases hx with ⟨_, _⟩ | h
+    · exact mem_ringPreordering_adjoin P a
+    · exact subset_ringPreordering_adjoin a h
+  · obtain ⟨_, _, _, _, rfl⟩ := hz; aesop
+
+end Subsemiring
+
+namespace RingPreordering
+
+variable {P a} in
+def adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
+    RingPreordering R where
+  __ := Subsemiring.ringPreordering_adjoin P a
+  square_mem' := by aesop
+  minus_one_not_mem' := h
+
+variable {P a} in
+@[aesop unsafe 70% apply (rule_sets := [SetLike])]
+lemma subset_adjoin' (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a)
+    {x : R} (hx : x ∈ P) : x ∈ adjoin h :=
+  Subsemiring.subset_ringPreordering_adjoin a hx
+
+variable {P a} in
+lemma subset_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
+    (P : Set R) ⊆ adjoin h := fun _ => by aesop
+
+variable {P a} in
+@[aesop safe 0 apply (rule_sets := [SetLike])]
+lemma mem_adjoin (h : -1 ∉ Subsemiring.ringPreordering_adjoin P a) :
+    a ∈ adjoin h := Subsemiring.mem_ringPreordering_adjoin P a
+
+/-
+## Sufficient conditions for adjoining an element
+-/
+
+variable {P} in
+theorem minus_one_not_mem_or {x y : R} (h : - (x * y) ∈ P) :
+    -1 ∉ Subsemiring.ringPreordering_adjoin P x ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P y := by
+  by_contra
+  have hx : -1 ∈ Subsemiring.ringPreordering_adjoin P x := by aesop
+  have hy : -1 ∈ Subsemiring.ringPreordering_adjoin P y := by aesop
+  rcases hx with ⟨t₁, ht₁, t₂, ht₂, eqx⟩
+  rcases hy with ⟨s₁, hs₁, s₂, hs₂, eqy⟩
+  /- annoying calculation -/
+  sorry
+
+theorem minus_one_not_mem_or' :
+    -1 ∉ Subsemiring.ringPreordering_adjoin P a ∨ -1 ∉ Subsemiring.ringPreordering_adjoin P (-a)
+    := RingPreordering.minus_one_not_mem_or (by aesop : - (a * (-a)) ∈ P)
+
+theorem minus_one_not_mem_ringPreordering_adjoin
+    (h : ∀ x y, x ∈ P → y ∈ P → x + (1 + y) * a + 1 ≠ 0) :
+    -1 ∉ Subsemiring.ringPreordering_adjoin P a := fun contr => by
+  have : -1 * (1 + a) ∈ Subsemiring.ringPreordering_adjoin P a :=
+    by aesop (config := { enableSimp := false })
+  obtain ⟨x, hx, y, hy, eqn⟩ := this
+  have : x + a * y + (1 + a) = 0 := (add_eq_zero_iff_eq_neg).mpr (by aesop)
+  exact h _ _ hx hy (by ring_nf at this ⊢; assumption)
+
+/--
+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 of the form `x + a * y` with `x` and `y` in `P`.
+-/
+theorem minus_one_not_mem_adjoin_linear
+    {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] {P : S} {a : F}
+    (ha : -a ∉ P) : -1 ∉ Subsemiring.ringPreordering_adjoin P a := fun h => by
+  rcases h with ⟨x, hx, y, hy, eqn⟩
+  apply ha
+  have : y ≠ 0 := fun _ => by simpa [*] using minus_one_not_mem P
+  rw [show -a = x * y⁻¹ + y⁻¹ by
+    field_simp
+    rw [neg_eq_iff_eq_neg.mp eqn]
+    ring]
+  aesop
+
+/-
+## Existence of prime orderings
+-/
+
+theorem exists_le :
+    ∃ Q : RingPreordering R, (P : Set R) ⊆ Q ∧ (a ∈ Q ∨ -a ∈ Q) := by
+  cases RingPreordering.minus_one_not_mem_or' P a with
+  | inl h => exact ⟨adjoin h, subset_adjoin _, by aesop⟩
+  | inr h => exact ⟨adjoin h, subset_adjoin _, by aesop⟩
+
+theorem exists_lt (hp : a ∉ P) (hn : -a ∉ P) :
+    ∃ Q : RingPreordering R, (P : Set R) ⊂ Q := by
+  rcases exists_le P a with ⟨Q, le, p_mem | n_mem⟩
+  · exact ⟨Q, lt_of_le_of_ne le <| Ne.symm (ne_of_mem_of_not_mem' p_mem hp)⟩
+  · exact ⟨Q, lt_of_le_of_ne le <| Ne.symm (ne_of_mem_of_not_mem' n_mem hn)⟩
+
+variable {P} in
+/- A preordering on `R` that is maximal with respect to inclusion is a prime ordering. -/
+theorem isPrimeOrdering_of_maximal
+    (max : Maximal Set.univ (RingPreorderingClass.toRingPreordering P)) :
+    IsPrimeOrdering P := isPrimeOrdering_iff.mpr (fun a b h => by
+  cases RingPreordering.minus_one_not_mem_or h with
+  | inl h => exact Or.inl <| Maximal.le_of_ge max trivial (subset_adjoin h) (mem_adjoin h)
+  | inr h => exact Or.inr <| Maximal.le_of_ge max trivial (subset_adjoin h) (mem_adjoin h))
+
+/- Every preordering on `R` extends to a prime ordering. -/
+theorem exists_le_isPrimeOrdering :
+    ∃ Q : RingPreordering R, (P : Set R) ⊆ Q ∧ IsPrimeOrdering Q := by
+  suffices ∃ Q, RingPreorderingClass.toRingPreordering P ≤ Q ∧ Maximal (fun x => x ∈ Set.univ) Q by
+    obtain ⟨Q, hQ⟩ := this
+    exact ⟨Q, by aesop, isPrimeOrdering_of_maximal hQ.2⟩
+  apply zorn_le_nonempty₀
+  · intro c _ hc P' hP'
+    simp_all [← bddAbove_def, nonempty_chain_bddAbove c hc (Set.nonempty_of_mem hP')]
+  · trivial

RealClosedField/RealClosedField/RingOrdering/Basic.lean

@@ -8,6 +8,7 @@ import Mathlib.Order.Chain
 import Mathlib.Tactic.Ring
 import Mathlib.Algebra.CharP.Defs
 import Mathlib.RingTheory.Ideal.Basic
+import Mathlib.Tactic.FieldSimp
 
 /-
 ## Definitions
@@ -45,34 +46,9 @@ instance RingPreordering.instRingPreorderingClass : RingPreorderingClass (RingPr
   square_mem {P} := P.square_mem'
   minus_one_not_mem {P} := P.minus_one_not_mem'
 
-/-- `RingOrderingClass S R` says that `S` is a type of orderings on `R`. -/
-class RingOrderingClass extends RingPreorderingClass S R : Prop where
-  mem_or_neg_mem (P : S) (x : R) : x ∈ P ∨ -x ∈ P
+variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R]
 
-export RingOrderingClass (mem_or_neg_mem)
-
-/-- An ordering `P` on a ring `R` is a preordering such that, for every `x` in `R`,
-either `x` or `-x` lies in `P`. Equivalently, an ordering is a maximal preordering. -/
-structure RingOrdering extends RingPreordering R where
-  mem_or_neg_mem' (x : R) : x ∈ carrier ∨ -x ∈ carrier
-
-instance RingOrdering.instSetLike : SetLike (RingOrdering R) R where
-  coe P := P.carrier
-  coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
-
-instance RingOrdering.instRingOrderingClass : RingOrderingClass (RingOrdering R) R where
-  zero_mem {P} := P.zero_mem'
-  one_mem {P} := P.one_mem'
-  add_mem {P} := P.add_mem'
-  mul_mem {P} := P.mul_mem'
-  square_mem {P} := P.square_mem'
-  minus_one_not_mem {P} := P.minus_one_not_mem'
-  mem_or_neg_mem {P} := P.mem_or_neg_mem'
-
-variable{S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R]
-
-def RingPreorderingClass.toRingPreordering (P : S) :
-    RingPreordering R where
+def RingPreorderingClass.toRingPreordering (P : S) : RingPreordering R where
   carrier := P
   zero_mem' := zero_mem P
   one_mem' := one_mem P
@@ -87,31 +63,35 @@ lemma RingPreorderingClass.coe_toRingPreordering (P : S) : (toRingPreordering P
 
 end Defns
 
-namespace RingPreordering
+variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S}
 
 /-
 ## Basic properties
 -/
 
+namespace RingPreordering
+
 @[aesop safe 2 apply (rule_sets := [SetLike])]
 /- There is no neg_mem -/
-lemma neg_mul_mem_of_mem [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} {x y : R}
-    (hx : x ∈ P) (hy : -y ∈ P) : -(x * y) ∈ P := by
+lemma neg_mul_mem_of_mem {x y : R} (hx : x ∈ P) (hy : -y ∈ P) : -(x * y) ∈ P := by
   simpa using mul_mem hx hy
 
 @[aesop safe 2 apply (rule_sets := [SetLike])]
 /- There is no neg_mem -/
-lemma neg_mul_mem_of_neg_mem [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} {x y : R}
-    (hx : -x ∈ P) (hy : y ∈ P) : -(x * y) ∈ P := by
+lemma neg_mul_mem_of_neg_mem {x y : R} (hx : -x ∈ P) (hy : y ∈ P) : -(x * y) ∈ P := by
   simpa using mul_mem hx hy
 
 @[aesop safe apply (rule_sets := [SetLike])]
-theorem inv_mem
-    {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} {a : Rˣ}
-    (ha : ↑a ∈ P) : ↑a⁻¹ ∈ P := by
+theorem inv_mem {a : Rˣ} (ha : ↑a ∈ P) : ↑a⁻¹ ∈ P := by
   rw [(by simp : (↑a⁻¹ : R) = a * (a⁻¹ * a⁻¹))]
   aesop (config := { enableSimp := false })
 
+@[aesop safe apply (rule_sets := [SetLike])]
+theorem Field.inv_mem {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F]
+    {P : S} {a : F} (ha : a ∈ P) : a⁻¹ ∈ P := by
+  rw [(by field_simp : a⁻¹ = a * (a⁻¹ * a⁻¹))]
+  aesop
+
 /- Construct a preordering from a minimal set of axioms. -/
 def mk' {R : Type*} [CommRing R] (P : Set R)
     (add   : ∀ {x y : R}, x ∈ P → y ∈ P → x + y ∈ P)
@@ -150,8 +130,6 @@ end RingPreordering
 ## Support
 -/
 
-variable {S R : Type*} [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S}
-
 namespace AddSubgroup
 
 variable (P) in
@@ -203,29 +181,17 @@ 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`.
 -/
 def preordering_support : Ideal R where
-  carrier := {x : R | x ∈ P ∧ -x ∈ P}
-  zero_mem' := by aesop
-  add_mem' := by aesop
+  __ := AddSubgroup.preordering_support P
   smul_mem' := by simpa using RingPreordering.HasIdealSupport.smul_mem_support (P := P)
 
 @[simp] lemma mem_support : x ∈ preordering_support P ↔ x ∈ P ∧ -x ∈ P := Iff.rfl
 @[simp, norm_cast] lemma coe_support : preordering_support P = {x : R | x ∈ P ∧ -x ∈ P} := rfl
 
 end Ideal
 
-instance RingPreordering.hasIdealSupport [RingOrderingClass S R] :
-    RingPreordering.HasIdealSupport P where
-  smul_mem_support x a ha := by
-    cases mem_or_neg_mem P x with
-    | inl => aesop
-    | inr hx =>
-        rw [AddSubgroup.mem_support] at *
-        exact ⟨by simpa using mul_mem hx ha.2, by simpa using mul_mem hx ha.1⟩
-
 theorem RingPreordering.hasIdealSupport_of_isUnit_2 (isUnit_2 : IsUnit (2 : R)) :
     RingPreordering.HasIdealSupport P := by
-  apply HasIdealSupport.hasIdealSupport
-  intro x a h₁a h₂a
+  refine HasIdealSupport.hasIdealSupport (fun x a h₁a h₂a => ?_)
   obtain ⟨half, h2⟩ := IsUnit.exists_left_inv isUnit_2
   let y := (1 + x) * half
   let z := (1 - x) * half
@@ -235,3 +201,86 @@ theorem RingPreordering.hasIdealSupport_of_isUnit_2 (isUnit_2 : IsUnit (2 : R))
   rw [this]
   ring_nf at mem ⊢
   assumption
+
+/-
+## (Prime) orderings
+-/
+
+namespace RingPreordering
+
+section IsOrdering
+
+variable (P) in
+/-- An ordering `P` on a ring `R` is a preordering such that, for every `x` in `R`,
+either `x` or `-x` lies in `P`. -/
+class IsOrdering : Prop where
+  mem_or_neg_mem' (x : R) : x ∈ P ∨ -x ∈ P
+
+variable [IsOrdering P]
+
+variable (P) in
+/-- Technical lemma to get P as explicit argument -/
+lemma mem_or_neg_mem : ∀ x : R, x ∈ P ∨ -x ∈ P := IsOrdering.mem_or_neg_mem' (P := P)
+
+@[aesop unsafe apply]
+lemma neg_mem_of_not_mem (x : R) (h : x ∉ P) : -x ∈ P := by
+  have := mem_or_neg_mem P x
+  simp_all
+
+@[aesop unsafe apply]
+lemma mem_of_not_neg_mem (x : R) (h : -x ∉ P) : x ∈ P := by
+  have := mem_or_neg_mem P x
+  simp_all
+
+instance hasIdealSupport : HasIdealSupport P where
+  smul_mem_support x a ha := by
+    cases mem_or_neg_mem (P := P) x with
+    | inl => aesop
+    | inr hx =>
+        rw [AddSubgroup.mem_support] at *
+        exact ⟨by simpa using mul_mem hx ha.2, by simpa using mul_mem hx ha.1⟩
+
+end IsOrdering
+
+variable (P) in
+/-- A prime ordering `P` on a ring `R` is an ordering whose support is a prime ideal. -/
+class IsPrimeOrdering : Prop where
+  mem_or_neg_mem' (x : R) : x ∈ P ∨ -x ∈ P
+  mem_or_mem' {x y : R} (h : x * y ∈ AddSubgroup.preordering_support P) :
+    x ∈ AddSubgroup.preordering_support P ∨ y ∈ AddSubgroup.preordering_support P
+
+instance isOrdering [IsPrimeOrdering P] :
+    IsOrdering P where
+  mem_or_neg_mem' := IsPrimeOrdering.mem_or_neg_mem'
+
+instance preordering_support_isPrime [IsPrimeOrdering P] :
+    (Ideal.preordering_support P).IsPrime where
+  ne_top' h := minus_one_not_mem P (by aesop : 1 ∈ Ideal.preordering_support P).2
+  mem_or_mem' := IsPrimeOrdering.mem_or_mem'
+
+instance isPrimeOrdering_of_isOrdering
+    [IsOrdering P] [(Ideal.preordering_support P).IsPrime] : IsPrimeOrdering P where
+  mem_or_neg_mem' := mem_or_neg_mem P
+  mem_or_mem' := Ideal.IsPrime.mem_or_mem (by assumption)
+
+theorem isPrimeOrdering_iff :
+    IsPrimeOrdering P ↔ (∀ a b : R, -(a * b) ∈ P → a ∈ P ∨ b ∈ P) := by
+  refine Iff.intro (fun prime a b h₁ => ?_) (fun h => ?_)
+  · by_contra h₂
+    have : a * b ∈ P := by simpa using mul_mem (by aesop : -a ∈ P) (by aesop : -b ∈ P)
+    have : a ∈ Ideal.preordering_support P ∨ b ∈ Ideal.preordering_support P :=
+      Ideal.IsPrime.mem_or_mem inferInstance (by simp_all)
+    simp_all
+  · constructor
+    · aesop
+    · intro x y hxy
+      by_contra h₂
+      cases (by aesop : x ∈ P ∨ -x ∈ P) with
+      | inl =>  have := h (-x) y (by aesop)
+                have := h (-x) (-y) (by aesop)
+                aesop
+      | inr =>  have := h x y (by aesop)
+                have := h x (-y) (by aesop)
+                aesop
+
+end RingPreordering