English
For any algebra hom f: A →ₐ[R] B, the underlying ring hom of the polynomial map mapAlgHom f equals the polynomial ring map applied to the underlying ring hom of f. Equivalently, toRingHom (Polynomial.mapAlgHom f) = Polynomial.mapRingHom (toRingHom f).
Русский
Пусть f: A →ₐ[R] B — алгебра-гомоморфизм. Тогда лежит равенство между каноническим отображением полиномов: подмножество отображения на полиномах совпадает с отображением по соответствующему кольцевому гомоморфизму: toRingHom (Polynomial.mapAlgHom f) = Polynomial.mapRingHom (toRingHom f).
LaTeX
$$$\\operatorname{toRingHom}(\\operatorname{Polynomial.mapAlgHom} f) = \\operatorname{Polynomial.mapRingHom}(\\operatorname{toRingHom} f)$$$
Lean4
@[simp]
theorem mapAlgHom_coe_ringHom (f : A →ₐ[R] B) :
↑(mapAlgHom f : _ →ₐ[R] Polynomial B) = (mapRingHom ↑f : Polynomial A →+* Polynomial B) :=
rfl
