instIsScalarTowerTensorProduct_2 — Mathlib

English

Let R, S, A, B be 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 S–B scalar tower: IsScalarTower S B (S ⊗_R Ω_{A/R}).

Русский

Пусть R, S, A, B — кольца с S как R-алгебра и B пуш-аут R, S, A, B. Тогда S ⊗_R Ω_{A/R} образует естественную цепочку скаляров над S и B: IsScalarTower S B (S ⊗_R Ω_{A/R}).

LaTeX

$$$IsScalarTower S B (S \\otimes_R \\Omega_{A/R})$$$

Lean4

instance [Algebra.IsPushout R S A B] : IsScalarTower S 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 S B r)) •
        x =
      r • x
  simp only [Algebra.pushoutDesc_left, Module.End.smul_def, Algebra.lsmul_coe]

Похожие утверждения