English
Let f be a ring homomorphism from the polynomial ring in τ over R to S, and g a family of polynomials. Then applying f to the result of bind₁ g φ equals evaluating φ with a tailored evaluation homomorphism built from f and g.
Русский
Пусть f — гомоморфизм кольца от полиномиального кольца над τ с основанием R к S, и g — семейство многочленов. Тогда применение f к результату bind₁ g φ равно вычислению φ при помощи особого гомоморфизма вывода, составленного из f и g.
LaTeX
$$$$ f\big( \mathrm{bind}_1\, g\, \varphi \big) = \mathrm{eval}_2\mathrm{Hom}\, (f \circ C)\, (\lambda i. f(g(i)))\, \varphi $$$$
Lean4
theorem hom_bind₁ (f : MvPolynomial τ R →+* S) (g : σ → MvPolynomial τ R) (φ : MvPolynomial σ R) :
f (bind₁ g φ) = eval₂Hom (f.comp C) (fun i => f (g i)) φ := by rw [bind₁, map_aeval, algebraMap_eq]
