instIsScalarTowerTensorProduct — Mathlib

English

The A-module structure on S ⊗R Ω[A/R] is defined via the commutativity isomorphism between S and Ω[A/R].

Русский

Структура модуля A действует на S ⊗R Ω[A/R] через каноническое коммутативное изоморфирование S и Ω[A/R].

LaTeX

$$$\\text{moduleBaseChange} :\\; \\text{Module}_A(S \\otimes_R \\Omega[A/R]).$$$

Lean4

instance : IsScalarTower R A (S ⊗[R] Ω[A⁄R]) :=
  by
  apply IsScalarTower.of_algebraMap_smul
  intro r x
  induction x
  · simp only [smul_zero]
  · rw [mulActionBaseChange_smul_tmul, algebraMap_smul, tmul_smul]
  · simp only [smul_add, *]

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