English
If R → S → T is a tower of algebras and P is a family of generators R → T, then there is a corresponding family of generators S → T given by keeping the same target T and replacing the domain map by the base change along R → S; more precisely, the σ′ map is obtained by applying algebraMap R S to the generators, and the aeval relation is inherited from the tower.
Русский
Если кольца R ⟶ S ⟶ T образуют тройку торов, и P — семейство генераторов R ⟶ T, то существует соответствующее семейство генераторов S ⟶ T, где val совпадает с P.val, σ′ задаётся через отображение R → S, а отношение aeval переносится через скалярное основание торов.
LaTeX
$$$\\exists G : \\text{Generators } S\\, T\\, ι \\text{ with } G.{val} = P.{val},\\; G.{σ'}(x) = (\\mathrm{algebraMap}\\, R\\, S)\\big( P.{val}(x) \\big),\\; G.aeval\\_val\\_σ'(s) = \\text{(aeval relation from the tower)}$$$
Lean4
/-- If `R → S → T` is a tower of algebras, a family of generators `R[X] → T`
gives a family of generators `S[X] → T`. -/
@[simps val]
noncomputable def extendScalars (P : Generators R T ι) : Generators S T ι
where
val := P.val
σ' x := map (algebraMap R S) (P.σ x)
aeval_val_σ' s := by simp [@aeval_def S, ← IsScalarTower.algebraMap_eq, ← @aeval_def R]
