join up to cones

RealClosedField/Mathlib/Algebra/Order/Ring/Cone.lean

@@ -7,6 +7,7 @@ import Mathlib.Algebra.Order.Group.Cone
 import Mathlib.Algebra.Order.Ring.Basic
 import Mathlib.Algebra.Ring.Subsemiring.Order
 import RealClosedField.RealClosedField.RingOrdering.Basic
+import Mathlib.RingTheory.Ideal.Quotient.Basic
 
 /-!
 # Construct ordered rings from rings with a specified positive cone.
@@ -46,6 +47,14 @@ instance RingCone.instRingConeClass (R : Type*) [Ring R] :
 
 namespace RingCone
 
+@[simp]
+theorem mem_toSubsemiring (R : Type*) [Ring R] (C : RingCone R) {x : R} :
+  x ∈ C.toSubsemiring ↔ x ∈ C := Iff.rfl
+
+@[simp]
+theorem coe_toSubsemiring (R : Type*) [Ring R] (C : RingCone R) :
+    (C.toSubsemiring : Set R) = C := rfl
+
 variable {T : Type*} [OrderedRing T] {a : T}
 
 variable (T) in
@@ -118,9 +127,42 @@ instance RingConeClass.instIsOrdering_of_isMaxCone {S R : Type*} [Nontrivial R]
     RingPreordering.IsOrdering C where
   mem_or_neg_mem' x := by obtain ⟨C, hC⟩ := C; exact mem_or_neg_mem C x
 
-/- TODO : decide whether to keep this cursed subtype instance, or whether to change to a def. -/
+/- TODO : decide whether to keep the above cursed subtype instance,
+          or whether to change to a def. -/
+
+@[reducible] def RingCone.mkOfRingPreordering {S R : Type*}
+    [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S}
+    (hP : RingPreordering.AddSubgroup.support P = ⊥) : RingCone R where
+  __ := (RingPreorderingClass.toRingPreordering P).toSubsemiring
+  eq_zero_of_mem_of_neg_mem' {a} := by
+    have : ∀ x, x ∈ RingPreordering.AddSubgroup.support P → x ∈ (⊥ : AddSubgroup R) := by simp_all
+    rcases hP with -
+    aesop
+  /- TODO : make this proof less awful -/
+
+instance RingCone.mkOfRingPreordering.inst_isMaxCone {S R : Type*}
+    [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} [RingPreordering.IsOrdering P]
+    (hP : RingPreordering.AddSubgroup.support P = ⊥) : IsMaxCone <| mkOfRingPreordering hP where
+  mem_or_neg_mem' := RingPreordering.mem_or_neg_mem P
+
+@[reducible] def LinearOrderedRing.mkOfRingOrdering {S R : Type*} [CommRing R] [IsDomain R]
+    [SetLike S R] [RingPreorderingClass S R] {P : S} [RingPreordering.IsOrdering P]
+    [DecidablePred (· ∈ P)]
+    (hP : RingPreordering.AddSubgroup.support P = ⊥) : LinearOrderedRing R :=
+  have : DecidablePred (· ∈ RingCone.mkOfRingPreordering hP) := by assumption
+  mkOfCone <| RingCone.mkOfRingPreordering hP
+
+@[reducible] def RingCone.mkOfRingPreordering_field {S F : Type*}
+    [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) : RingCone F :=
+  mkOfRingPreordering <| RingPreordering.support_eq_bot P
+
+variable {S R : Type*} [CommRing R] (I : Ideal R)
+
+#check Ideal.Quotient.one
+
+@[reducible] def RingCone.mkOfRingPoreordering_quot {S R : Type*}
+    [CommRing R] [SetLike S R] [RingPreorderingClass S R] {P : S} [RingPreordering.IsOrdering P] :
+    RingCone (R ⧸ (RingPreordering.Ideal.support P))
 
-/- TODO: prime orderings with support {0} are maximal cones;
-         deduce prime orderings on fields are maximal cones -/
 /- TODO: orderings with support I induce maximal ring cones on R/I -/
 /- TODO: ordering on an ID <-> ordering on its fraction field -/

RealClosedField/RealClosedField/RingOrdering/Basic.lean

