English
For continuous φ and HasEval a, and any ε: S →+* T, the composition with eval₂φa equals eval₂ of the composed φ and a.
Русский
При непрерывном φ и HasEval a композиция с eval₂φa равна eval₂ с композициями ε∘φ и ε∘a.
LaTeX
$$$$\varepsilon \circ \operatorname{eval}_{\phi}^{a} = \operatorname{eval}_{\varepsilon\circ\phi}^{\varepsilon\circ a}.$$$$
Lean4
theorem comp_eval₂ (hφ : Continuous φ) (ha : HasEval a) {T : Type*} [UniformSpace T] [CompleteSpace T] [T2Space T]
[CommRing T] [IsTopologicalRing T] [IsLinearTopology T T] [IsUniformAddGroup T] {ε : S →+* T} (hε : Continuous ε) :
ε ∘ eval₂ φ a = eval₂ (ε.comp φ) (ε ∘ a) :=
by
apply eval₂_unique _ (ha.map hε)
· exact Continuous.comp hε (continuous_eval₂ hφ ha)
· intro p
simp only [Function.comp_apply, eval₂_coe]
rw [← MvPolynomial.coe_eval₂Hom, ← comp_apply, MvPolynomial.comp_eval₂Hom, MvPolynomial.coe_eval₂Hom]
· simp only [coe_comp, Continuous.comp hε hφ]
