toAlgHom — Mathlib

English

A hom between two families of generators induces an algebra homomorphism between the corresponding polynomial rings, given by evaluation along the hom’s values.

Русский

Гомоморфизм между двумя семействами генераторов порождает алгебра-хомоморфизм между соответствующими кольцевыми многочленами, заданный через вычисление по значениям гомоморфизма.

LaTeX

$$$\\text{toAlgHom} : \\text{Hom } P P' \\to (P.Ring \\to_a[R] P'.Ring)$ is defined by $f \\mapsto \\mathrm{aeval}\\, f.\\mathrm{val}$$$

Lean4

/-- A hom between two families of generators gives
an algebra homomorphism between the polynomial rings. -/
noncomputable def toAlgHom (f : Hom P P') : P.Ring →ₐ[R] P'.Ring :=
  MvPolynomial.aeval f.val

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