English
The induced map by a local ring hom between mv power series is local: IsLocalHom (MvPowerSeries.map (σ := σ) f).
Русский
Индукционное отображение между многомерными формальными степенными рядами, индуцированное локальным кольцевым гомоморфизмом, локально: IsLocalHom (MvPowerSeries.map (σ := σ) f).
LaTeX
$$$ IsLocalHom (\mathrm{MvPowerSeries.map}(\sigma := \sigma) f) $$$
Lean4
/-- The map between multivariate formal power series over the same indexing set
induced by a local ring hom `A → B` is local -/
@[instance]
theorem isLocalHom : IsLocalHom (map (σ := σ) f) :=
⟨by
rintro φ ⟨ψ, h⟩
replace h := congr_arg constantCoeff h
rw [constantCoeff_map] at h
have : IsUnit (constantCoeff ψ.val) := isUnit_constantCoeff _ ψ.isUnit
rw [h] at this
rcases isUnit_of_map_unit f _ this with ⟨c, hc⟩
exact isUnit_of_mul_eq_one φ (invOfUnit φ c) (mul_invOfUnit φ c hc.symm)⟩
