English
Equality of baseEmbedding to a constructed expression via hahnCoeff and decompositions is established, i.e., seed.baseEmbedding equals a composed map built from seed.hahnCoeff.
Русский
Справляется равенство базового вложения с построенным выражением через hahnCoeff и разложения: seed.baseEmbedding равен композиции из seed.hahnCoeff.
LaTeX
$$$ seed.baseEmbedding = { domain := seed.baseDomain, toFun := (toLexLinearEquiv K (HahnSeries (FiniteArchimedeanClass M) R)).toLinearMap \circ (HahnSeries.ofFinsuppLinearMap _) \circ (Finsupp.lcomapDomain Subtype.val_injective) \circ (finsuppLequivDFinsupp K).symm.toLinearMap \circ seed.hahnCoeff } $$$
Lean4
theorem hahnCoeff_apply {x : seed.baseDomain} {f : Π₀ c, seed.stratum c}
(h : x.val = f.sum fun c ↦ (seed.stratum c).subtype) (c : ArchimedeanClass M) :
seed.hahnCoeff x c = seed.coeff c (f c) :=
by
suffices seed.baseDomain.subtype.submoduleComap (seed.stratum c) (DirectSum.decompose seed.stratum' x c) = f c by
simp [Seed.hahnCoeff, coeff', this]
have hxm {c : ArchimedeanClass M} (x : seed.stratum c) : x.val ∈ seed.baseDomain :=
by
apply Set.mem_of_mem_of_subset x.prop
simpa using le_iSup _ _
let f' : ⨁ c, seed.stratum' c := f.mapRange (fun c x ↦ (⟨⟨x.val, hxm x⟩, by simp⟩ : seed.stratum' c)) (by simp)
have hf : f c = (seed.baseDomain.subtype.submoduleComap (seed.stratum c)) (f' c) :=
by
apply Subtype.eq
simp [f']
have hx : x = (decompose seed.stratum').symm f' :=
by
change x = f'.coeAddMonoidHom _
apply Submodule.subtype_injective
rw [DirectSum.coeAddMonoidHom_eq_dfinsuppSum, DFinsupp.sum_mapRange_index (by simp)]
simp [h]
simp [hf, hx]
