feat: Hahn embedding theorem

Author: wwylele

Mathlib.lean

@@ -844,6 +844,7 @@ import Mathlib.Algebra.Order.Group.DenselyOrdered
 import Mathlib.Algebra.Order.Group.End
 import Mathlib.Algebra.Order.Group.Equiv
 import Mathlib.Algebra.Order.Group.Finset
+import Mathlib.Algebra.Order.Group.HahnEmbedding
 import Mathlib.Algebra.Order.Group.Indicator
 import Mathlib.Algebra.Order.Group.InjSurj
 import Mathlib.Algebra.Order.Group.Instances

Mathlib/Algebra/Order/Archimedean/Class.lean

@@ -707,4 +707,22 @@ theorem withTopOrderIso_symm_apply {a : M} (h : a ≠ 1) :
   unfold mk withTopOrderIso
   convert WithTop.subtypeOrderIso_symm_apply (MulArchimedeanClass.mk_eq_top_iff.ne.mpr h)
 
+variable {N : Type*} [CommGroup N] [LinearOrder N] [IsOrderedMonoid N]
+
+@[to_additive]
+noncomputable
+def congrOrderIso (e : MulArchimedeanClass M ≃o MulArchimedeanClass N) :
+    FiniteMulArchimedeanClass M ≃o FiniteMulArchimedeanClass N where
+  __ := Equiv.subtypeEquiv e (by simp)
+  map_rel_iff' := by simp
+
+@[to_additive (attr := simp)]
+theorem coe_congrOrderIso (e : MulArchimedeanClass M ≃o MulArchimedeanClass N)
+    (a : FiniteMulArchimedeanClass M) :
+    (congrOrderIso e a : MulArchimedeanClass N) = e a := rfl
+
+@[to_additive (attr := simp)]
+theorem congrOrderIso_symm (e : MulArchimedeanClass M ≃o MulArchimedeanClass N) :
+    (congrOrderIso e).symm = congrOrderIso e.symm := rfl
+
 end FiniteMulArchimedeanClass

Mathlib/Algebra/Order/Group/HahnEmbedding.lean

