Scalar multiples and the tensor product in a monoidal linear category #
In an R-linear monoidal category whose whiskerings are R-linear (Mathlib's
CategoryTheory.MonoidalLinear), the tensor product of morphisms commutes with scalar
multiplication in each variable. Mathlib records this only for the whiskerings; these are the
statements needed to see that a tensor product of morphisms is R-bilinear.
@[simp]
theorem
CategoryTheory.smul_tensorHom
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[Category.{v_1, u_2} C]
[Preadditive C]
[Linear R C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
{W X Y Z : C}
(r : R)
(f : W ⟶ X)
(g : Y ⟶ Z)
:
Tensoring morphisms commutes with scalar multiplication in the first variable.
@[simp]
theorem
CategoryTheory.tensorHom_smul
{R : Type u_1}
[Semiring R]
{C : Type u_2}
[Category.{v_1, u_2} C]
[Preadditive C]
[Linear R C]
[MonoidalCategory C]
[MonoidalPreadditive C]
[MonoidalLinear R C]
{W X Y Z : C}
(r : R)
(f : W ⟶ X)
(g : Y ⟶ Z)
:
Tensoring morphisms commutes with scalar multiplication in the second variable.