English
Given a base algebra hom φ: A →ₐ[R] B, there is a corresponding algebra hom mapAlgHom φ: MvPowerSeries σ A →ₐ[R] MvPowerSeries σ B, defined by applying φ coefficientwise.
Русский
Для гомоморфизма алгебр φ: A →ₐ[R] B существует соответствующий алгебра-гомоморфизм mapAlgHom φ: MvPowerSeries σ A →ₐ[R] MvPowerSeries σ B, определяемый по каждому коэффициенту.
LaTeX
$$$\\mathrm{mapAlgHom}(\\varphi): \\mathrm{MvPowerSeries}(\\sigma, A) \\to_R \\mathrm{MvPowerSeries}(\\sigma, B) \\text{ является } R\\text{-алгебра-гомоморфизм}$$$
Lean4
/-- Change of coefficients in mv power series, as an `AlgHom` -/
def mapAlgHom (φ : A →ₐ[R] B) : MvPowerSeries σ A →ₐ[R] MvPowerSeries σ B
where
toRingHom := MvPowerSeries.map φ
commutes'
r := by
simp only [RingHom.toMonoidHom_eq_coe, OneHom.toFun_eq_coe, MonoidHom.toOneHom_coe, MonoidHom.coe_coe,
MvPowerSeries.algebraMap_apply, map_C, RingHom.coe_coe, AlgHom.commutes]