@@ -0,0 +1,114 @@
+/-
+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.Order.Module.HahnEmbedding
+import Mathlib.Algebra.Module.LinearMap.Rat
+import Mathlib.Algebra.Field.Rat
+import Mathlib.Analysis.RCLike.Basic
+import Mathlib.Data.Real.Embedding
+import Mathlib.GroupTheory.DivisibleHull
+import Mathlib.LinearAlgebra.Basis.VectorSpace
+
+/-!
+
+# Hahn embedding theorem
+
+In this file, we prove the Hahn embedding theorem: every linearly ordered abelian group
+can be embedded as an ordered subgroup of `Lex (HahnSeries Ω ℝ)`, where `Ω` is the finite
+Archimedean classes of the group. The theorem is stated as
+`exists_orderAddMonoidHom_hahnSeries_real_injective_and_archimedeanClassMk_eq`.
+
+## References
+
+* [A. H. Clifford, *Note on Hahn’s theorem on ordered Abelian groups.*][zbMATH03090187]
+
+-/
+
+open ArchimedeanClass
+
+variable (M : Type*) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M]
+
+section Module
+variable [Module ℚ M] [PosSMulMono ℚ M]
+
+instance : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := by
+  have : ComplementedLattice (Submodule ℚ M) := inferInstance
+  have stratum (c : ArchimedeanClass M) :
+      ∃ G : Submodule ℚ M, Disjoint (ball ℚ c) G ∧ ball ℚ c ⊔ G = closedBall ℚ c := by
+    apply IsModularLattice.exists_disjoint_and_sup_eq
+    apply ball_le_closedBall
+  choose g h1 h2 using stratum
+  exact ⟨g, h1, h2⟩
+
+instance : Nonempty (HahnEmbedding.Seed ℚ M ℝ) := by
+  obtain ⟨strata⟩ : Nonempty (HahnEmbedding.ArchimedeanStrata ℚ M) := inferInstance
+  choose f hf using fun c ↦ Archimedean.exists_orderAddMonoidHom_real_injective (strata.stratum c)
+  refine ⟨strata, fun c ↦ (f c).toRatLinearMap, fun c ↦ ?_⟩
+  apply Monotone.strictMono_of_injective
+  · simpa using (f c).monotone'
+  · simpa using hf c
+
+theorem exists_linearMap_hahnSeries_real_strictMono_and_archimedeanClassMk_eq :
+    ∃ f : M →ₗ[ℚ] Lex (HahnSeries (FiniteArchimedeanClass M) ℝ), StrictMono f ∧
+      ∀ (a : M), mk a = FiniteArchimedeanClass.withTopOrderIso M (ofLex (f a)).orderTop := by
+  apply exists_linearMap_hahnSeries_strictMono_and_archimedeanClassMk_eq
+
+end Module
+
+/--
+**Hahn embedding theorem**
+
+For a linearly ordered additive group `M`, there exists an `OrderAddMonoidHom` from `M` to
+`Lex (HahnSeries (FiniteArchimedeanClass M) ℝ)` that is injective, and transfers the Archimedean
+class of each element to `HahnSeries.orderTop`.
+-/
+theorem exists_orderAddMonoidHom_hahnSeries_real_injective_and_archimedeanClassMk_eq :
+    ∃ f : M →+o Lex (HahnSeries (FiniteArchimedeanClass M) ℝ), Function.Injective f ∧
+      ∀ (a : M), mk a = FiniteArchimedeanClass.withTopOrderIso M (ofLex (f a)).orderTop := by
+  /-
+  The desired embedding is the composition of three functions:
+
+      Group type                                    `ArchimedeanClass` / `HahnSeries.orderTop` type
+
+      `M`                                           `ArchimedeanClass M`
+  `f₁` ↓+o                                           ↓o~
+      `D-Hull M`                                    `ArchimedeanClass (D-Hull M)`
+  `f₂` ↓+o                                           ↓o~
+      `Lex (HahnSeries (F-A-Class (D-Hull M)) ℝ)`   `WithTop (F-A-Class (D-Hull M))`
+  `f₃` ↓+o(~)                                        ↓o~
+      `Lex (HahnSeries (F-A-Class M) ℝ)`            `WithTop (F-A-Class M)`
+  -/
+
+  let f₁ := DivisibleHull.coeOrderAddMonoidHom M
+  have hf₁ : Function.Injective f₁ := DivisibleHull.coeOrderAddMonoidHom_injective
+  have hf₁class (a : M) : mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (mk (f₁ a)) := by
+    simp [f₁]
+
+  obtain ⟨f₂', hf₂', hf₂class'⟩ :=
+    exists_linearMap_hahnSeries_real_strictMono_and_archimedeanClassMk_eq (DivisibleHull M)
+  let f₂ := OrderAddMonoidHom.mk f₂'.toAddMonoidHom hf₂'.monotone
+  have hf₂ : Function.Injective f₂ := hf₂'.injective
+  have hf₂class (a : DivisibleHull M) :
+      mk a = (FiniteArchimedeanClass.withTopOrderIso (DivisibleHull M)) (ofLex (f₂ a)).orderTop :=
+    hf₂class' a
+
+  let f₃ : Lex (HahnSeries (FiniteArchimedeanClass (DivisibleHull M)) ℝ) →+o
+      Lex (HahnSeries (FiniteArchimedeanClass M) ℝ) :=
+    HahnSeries.embDomainOrderAddMonoidHom
+    (FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M).symm)
+  have hf₃ : Function.Injective f₃ := HahnSeries.embDomainOrderAddMonoidHom_injective _
+  have hf₃class (a : Lex (HahnSeries (FiniteArchimedeanClass (DivisibleHull M)) ℝ)) :
+      (ofLex a).orderTop = OrderIso.withTopCongr
+      ((FiniteArchimedeanClass.congrOrderIso (DivisibleHull.archimedeanClassOrderIso M)))
+      (ofLex (f₃ a)).orderTop := by
+    rw [← OrderIso.symm_apply_eq]
+    simp [f₃, ← OrderIso.withTopCongr_symm]
+
+  refine ⟨f₃.comp (f₂.comp f₁), hf₃.comp (hf₂.comp hf₁), ?_⟩
+  intro a
+  simp_rw [hf₁class, hf₂class, hf₃class, OrderAddMonoidHom.comp_apply]
+  cases (ofLex (f₃ (f₂ (f₁ a)))).orderTop with
+  | top => simp
+  | coe x => simp [-DivisibleHull.archimedeanClassOrderIso_apply]

