English
There is a ring isomorphism between HahnSeries with index σ →₀ ℕ (finite σ) over R and the multivariate power series MvPowerSeries σ R.
Русский
Существует изоморфизм колец между рядами Хана с индексами σ →₀ ℕ над R и многоварьными степенными рядами MvPowerSeries σ R, когда σ конечно.
LaTeX
$$$HahnSeries( (\\sigma \\to_0 \\mathbb{N}) \\; R ) \\cong+* MvPowerSeries \\sigma R$$$
Lean4
/-- The ring `HahnSeries (σ →₀ ℕ) R` is isomorphic to `MvPowerSeries σ R` for a `Finite` `σ`.
We take the index set of the hahn series to be `Finsupp` rather than `pi`,
even though we assume `Finite σ` as this is more natural for alignment with `MvPowerSeries`.
After importing `Mathlib/Algebra/Order/Pi.lean` the ring `HahnSeries (σ → ℕ) R` could be constructed
instead.
-/
@[simps]
def toMvPowerSeries {σ : Type*} [Finite σ] : HahnSeries (σ →₀ ℕ) R ≃+* MvPowerSeries σ R
where
toFun f := f.coeff
invFun f := ⟨(f : (σ →₀ ℕ) → R), Finsupp.isPWO _⟩
left_inv
f := by
ext
simp
right_inv
f := by
ext
simp
map_add' f
g := by
ext
simp
map_mul' f
g := by
ext n
classical
change (f * g).coeff n = _
simp_rw [coeff_mul]
refine (sum_filter_ne_zero _).symm.trans <| (sum_congr ?_ fun _ _ ↦ rfl).trans <| sum_filter_ne_zero _
ext m
simp only [and_congr_left_iff, mem_addAntidiagonal, mem_filter, mem_support, Finset.mem_antidiagonal]
rintro h
rw [and_iff_right (left_ne_zero_of_mul h), and_iff_right (right_ne_zero_of_mul h)]
