English
For ring hom k: S1 → S2, f: R →+* S1, g: σ → S1 and p, we have k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p).
Русский
Для гомоморфизма k: S1 → S2, f: R →+* S1, g: σ → S1 и p: MvPolynomial, выполняется k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p).
LaTeX
$$$$k\bigl(\mathrm{eval}_2 f\; g\; p\bigr) = \mathrm{eval}_2 k\; (k \circ g)\; (\mathrm{map} f\; p).$$$$
Lean4
theorem eval₂_comp_right {S₂} [CommSemiring S₂] (k : S₁ →+* S₂) (f : R →+* S₁) (g : σ → S₁) (p) :
k (eval₂ f g p) = eval₂ k (k ∘ g) (map f p) :=
by
apply MvPolynomial.induction_on p
· intro r
rw [eval₂_C, map_C, eval₂_C]
· intro p q hp hq
rw [eval₂_add, k.map_add, (map f).map_add, eval₂_add, hp, hq]
· intro p s hp
rw [eval₂_mul, k.map_mul, (map f).map_mul, eval₂_mul, map_X, hp, eval₂_X, eval₂_X, comp_apply]
