moduleBaseChange — Mathlib

English

The tensor-product module supports a SMulCommClass between S and the Kahler differential module under base-change.

Русский

У модуля тензорного произведения существует SMulCommClass между S и KahlerDifferential при базовом изменении.

LaTeX

$$$\\text{SMulCommClass } S A (S \\otimes_R \\Omega[A/R]).$$$

Lean4

/-- (Implementation). `A`-module structure on `S ⊗[R] Ω[A⁄R]`. -/
noncomputable abbrev moduleBaseChange : Module A (S ⊗[R] Ω[A⁄R])
    where
  __ := (TensorProduct.comm R S Ω[A⁄R]).toEquiv.mulAction A
  add_smul r s x := by induction x <;> simp [add_smul, tmul_add, *, add_add_add_comm]
  zero_smul x := by induction x <;> simp [*]
  smul_zero := by simp
  smul_add := by simp

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