feat: ArchimedeanSubgroup

Author: wwylele

Mathlib.lean

@@ -871,9 +871,11 @@ import Mathlib.Algebra.Order.Interval.Set.SuccPred
 import Mathlib.Algebra.Order.Invertible
 import Mathlib.Algebra.Order.Kleene
 import Mathlib.Algebra.Order.Module.Algebra
+import Mathlib.Algebra.Order.Module.Archimedean
 import Mathlib.Algebra.Order.Module.Basic
 import Mathlib.Algebra.Order.Module.Defs
 import Mathlib.Algebra.Order.Module.Field
+import Mathlib.Algebra.Order.Module.HahnEmbedding
 import Mathlib.Algebra.Order.Module.OrderedSMul
 import Mathlib.Algebra.Order.Module.Pointwise
 import Mathlib.Algebra.Order.Module.PositiveLinearMap

Mathlib/Algebra/Order/Archimedean/Class.lean

@@ -4,10 +4,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Weiyi Wang
 -/
 import Mathlib.Algebra.BigOperators.Group.Finset.Basic
+import Mathlib.Algebra.Group.Subgroup.Lattice
+import Mathlib.Algebra.Group.Subgroup.Order
 import Mathlib.Algebra.Order.Archimedean.Basic
 import Mathlib.Algebra.Order.Hom.Monoid
 import Mathlib.Data.Finset.Max
 import Mathlib.Order.Antisymmetrization
+import Mathlib.Order.SupIndep
+import Mathlib.Order.UpperLower.CompleteLattice
+import Mathlib.Order.UpperLower.Principal
 
 /-!
 # Archimedean classes of a linearly ordered group
