mapAlgHom_coe_ringHom — Mathlib

English

The range of mapAlgHom is described by the coefficients lying in the range of f when viewed in the coefficient ring.

Русский

Диапазон mapAlgHom описывается коэффициентами, лежащими в диапазоне f в кольце коэффициентов.

LaTeX

$$$\\mathrm{range}(\\\\mathrm{mapAlgHom} f).\\\\toSubmodule = \\\\mathrm{coeffsIn} σ f.range.\\\\toSubmodule$$$

Lean4

@[simp]
theorem mapAlgHom_coe_ringHom [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
    ↑(mapAlgHom f : _ →ₐ[R] MvPolynomial σ S₂) = (map ↑f : MvPolynomial σ S₁ →+* MvPolynomial σ S₂) :=
  RingHom.mk_coe _ _ _ _ _

Похожие утверждения