English
Let f be a ring homomorphism and g a family of polynomials. Then applying map to bind₁ g φ distributes as a bind₁ over the images under map f of g i, with φ also mapped by map f.
Русский
Пусть f — гомоморфизм кольца и g — семейство многочленов. Тогда применение map к bind₁ g φ распадается в bind₁ над изображениями g i через map f, при этом φ также преобразуется под map f.
LaTeX
$$$$ \mathrm{map}\, f\, (\mathrm{bind}_1\, g\, \varphi) = \mathrm{bind}_1\, (\lambda i. \mathrm{map}\, f\, (g i))\, (\mathrm{map}\, f\, \varphi) $$$$
Lean4
theorem map_bind₁ (f : R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
map f (bind₁ g φ) = bind₁ (fun i : σ => (map f) (g i)) (map f φ) :=
by
rw [hom_bind₁, map_comp_C, ← eval₂Hom_map_hom]
rfl