@@ -60,20 +60,38 @@ theorem nonempty_chain_bddAbove {R : Type*} [CommRing R]
               (by simpa using (hc.some.square_mem' x)))
     (by
       have a : ∀ x ∈ (toSubsemiring '' c), -1 ∉ x := fun P' hP' => by
-        obtain ⟨P, _, rfl⟩ := (by aesop : ∃ x ∈ c, x.toSubsemiring = P')
+        obtain ⟨P, _, rfl⟩ := show ∃ x ∈ c, x.toSubsemiring = P' by simp_all
         simpa using P.minus_one_not_mem'
       simp_all [Subsemiring.coe_sSup_of_directedOn (by simp [hc])
         (IsChain.directedOn (IsChain.image _ _ _ (by aesop) hcc))]),
   fun _ _ => by simpa using CompleteLattice.le_sSup (toSubsemiring '' c) _ (by aesop)⟩
 
+variable (P) in
+theorem AddSubgroup.one_not_mem_support : 1 ∉ support P := by
+  aesop (add unsafe forward (minus_one_not_mem P))
+
+variable (P) in
+theorem AddSubgroup.support_neq_top : support P ≠ ⊤ := fun eq => by
+  have : 1 ∉ (⊤ : AddSubgroup R) := by rw[← eq]; exact one_not_mem_support P
+  simp_all
+
+variable (P) in
+theorem Ideal.one_not_mem_support [HasIdealSupport P] : 1 ∉ support P :=
+  AddSubgroup.one_not_mem_support P
+
+variable (P) in
+theorem Ideal.support_neq_top [HasIdealSupport P] : support P ≠ ⊤ := fun eq => by
+  have : 1 ∉ (⊤ : Ideal R) := by rw[← eq]; exact one_not_mem_support P
+  simp_all
+
 namespace HasIdealSupport
 
-theorem smul_mem [RingPreordering.HasIdealSupport P]
+theorem smul_mem [HasIdealSupport P]
   (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : x * a ∈ P := by
   have := smul_mem_support P
   simp_all
 
-theorem neg_smul_mem [RingPreordering.HasIdealSupport P]
+theorem neg_smul_mem [HasIdealSupport P]
   (x : R) {a : R} (h₁a : a ∈ P) (h₂a : -a ∈ P) : -(x * a) ∈ P := by
   have := smul_mem_support P
   simp_all
@@ -90,7 +108,30 @@ theorem hasIdealSupport_of_isUnit_2 (isUnit_2 : IsUnit (2 : R)) : HasIdealSuppor
   ring_nf at mem ⊢
   assumption
 
-/- TODO: support always 0 in a field (elementary approach) -/
+theorem support_eq_bot {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) :
+    AddSubgroup.support P = ⊥ := by
+  refine AddSubgroup.ext (fun x => Iff.intro (fun h => ?_) (fun h => by aesop))
+  by_contra hz
+  apply minus_one_not_mem P
+  rw [show -1 = x * (-x)⁻¹ by field_simp [show x ≠ 0 by simp_all]]
+  aesop
+
+theorem support_eq_bot' {S F : Type*} [Field F] [SetLike S F] [RingPreorderingClass S F] (P : S) :
+    AddSubgroup.support P = ⊥ := by
+  rcases em <| (2 : F) = 0 with eq | neq
+  · refine False.elim <| minus_one_not_mem P ?_
+    rw [show (-1 : F) = 1 by linear_combination -eq]
+    apply one_mem
+  · apply AddSubgroup.ext
+    have : HasIdealSupport P := hasIdealSupport_of_isUnit_2 (by aesop)
+    have h : Ideal.support P = ⊥ := by
+      aesop (add unsafe forward (eq_bot_or_eq_top (Ideal.support P)),
+                 unsafe forward (Ideal.support_neq_top P))
+    have : ∀ x, x ∈ Ideal.support P ↔ x ∈ (⊥ : Ideal F) := by simp_all
+    rcases h with -
+    simp_all
+
+/- TODO : decide which proof to use -/
 
 /-!
 ## (Prime) orderings
@@ -118,13 +159,13 @@ instance IsOrdering.hasIdealSupport : HasIdealSupport P where
 
 end IsOrdering
 
-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
+instance support_isPrime [IsPrimeOrdering P] :
+    (Ideal.support P).IsPrime where
+  ne_top' h := minus_one_not_mem P (by aesop : 1 ∈ Ideal.support P).2
   mem_or_mem' := IsPrimeOrdering.mem_or_mem'
 
 instance isPrimeOrdering_of_isOrdering
-    [IsOrdering P] [(Ideal.preordering_support P).IsPrime] : IsPrimeOrdering P where
+    [IsOrdering P] [(Ideal.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)
 
@@ -133,7 +174,7 @@ theorem isPrimeOrdering_iff :
   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 :=
+    have : a ∈ Ideal.support P ∨ b ∈ Ideal.support P :=
       Ideal.IsPrime.mem_or_mem inferInstance (by simp_all)
     simp_all
   · refine ⟨by aesop, fun {x y} hxy => ?_⟩
@@ -173,12 +214,12 @@ instance comap.instIsOrdering (P : RingPreordering B) [IsOrdering P] (f : A →+
 
 @[simp]
 theorem mem_comap_support {P : RingPreordering B} {f : A →+* B} {x : A} :
-    x ∈ AddSubgroup.preordering_support (P.comap f) ↔ f x ∈ AddSubgroup.preordering_support P :=
+    x ∈ AddSubgroup.support (P.comap f) ↔ f x ∈ AddSubgroup.support P :=
   by simp
 
 @[simp]
 theorem comap_support {P : RingPreordering B} {f : A →+* B} :
-    AddSubgroup.preordering_support (P.comap f) = (AddSubgroup.preordering_support P).comap f :=
+    AddSubgroup.support (P.comap f) = (AddSubgroup.support P).comap f :=
   by ext; simp
 
 instance comap_hasIdealSupport (P : RingPreordering B) [HasIdealSupport P] (f : A →+* B) :
@@ -187,25 +228,25 @@ instance comap_hasIdealSupport (P : RingPreordering B) [HasIdealSupport P] (f :
 
 @[simp]
 theorem mem_comap_support' {P : RingPreordering B} [HasIdealSupport P] {f : A →+* B} {x : A} :
-    x ∈ Ideal.preordering_support (P.comap f) ↔ f x ∈ Ideal.preordering_support P := by simp
+    x ∈ Ideal.support (P.comap f) ↔ f x ∈ Ideal.support P := by simp
 
 @[simp]
 theorem comap_support' {P : RingPreordering B} [HasIdealSupport P] {f : A →+* B} :
-    Ideal.preordering_support (P.comap f) = (Ideal.preordering_support P).comap f :=
+    Ideal.support (P.comap f) = (Ideal.support P).comap f :=
   by ext; simp
 
 /-- The preimage of a prime ordering along a ring homomorphism is a prime ordering. -/
 instance comap.instIsPrimeOrdering (P : RingPreordering B) [IsPrimeOrdering P] (f : A →+* B) :
     IsPrimeOrdering (comap f P) := by
-  have : (Ideal.preordering_support (P.comap f)).IsPrime := by rw [comap_support']; infer_instance
+  have : (Ideal.support (P.comap f)).IsPrime := by rw [comap_support']; infer_instance
   infer_instance
 
 /-! ## map -/
 
 /-- The image of a preordering `P` along a surjective ring homomorphism
   with kernel contained in the support of `P` is a preordering. -/
 def map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f)
-    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) : RingPreordering B where
+    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) : RingPreordering B where
   __ := P.toSubsemiring.map f
   square_mem' x := by
     obtain ⟨x', rfl⟩ := hf x
@@ -218,43 +259,43 @@ def map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f)
 
 @[simp]
 theorem coe_map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f)
-    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) :
+    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) :
     (map hf hsupp : Set B) = f '' P := rfl
 
 @[simp]
 theorem mem_map {f : A →+* B} {P : RingPreordering A} (hf : Function.Surjective f)
-    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) :
+    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) :
     y ∈ map hf hsupp ↔ ∃ x ∈ P, f x = y := Iff.rfl
 
 /-- The image of an ordering `P` along a surjective ring homomorphism
   with kernel contained in the support of `P` is an ordering. -/
 instance map.instIsOrdering {f : A →+* B} {P : RingPreordering A} [IsOrdering P]
     (hf : Function.Surjective f)
