English
There is a canonical way to regard a Hahn series on the lexicographic product Γ ×ℓ Γ' with coefficients in R as a Hahn series over Γ whose coefficients are Hahn series in Γ' R.
Русский
Существует канонический способ рассматривать ряд Ханна над лексикографическим произведением Γ ×ℓ Γ' со степенью коэффициентов в R как ряд Ханна над Γ с коэффициентами в HahnSeries Γ' R.
LaTeX
$$$\text{toIterate} : \mathrm{HahnSeries}_{(Γ \times_ℓ Γ')} (R) \to \mathrm{HahnSeries}_{Γ}(\mathrm{HahnSeries}_{Γ'}(R))$$$
Lean4
/-- Change a Hahn series on a lex product to a Hahn series with coefficients in a Hahn series. -/
def toIterate [PartialOrder Γ'] (x : HahnSeries (Γ ×ₗ Γ') R) : HahnSeries Γ (HahnSeries Γ' R)
where
coeff := fun g =>
{ coeff := fun g' => coeff x (g, g')
isPWO_support' := Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g }
isPWO_support' :=
by
have h₁ :
(Function.support fun g =>
HahnSeries.mk (fun g' => x.coeff (g, g')) (Set.PartiallyWellOrderedOn.fiberProdLex x.isPWO_support' g)) =
Function.support fun g => fun g' => x.coeff (g, g') :=
by simp only [Function.support, ne_eq, mk_eq_zero]
rw [h₁, Function.support_fun_curry x.coeff]
exact Set.PartiallyWellOrderedOn.imageProdLex x.isPWO_support'
