English
The value of the composed polynomial evaluation equals the evaluation done in stages: (g ∘ f).toAlgHom x = g.toAlgHom (f.toAlgHom x).
Русский
Значение композиции равно последовательному применению оценок гомоморфизмов.
LaTeX
$$$ (g.comp f).toAlgHom(x) = g.toAlgHom(f.toAlgHom(x)) $$$
Lean4
/-- The composition of two homs. -/
@[simps]
noncomputable def comp [IsScalarTower R' R'' S''] [IsScalarTower R' S' S''] [IsScalarTower S S' S''] (f : Hom P' P'')
(g : Hom P P') : Hom P P'' where
val x := aeval f.val (g.val x)
aeval_val
x := by
rw [IsScalarTower.algebraMap_apply S S' S'', ← g.aeval_val]
induction g.val x using MvPolynomial.induction_on with
| C r => simp [← IsScalarTower.algebraMap_apply]
| add x y hx hy => simp only [map_add, hx, hy]
| mul_X p i hp => simp only [map_mul, hp, aeval_X, aeval_val]
