English
Let R,S,T,U be rings with algebra structures and ring homomorphisms φ: R → T and ψ: S → U such that the square of algebra maps commutes: (algebraMap T U) ∘ φ = ψ ∘ (algebraMap R S). For any p ∈ R[X] and a ∈ S, evaluating p at a and then transporting along ψ equals evaluating the mapped polynomial p.map φ at ψ(a).
Русский
Пусть кольца R,S,T,U образуют основанные на R-алгебрах кольца, и есть гомоморфизмы φ: R → T, ψ: S → U так, что диаграмма сопряжения квадратных квадратов выполняется: (algebraMap T U) ∘ φ = ψ ∘ (algebraMap R S). Тогда для любого p ∈ R[X] и a ∈ S верно: ψ(aeval a p) = aeval(ψ(a)) (p.map φ).
LaTeX
$$$\psi\big(\mathrm{aeval}_a p\big) = \mathrm{aeval}_{\psi(a)}\big(p\mapsto p^{\mathrm{map}\,\phi}\big)\; \text{ i.e. }\psi\big(\mathrm{aeval}_a p\big) = \mathrm{aeval}_{\psi(a)}(p.map \phi).$$$
Lean4
theorem map_aeval_eq_aeval_map {S T U : Type*} [Semiring S] [CommSemiring T] [Semiring U] [Algebra R S] [Algebra T U]
{φ : R →+* T} {ψ : S →+* U} (h : (algebraMap T U).comp φ = ψ.comp (algebraMap R S)) (p : R[X]) (a : S) :
ψ (aeval a p) = aeval (ψ a) (p.map φ) :=
by
conv_rhs => rw [aeval_def, ← eval_map]
rw [map_map, h, ← map_map, eval_map, eval₂_at_apply, aeval_def, eval_map]