Mathlib/Algebra/Order/Module/Archimedean.lean

@@ -100,4 +100,11 @@ theorem ball_antitone : Antitone (ball (M := M) K) := by
   intro _ _ h
   exact (Submodule.toAddSubgroup_le _ _).mp <| ballAddSubgroup_antitone h
 
+theorem ball_le_closedBall (c : ArchimedeanClass M) :
+    ball K c ≤ closedBall K c := by
+  obtain rfl | hc := eq_or_ne c ⊤
+  · simp
+  intro a ha
+  simpa using ((mem_ball_iff K hc).mp ha).le
+
 end ArchimedeanClass

Mathlib/GroupTheory/DivisibleHull.lean

@@ -62,14 +62,9 @@ def mk (m : M) (s : nonZeroDivisors ℕ) : DivisibleHull M := LocalizedModule.mk
 instance : Coe M (DivisibleHull M) where
   coe m := mk m 1
 
-theorem coe_eq_mk (m : M) : m = mk m 1 := rfl
-
 @[simp]
 theorem mk_zero (s : nonZeroDivisors ℕ) : mk (0 : M) s = 0 := by simp [mk]
 
-@[simp]
-theorem coe_zero : (0 : M) = (0 : DivisibleHull M) := by simp
-
 theorem ind {motive : DivisibleHull M → Prop} (mk : ∀ num den, motive (.mk num den)) :
     ∀ x, motive x := by
   apply LocalizedModule.induction_on

Mathlib/RingTheory/HahnSeries/Basic.lean

