English
There exists an injective order-preserving (as an additive monoid hom) embedding from M into Lex(HahnSeries(FiniteArchimedeanClass M) ℝ), with a compatibility describing how mk a is realized via ofLex (f a).orderTop.
Русский
Существует инъективное упорядоченное вложение от M в Lex(HahnSeries(FiniteArchimedeanClass M) ℝ), сохраняющее аддитивную структуру и совместимое с mk a через ofLex (f a).orderTop.
LaTeX
$$$ \\exists f : M \\to_ {+o}^{\\mathbb{Q}} \\; \\mathrm{Lex} (\\mathrm{HahnSeries} (\\mathrm{FiniteArchimedeanClass} M) \\mathbb{R}),\\; \\text{Injective } f \\wedge ∀ a, mk a = \\mathrm{FiniteArchimedeanClass.withTopOrderIso M (\\mathrm{ofLex} (f a)).orderTop} $$$
Lean4
/-- **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]
