English
In a tower of algebras R → S → T, for a subset a ⊆ S, the span of its image in T under algebraMap equals the image (via the restricted linear map) of the span of a in S.
Русский
В башне алгебр R → S → T для подмножества a ⊆ S выполняется равенство образа изображения a в T под алгебраMap равно образу порожденного спана a через ограниченное по R линейное отображение.
LaTeX
$$$\\\\operatorname{span}_R\\\\left(\\\\mathrm{algebraMap} S T \\\\text{''} a\\\\right) \\\\;=\\\\; \\\\left(\\\\operatorname{span}_R a\\\\right)\\\\.map\\\\left((\\\\mathrm{Algebra.linearMap} S T)\\\\restrictScalars R\\\\right).$$
Lean4
theorem span_algebraMap_image_of_tower {S T : Type*} [CommSemiring S] [Semiring T] [Module R S] [Algebra R T]
[Algebra S T] [IsScalarTower R S T] (a : Set S) :
Submodule.span R (algebraMap S T '' a) = (Submodule.span R a).map ((Algebra.linearMap S T).restrictScalars R) :=
(Submodule.span_image <| (Algebra.linearMap S T).restrictScalars R).trans rfl
