mapRangeRingHom_comp_algebraMap — Mathlib

English

There is a construction mapRangeAlgHom that, given an algebra hom f: A →ₐ[R] B, yields an algebra homomorphism MonoidAlgebra A M → MonoidAlgebra B M compatible with the base-algebra map.

Русский

Существует конструктор mapRangeAlgHom: если f: A →ₐ[R] B, то получаем алгебро-гомоморфизм MonoidAlgebra A M → MonoidAlgebra B M, совместимый с отображением оснований.

LaTeX

$$$\\mathrm{mapRangeAlgHom}\\ M f : MonoidAlgebra A M \\to_{\\mathsf{Alg}} MonoidAlgebra B M$$$

Lean4

@[to_additive (attr := simp)]
theorem mapRangeRingHom_comp_algebraMap (f : R →+* S) :
    (mapRangeRingHom (M := M) f).comp (algebraMap _ _) = (algebraMap _ _).comp f := by ext; simp

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