English
The construction aevalTower provides an algebra homomorphism R[X] → A' obtained by evaluating polynomials over R with a base ring hom f: R → S and an element y ∈ A', satisfying a commuting condition with scalar towers.
Русский
Построение aevalTower задаёт алгебра-гомоморфизм R[X] → A', получаемый посредством эвалюации полиномов над R с основанием-гомоморфизм f: R → S и элементом y ∈ A', удовлетворяющим условию совместимости со скалярами.
LaTeX
$$aevalTower (f) (y) : R[X] →ₐ[S] A' := eval₂AlgHom' f y (λ _ => Commute.all _ _) $$
Lean4
/-- Version of `aeval` for defining algebra homs out of `R[X]` over a smaller base ring
than `R`. -/
def aevalTower (f : R →ₐ[S] A') (x : A') : R[X] →ₐ[S] A' :=
eval₂AlgHom' f x fun _ => Commute.all _ _
