instMonoidalLinear — Mathlib

English

The category of modules over a commutative ring R carries a canonical structure of a Monoidal Linear category over R; i.e., the tensor product is bilinear in each variable with respect to the R-module structure.

Русский

Категория R-модулей обладает естественной структурой моноидальной линейности над R; тензорное произведение линейно по каждому аргументу по модульной структуре над R.

LaTeX

$$$\\text{MonoidalLinear}_R(\\text{ModuleCat } R)$$$

Lean4

instance : MonoidalLinear R (ModuleCat.{u} R) := by
  refine ⟨?_, ?_⟩
  · intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply, hom_smul, LinearMap.smul_apply]
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

    erw [MonoidalCategory.whiskerLeft_apply, MonoidalCategory.whiskerLeft_apply]
    simp
  · intros
    ext : 1
    refine TensorProduct.ext (LinearMap.ext fun x => LinearMap.ext fun y => ?_)
    simp only [LinearMap.compr₂_apply, TensorProduct.mk_apply, hom_smul, LinearMap.smul_apply]
      -- This used to be `rw`, but we need `erw` after https://github.com/leanprover/lean4/pull/2644

    erw [MonoidalCategory.whiskerRight_apply, MonoidalCategory.whiskerRight_apply]
    simp [TensorProduct.smul_tmul, TensorProduct.tmul_smul]

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