@@ -484,6 +484,21 @@ theorem embDomain_injective {f : Γ ↪o Γ'} :
   have xyg := xy (f g)
   rwa [embDomain_coeff, embDomain_coeff] at xyg
 
+@[simp]
+theorem orderTop_embDomain {Γ : Type*} [LinearOrder Γ] {f : Γ ↪o Γ'} {x : HahnSeries Γ R} :
+    (embDomain f x).orderTop = WithTop.map f x.orderTop := by
+  obtain rfl | hx := eq_or_ne x 0
+  · simp
+  rw [← WithTop.coe_untop x.orderTop (by simpa using hx), WithTop.map_coe]
+  apply orderTop_eq_of_le
+  · simpa using HahnSeries.coeff_orderTop_ne (by simp)
+  intro y hy
+  obtain ⟨z, hz, rfl⟩ :=
+    (Set.mem_image _ _ _).mp <| Set.mem_of_subset_of_mem support_embDomain_subset hy
+  rw [OrderEmbedding.le_iff_le, WithTop.untop_le_iff]
+  apply HahnSeries.orderTop_le_of_coeff_ne_zero
+  simpa using hz
+
 end Domain
 
 end Zero

Mathlib/RingTheory/HahnSeries/Lex.lean

@@ -353,4 +353,55 @@ end Archimedean
 
 end OrderedGroup
 
+
+section EmbDomain
+variable {Γ Γ' R : Type*} [LinearOrder Γ] [LinearOrder Γ'] [Zero R] [PartialOrder R]
+variable (f : Γ ↪o Γ')
+
+/-- `HahnSeries.embDomain` as an `OrderEmbedding`. -/
+@[simps]
+noncomputable
+def embDomainOrderEmbedding : Lex (HahnSeries Γ R) ↪o Lex (HahnSeries Γ' R) where
+  toFun a := toLex (HahnSeries.embDomain f (ofLex a))
+  inj' := HahnSeries.embDomain_injective
+  map_rel_iff' {a b} := by
+    simp_rw [le_iff_lt_or_eq, lt_iff]
+    simp only [Function.Embedding.coeFn_mk, ofLex_toLex, EmbeddingLike.apply_eq_iff_eq]
+    constructor
+    · rintro (⟨i, hj, hi⟩ | heq)
+      · have himem : i ∈ Set.range f := by
+          contrapose! hi
+          simp [embDomain_notin_range hi]
+        obtain ⟨k, hk⟩ := himem
+        rw [← hk] at hj hi
+        refine Or.inl ⟨k, fun j hjk ↦ ?_, by simpa using hi⟩
+        simpa using hj (f j) (f.lt_iff_lt.mpr hjk)
+      · exact Or.inr <| HahnSeries.embDomain_injective heq
+    · rintro (⟨i, hj, hi⟩ | rfl)
+      · refine Or.inl ⟨f i, fun k hki ↦ ?_, by simpa using hi⟩
+        by_cases hkmem : k ∈ Set.range f
+        · obtain ⟨j', hj'⟩ := hkmem
+          rw [← hj'] at ⊢ hki
+          simpa using hj _ <| f.lt_iff_lt.mp hki
+        · simp_rw [embDomain_notin_range hkmem]
+      · simp
+
+variable {Γ Γ' R : Type*} [LinearOrder Γ] [LinearOrder Γ'] [AddMonoid R] [PartialOrder R]
+variable (f : Γ ↪o Γ')
+
+/-- `HahnSeries.embDomain` as an `OrderAddMonoidHom`. -/
+@[simps]
+noncomputable
+def embDomainOrderAddMonoidHom : Lex (HahnSeries Γ R) →+o Lex (HahnSeries Γ' R) where
+  toFun := embDomainOrderEmbedding f
+  map_zero' := by simp
+  map_add' a b := embDomain_add f a b
+  monotone' := OrderEmbedding.monotone _
+
+theorem embDomainOrderAddMonoidHom_injective :
+    Function.Injective (embDomainOrderAddMonoidHom f (R := R)) := embDomain_injective
+
+
+end EmbDomain
+
 end HahnSeries

docs/1000.yaml

@@ -3157,6 +3157,9 @@ Q5638112:
 
 Q5638886:
   title: Hahn embedding theorem
+  decl: exists_orderAddMonoidHom_hahnSeries_real_injective
+  authors: Weiyi Wang
+  date: 2025
 
 Q5643485:
   title: Halpern–Läuchli theorem

docs/references.bib

@@ -4526,6 +4526,21 @@ @Book{            zbMATH02107988
   zbl           = {1052.54001}
 }
 
+@Article{         zbMATH03090187,
+  author        = {Clifford, A. H.},
+  title         = {Note on {Hahn}'s theorem on ordered {Abelian} groups},
+  fjournal      = {Proceedings of the American Mathematical Society},
+  journal       = {Proc. Am. Math. Soc.},
+  issn          = {0002-9939},
+  volume        = {5},
+  pages         = {860--863},
+  year          = {1954},
+  language      = {English},
+  doi           = {10.2307/2032549},
+  zbMATH        = {3090187},
+  Zbl           = {0056.25503}
+}
+
 @Article{         zbMATH06785026,
   author        = {John F. {Clauser} and Michael A. {Horne} and Abner
                   {Shimony} and Richard A. {Holt}},