update

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

@@ -17,6 +17,20 @@ We also provide constructors that convert between
 cones in groups and the corresponding ordered groups.
 -/
 
+/-- `AddGroupConeClass S G` says that `S` is a type of cones in `G`. -/
+class AddGroupConeClass (S : Type*) (G : outParam Type*) [AddCommGroup G] [SetLike S G]
+    extends AddSubmonoidClass S G : Prop where
+  eq_zero_of_mem_of_neg_mem {C : S} {a : G} : a ∈ C → -a ∈ C → a = 0
+
+/-- `GroupConeClass S G` says that `S` is a type of cones in `G`. -/
+@[to_additive]
+class GroupConeClass (S : Type*) (G : outParam Type*) [CommGroup G] [SetLike S G] extends
+    SubmonoidClass S G : Prop where
+  eq_one_of_mem_of_inv_mem {C : S} {a : G} : a ∈ C → a⁻¹ ∈ C → a = 1
+
+export GroupConeClass (eq_one_of_mem_of_inv_mem)
+export AddGroupConeClass (eq_zero_of_mem_of_neg_mem)
+
 /-- A (positive) cone in an abelian group is a submonoid that
 does not contain both `a` and `-a` for any nonzero `a`.
 This is equivalent to being the set of non-negative elements of
@@ -33,77 +47,75 @@ structure GroupCone (G : Type*) [CommGroup G] extends Submonoid G where
   eq_one_of_mem_of_inv_mem' {a} : a ∈ carrier → a⁻¹ ∈ carrier → a = 1
 
 @[to_additive]
-instance (G : Type*) [CommGroup G] : SetLike (GroupCone G) G where
+instance GroupCone.instSetLike (G : Type*) [CommGroup G] : SetLike (GroupCone G) G where
   coe C := C.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
 @[to_additive]
-instance (G : Type*) [CommGroup G] : SubmonoidClass (GroupCone G) G where
+instance GroupCone.instGroupConeClass (G : Type*) [CommGroup G] :
+    GroupConeClass (GroupCone G) G where
   mul_mem {C} := C.mul_mem'
   one_mem {C} := C.one_mem'
+  eq_one_of_mem_of_inv_mem {C} := C.eq_one_of_mem_of_inv_mem'
 
-@[to_additive]
-protected theorem GroupCone.eq_one_of_mem_of_inv_mem {G : Type*} [CommGroup G] {C : GroupCone G}
-    {a : G} (h₁ : a ∈ C) (h₂ : a⁻¹ ∈ C) : a = 1 := C.eq_one_of_mem_of_inv_mem' h₁ h₂
+initialize_simps_projections GroupCone (carrier → coe, as_prefix coe)
+initialize_simps_projections AddGroupCone (carrier → coe, as_prefix coe)
 
 /-- Typeclass for maximal additive cones. -/
-class IsMaxCone {S G : Type*} [AddCommGroup G] [SetLike S G] (C : S) : Prop where
-  mem_or_neg_mem' (a : G) : a ∈ C ∨ -a ∈ C
-/- TODO : decide whether to unify with RingPreordering.IsOrdering as a "mixin" -/
+class IsMaxCone {S G : Type*} [AddGroup G] [SetLike S G] (C : S) : Prop where
+  mem_or_neg_mem (a : G) : a ∈ C ∨ -a ∈ C
 
 /-- Typeclass for maximal multiplicative cones. -/
 @[to_additive IsMaxCone]
-class IsMaxMulCone {S G : Type*} [CommGroup G] [SetLike S G] (C : S) : Prop where
-  mem_or_inv_mem' (a : G) : a ∈ C ∨ a⁻¹ ∈ C
+class IsMaxMulCone {S G : Type*} [Group G] [SetLike S G] (C : S) : Prop where
+  mem_or_inv_mem (a : G) : a ∈ C ∨ a⁻¹ ∈ C
 
