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 ℝ⟦Ω⟧, where Ω is the type of 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.

instance instNonemptySeedRatReal (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module ℚ M] [IsOrderedModule ℚ M] : Nonempty (HahnEmbedding.Seed ℚ M ℝ)

theorem hahnEmbedding_isOrderedModule_rat (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] [Module ℚ M] [IsOrderedModule ℚ M] : ∃ (f : M →ₗ[ℚ] Lex (HahnSeries (FiniteArchimedeanClass M) ℝ)), StrictMono ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

theorem hahnEmbedding_isOrderedAddMonoid (M : Type u_1) [AddCommGroup M] [LinearOrder M] [IsOrderedAddMonoid M] : ∃ (f : M →+o Lex (HahnSeries (FiniteArchimedeanClass M) ℝ)), Function.Injective ⇑f ∧ ∀ (a : M), ArchimedeanClass.mk a = (FiniteArchimedeanClass.withTopOrderIso M) (ofLex (f a)).orderTop

Hahn embedding theorem

For a linearly ordered additive group M, there exists an injective OrderAddMonoidHom from M to Lex ℝ⟦FiniteArchimedeanClass M⟧ that sends each a : M to an element of the a-Archimedean class of the Hahn series.