mapAlgHom_eq_eval₂AlgHom'_CAlgHom

English

For any algebra hom f: A →ₐ[R] B, the induced polynomial map coincides with an evaluation map built from f.

Русский

Для любого алгебраического гомоморфа f: A →ₐ[R] B индуцированная карта полиномов совмещается с отображением по значению, построенным из f.

LaTeX

$$$\\operatorname{mapAlgHom} f = \\operatorname{eval_2AlgHom'} (\\mathrm{CAlgHom.comp} f) X \\;\\big( (\\operatorname{commute}_X (\\mathrm{C} (f a))).\\mathrm{symm} \\big)$$$

Lean4

theorem mapAlgHom_eq_eval₂AlgHom'_CAlgHom (f : A →ₐ[R] B) :
    mapAlgHom f = eval₂AlgHom' (CAlgHom.comp f) X (fun a => (commute_X (C (f a))).symm) := by rfl

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