-@[to_additive]
-theorem mem_or_inv_mem {S G : Type*} [CommGroup G] [SetLike S G] (C : S) [IsMaxMulCone C] (a : G) :
-    a ∈ C ∨ a⁻¹ ∈ C := IsMaxMulCone.mem_or_inv_mem' a
+export IsMaxCone (mem_or_neg_mem)
+export IsMaxMulCone (mem_or_inv_mem)
 
 namespace GroupCone
 variable {H : Type*} [OrderedCommGroup H] {a : H}
 
 variable (H) in
-/-- Construct a cone from the set of elements of
-a partially ordered abelian group that are at least 1. -/
-@[to_additive nonneg
-"Construct a cone from the set of non-negative elements of a partially ordered abelian group."]
+/-- The cone of elements that are at least 1. -/
+@[to_additive "The cone of non-negative elements."]
 def oneLE : GroupCone H where
   __ := Submonoid.oneLE H
   eq_one_of_mem_of_inv_mem' {a} := by simpa using ge_antisymm
 
-@[to_additive (attr := simp) nonneg_toAddSubmonoid]
+@[to_additive (attr := simp)]
 lemma oneLE_toSubmonoid : (oneLE H).toSubmonoid = .oneLE H := rfl
-@[to_additive (attr := simp) mem_nonneg]
+@[to_additive (attr := simp)]
 lemma mem_oneLE : a ∈ oneLE H ↔ 1 ≤ a := Iff.rfl
-@[to_additive (attr := simp, norm_cast) coe_nonneg]
+@[to_additive (attr := simp, norm_cast)]
 lemma coe_oneLE : oneLE H = {x : H | 1 ≤ x} := rfl
 
 @[to_additive nonneg.isMaxCone]
 instance oneLE.isMaxMulCone {H : Type*} [LinearOrderedCommGroup H] : IsMaxMulCone (oneLE H) where
-  mem_or_inv_mem' := by simpa using le_total 1
+  mem_or_inv_mem := by simpa using le_total 1
 
 end GroupCone
 
-variable {G : Type*} [CommGroup G] (C : GroupCone G)
+variable {S G : Type*} [CommGroup G] [SetLike S G] (C : S)
 
 /-- Construct a partially ordered abelian group by designating a cone in an abelian group. -/
 @[to_additive (attr := reducible)
 "Construct a partially ordered abelian group by designating a cone in an abelian group."]
-def OrderedCommGroup.mkOfCone :
+def OrderedCommGroup.mkOfCone [GroupConeClass S G] :
     OrderedCommGroup G where
   le a b := b / a ∈ C
   le_refl a := by simp [one_mem]
   le_trans a b c nab nbc := by simpa using mul_mem nbc nab
   le_antisymm a b nab nba := by
-    simpa [div_eq_one, eq_comm] using GroupCone.eq_one_of_mem_of_inv_mem nab (by simpa using nba)
+    simpa [div_eq_one, eq_comm] using eq_one_of_mem_of_inv_mem nab (by simpa using nba)
   mul_le_mul_left a b nab c := by simpa using nab
 
 /-- Construct a linearly ordered abelian group by designating a maximal cone in an abelian group. -/
 @[to_additive (attr := reducible)
 "Construct a linearly ordered abelian group by designating a maximal cone in an abelian group."]
-def LinearOrderedCommGroup.mkOfCone [IsMaxMulCone C] (dec : DecidablePred (· ∈ C)) :
+def LinearOrderedCommGroup.mkOfCone
+    [GroupConeClass S G] [IsMaxMulCone C] [DecidablePred (· ∈ C)] :
     LinearOrderedCommGroup G where
   __ := OrderedCommGroup.mkOfCone C
-  le_total a b := by simpa using mem_or_inv_mem C (b / a)
-  decidableLE _ _ := dec _
+  le_total a b := by simpa using mem_or_inv_mem (b / a)
+  decidableLE _ := _

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

@@ -6,9 +6,6 @@ Authors: Jeremy Avigad, Leonardo de Moura, Mario Carneiro, Artie Khovanov
 import RealClosedField.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.Operations
