Linear monoidal categories #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
A monoidal category is monoidal_linear R if it is monoidal preadditive and
tensor product of morphisms is R-linear in both factors.
@[class]
structure
category_theory.monoidal_linear
(R : Type u_1)
[semiring R]
(C : Type u_2)
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C] :
Prop
- tensor_smul' : (∀ {W X Y Z : C} (f : W ⟶ X) (r : R) (g : Y ⟶ Z), f ⊗ r • g = r • (f ⊗ g)) . "obviously"
- smul_tensor' : (∀ {W X Y Z : C} (r : R) (f : W ⟶ X) (g : Y ⟶ Z), r • f ⊗ g = r • (f ⊗ g)) . "obviously"
A category is monoidal_linear R if tensoring is R-linear in both factors.
@[simp]
theorem
category_theory.monoidal_linear.tensor_smul
{R : Type u_1}
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[self : category_theory.monoidal_linear R C]
{W X Y Z : C}
(f : W ⟶ X)
(r : R)
(g : Y ⟶ Z) :
@[simp]
theorem
category_theory.monoidal_linear.smul_tensor
{R : Type u_1}
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[self : category_theory.monoidal_linear R C]
{W X Y Z : C}
(r : R)
(f : W ⟶ X)
(g : Y ⟶ Z) :
@[protected, instance]
def
category_theory.tensor_left_linear
(R : Type u_1)
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
@[protected, instance]
def
category_theory.tensor_right_linear
(R : Type u_1)
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
@[protected, instance]
def
category_theory.tensoring_left_linear
(R : Type u_1)
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
@[protected, instance]
def
category_theory.tensoring_right_linear
(R : Type u_1)
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
(X : C) :
theorem
category_theory.monoidal_linear_of_faithful
(R : Type u_1)
[semiring R]
{C : Type u_2}
[category_theory.category C]
[category_theory.preadditive C]
[category_theory.linear R C]
[category_theory.monoidal_category C]
[category_theory.monoidal_preadditive C]
[category_theory.monoidal_linear R C]
{D : Type u_4}
[category_theory.category D]
[category_theory.preadditive D]
[category_theory.linear R D]
[category_theory.monoidal_category D]
[category_theory.monoidal_preadditive D]
(F : category_theory.monoidal_functor D C)
[category_theory.faithful F.to_lax_monoidal_functor.to_functor]
[F.to_lax_monoidal_functor.to_functor.additive]
[category_theory.functor.linear R F.to_lax_monoidal_functor.to_functor] :
A faithful linear monoidal functor to a linear monoidal category ensures that the domain is linear monoidal.