mathlib3 documentation

category_theory.monoidal.category

Monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

A monoidal category is a category equipped with a tensor product, unitors, and an associator. In the definition, we provide the tensor product as a pair of functions

The tensor product can be expressed as a functor via tensor : C × C ⥤ C. The unitors and associator are gathered together as natural isomorphisms in left_unitor_nat_iso, right_unitor_nat_iso and associator_nat_iso.

Some consequences of the definition are proved in other files, e.g. (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom in category_theory.monoidal.unitors_equal.

Implementation #

Dealing with unitors and associators is painful, and at this stage we do not have a useful implementation of coherence for monoidal categories.

In an effort to lessen the pain, we put some effort into choosing the right simp lemmas. Generally, the rule is that the component index of a natural transformation "weighs more" in considering the complexity of an expression than does a structural isomorphism (associator, etc).

As an example when we prove Proposition 2.2.4 of http://www-math.mit.edu/~etingof/egnobookfinal.pdf we state it as a @[simp] lemma as

(λ_ (X  Y)).hom = (α_ (𝟙_ C) X Y).inv  (λ_ X).hom  (𝟙 Y)

This is far from completely effective, but seems to prove a useful principle.

References #

@[class]
structure category_theory.monoidal_category (C : Type u) [𝒞 : category_theory.category C] :
Type (max u v)

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.

See https://stacks.math.columbia.edu/tag/0FFK.

Instances of this typeclass
Instances of other typeclasses for category_theory.monoidal_category
  • category_theory.monoidal_category.has_sizeof_inst
@[simp]
theorem category_theory.monoidal_category.tensor_id {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (X₁ X₂ : C) :
𝟙 X₁ 𝟙 X₂ = 𝟙 (X₁ X₂)
@[simp]
theorem category_theory.monoidal_category.tensor_comp {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {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₂)
theorem category_theory.monoidal_category.tensor_comp_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) {X' : C} (f' : Z₁ Z₂ X') :
(f₁ g₁ f₂ g₂) f' = (f₁ f₂) (g₁ g₂) f'
theorem category_theory.monoidal_category.associator_naturality {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {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₃)
theorem category_theory.monoidal_category.associator_naturality_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃) {X' : C} (f' : Y₁ Y₂ Y₃ X') :
((f₁ f₂) f₃) (α_ Y₁ Y₂ Y₃).hom f' = (α_ X₁ X₂ X₃).hom (f₁ f₂ f₃) f'
theorem category_theory.monoidal_category.left_unitor_naturality_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
(𝟙 (𝟙_ C) f) (λ_ Y).hom f' = (λ_ X).hom f f'
theorem category_theory.monoidal_category.right_unitor_naturality_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] {X Y : C} (f : X Y) {X' : C} (f' : Y X') :
(f 𝟙 (𝟙_ C)) (ρ_ Y).hom f' = (ρ_ X).hom f f'
theorem category_theory.monoidal_category.pentagon {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (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
@[simp]
theorem category_theory.monoidal_category.pentagon_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (W X Y Z : C) {X' : C} (f' : W X Y Z X') :
((α_ W X Y).hom 𝟙 Z) (α_ W (X Y) Z).hom (𝟙 W (α_ X Y Z).hom) f' = (α_ (W X) Y Z).hom (α_ W X (Y Z)).hom f'
@[simp]
theorem category_theory.monoidal_category.triangle_assoc {C : Type u} [𝒞 : category_theory.category C] [self : category_theory.monoidal_category C] (X Y : C) {X' : C} (f' : X Y X') :
(α_ X (𝟙_ C) Y).hom (𝟙 X (λ_ Y).hom) f' = ((ρ_ X).hom 𝟙 Y) f'
@[simp]
theorem category_theory.tensor_iso_hom {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category C] (f : X Y) (g : X' Y') :
(f g).hom = f.hom g.hom
@[simp]
theorem category_theory.tensor_iso_inv {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category C] (f : X Y) (g : X' Y') :
(f g).inv = f.inv g.inv
def category_theory.tensor_iso {C : Type u} {X Y X' Y' : C} [category_theory.category C] [category_theory.monoidal_category C] (f : X Y) (g : X' Y') :
X X' Y Y'

The tensor product of two isomorphisms is an isomorphism.

Equations
theorem category_theory.monoidal_category.tensor_dite {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {P : Prop} [decidable P] {W X Y Z : C} (f : W X) (g : P (Y Z)) (g' : ¬P (Y Z)) :
f dite P (λ (h : P), g h) (λ (h : ¬P), g' h) = dite P (λ (h : P), f g h) (λ (h : ¬P), f g' h)
theorem category_theory.monoidal_category.dite_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {P : Prop} [decidable P] {W X Y Z : C} (f : W X) (g : P (Y Z)) (g' : ¬P (Y Z)) :
dite P (λ (h : P), g h) (λ (h : ¬P), g' h) f = dite P (λ (h : P), g h f) (λ (h : ¬P), g' h f)
@[simp]
theorem category_theory.monoidal_category.comp_tensor_id_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : X Y) {X' : C} (f' : Y Z X') :
(f g 𝟙 Z) f' = (f 𝟙 Z) (g 𝟙 Z) f'
@[simp]
theorem category_theory.monoidal_category.id_tensor_comp_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : X Y) {X' : C} (f' : Z Y X') :
(𝟙 Z f g) f' = (𝟙 Z f) (𝟙 Z g) f'
@[simp]
theorem category_theory.monoidal_category.id_tensor_comp_tensor_id_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : Y Z) {X' : C} (f' : Z X X') :
(𝟙 Y f) (g 𝟙 X) f' = (g f) f'
@[simp]
theorem category_theory.monoidal_category.tensor_id_comp_id_tensor_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {W X Y Z : C} (f : W X) (g : Y Z) {X' : C} (f' : Z X X') :
(g 𝟙 W) (𝟙 Z f) f' = (g f) f'
theorem category_theory.monoidal_category.left_unitor_inv_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' : C} (f : X X') {X'_1 : C} (f' : 𝟙_ C X' X'_1) :
f (λ_ X').inv f' = (λ_ X).inv (𝟙 (𝟙_ C) f) f'
theorem category_theory.monoidal_category.right_unitor_inv_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' : C} (f : X X') {X'_1 : C} (f' : X' 𝟙_ C X'_1) :
f (ρ_ X').inv f' = (ρ_ X).inv (f 𝟙 (𝟙_ C)) f'

The lemmas in the next section are true by coherence, but we prove them directly as they are used in proving the coherence theorem.

theorem category_theory.monoidal_category.pentagon_inv {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (W X Y Z : C) :
(𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) = (α_ W X (Y Z)).inv (α_ (W X) Y Z).inv
theorem category_theory.monoidal_category.pentagon_inv_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] (W X Y Z : C) {X' : C} (f' : ((W X) Y) Z X') :
(𝟙 W (α_ X Y Z).inv) (α_ W (X Y) Z).inv ((α_ W X Y).inv 𝟙 Z) f' = (α_ W X (Y Z)).inv (α_ (W X) Y Z).inv f'
theorem category_theory.monoidal_category.associator_inv_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y Z X' Y' Z' : C} (f : X X') (g : Y Y') (h : Z Z') {X'_1 : C} (f' : (X' Y') Z' X'_1) :
(f g h) (α_ X' Y' Z').inv f' = (α_ X Y Z).inv ((f g) h) f'
theorem category_theory.monoidal_category.associator_inv_naturality {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y Z X' Y' Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
(f g h) (α_ X' Y' Z').inv = (α_ X Y Z).inv ((f g) h)
theorem category_theory.monoidal_category.associator_conjugation_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') {X'_1 : C} (f' : (X' Y') Z' X'_1) :
((f g) h) f' = (α_ X Y Z).hom (f g h) (α_ X' Y' Z').inv f'
@[simp]
theorem category_theory.monoidal_category.associator_conjugation {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
(f g) h = (α_ X Y Z).hom (f g h) (α_ X' Y' Z').inv
theorem category_theory.monoidal_category.associator_inv_conjugation_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') {X'_1 : C} (f' : X' Y' Z' X'_1) :
(f g h) f' = (α_ X Y Z).inv ((f g) h) (α_ X' Y' Z').hom f'
theorem category_theory.monoidal_category.associator_inv_conjugation {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X X' Y Y' Z Z' : C} (f : X X') (g : Y Y') (h : Z Z') :
f g h = (α_ X Y Z).inv ((f g) h) (α_ X' Y' Z').hom
theorem category_theory.monoidal_category.id_tensor_associator_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y Z Z' : C} (h : Z Z') {X' : C} (f' : X Y Z' X') :
(𝟙 (X Y) h) (α_ X Y Z').hom f' = (α_ X Y Z).hom (𝟙 X 𝟙 Y h) f'
theorem category_theory.monoidal_category.id_tensor_associator_inv_naturality_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {X Y Z X' : C} (f : X X') {X'_1 : C} (f' : (X' Y) Z X'_1) :
(f 𝟙 (Y Z)) (α_ X' Y Z).inv f' = (α_ X Y Z).inv ((f 𝟙 Y) 𝟙 Z) f'
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : V Z X') :
(f.hom g) (f.inv h) f' = (𝟙 V g) (𝟙 V h) f'
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(f.hom g) (f.inv h) = (𝟙 V g) (𝟙 V h)
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(f.inv g) (f.hom h) = (𝟙 W g) (𝟙 W h)
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : W Z X') :
(f.inv g) (f.hom h) f' = (𝟙 W g) (𝟙 W h) f'
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : Z V X') :
(g f.hom) (h f.inv) f' = (g 𝟙 V) (h 𝟙 V) f'
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(g f.hom) (h f.inv) = (g 𝟙 V) (h 𝟙 V)
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) {X' : C} (f' : Z W X') :
(g f.inv) (h f.hom) f' = (g 𝟙 W) (h 𝟙 W) f'
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) (g : X Y) (h : Y Z) :
(g f.inv) (h f.hom) = (g 𝟙 W) (h 𝟙 W)
@[simp]
theorem category_theory.monoidal_category.hom_inv_id_tensor'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) [category_theory.is_iso f] (g : X Y) (h : Y Z) {X' : C} (f' : V Z X') :
(f g) (category_theory.inv f h) f' = (𝟙 V g) (𝟙 V h) f'
@[simp]
theorem category_theory.monoidal_category.inv_hom_id_tensor'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) [category_theory.is_iso f] (g : X Y) (h : Y Z) {X' : C} (f' : W Z X') :
(category_theory.inv f g) (f h) f' = (𝟙 W g) (𝟙 W h) f'
@[simp]
theorem category_theory.monoidal_category.tensor_hom_inv_id'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) [category_theory.is_iso f] (g : X Y) (h : Y Z) {X' : C} (f' : Z V X') :
(g f) (h category_theory.inv f) f' = (g 𝟙 V) (h 𝟙 V) f'
@[simp]
theorem category_theory.monoidal_category.tensor_inv_hom_id'_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] {V W X Y Z : C} (f : V W) [category_theory.is_iso f] (g : X Y) (h : Y Z) {X' : C} (f' : Z W X') :
(g category_theory.inv f) (h f) f' = (g 𝟙 W) (h 𝟙 W) f'

The tensor product expressed as a functor.

Equations

The left-associated triple tensor product as a functor.

Equations

The right-associated triple tensor product as a functor.

Equations

The functor λ X, 𝟙_ C ⊗ X.

Equations

The functor λ X, X ⊗ 𝟙_ C.

Equations

Tensoring on the right with a fixed object, as a functor.

Equations
Instances for category_theory.monoidal_category.tensor_right

Tensoring on the left, as a functor from C into endofunctors of C.

TODO: show this is a op-monoidal functor.

Equations
Instances for category_theory.monoidal_category.tensoring_left

Tensoring on the right, as a functor from C into endofunctors of C.

We later show this is a monoidal functor.

Equations
Instances for category_theory.monoidal_category.tensoring_right
@[simp]
theorem category_theory.monoidal_category.prod_monoidal_tensor_hom (C₁ : Type u₁) [category_theory.category C₁] [category_theory.monoidal_category C₁] (C₂ : Type u₂) [category_theory.category C₂] [category_theory.monoidal_category C₂] (_x _x_1 _x_2 _x_3 : C₁ × C₂) (f : _x _x_1) (g : _x_2 _x_3) :
f g = (f.fst g.fst, f.snd g.snd)
@[protected, instance]
Equations