-import Mathlib.GroupTheory.Coset.Defs
 
 /-!
 # Construct ordered rings from rings with a specified positive cone.
@@ -21,6 +18,10 @@ We also provide constructors that convert between
 cones in rings and the corresponding ordered rings.
 -/
 
+/-- `RingConeClass S R` says that `S` is a type of cones in `R`. -/
+class RingConeClass (S : Type*) (R : outParam Type*) [Ring R] [SetLike S R]
+    extends AddGroupConeClass S R, SubsemiringClass S R : Prop
+
 /-- A (positive) cone in a ring is a subsemiring that
 does not contain both `a` and `-a` for any nonzero `a`.
 This is equivalent to being the set of non-negative elements of
@@ -30,33 +31,24 @@ structure RingCone (R : Type*) [Ring R] extends Subsemiring R, AddGroupCone R
 /-- Interpret a cone in a ring as a cone in the underlying additive group. -/
 add_decl_doc RingCone.toAddGroupCone
 
-instance (R : Type*) [Ring R] : SetLike (RingCone R) R where
+instance RingCone.instSetLike (R : Type*) [Ring R] : SetLike (RingCone R) R where
   coe C := C.carrier
   coe_injective' p q h := by cases p; cases q; congr; exact SetLike.ext' h
 
-instance (R : Type*) [Ring R] : SubsemiringClass (RingCone R) R where
+instance RingCone.instRingConeClass (R : Type*) [Ring R] :
+    RingConeClass (RingCone R) R where
   add_mem {C} := C.add_mem'
   zero_mem {C} := C.zero_mem'
   mul_mem {C} := C.mul_mem'
   one_mem {C} := C.one_mem'
+  eq_zero_of_mem_of_neg_mem {C} := C.eq_zero_of_mem_of_neg_mem'
 
 namespace RingCone
 
