feat: Hahn embedding theorem (leanprover-community#27268)

This proves [Hahn embedding theorem](https://en.wikipedia.org/wiki/Hahn_embedding_theorem), one among the 1000+ theorems project.

Note on file location: I originally placed it in Algebra/Order/Group, but got prompted that Algebra can't import Analysis (needed for `Real` being a `Rat`-module` and related fact), so now I moved it under HahnSeries

Author: wwylele

Mathlib.lean

@@ -5587,6 +5587,7 @@ import Mathlib.RingTheory.Grassmannian
 import Mathlib.RingTheory.HahnSeries.Addition
 import Mathlib.RingTheory.HahnSeries.Basic
 import Mathlib.RingTheory.HahnSeries.HEval
+import Mathlib.RingTheory.HahnSeries.HahnEmbedding
 import Mathlib.RingTheory.HahnSeries.Lex
 import Mathlib.RingTheory.HahnSeries.Multiplication
 import Mathlib.RingTheory.HahnSeries.PowerSeries

Mathlib/Algebra/Order/Module/HahnEmbedding.lean

@@ -28,7 +28,7 @@ under `ArchimedeanClass.closedBall K c`. The embeddings from these submodules ar
 `HahnEmbedding.Seed K M R`.
 
 By setting `K = ℚ` and `R = ℝ`, the condition can be trivially satisfied, leading
-to a proof of the classic Hahn embedding theorem. (TODO: implement this)
+to a proof of the classic Hahn embedding theorem. (See `hahnEmbedding_isOrderedAddMonoid`)
 
 ## Main theorem
 

Mathlib/RingTheory/HahnSeries/HahnEmbedding.lean

@@ -0,0 +1,102 @@
+/-
+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
+
+/-!
+
+# 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 `hahnEmbedding_isOrderedAddMonoid`.
+
+## References
+
+* [A. H. Clifford, *Note on Hahn’s theorem on ordered Abelian groups.*][clifford1954]
+
+-/
+
+open ArchimedeanClass
+
+variable (M : Type*) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M]
+
+section Module
+variable [Module ℚ M] [IsOrderedModule ℚ M]
+
+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 OrderHomClass.monotone (f c)
+  · simpa using hf c
+
+theorem hahnEmbedding_isOrderedModule_rat :
+    ∃ f : M →ₗ[ℚ] Lex (HahnSeries (FiniteArchimedeanClass M) ℝ), StrictMono f ∧
+      ∀ a, mk a = FiniteArchimedeanClass.withTopOrderIso M (ofLex (f a)).orderTop := by
+  apply hahnEmbedding_isOrderedModule
+
+end Module
+
+/--
+**Hahn embedding theorem**
+
+For a linearly ordered additive group `M`, there exists an injective `OrderAddMonoidHom` from `M` to
+`Lex (HahnSeries (FiniteArchimedeanClass M) ℝ)` that sends each `a : M` to an element of the
+`a`-Archimedean class of the Hahn series.
+-/
+theorem hahnEmbedding_isOrderedAddMonoid :
+    ∃ f : M →+o Lex (HahnSeries (FiniteArchimedeanClass M) ℝ), Function.Injective f ∧
+      ∀ a, 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.coe_injective
+  have hf₁class (a : M) : mk a = (DivisibleHull.archimedeanClassOrderIso M).symm (mk (f₁ a)) := by
+    simp [f₁]
+
+  obtain ⟨f₂', hf₂', hf₂class'⟩ := hahnEmbedding_isOrderedModule_rat (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]

docs/1000.yaml

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

docs/references.bib

@@ -1139,6 +1139,21 @@ @Book{            clark_gon
   url           = {http://alpha.math.uga.edu/~pete/geometryofnumbers.pdf}
 }
 
+@Article{         clifford1954,
+  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{         cockett1993,
   author        = {J.R.B. Cockett},
   title         = {Introduction to Distributive Categories},