-    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) :
+    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) :
     IsOrdering (map hf hsupp) where
   mem_or_neg_mem' x := by
     obtain ⟨x', rfl⟩ := hf x
     have := mem_or_neg_mem P x'
     aesop
 
-@[simp]
+@[simp↓]
 theorem mem_map_support {f : A →+* B} {P : RingPreordering A} {hf : Function.Surjective f}
-    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} {x : B} :
-    x ∈ AddSubgroup.preordering_support (map hf hsupp) ↔
-      ∃ y ∈ AddSubgroup.preordering_support P, f y = x := by
+    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} {x : B} :
+    x ∈ AddSubgroup.support (map hf hsupp) ↔
+      ∃ y ∈ AddSubgroup.support P, f y = x := by
   refine Iff.intro (fun ⟨⟨a, ⟨ha₁, ha₂⟩⟩, ⟨b, ⟨hb₁, hb₂⟩⟩⟩ => ?_) (by aesop)
   have : -(a + b) + b ∈ P := by exact add_mem (hsupp (show f (a + b) = 0 by simp_all)).2 hb₁
   aesop
 
 @[simp]
 theorem map_support {f : A →+* B} {P : RingPreordering A} {hf : Function.Surjective f}
-    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} :
-    AddSubgroup.preordering_support (map hf hsupp) = (AddSubgroup.preordering_support P).map f :=
-  by ext; rw [mem_map_support]; simp
+    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} :
+    AddSubgroup.support (map hf hsupp) = (AddSubgroup.support P).map f := by
+  ext; simp
 
 instance map_hasIdealSupport {f : A →+* B} {P : RingPreordering A} [HasIdealSupport P]
     (hf : Function.Surjective f)
