English
Let ha be HasEval a. For any ε : S →ₐ[R] T with hε continuous, ε ∘ aeval ha = aeval (ha.map hε).
Русский
Пусть ha имеется HasEval a. Для любого ε : S →ₐ[R] T непрерывного, выполняется равенство ε ∘ aeval ha = aeval (ha.map hε).
LaTeX
$$$ \varepsilon \circ (\mathrm{aeval}_{ha}) = \mathrm{aeval}_{ha.map(h\varepsilon)} $$$
Lean4
theorem comp_aeval (ha : HasEval a) {T : Type*} [CommRing T] [UniformSpace T] [IsUniformAddGroup T]
[IsTopologicalRing T] [IsLinearTopology T T] [T2Space T] [Algebra R T] [ContinuousSMul R T] [CompleteSpace T]
{ε : S →ₐ[R] T} (hε : Continuous ε) : ε.comp (aeval ha) = aeval (ha.map hε) :=
by
apply DFunLike.ext'
simp only [AlgHom.coe_comp, coe_aeval ha]
rw [← RingHom.coe_coe, comp_eval₂ (continuous_algebraMap R S) ha (show Continuous (ε : S →+* T) from hε), coe_aeval]
congr!
simp only [AlgHom.comp_algebraMap_of_tower]
