English
Let R and S be commutative semirings. For any ring homomorphism f: R →+* S and any x, y in S, evaluating a two-variable polynomial p ∈ R[X][Y] first in X at x and then in Y at y yields the same result as evaluating p at (x, y) using the base-change map f. In particular, eval₂RingHom (eval₂RingHom f x) y equals the composition of the two-variable evaluation with the map induced by f: (evalEvalRingHom x y) ∘ (mapRingHom (mapRingHom f)).
Русский
Пусть R и S - коммутативные полугруппы, f: R →+* S – гомоморфизм колец. Для любых x, y ∈ S и p ∈ R[X][Y] два раза подряд производить подстановку: сначала X↦x, затем Y↦y, даст тот же результат, что и полное подстановочное вычисление p(x,y) в S, получаемое через отображение, индукируемое f. Формально: eval₂RingHom (eval₂RingHom f x) y = (evalEvalRingHom x y) ∘ (mapRingHom (mapRingHom f)).
LaTeX
$$$\\operatorname{eval}_{2}(\\operatorname{eval}_{2}(f,x),\\;y) = \\bigl(\\operatorname{evalEvalEngine}(x,y)\\bigr) \\circ \\bigl(\\operatorname{mapRingHom}(\\operatorname{mapRingHom}(f))\\bigr)$.$$
Lean4
/-- Two equivalent ways to express the evaluation of a bivariate polynomial over `R`
at a point in the affine plane over an `R`-algebra `S`. -/
theorem eval₂RingHom_eval₂RingHom (f : R →+* S) (x y : S) :
eval₂RingHom (eval₂RingHom f x) y = (evalEvalRingHom x y).comp (mapRingHom <| mapRingHom f) := by ext <;> simp
