English
Let R, S, A, B be commutative rings with S an R-algebra, and B the pushout of R, S, A, B. Then the module S ⊗_R Ω_{A/R} carries a natural A–B-bimodule structure, and the scalar actions satisfy the tower condition: IsScalarTower A B (S ⊗_R Ω_{A/R}).
Русский
Пусть R, S, A, B — коммутативные кольца, S — алгебра над R, и B является пуш-аутом R, S, A, B. Тогда модуль S ⊗_R Ω_{A/R} естественным образом образует парный по A и B модуль, удовлетворяющий условию касания скаляров: IsScalarTower A B (S ⊗_R Ω_{A/R}).
LaTeX
$$$IsScalarTower A B (S \\otimes_R \\Omega_{A/R})$$$
Lean4
instance [Algebra.IsPushout R S A B] : IsScalarTower A B (S ⊗[R] Ω[A⁄R]) :=
by
apply IsScalarTower.of_algebraMap_smul
intro r x
change
(Algebra.pushoutDesc B (Algebra.lsmul R (A := S) S (S ⊗[R] Ω[A⁄R])) (Algebra.lsmul R (A := A) _ _)
(LinearMap.ext <| smul_comm · ·) (algebraMap A B r)) •
x =
r • x
simp only [Algebra.pushoutDesc_right, Module.End.smul_def, Algebra.lsmul_coe]