@@ -451,6 +456,185 @@ theorem liftOrderHom_mk (f : M → α) (h : ∀ a b, mk a ≤ mk b → f a ≤ f
 
 end LiftHom
 
+/-- Given a non-empty `UpperSet` of `MulArchimedeanClass`,
+all group elements belonging to these classes form a subgroup. -/
+@[to_additive "Given a non-empty `UpperSet` of `ArchimedeanClass`,
+all group elements belonging to these classes form a subgroup."]
+def subgroup' {s : UpperSet (MulArchimedeanClass M)} (hs : s ≠ ⊤) : Subgroup M where
+  carrier := mk ⁻¹' s
+  mul_mem' {a b} ha hb := by
+    rw [Set.mem_preimage] at ha hb ⊢
+    obtain h | h := min_le_iff.mp (min_le_mk_mul a b)
+    · exact s.upper h ha
+    · exact s.upper h hb
+  one_mem' := by
+    rw [Set.mem_preimage]
+    obtain ⟨u, hu⟩ := UpperSet.coe_nonempty.mpr hs
+    simpa using s.upper (by simp) hu
+  inv_mem' {a} h := by simpa using h
+
+/-- Extend `MulArchimedeanClass.subgroup'` to any `UpperSet`
+with a junk value `⊥` assigned to the empty set. -/
+@[to_additive "Extend `ArchimedeanClass.subgroup'` to any `UpperSet`
+with a junk value `⊥` assigned to the empty set."]
+noncomputable
+def subgroup (s : UpperSet (MulArchimedeanClass M)) : Subgroup M :=
+  open Classical in
+  if hs : s = ⊤ then
+    ⊥
+  else
+    subgroup' hs
+
+variable {s : UpperSet (MulArchimedeanClass M)}
+
+@[to_additive]
+theorem subgroup_eq_of_ne_top (hs : s ≠ ⊤) : subgroup s = subgroup' hs := by
+  simp [subgroup, hs]
+
+variable (M) in
+@[to_additive (attr := simp)]
+theorem subgroup_eq_bot : subgroup (M := M) ⊤ = ⊥ := by
+  simp [subgroup]
+
+@[to_additive]
+theorem mem_subgroup_iff (hs : s ≠ ⊤) : a ∈ subgroup s ↔ mk a ∈ s := by
+  rw [subgroup_eq_of_ne_top hs]
+  exact Set.mem_preimage
+
+/-- An open ball defined by `MulArchimedeanClass.subgroup` of `UpperSet.Ioi A`.
+For `A = ⊤`, we assign the junk value `⊥`. -/
+@[to_additive "An open ball defined by `ArchimedeanClass.addSubgroup` of `UpperSet.Ioi A`.
+For `A = ⊤`, we assign the junk value `⊥`. "]
+noncomputable
+abbrev ballSubgroup (A : MulArchimedeanClass M) := subgroup (UpperSet.Ioi A)
+
+/-- A closed ball defined by `MulArchimedeanClass.subgroup` of `UpperSet.Ici A`. -/
+@[to_additive "An closed ball defined by `ArchimedeanClass.addSubgroup` of `UpperSet.Ici A`."]
+noncomputable
+abbrev closedBallSubgroup (A : MulArchimedeanClass M) := subgroup (UpperSet.Ici A)
+
+@[to_additive]
+theorem mem_ballSubgroup_iff {a : M} {A : MulArchimedeanClass M} (hA : A ≠ ⊤) :
+    a ∈ ballSubgroup A ↔ A < mk a := by
+  have : UpperSet.Ioi A ≠ ⊤ := by
+    contrapose! hA
+    rw [UpperSet.ext_iff] at hA
+    simpa using hA
+  simp [mem_subgroup_iff this]
+
+@[to_additive (attr := simp)]
+theorem mem_closedBallSubgroup_iff {a : M} {A : MulArchimedeanClass M} :
+    a ∈ closedBallSubgroup A ↔ A ≤ mk a := by
+  have : UpperSet.Ici A ≠ ⊤ := by simp
+  simp [mem_subgroup_iff this]
+
+variable (M) in
+@[to_additive (attr := simp)]
+theorem ballSubgroup_top : ballSubgroup (M := M) ⊤ = ⊥ := by
+  convert subgroup_eq_bot M
+  simp
+
+variable (M) in
+@[to_additive (attr := simp)]
+theorem closedBallSubgroup_top : closedBallSubgroup (M := M) ⊤ = ⊥ := by
+  ext
+  simp
+
+variable (M) in
+@[to_additive]
+theorem subgroup_strictAntiOn : StrictAntiOn (subgroup (M := M)) (Set.Iio ⊤) := by
+  intro s hs t ht hst
+  rw [subgroup_eq_of_ne_top (Set.mem_Iio.mp hs).ne_top]
+  rw [subgroup_eq_of_ne_top (Set.mem_Iio.mp ht).ne_top]
+  apply lt_of_le_of_ne
+  · rw [Subgroup.mk_le_mk]
+    exact (Set.preimage_subset_preimage_iff (by simp)).mpr (by simpa using hst.le)
+  · contrapose! hst with heq
+    apply le_of_eq
+    simpa [mk_surjective, subgroup'] using heq
+
+variable (M) in
+@[to_additive]
+theorem subgroup_antitone : Antitone (subgroup (M := M)) := by
+  intro s t hst
+  obtain hs | rfl := ne_or_eq s ⊤
+  · obtain ht | rfl := ne_or_eq t ⊤
+    · exact ((subgroup_strictAntiOn M).le_iff_le
+        (Set.mem_Iio.mpr ht.lt_top) (Set.mem_Iio.mpr hs.lt_top)).mpr hst
+    · simp
+  · rw [eq_top_iff.mpr hst]
+
+variable (M) in
+@[to_additive]
+theorem ballSubgroup_antitone : Antitone (ballSubgroup (M := M)) := by
+  intro A B h
+  exact subgroup_antitone _ <| (UpperSet.Ioi_strictMono _).monotone h
+
+
+/-- A subgroup `G` is called a grade at `c` iff
+`ballSubgroup c` and `G` are complements in the lattice under `closedBallSubgroup c`. -/
+@[to_additive /-- A subgroup `G` is called a grade at `c` iff
+`ballAddSubgroup c` and `G` are complements in the lattice under `closedBallAddSubgroup c`. -/]
+def IsGradeSubgroup (c : MulArchimedeanClass M) (G : Subgroup M) : Prop :=
+  Disjoint (ballSubgroup c) G ∧ ballSubgroup c ⊔ G = closedBallSubgroup c
+
+namespace IsGradeSubgroup
+variable {c : MulArchimedeanClass M} {G : Subgroup M}
+
+@[to_additive]
+theorem disjoint (hgrade : IsGradeSubgroup c G) : Disjoint (ballSubgroup c) G := hgrade.1
+
+@[to_additive]
+theorem sup_eq (hgrade : IsGradeSubgroup c G) : ballSubgroup c ⊔ G = closedBallSubgroup c :=
+  hgrade.2
+
+@[to_additive]
+theorem eq_bot_iff (hgrade : IsGradeSubgroup c G) : G = ⊥ ↔ c = ⊤ := by
+  obtain hsup := hgrade.sup_eq
+  constructor
+  · rintro rfl
+    replace hsup : c.ballSubgroup = c.closedBallSubgroup := by simpa using hsup
+    contrapose! hsup with h
+    apply Subgroup.ext_iff.not.mpr
+    induction c using ind with | mk a
+    rw [not_forall]
+    exact ⟨a, by simp [h]⟩
+  · rintro rfl
+    simpa using hsup
+
+@[to_additive]
+theorem nontrivial (hgrade : IsGradeSubgroup c G) (h : c ≠ ⊤) : Nontrivial G :=
+  (Subgroup.nontrivial_iff_ne_bot _).mpr (hgrade.eq_bot_iff.ne.mpr h)
+
+@[to_additive]
+theorem le_closedBallSubgroup (hgrade : IsGradeSubgroup c G) : G ≤ closedBallSubgroup c := by
+  simp [← hgrade.sup_eq]
+
+@[to_additive archimedeanClassMk_eq]
+theorem mulArchimedeanClassMk_eq (hgrade : IsGradeSubgroup c G) {a : M} (ha : a ∈ G) (h0 : a ≠ 1) :
+    mk a = c := by
+  apply le_antisymm
+  · have hA : c ≠ ⊤ := by
+      contrapose! h0
+      rw [hgrade.eq_bot_iff.mpr h0] at ha
+      simpa using ha
+    contrapose! h0 with hlt
+    have ha' : a ∈ ballSubgroup c := (mem_ballSubgroup_iff hA).mpr hlt
+    exact (Subgroup.disjoint_def.mp hgrade.disjoint) ha' ha
+  · simpa using hgrade.le_closedBallSubgroup ha
+
+@[to_additive archimedean]
+theorem mulArchimedean (hgrade : IsGradeSubgroup c G) : MulArchimedean G := by
+  apply mulArchimedean_of_mk_eq_mk
+  intro a ha b hb
+  suffices mk a.val = mk b.val by
+    rw [mk_eq_mk] at this ⊢
+    exact this
+  rw [hgrade.mulArchimedeanClassMk_eq a.prop (by simpa using ha)]
+  rw [hgrade.mulArchimedeanClassMk_eq b.prop (by simpa using hb)]
+
+end IsGradeSubgroup
+
 end MulArchimedeanClass
 
 variable (M) in

Mathlib/Algebra/Order/Module/Archimedean.lean

@@ -0,0 +1,150 @@
+/-
+Copyright (c) 2025 Weiyi Wang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Weiyi Wang
+-/
+
+import Mathlib.Algebra.Module.Submodule.Order
+import Mathlib.Algebra.Order.Archimedean.Class
+import Mathlib.Algebra.Order.Module.Basic
+import Mathlib.LinearAlgebra.DFinsupp
+
+/-!
+# Further lemmas related to Archimedean classes for ordered module.
+
+## Main definitions
+* `ArchimedeanClass.ball` and `ArchimedeanClass.closedBall`:
+  `ArchimedeanClass.ballAddSubgroup` and `ArchimedeanClass.closedBallAddSubgroup` as a submodules.
+* `ArchimedeanClass.IsGrade`: The module version of `ArchimedeanClass.IsGradeAddSubgroup`.
+-/
+
+namespace ArchimedeanClass
+
+variable {M : Type*}
+variable [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M]
+variable {K : Type*} [Ring K] [LinearOrder K] [IsOrderedRing K] [Archimedean K]
+variable [Module K M] [PosSMulMono K M]
+
+variable (K) in
+/-- For a ordered module over an `Archimedean` ring,
+`ArchimedeanClass.addSubgroup` is a submodule. -/
+noncomputable
+def submodule (s : UpperSet (ArchimedeanClass M)) : Submodule K M where
+  __ := addSubgroup s
+  smul_mem' k {a} := by
+    obtain rfl | hs := eq_or_ne s ⊤
+    · aesop
+    · change a ∈ addSubgroup s → k • a ∈ addSubgroup s
+      simp_rw [mem_addSubgroup_iff hs]
+      intro ha
+      obtain _ | _ := subsingleton_or_nontrivial K
+      · rw [Subsingleton.eq_zero k]
+        simpa using (IsUpperSet.top_mem s.upper).mpr <| UpperSet.coe_nonempty.mpr hs
+      · obtain ⟨n, hn⟩ := Archimedean.arch |k| (show 0 < 1 by simp)
+        refine s.upper (mk_le_mk.mpr ⟨n, ?_⟩) ha
+        have : n • |a| = (n • (1 : K)) • |a| := by rw [smul_assoc, one_smul]
+        rw [this, abs_smul]
+        exact smul_le_smul_of_nonneg_right hn (by simp)
+
+variable (K) in
+/-- `ArchimedeanClass.ballAddSubgroup` as a submodule. -/
+noncomputable
+abbrev ball (A : ArchimedeanClass M) := submodule K (UpperSet.Ioi A)
+
+variable (K) in
+/-- `ArchimedeanClass.closedBallAddSubgroup` as a submodule. -/
+noncomputable
+abbrev closedBall (A : ArchimedeanClass M) := submodule K (UpperSet.Ici A)
+
+variable (K) in
+theorem toAddSubgroup_ball (A : ArchimedeanClass M) :
+    (ball K A).toAddSubgroup = ballAddSubgroup A := rfl
+
+variable (K) in
+theorem toAddSubgroup_closedBall (A : ArchimedeanClass M) :
+    (closedBall K A).toAddSubgroup = closedBallAddSubgroup A := rfl
+
+variable (K) in
+theorem mem_ball_iff {a : M} {A : ArchimedeanClass M} (hA : A ≠ ⊤) : a ∈ ball K A ↔ A < mk a :=
+  mem_ballAddSubgroup_iff hA
+
+variable (K) in
+@[simp]
+theorem mem_closedBall_iff {a : M} {A : ArchimedeanClass M} : a ∈ closedBall K A ↔ A ≤ mk a :=
+  mem_closedBallAddSubgroup_iff
+
+variable (M K) in
+@[simp]
+theorem ball_top : ball (M := M) K ⊤ = ⊥ :=
+  (Submodule.toAddSubgroup_inj _ _).mp <| ballAddSubgroup_top M
+
+variable (M K) in
+@[simp]
+theorem closedBall_top : closedBall (M := M) K ⊤ = ⊥ :=
+  (Submodule.toAddSubgroup_inj _ _).mp <| closedBallAddSubgroup_top M
+
+variable (M K) in
+theorem ball_antitone : Antitone (ball (M := M) K) := by
+  intro A B h
+  exact (Submodule.toAddSubgroup_le _ _).mp <| ballAddSubgroup_antitone M h
+
+/-- The module version of `ArchimedeanClass.IsGradeAddSubgroup`. -/
+def IsGrade (A : ArchimedeanClass M) (G : Submodule K M) :=
+  Disjoint (ball K A) G ∧ ball K A ⊔ G = closedBall K A
+
+namespace IsGrade
+variable {A : ArchimedeanClass M} {G : Submodule K M}
+
+theorem disjoint (hgrade : IsGrade A G) : Disjoint (ball K A) G := hgrade.1
+
+theorem sup_eq (hgrade : IsGrade A G) : ball K A ⊔ G = closedBall K A := hgrade.2
+
+theorem isGradeAddSubgroup (hgrade : IsGrade A G) : IsGradeAddSubgroup A G.toAddSubgroup := by
+  constructor
+  · simpa [disjoint_iff, ← SetLike.coe_set_eq] using hgrade.disjoint
+  · rw [← toAddSubgroup_ball K A, ← toAddSubgroup_closedBall K A]
+    rw [← Submodule.sup_toAddSubgroup, hgrade.sup_eq]
+
+theorem nontrivial (hgrade : IsGrade A G) (h : A ≠ ⊤) : Nontrivial G :=
+  hgrade.isGradeAddSubgroup.nontrivial h
+
+theorem archimedeanClass_eq (hgrade : IsGrade A G) {a : M} (ha : a ∈ G) (h0 : a ≠ 0) : mk a = A :=
+  hgrade.isGradeAddSubgroup.archimedeanClass_eq ha h0
+
+theorem archimedean (hgrade : IsGrade A G) : Archimedean G :=
+  hgrade.isGradeAddSubgroup.archimedean
+
+end IsGrade
+
+theorem iSupIndep_of_isGrade {F : ArchimedeanClass M → Submodule K M}
+    (hgrade : ∀ A : ArchimedeanClass M, IsGrade A (F A)) : iSupIndep F := by
+  rw [iSupIndep_def]
+  intro A
+  rw [Submodule.disjoint_def']
+  intro a ha b hb hab
+  obtain ⟨f, hf⟩ := (Submodule.mem_iSup_iff_exists_dfinsupp' _ b).mp hb
+  obtain hf' := congrArg mk hf
+  contrapose! hf' with h0
+  rw [← hab, DFinsupp.sum]
+  by_cases hnonempty : f.support.Nonempty
+  · have hmem (x : ArchimedeanClass M) : (f x).val ∈ F x :=
+      Set.mem_of_mem_of_subset (f x).prop (by simp)
+    have hmono : StrictMonoOn (fun i ↦ mk (f i).val) f.support := by
+      intro x hx y hy hxy
+      change mk (f x).val < mk (f y).val
+      rw [(hgrade x).archimedeanClass_eq (hmem x) (by simpa using hx)]
+      rw [(hgrade y).archimedeanClass_eq (hmem y) (by simpa using hy)]
+      exact hxy
+    rw [mk_sum hnonempty hmono]
+    rw [(hgrade _).archimedeanClass_eq (hmem _)
+      (by simpa using Finset.min'_mem f.support hnonempty)]
+    by_contra!
+    obtain h := this ▸ Finset.min'_mem f.support hnonempty
+    contrapose! h
+    rw [DFinsupp.notMem_support_iff, (hgrade _).archimedeanClass_eq ha h0]
+    simpa using (f A).prop
+  · rw [Finset.not_nonempty_iff_eq_empty.mp hnonempty]
+    symm
+    simpa using h0
+
+end ArchimedeanClass