English
If R,S,A are commutative semirings with A carrying R- and S-algebra structures and IsScalarTower R S A, then the same scalar tower property holds for FreeAlgebra A X: IsScalarTower R S (FreeAlgebra A X).
Русский
Пусть R,S,A — коммутативные полукольца с структурами A над R-алгеброй и S-алгеброй, и IsScalarTower R S A. Тогда аналогичное свойство тензорной (скаляpной) башни выполняется и для FreeAlgebra A X: IsScalarTower R S (FreeAlgebra A X).
LaTeX
$$$\text{IsScalarTower } R S A \Rightarrow \text{IsScalarTower } R S (\mathrm{FreeAlgebra}(A,X)).$$$
Lean4
instance {R S A} [CommSemiring R] [CommSemiring S] [CommSemiring A] [SMul R S] [Algebra R A] [Algebra S A]
[IsScalarTower R S A] : IsScalarTower R S (FreeAlgebra A X) where
smul_assoc r s
x := by
change algebraMap S A (r • s) • x = algebraMap R A _ • (algebraMap S A _ • x)
rw [← smul_assoc]
congr
simp only [Algebra.algebraMap_eq_smul_one, smul_eq_mul]
rw [smul_assoc, ← smul_one_mul]