-    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) :
+    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) :
     HasIdealSupport (map hf hsupp) where
   smul_mem_support' x a ha := by
     rw [mem_map_support] at ha
@@ -263,30 +304,30 @@ instance map_hasIdealSupport {f : A →+* B} {P : RingPreordering A} [HasIdealSu
     have := smul_mem_support P x' ha'
     aesop
 
-@[simp]
+@[simp↓]
 theorem mem_map_support' {f : A →+* B} {P : RingPreordering A} [HasIdealSupport P]
     {hf : Function.Surjective f}
-    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} {x : B} :
-    x ∈ Ideal.preordering_support (map hf hsupp) ↔
-      ∃ y ∈ Ideal.preordering_support P, f y = x := by simp [Ideal.preordering_support]
+    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} {x : B} :
+    x ∈ Ideal.support (map hf hsupp) ↔
+      ∃ y ∈ Ideal.support P, f y = x := by simp [Ideal.support]
 
 @[simp]
 theorem map_support' {f : A →+* B} {P : RingPreordering A} [HasIdealSupport P]
     {hf : Function.Surjective f}
-    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P} :
-    Ideal.preordering_support (map hf hsupp) = (Ideal.preordering_support P).map f := by
-  ext; rw [mem_map_support']; refine Iff.intro (fun h => ?_) (fun h => ?_)
-  · rcases h with ⟨x', hx', rfl⟩; exact Ideal.mem_map_of_mem f hx'
-  · exact Ideal.mem_image_of_mem_map_of_surjective f hf h
+    {hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P} :
+    Ideal.support (map hf hsupp) = (Ideal.support P).map f := by
+  ext; simp [Ideal.mem_map_iff_of_surjective f hf]
 
 /-- The image of a prime ordering `P` along a surjective ring homomorphism
   with kernel contained in the support of `P` is a prime ordering. -/
 instance map.instIsPrimeOrdering {f : A →+* B} {P : RingPreordering A} [IsPrimeOrdering P]
     (hf : Function.Surjective f)
-    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.preordering_support P) :
+    (hsupp : (RingHom.ker f : Set A) ⊆ AddSubgroup.support P) :
     IsPrimeOrdering (map hf hsupp) := by
-  have : (Ideal.preordering_support (map hf hsupp)).IsPrime := by
+  have : (Ideal.support (map hf hsupp)).IsPrime := by
     simpa using Ideal.map_isPrime_of_surjective hf (by simpa using hsupp)
   infer_instance
 
 end RingPreordering
+
+/- TODO : specialise to quotient map R ->> R/supp(P) -/