English
The Hahn embedding theorem for an ordered module asserts the existence of a strict monomorphism from M into Lex(HahnSeries(...)) preserving Archimedean structure.
Русский
Теорема Ган-встраивания для упорядоченного модуля утверждает существование строгого монофункционального отображения из M в Lex(HahnSeries(...)) сохраняющего Archimedean структуру.
LaTeX
$$$\\exists f : M \\to_\\mathbb{K}^\\mathrm{lex} \\; (\\text{HahnSeries}(\\mathrm{FiniteArchimedeanClass} M)\\, R), \\; \\text{StrictMono}(f) \\land \\dots$$$
Lean4
/-- **Hahn embedding theorem for an ordered module**
There exists a strictly monotone `M →ₗ[K] Lex (HahnSeries (FiniteArchimedeanClass M) R)` that maps
`ArchimedeanClass M` to `HahnSeries.orderTop` in the expected way, as long as
`HahnEmbedding.Seed K M R` is nonempty. The `HahnEmbedding.Partial` with maximal domain is the
desired embedding. -/
theorem hahnEmbedding_isOrderedModule [IsOrderedAddMonoid R] [Archimedean R] [h : Nonempty (HahnEmbedding.Seed K M R)] :
∃ f : M →ₗ[K] Lex (HahnSeries (FiniteArchimedeanClass M) R),
StrictMono f ∧ ∀ (a : M), mk a = FiniteArchimedeanClass.withTopOrderIso M (ofLex (f a)).orderTop :=
by
obtain ⟨e, hdomain⟩ := HahnEmbedding.Partial.exists_domain_eq_top h.some
obtain harch := e.orderTop_eq_archimedeanClassMk
obtain ⟨⟨fdomain, f⟩, hpartial⟩ := e
obtain rfl := hdomain
refine ⟨f ∘ₗ LinearMap.id.codRestrict ⊤ (by simp), ?_, ?_⟩
· apply hpartial.strictMono.comp
intro _ _ h
simpa [← Subtype.coe_lt_coe] using h
· simp_rw [LinearPMap.mk_apply] at harch
simp [harch]
