@[class]
structure
category_theory.monoidal_category
(C : Type u)
[š : category_theory.category C] :
Type (max u v)
- tensor_obj : C ā C ā C
- tensor_hom : Ī {Xā Yā Xā Yā : C}, (Xā ā¶ Yā) ā (Xā ā¶ Yā) ā (Xā ā Xā ā¶ Yā ā Yā)
- tensor_id' : (ā (Xā Xā : C), š Xā ā š Xā = š (Xā ā Xā)) . "obviously"
- tensor_comp' : (ā {Xā Yā Zā Xā Yā Zā : C} (fā : Xā ā¶ Yā) (fā : Xā ā¶ Yā) (gā : Yā ā¶ Zā) (gā : Yā ā¶ Zā), fā ā« gā ā fā ā« gā = (fā ā fā) ā« (gā ā gā)) . "obviously"
- tensor_unit : C
- associator : Ī (X Y Z : C), (X ā Y) ā Z ā X ā Y ā Z
- associator_naturality' : (ā {Xā Xā Xā Yā Yā Yā : C} (fā : Xā ā¶ Yā) (fā : Xā ā¶ Yā) (fā : Xā ā¶ Yā), ((fā ā fā) ā fā) ā« (Ī±_ Yā Yā Yā).hom = (Ī±_ Xā Xā Xā).hom ā« (fā ā fā ā fā)) . "obviously"
- left_unitor : Ī (X : C), š_ C ā X ā X
- left_unitor_naturality' : (ā {X Y : C} (f : X ā¶ Y), (š (š_ C) ā f) ā« (Ī»_ Y).hom = (Ī»_ X).hom ā« f) . "obviously"
- right_unitor : Ī (X : C), X ā š_ C ā X
- right_unitor_naturality' : (ā {X Y : C} (f : X ā¶ Y), (f ā š (š_ C)) ā« (Ļ_ Y).hom = (Ļ_ X).hom ā« f) . "obviously"
- pentagon' : (ā (W X Y Z : C), ((Ī±_ W X Y).hom ā š Z) ā« (Ī±_ W (X ā Y) Z).hom ā« (š W ā (Ī±_ X Y Z).hom) = (Ī±_ (W ā X) Y Z).hom ā« (Ī±_ W X (Y ā Z)).hom) . "obviously"
- triangle' : (ā (X Y : C), (Ī±_ X (š_ C) Y).hom ā« (š X ā (Ī»_ Y).hom) = (Ļ_ X).hom ā š Y) . "obviously"
In a monoidal category, we can take the tensor product of objects, X ā Y and of morphisms f ā g.
Tensor product does not need to be strictly associative on objects, but there is a
specified associator, Ī±_ X Y Z : (X ā Y) ā Z ā
X ā (Y ā Z). There is a tensor unit š_ C,
with specified left and right unitor isomorphisms Ī»_ X : š_ C ā X ā
X and Ļ_ X : X ā š_ C ā
X.
These associators and unitors satisfy the pentagon and triangle equations.
def
category_theory.tensor_iso
{C : Type u}
{X Y X' Y' : C}
[category_theory.category C]
[category_theory.monoidal_category C] :
The tensor product of two isomorphisms is an isomorphism.
@[instance]
def
category_theory.monoidal_category.tensor_is_iso
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
(f : W ā¶ X)
[category_theory.is_iso f]
(g : Y ā¶ Z)
[category_theory.is_iso g] :
category_theory.is_iso (f ā g)
Equations
- category_theory.monoidal_category.tensor_is_iso f g = {inv := (category_theory.as_iso f ā category_theory.as_iso g).inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.monoidal_category.inv_tensor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
(f : W ā¶ X)
[category_theory.is_iso f]
(g : Y ā¶ Z)
[category_theory.is_iso g] :
@[simp]
theorem
category_theory.monoidal_category.comp_tensor_id
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
(f : W ā¶ X)
(g : X ā¶ Y) :
@[simp]
theorem
category_theory.monoidal_category.id_tensor_comp
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
(f : W ā¶ X)
(g : X ā¶ Y) :
@[simp]
theorem
category_theory.monoidal_category.id_tensor_comp_tensor_id
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
(f : W ā¶ X)
(g : Y ā¶ Z) :
@[simp]
theorem
category_theory.monoidal_category.tensor_id_comp_id_tensor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{W X Y Z : C}
(f : W ā¶ X)
(g : Y ā¶ Z) :
theorem
category_theory.monoidal_category.left_unitor_inv_naturality
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' : C}
(f : X ā¶ X') :
theorem
category_theory.monoidal_category.right_unitor_inv_naturality
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X X' : C}
(f : X ā¶ X') :
@[simp]
theorem
category_theory.monoidal_category.right_unitor_conjugation
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(f : X ā¶ Y) :
@[simp]
theorem
category_theory.monoidal_category.left_unitor_conjugation
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(f : X ā¶ Y) :
@[simp]
theorem
category_theory.monoidal_category.tensor_left_iff
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(f g : X ā¶ Y) :
@[simp]
theorem
category_theory.monoidal_category.tensor_right_iff
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C}
(f g : X ā¶ Y) :
theorem
category_theory.monoidal_category.left_unitor_product_aux_perimeter
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
theorem
category_theory.monoidal_category.left_unitor_product_aux_triangle
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
theorem
category_theory.monoidal_category.left_unitor_product_aux_square
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
theorem
category_theory.monoidal_category.right_unitor_product_aux_perimeter
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
theorem
category_theory.monoidal_category.right_unitor_product_aux_triangle
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
theorem
category_theory.monoidal_category.right_unitor_product_aux_square
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
def
category_theory.monoidal_category.tensor
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
The tensor product expressed as a functor.
def
category_theory.monoidal_category.left_assoc_tensor
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
The left-associated triple tensor product as a functor.
@[simp]
theorem
category_theory.monoidal_category.left_assoc_tensor_obj
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C Ć C Ć C) :
@[simp]
theorem
category_theory.monoidal_category.left_assoc_tensor_map
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C Ć C Ć C}
(f : X ā¶ Y) :
def
category_theory.monoidal_category.right_assoc_tensor
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
The right-associated triple tensor product as a functor.
@[simp]
theorem
category_theory.monoidal_category.right_assoc_tensor_obj
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C Ć C Ć C) :
@[simp]
theorem
category_theory.monoidal_category.right_assoc_tensor_map
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
{X Y : C Ć C Ć C}
(f : X ā¶ Y) :
def
category_theory.monoidal_category.tensor_unit_left
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
C ā„¤ C
The functor Ī» X, š_ C ā X.
def
category_theory.monoidal_category.tensor_unit_right
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
C ā„¤ C
The functor Ī» X, X ā š_ C.
def
category_theory.monoidal_category.associator_nat_iso
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
The associator as a natural isomorphism.
@[simp]
theorem
category_theory.monoidal_category.associator_nat_iso_inv_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C Ć C Ć C) :
@[simp]
theorem
category_theory.monoidal_category.associator_nat_iso_hom_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C Ć C Ć C) :
@[simp]
theorem
category_theory.monoidal_category.left_unitor_nat_iso_hom_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C) :
def
category_theory.monoidal_category.left_unitor_nat_iso
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
The left unitor as a natural isomorphism.
Equations
@[simp]
theorem
category_theory.monoidal_category.left_unitor_nat_iso_inv_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C) :
(category_theory.monoidal_category.left_unitor_nat_iso C).inv.app X = category_theory.is_iso.inv ({app := Ī» (X : C), ((Ī» (X : C), Ī»_ X) X).hom, naturality' := _}.app X)
@[simp]
theorem
category_theory.monoidal_category.right_unitor_nat_iso_hom_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C) :
@[simp]
theorem
category_theory.monoidal_category.right_unitor_nat_iso_inv_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C) :
(category_theory.monoidal_category.right_unitor_nat_iso C).inv.app X = category_theory.is_iso.inv ({app := Ī» (X : C), ((Ī» (X : C), Ļ_ X) X).hom, naturality' := _}.app X)
def
category_theory.monoidal_category.right_unitor_nat_iso
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
The right unitor as a natural isomorphism.
Equations
@[simp]
theorem
category_theory.monoidal_category.tensor_left_map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Y' : C)
(f : Y ā¶ Y') :
(category_theory.monoidal_category.tensor_left X).map f = š X ā f
@[simp]
theorem
category_theory.monoidal_category.tensor_left_obj
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
(category_theory.monoidal_category.tensor_left X).obj Y = X ā Y
def
category_theory.monoidal_category.tensor_left
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
C ā C ā„¤ C
Tensoring on the left with as fixed object, as a functor.
def
category_theory.monoidal_category.tensor_left_tensor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
Tensoring on the left with X ā Y is naturally isomorphic to
tensoring on the left with Y, and then again with X.
Equations
@[simp]
theorem
category_theory.monoidal_category.tensor_left_tensor_hom_app
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :
@[simp]
theorem
category_theory.monoidal_category.tensor_left_tensor_inv_app
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :
@[simp]
theorem
category_theory.monoidal_category.tensor_right_map
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Y' : C)
(f : Y ā¶ Y') :
def
category_theory.monoidal_category.tensor_right
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C] :
C ā C ā„¤ C
Tensoring on the right with as fixed object, as a functor.
@[simp]
theorem
category_theory.monoidal_category.tensor_right_obj
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
@[simp]
theorem
category_theory.monoidal_category.tensoring_right_obj
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X : C) :
def
category_theory.monoidal_category.tensoring_right
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Tensoring on the right, as a functor from C into endofunctors of C.
We later show this is a monoidal functor.
Equations
- category_theory.monoidal_category.tensoring_right C = {obj := category_theory.monoidal_category.tensor_right _inst_2, map := Ī» (X Y : C) (f : X ā¶ Y), {app := Ī» (Z : C), š Z ā f, naturality' := _}, map_id' := _, map_comp' := _}
@[simp]
theorem
category_theory.monoidal_category.tensoring_right_map_app
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C)
(f : X ā¶ Y)
(Z : C) :
@[instance]
def
category_theory.monoidal_category.category_theory.faithful
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Equations
- _ = _
def
category_theory.monoidal_category.tensor_right_tensor
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y : C) :
Tensoring on the right with X ā Y is naturally isomorphic to
tensoring on the right with X, and then again with Y.
Equations
- category_theory.monoidal_category.tensor_right_tensor X Y = category_theory.nat_iso.of_components (Ī» (Z : C), (Ī±_ Z X Y).symm) _
@[simp]
theorem
category_theory.monoidal_category.tensor_right_tensor_hom_app
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :
@[simp]
theorem
category_theory.monoidal_category.tensor_right_tensor_inv_app
{C : Type u}
[category_theory.category C]
[category_theory.monoidal_category C]
(X Y Z : C) :