-protected theorem eq_zero_of_mem_of_neg_mem {R : Type*} [Ring R] {C : RingCone R}
-    {a : R} (h₁ : a ∈ C) (h₂ : -a ∈ C) : a = 0 := C.eq_zero_of_mem_of_neg_mem' h₁ h₂
-
-@[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
-/-- Construct a cone from the set of non-negative elements of a partially ordered ring. -/
+/-- The cone of non-negative elements. -/
 def nonneg : RingCone T where
   __ := Subsemiring.nonneg T
   eq_zero_of_mem_of_neg_mem' {a} := by simpa using ge_antisymm
@@ -67,113 +59,28 @@ def nonneg : RingCone T where
 @[simp, norm_cast] lemma coe_nonneg : nonneg T = {x : T | 0 ≤ x} := rfl
 
 instance nonneg.isMaxCone {T : Type*} [LinearOrderedRing T] : IsMaxCone (nonneg T) where
-  mem_or_neg_mem' := mem_or_neg_mem <| AddGroupCone.nonneg T
+  mem_or_neg_mem := mem_or_neg_mem (C := AddGroupCone.nonneg T)
 
 end RingCone
 
-variable {R : Type*} [Ring R] (C : RingCone R)
+variable {S R : Type*} [Ring R] [SetLike S R] (C : S)
 
 /-- Construct a partially ordered ring by designating a cone in a ring.
 Warning: using this def as a constructor in an instance can lead to diamonds
 due to non-customisable field: `lt`. -/
-@[reducible] def OrderedRing.mkOfCone : OrderedRing R where
+@[reducible] def OrderedRing.mkOfCone [RingConeClass S R] : OrderedRing R where
   __ := ‹Ring R›
-  __ := OrderedAddCommGroup.mkOfCone C.toAddGroupCone
-  zero_le_one := show _ ∈ C by simpa using C.one_mem
-  mul_nonneg _ _ hx hy := show _ ∈ C by simpa using C.mul_mem hx hy
+  __ := OrderedAddCommGroup.mkOfCone C
+  zero_le_one := show _ ∈ C by simpa using one_mem C
+  mul_nonneg x y xnn ynn := show _ ∈ C by simpa using mul_mem xnn ynn
 
 /-- Construct a linearly ordered domain by designating a maximal cone in a domain.
 Warning: using this def as a constructor in an instance can lead to diamonds
 due to non-customisable fields: `lt`, `decidableLT`, `decidableEq`, `compare`. -/
 @[reducible] def LinearOrderedRing.mkOfCone
-    [IsDomain R] [IsMaxCone C] [DecidablePred (· ∈ C)] : LinearOrderedRing R where
+    [IsDomain R] [RingConeClass S R] [IsMaxCone C] [DecidablePred (· ∈ C)] :
+  LinearOrderedRing R where
   __ := OrderedRing.mkOfCone C
   __ := OrderedRing.toStrictOrderedRing R
-  le_total a b := by simpa using mem_or_neg_mem C (b - a)
-  decidableLE a b := _
-
-@[reducible]
-def RingPreordering.mkOfCone {R : Type*} [Nontrivial R] [CommRing R] (C : RingCone R) [IsMaxCone C] :
-    RingPreordering R where
-  __ := RingCone.toSubsemiring C
-  isSquare_mem' x := by
-    rcases x with ⟨y, rfl⟩
-    cases mem_or_neg_mem C y with
-    | inl h  => aesop
-    | inr h => simpa using (show -y * -y ∈ C by aesop (config := { enableSimp := false }))
-  minus_one_not_mem' h := one_ne_zero <| RingCone.eq_zero_of_mem_of_neg_mem (one_mem _) h
-
-/-- A maximal cone over a commutative ring `R` is an ordering on `R`. -/
-instance {R : Type*} [CommRing R] [Nontrivial R] (C : RingCone R) [IsMaxCone C] :
-    RingPreordering.IsOrdering <| RingPreordering.mkOfCone C where
-  mem_or_neg_mem' x := mem_or_neg_mem C x
-
-/- TODO : decide what to do about the maximality typeclasses -/
-
-@[reducible] def RingCone.mkOfRingPreordering {R : Type*} [CommRing R] {P : RingPreordering R}
-    (hP : RingPreordering.AddSubgroup.support P = ⊥) : RingCone R where
-  __ := 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 {R : Type*} [CommRing R]
-    {P : RingPreordering R} [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 {R : Type*} [CommRing R] [IsDomain R]
-    {P : RingPreordering R} [RingPreordering.IsOrdering P] [DecidablePred (· ∈ P)]
-    (hP : RingPreordering.AddSubgroup.support P = ⊥) : LinearOrderedRing R :=
-  mkOfCone <| RingCone.mkOfRingPreordering hP
-
-@[reducible] def RingCone.mkOfRingPreordering_field {F : Type*} [Field F] (P : RingPreordering F) :
-    RingCone F := mkOfRingPreordering <| RingPreordering.support_eq_bot P
-
-@[reducible] def LinearOrderedRing.mkOfRingPreordering_field {F : Type*} [Field F]
-    (P : RingPreordering F) [DecidablePred (· ∈ P)] [RingPreordering.IsOrdering P] :
-    LinearOrderedRing F :=
-  mkOfCone <| RingCone.mkOfRingPreordering_field P
-
-@[reducible] def RingCone.mkOfRingPreordering_quot {R : Type*} [CommRing R] (P : RingPreordering R)
-    [RingPreordering.IsOrdering P] : RingCone (R ⧸ (RingPreordering.Ideal.support P)) := by
-  refine mkOfRingPreordering (P := P.map Ideal.Quotient.mk_surjective (by simp)) ?_
-  have : Ideal.map (Ideal.Quotient.mk <| RingPreordering.Ideal.support P)
-    (RingPreordering.Ideal.support P) = ⊥ := by simp
-  ext x
-  apply_fun (x ∈ ·) at this
-  rw [Ideal.mem_map_iff_of_surjective _ Ideal.Quotient.mk_surjective] at this
-  simp_all
-  /- TODO : make this proof better -/
-
-/- TODO : move to the right place -/
-theorem Quotient.image_mk_eq_lift {α : Type*} {s : Setoid α} (A : Set α)
-    (h : ∀ x y, x ≈ y → (x ∈ A ↔ y ∈ A)) :
-    (Quotient.mk s) '' A = (Quotient.lift (· ∈ A) (by simpa)) := by
-  aesop (add unsafe forward Quotient.exists_rep)
-
-/- TODO : move to the right place -/
-@[to_additive]
-theorem QuotientGroup.mem_iff_mem_of_quotientRel {G : Type*} [CommGroup G] {H : Subgroup G}
-    {M : Submonoid G} (hM : (H : Set G) ⊆ M) :
-    ∀ x y, QuotientGroup.leftRel H x y → (x ∈ M ↔ y ∈ M) := fun x y hxy => by
-  rw [QuotientGroup.leftRel_apply] at hxy
-  exact ⟨fun h => by have := mul_mem h <| hM hxy; simpa,
-        fun h => by have := mul_mem h <| hM <| inv_mem hxy; simpa⟩
-
-@[reducible] def LinearOrderedRing.mkOfRingPreordering_quot {R : Type*} [CommRing R]
-    (P : RingPreordering R) [RingPreordering.IsPrimeOrdering P] [DecidablePred (· ∈ P)] :
-    LinearOrderedRing (R ⧸ (RingPreordering.Ideal.support P)) :=
-  /- technical instance -/
-  /- TODO : generalise this quotient instance? -/
-  have : DecidablePred (· ∈ RingCone.mkOfRingPreordering_quot P) := by
-    rw [show (· ∈ RingCone.mkOfRingPreordering_quot P) = (· ∈ (Quotient.mk _) '' P) by rfl]
-    have : ∀ x y, (RingPreordering.Ideal.support P).quotientRel x y → (x ∈ P ↔ y ∈ P) :=
-      QuotientAddGroup.mem_iff_mem_of_quotientRel
-        (M := P.toAddSubmonoid) (H := (RingPreordering.Ideal.support P).toAddSubgroup)
-        (by aesop (add unsafe apply Set.sep_subset))
-    rw [Quotient.image_mk_eq_lift _ this]
-    exact Quotient.lift.decidablePred (· ∈ P) (by simpa)
-  mkOfCone (RingCone.mkOfRingPreordering_quot P)
+  le_total a b := by simpa using mem_or_neg_mem (b - a)
+  decidableLE _ := _

RealClosedField/Mathlib/Algebra/Ring/Semireal/Defs.lean

@@ -3,7 +3,7 @@ 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 Mathlib.Algebra.Ring.SumsOfSquares
+import RealClosedField.Mathlib.Algebra.Ring.SumsOfSquares
 
 /-!
 # Semireal rings

RealClosedField/RealClosedField/FormallyReal.lean

@@ -63,7 +63,7 @@ instance LinearOrderedRing.instIsFormallyReal [LinearOrderedRing R] : IsFormally
       (mul_self_nonneg <| x i))
 
 namespace RingCone
-variable {T : Type*} [CommRing T] [IsFormallyReal T] {a : T}
+variable {T : Type*} [CommRing T] [IsFormallyReal T]
 
 variable (T) in
 /--
@@ -76,7 +76,7 @@ def sumSqIn : RingCone T where
     IsFormallyReal.eq_zero_of_isSumSq_of_sum_eq_zero hx hnx (add_neg_cancel x)
 
 @[simp] lemma sumSqIn_toSubsemiring : (sumSqIn T).toSubsemiring = .sumSqIn T := rfl
-@[simp] lemma mem_sumSqIn : a ∈ sumSqIn T ↔ IsSumSq a := Iff.rfl
+@[simp] lemma mem_sumSqIn {a : T} : a ∈ sumSqIn T ↔ IsSumSq a := Iff.rfl
 @[simp, norm_cast] lemma coe_sumSqIn : sumSqIn T = {x : T | IsSumSq x} := rfl
 
 end RingCone