moduleBaseChange' — Mathlib

English

A pushout-based construction yields an A-module structure on S ⊗R Ω[A/R] compatible with pushout data.

Русский

Построение через pushout даёт A-модульную структуру на S ⊗R Ω[A/R], совместимую с данными pushout.

LaTeX

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

Lean4

/-- (Implementation). `B = S ⊗[R] A`-module structure on `S ⊗[R] Ω[A⁄R]`. -/
@[reducible]
noncomputable def moduleBaseChange' [Algebra.IsPushout R S A B] : Module B (S ⊗[R] Ω[A⁄R]) :=
  Module.compHom _
    (Algebra.pushoutDesc B (Algebra.lsmul R (A := S) S (S ⊗[R] Ω[A⁄R])) (Algebra.lsmul R (A := A) _ _)
        (LinearMap.ext <| smul_comm · ·)).toRingHom

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