feat(GroupTheory): add DivisibleHull

Author: wwylele

Mathlib.lean

@@ -3878,6 +3878,7 @@ import Mathlib.GroupTheory.Coxeter.Inversion
 import Mathlib.GroupTheory.Coxeter.Length
 import Mathlib.GroupTheory.Coxeter.Matrix
 import Mathlib.GroupTheory.Divisible
+import Mathlib.GroupTheory.DivisibleHull
 import Mathlib.GroupTheory.DoubleCoset
 import Mathlib.GroupTheory.EckmannHilton
 import Mathlib.GroupTheory.Exponent

Mathlib/GroupTheory/DivisibleHulll.lean

@@ -0,0 +1,273 @@
+/-
+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.LocalizedModule.Basic
+import Mathlib.Algebra.Order.GroupWithZero.Submonoid
+import Mathlib.Algebra.Order.Module.Archimedean
+import Mathlib.Algebra.Order.Module.Defs
+import Mathlib.GroupTheory.Divisible
+import Mathlib.RingTheory.Localization.FractionRing
+
+/-!
+# Divisible Hull of an Abelian group
+
+This file constructs the divisible hull of an Abelian group as a ℤ-module localized by
+`Submonoid.pos ℤ`. Further more, we show that `DivisibleHul` is an ordered ℚ-module when the source
+group is linearly ordered, and that `ArchimedeanClass` are preserved.
+
+## Implementation notes
+
+This could be equivalently implemented as localization by `ℤ`, but it will complicate the ordering
+implementation.
+
+-/
+
+instance : IsLocalization (Submonoid.pos ℤ) ℚ where
+  map_units' a := by simpa using ne_of_gt a.prop
+  surj' z := by
+    obtain ⟨⟨x1, x2⟩, hx⟩ := IsLocalization.surj (nonZeroDivisors ℤ) z
+    obtain hx2 | hx2 := lt_or_gt_of_ne (show x2.val ≠ 0 by simp)
+    · exact ⟨⟨-x1, ⟨-x2.val, by simpa using hx2⟩⟩, by simpa using hx⟩
+    · exact ⟨⟨x1, ⟨x2.val, hx2⟩⟩, hx⟩
+  exists_of_eq {x y} h := ⟨1, by simpa using Rat.intCast_inj.mp h⟩
+
+variable (M : Type*) [AddCommGroup M]
+
+abbrev DivisibleHull := LocalizedModule (Submonoid.pos ℤ) M
+
+namespace DivisibleHull
+variable {M}
+
+def mk (m : M) (s : Submonoid.pos ℤ) : DivisibleHull M := LocalizedModule.mk m s
+
+theorem ind {motive : DivisibleHull M → Prop} (mk : ∀ num den, motive (.mk num den)) :
+    ∀ x, motive x := by
+  apply LocalizedModule.induction_on
+  intro a
+  apply mk
+
+def liftOn {α : Type*} (x : DivisibleHull M)
+    (f : M → (Submonoid.pos ℤ) → α)
+    (h : ∀ (m m' : M) (s s' : Submonoid.pos ℤ), mk m s = mk m' s' → f m s = f m' s') : α :=
+  LocalizedModule.liftOn x (Function.uncurry f) fun p p' heq ↦
+    h p.1 p'.1 p.2 p'.2 (Quotient.eq'.mpr heq)
+
+@[simp]
+theorem liftOn_mk {α : Type*} (m : M) (s : Submonoid.pos ℤ)
+    (f : M → (Submonoid.pos ℤ) → α)
+    (h : ∀ (m m' : M) (s s' : Submonoid.pos ℤ), mk m s = mk m' s' → f m s = f m' s') :
+    liftOn (mk m s) f h = f m s := rfl
+
+def liftOn₂ {α : Type*} (x y : DivisibleHull M)
+    (f : M → (Submonoid.pos ℤ) → M → (Submonoid.pos ℤ) → α)
+    (h : ∀ (m n m' n' : M) (s t s' t' : Submonoid.pos ℤ),
+      mk m s = mk m' s' → mk n t = mk n' t' → f m s n t = f m' s' n' t') : α :=
+  LocalizedModule.liftOn₂ x y (fun p q ↦ f p.1 p.2 q.1 q.2) fun p q p' q' heq heq' ↦
+    h p.1 q.1 p'.1 q'.1 p.2 q.2 p'.2 q'.2 (Quotient.eq'.mpr heq) (Quotient.eq'.mpr heq')
+
+theorem mk_eq_mk {m m' : M} {s s' : Submonoid.pos ℤ} :
+    mk m s = mk m' s' ↔ ∃ u : Submonoid.pos ℤ, u • s' • m = u • s • m' := by
+  unfold mk
+  exact LocalizedModule.mk_eq
+
+theorem mk_eq_mk_iff_smul_eq_smul [IsAddTorsionFree M] {m m' : M} {s s' : Submonoid.pos ℤ} :
+    mk m s = mk m' s' ↔ s' • m = s • m' := by
+  rw [mk_eq_mk]
+  constructor
+  · intro ⟨u, h⟩
+    simp_rw [Submonoid.smul_def] at ⊢ h
+    exact (smul_right_inj (ne_of_gt u.prop)).mp h
+  · intro hr
+    use 1
+    rw [hr]
+
+theorem mk_add_mk {m1 m2 : M} {s1 s2 : Submonoid.pos ℤ} :
+    mk m1 s1 + mk m2 s2 = mk (s2 • m1 + s1 • m2) (s1 * s2) := LocalizedModule.mk_add_mk
+
+theorem mk_neg (m : M) (s : Submonoid.pos ℤ) : mk (-m) s = -mk m s := LocalizedModule.mk_neg
+
+theorem qsmul_mk (a : ℚ) (m : M) (s : Submonoid.pos ℤ) :
+    a • mk m s = mk (a.num • m) (⟨a.den, Int.natCast_pos.mpr a.den_pos⟩ * s) := by
+  convert LocalizedModule.mk'_smul_mk ℚ a.num m ⟨a.den, Int.natCast_pos.mpr a.den_pos⟩ s
+  rw [IsLocalization.eq_mk'_iff_mul_eq]
+  simp
+
+theorem zsmul_mk (a : ℤ) (m : M) (s : Submonoid.pos ℤ) : a • mk m s = mk (a • m) s := by
+  suffices (a : ℚ) • mk m s = mk (a • m) s by
+    rw [Int.cast_smul_eq_zsmul] at this
+    exact this
+  rw [qsmul_mk]
+  exact congrArg _ <| Subtype.eq (by simp)
+
+theorem nsmul_mk (a : ℕ) (m : M) (s : Submonoid.pos ℤ) : a • mk m s = mk (a • m) s := by
+  suffices (a : ℤ) • mk m s = mk ((a : ℤ) • m) s by simpa using this
+  exact zsmul_mk _ _ _
+
+instance : DivisibleBy (DivisibleHull M) ℕ where
+  div m n :=
+    if h : n = 0 then
+      0
+    else
+      liftOn m (fun m s ↦ mk m (⟨s.val * n, by
+        rw [Submonoid.mem_pos]
+        apply mul_pos s.prop
+        simpa using Nat.pos_of_ne_zero h
+      ⟩)) (by
+        intro m m' s s'
+        suffices ∀ a : ℤ, 0 < a → a • s' • m = a • s • m' →
+            ∃ a : ℤ, 0 < a ∧ a • (s'.val * n) • m = a • (s.val * n) • m' by simpa [mk_eq_mk]
+        intro a ha h
+        simp_rw [Submonoid.smul_def] at h
+        refine ⟨a, ha, ?_⟩
+        simp_rw [smul_smul, ← mul_assoc, mul_comm _ (n : ℤ)]
+        simp_rw [mul_smul]
+        rw [h]
+      )
+  div_zero := by simp
+  div_cancel n {m} h := by
+    induction m using ind with | mk m s
+    suffices ∃ a : ℤ, 0 < a ∧ a • s • n • m = a • (s.val * n) • m by simpa [h, nsmul_mk, mk_eq_mk]
+    use 1
+    suffices s • n • m = (s.val * n) • m by simpa
+    rw [mul_smul, natCast_zsmul, Submonoid.smul_def]
+
+variable [LinearOrder M] [IsOrderedAddMonoid M]
+
+instance : LE (DivisibleHull M) where
+  le x y := liftOn₂ x y (fun m s n t ↦ t • m ≤ s • n) fun m n m' n' s t s' t' h h' ↦ by
+    rw [mk_eq_mk_iff_smul_eq_smul] at h h'
+    suffices t • m ≤ s • n ↔ t' • m' ≤ s' • n' by simpa
+    simp_rw [Submonoid.smul_def] at ⊢ h h'
+    rw [← zsmul_le_zsmul_iff_right (mul_pos s'.prop t'.prop)]
+    rw [show (s'.val * t'.val) • t.val • m = (t.val * t'.val) • s'.val • m by
+      simp_rw [smul_smul]
+      ring_nf]
+    rw [show (s'.val * t'.val) • s.val • n = (s.val * s'.val) • t'.val • n by
+      simp_rw [smul_smul]
+      ring_nf]
+    rw [h, h']
+    rw [show (t.val * t'.val) • s.val • m' = (s.val * t.val) • t'.val • m' by
+      simp_rw [smul_smul]
+      ring_nf]
+    rw [show (s.val * s'.val) • t.val • n' = (s.val * t.val) • s'.val • n' by
+      simp_rw [smul_smul]
+      ring_nf]
+    exact zsmul_le_zsmul_iff_right (mul_pos s.prop t.prop)
+
+theorem mk_le_mk {m m' : M} {s s' : Submonoid.pos ℤ} :
+    mk m s ≤ mk m' s' ↔ s' • m ≤ s • m' := by rfl
+
+theorem mk_le_mk_left {m m' : M} {s : Submonoid.pos ℤ} :
+    mk m s ≤ mk m' s ↔ m ≤ m' := by
+  simpa [mk_le_mk, Submonoid.smul_def] using zsmul_le_zsmul_iff_right s.prop
+
+instance : PartialOrder (DivisibleHull M) where
+  le_refl a := by
+    induction a using ind with | mk m s
+    rw [mk_le_mk]
+  le_trans a b c hab hbc := by
+    induction a using ind with | mk ma sa
+    induction b using ind with | mk mb sb
+    induction c using ind with | mk mc sc
+    rw [mk_le_mk, Submonoid.smul_def] at ⊢ hab hbc
+    rw [← zsmul_le_zsmul_iff_right (show 0 < sb.val from sb.prop)]
+    rw [← zsmul_le_zsmul_iff_right (show 0 < sc.val from sc.prop)] at hab
+    rw [← zsmul_le_zsmul_iff_right (show 0 < sa.val from sa.prop)] at hbc
+    rw [smul_comm _ _ ma, smul_comm _ _ mc]
+    rw [smul_comm _ _ mb] at hab
+    exact hab.trans hbc
+  le_antisymm a b h h' := by
+    induction a using ind with | mk ma sa
+    induction b using ind with | mk mb sb
+    rw [mk_le_mk] at h h'
+    rw [mk_eq_mk_iff_smul_eq_smul]
+    exact le_antisymm h h'
+
+noncomputable
+instance : LinearOrder (DivisibleHull M) where
+  le_total a b := by
+    induction a using ind with | mk ma sa
+    induction b using ind with | mk mb sb
+    exact le_total _ _
+  toDecidableLE := Classical.decRel LE.le
+
+noncomputable
+instance : IsOrderedAddMonoid (DivisibleHull M) where
+  add_le_add_left a b h c := by
+    induction a using ind with | mk ma sa
+    induction b using ind with | mk mb sb
+    induction c using ind with | mk mc sc
+    rw [mk_le_mk] at h
+    simp_rw [mk_add_mk, mk_le_mk, smul_add, ← mul_smul]
+    rw [mul_right_comm sc sa sb, add_le_add_iff_left]
+    rw [mul_right_comm sc sa sc, mul_right_comm sc sb sc]
+    rw [mul_smul _ _ ma, mul_smul _ _ mb]
+    exact zsmul_le_zsmul_right (le_of_lt (sc * sc).prop) h
+
+noncomputable
+instance : PosSMulStrictMono ℚ (DivisibleHull M) where
+  elim a ha b c h := by
+    induction b using ind with | mk mb sb
+    induction c using ind with | mk mc sc
+    contrapose! h
+    simp_rw [qsmul_mk, mk_le_mk, Submonoid.smul_def, Submonoid.mul_def] at h
+    simp_rw [← mul_smul, mul_right_comm _ _ a.num, mul_smul _ _ mc, mul_smul _ _ mb] at h
+    rw [mk_le_mk]
+    refine (zsmul_le_zsmul_iff_right ?_).mp h
+    exact mul_pos (Int.natCast_pos.mpr a.den_pos) (Rat.num_pos.mpr ha)
+
+variable (M) in
+noncomputable
+def orderAddMonoidHom : M →+o DivisibleHull M where
+  __ := LocalizedModule.mkLinearMap _ _
+  map_zero' := by simp
+  monotone' := by
+    intro a b h
+    suffices mk a 1 ≤ mk b 1 by simpa using this
+    rw [mk_le_mk]
+    simpa using h
+
+@[simp]
+theorem orderAddMonoidHom_apply (a : M) : (orderAddMonoidHom M) a = mk a 1 := by rfl
+
+variable (M) in
+theorem orderAddMonoidHom_injective : Function.Injective (orderAddMonoidHom M) := by
+  intro a b
+  simp [mk_eq_mk_iff_smul_eq_smul]
+
+theorem mk_max (m1 m2 : M) (s : Submonoid.pos ℤ) : mk (max m1 m2) s = max (mk m1 s) (mk m2 s) := by
+  obtain h | h := le_total m1 m2
+  all_goals simpa [h] using mk_le_mk_left.mpr h
+
+theorem mk_min (m1 m2 : M) (s : Submonoid.pos ℤ) : mk (min m1 m2) s = min (mk m1 s) (mk m2 s) := by
+  obtain h | h := le_total m1 m2
+  all_goals simpa [h] using mk_le_mk_left.mpr h
+
+theorem mk_abs (m : M) (s : Submonoid.pos ℤ) : mk |m| s = |mk m s| := by
+  simp_rw [abs, mk_max, mk_neg]
+
+variable (M) in
+noncomputable
+def archimedeanClassOrderHom : ArchimedeanClass M →o ArchimedeanClass (DivisibleHull M) :=
+  ArchimedeanClass.orderHom (orderAddMonoidHom M)
+
+variable (M) in
+theorem archimedeanClassOrderHom_injective : Function.Injective (archimedeanClassOrderHom M) :=
+  ArchimedeanClass.orderHom_injective (orderAddMonoidHom_injective M)
+
+variable (M) in
+theorem archimedeanClassOrderHom_surjective : Function.Surjective (archimedeanClassOrderHom M) := by
+  intro A
+  induction A using ArchimedeanClass.ind with | mk a
+  induction a using ind with | mk m s
+  use ArchimedeanClass.mk m
+  suffices ArchimedeanClass.mk (mk m 1) = ArchimedeanClass.mk (mk m s) by
+    simpa using this
+  rw [show mk m 1 = s.val • mk m s by
+    simp [zsmul_mk, mk_eq_mk_iff_smul_eq_smul, Submonoid.smul_def]]
+  exact ArchimedeanClass.mk_smul _ (ne_of_gt s.prop)
+
+end DivisibleHull