Documentation

TauCeti.Algebra.Category.ModuleCat.Monoidal.TensorMk

Tensoring on the left with a fixed element #

For modules M and N over a commutative ring k and an element z ∈ M, the morphism TauCeti.ModuleCat.tensorMk z : N ⟶ M ⊗ N sends v to z ⊗ₜ v; it is Mathlib's TensorProduct.mk k M N z as a morphism of ModuleCat k. This file records how it interacts with the whiskerings of the monoidal structure and that it is additive and k-linear in z, so that a calculation with morphisms out of a tensor product evaluated at a fixed first factor stays in the category.

source
noncomputable def TauCeti.ModuleCat.tensorMk {k : Type u} [CommRing k] {M N : ModuleCat k} (z : ↑M) :
N ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj M N

Tensoring on the left with a fixed element z ∈ M, as a morphism N ⟶ M ⊗ N: Mathlib's TensorProduct.mk k M N z in ModuleCat k.

Instances For
    source
    @[simp]
    theorem TauCeti.ModuleCat.tensorMk_apply {k : Type u} [CommRing k] {M N : ModuleCat k} (z : ↑M) (v : ↑N) :
    (CategoryTheory.ConcreteCategory.hom (tensorMk z)) v = z ⊗ₜ[k] v

    TauCeti.ModuleCat.tensorMk z sends v to the pure tensor z ⊗ₜ v.

    source
    theorem TauCeti.ModuleCat.comp_tensorMk {k : Type u} [CommRing k] {M N N' : ModuleCat k} (z : ↑M) (g : N' ⟶ N) :
    CategoryTheory.CategoryStruct.comp g (tensorMk z) = CategoryTheory.CategoryStruct.comp (tensorMk z) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g)

    Precomposing TauCeti.ModuleCat.tensorMk z with g is whiskering g on the left.

    source
    theorem TauCeti.ModuleCat.comp_tensorMk_assoc {k : Type u} [CommRing k] {M N N' : ModuleCat k} (z : ↑M) (g : N' ⟶ N) {Z : ModuleCat k} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M N ⟶ Z) :
    CategoryTheory.CategoryStruct.comp g (CategoryTheory.CategoryStruct.comp (tensorMk z) h) = CategoryTheory.CategoryStruct.comp (tensorMk z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft M g) h)

    Precomposing TauCeti.ModuleCat.tensorMk z with g is whiskering g on the left.

    source
    @[simp]
    theorem TauCeti.ModuleCat.tensorMk_whiskerRight {k : Type u} [CommRing k] {M M' N : ModuleCat k} (z : ↑M) (g : M ⟶ M') :
    CategoryTheory.CategoryStruct.comp (tensorMk z) (CategoryTheory.MonoidalCategoryStruct.whiskerRight g N) = tensorMk ((CategoryTheory.ConcreteCategory.hom g) z)

    Whiskering g on the right after TauCeti.ModuleCat.tensorMk z is tensoring with g z.

    source
    @[simp]
    theorem TauCeti.ModuleCat.tensorMk_whiskerRight_assoc {k : Type u} [CommRing k] {M M' N : ModuleCat k} (z : ↑M) (g : M ⟶ M') {Z : ModuleCat k} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj M' N ⟶ Z) :
    CategoryTheory.CategoryStruct.comp (tensorMk z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight g N) h) = CategoryTheory.CategoryStruct.comp (tensorMk ((CategoryTheory.ConcreteCategory.hom g) z)) h

    Whiskering g on the right after TauCeti.ModuleCat.tensorMk z is tensoring with g z.

    source
    theorem TauCeti.ModuleCat.tensorMk_add {k : Type u} [CommRing k] {M N : ModuleCat k} (z z' : ↑M) :
    tensorMk (z + z') = tensorMk z + tensorMk z'

    TauCeti.ModuleCat.tensorMk is additive in the fixed element.

    source
    theorem TauCeti.ModuleCat.tensorMk_smul {k : Type u} [CommRing k] {M N : ModuleCat k} (r : k) (z : ↑M) :
    tensorMk (r • z) = r • tensorMk z

    TauCeti.ModuleCat.tensorMk is k-linear in the fixed element.