English
For a ring hom f and a map g, map f composed with eval₂ on p equals eval₂ on map f p with g replaced by map f ∘ g.
Русский
Для гомоморфизма f и отображения g выполняется равенство map f (eval₂ C g p) = eval₂ C (map f ∘ g) (map f p).
LaTeX
$$$$\operatorname{map} f\bigl(\operatorname{eval}_2 \mathbf{C} g\; p\bigr) = \operatorname{eval}_2 \mathbf{C} (\operatorname{map} f \circ g) (\operatorname{map} f\; p).$$$$
Lean4
theorem eval₂_eq_eval_map (g : σ → S₁) (p : MvPolynomial σ R) : p.eval₂ f g = eval g (map f p) :=
by
unfold map eval; simp only [coe_eval₂Hom]
have h := eval₂_comp_left (eval₂Hom (RingHom.id S₁) g) (C.comp f) X p
dsimp only [coe_eval₂Hom] at h
rw [h]
congr
· ext1 a
simp only [coe_eval₂Hom, RingHom.id_apply, comp_apply, eval₂_C, RingHom.coe_comp]
· ext1 n
simp only [comp_apply, eval₂_X]
