mapAlgHom — Mathlib

English

The mapAlgHom constructed from the identity algebra hom equals the ordinary identity map on polynomials.

Русский

Конструкция mapAlgHom, полученная из тождества алгебр, совпадает с обычным тождественным отображением полиномов.

LaTeX

$$$mapAlgHom (AlgHom.id R S_1) = AlgHom.id R (MvPolynomial σ S_1)$$$

Lean4

/-- If `f : S₁ →ₐ[R] S₂` is a morphism of `R`-algebras, then so is `MvPolynomial.map f`. -/
@[simps!]
def mapAlgHom [CommSemiring S₂] [Algebra R S₁] [Algebra R S₂] (f : S₁ →ₐ[R] S₂) :
    MvPolynomial σ S₁ →ₐ[R] MvPolynomial σ S₂ :=
  { map (↑f : S₁ →+* S₂) with commutes' r := by simp }

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