Documentation

Mathlib.CategoryTheory.Monoidal.Category

Monoidal categories #

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 leftUnitor_nat_iso, rightUnitor_nat_iso and associator_nat_iso.

Some consequences of the definition are proved in other files after proving the coherence theorem, e.g. (λ_ (𝟙_ C)).hom = (ρ_ (𝟙_ C)).hom in CategoryTheory.Monoidal.CoherenceLemmas.

Implementation notes #

In the definition of monoidal categories, we also provide the whiskering operators:

If you want to provide tensorHom and define whiskerLeft and whiskerRight in terms of it, you can use the alternative constructor CategoryTheory.MonoidalCategory.ofTensorHom.

The whiskerings are useful when considering simp-normal forms of morphisms in monoidal categories.

References #

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
    @[inline, reducible]

    The tensor unity in the monoidal structure 𝟙_ C

    Instances For

      Notation for tensorObj, the tensor product of objects in a monoidal category

      Instances For

        Notation for the whiskerLeft operator of monoidal categories

        Instances For

          Notation for the whiskerRight operator of monoidal categories

          Instances For

            Notation for tensorHom, the tensor product of morphisms in a monoidal category

            Instances For

              Notation for tensorUnit, the two-sided identity of

              Instances For

                Notation for the monoidal associator: (X ⊗ Y) ⊗ Z) ≃ X ⊗ (Y ⊗ Z)

                Instances For

                  Notation for the leftUnitor: 𝟙_C ⊗ X ≃ X

                  Instances For

                    Notation for the rightUnitor: X ⊗ 𝟙_C ≃ X

                    Instances For
                      @[simp]
                      theorem CategoryTheory.tensorIso_hom {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f : X Y) (g : X' Y') :
                      @[simp]
                      theorem CategoryTheory.tensorIso_inv {C : Type u} {X : C} {Y : C} {X' : C} {Y' : C} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (f : X Y) (g : X' Y') :

                      The tensor product of two isomorphisms is an isomorphism.

                      Instances For

                        Notation for tensorIso, the tensor product of isomorphisms

                        Instances For
                          theorem CategoryTheory.MonoidalCategory.tensor_dite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : Prop} [Decidable P] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : P → (Y Z)) (g' : ¬P → (Y Z)) :
                          theorem CategoryTheory.MonoidalCategory.dite_tensor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : Prop} [Decidable P] {W : C} {X : C} {Y : C} {Z : C} (f : W X) (g : P → (Y Z)) (g' : ¬P → (Y Z)) :

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

                          def CategoryTheory.MonoidalCategory.ofTensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] (tensorObj : CCC) (tensorHom : {X₁ Y₁ X₂ Y₂ : C} → (X₁ Y₁) → (X₂ Y₂) → (tensorObj X₁ X₂ tensorObj Y₁ Y₂)) (whiskerLeft : optParam ((X : C) → {Y₁ Y₂ : C} → (Y₁ Y₂) → (tensorObj X Y₁ tensorObj X Y₂)) fun X x x_1 f => tensorHom X X x x_1 (CategoryTheory.CategoryStruct.id X) f) (whiskerRight : optParam ({X₁ X₂ : C} → (X₁ X₂) → (Y : C) → tensorObj X₁ Y tensorObj X₂ Y) fun {X₁ X₂} f Y => tensorHom X₁ X₂ Y Y f (CategoryTheory.CategoryStruct.id Y)) (tensor_id : autoParam (∀ (X₁ X₂ : C), tensorHom X₁ X₁ X₂ X₂ (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (tensorObj X₁ X₂)) _auto✝) (id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ Y₂), tensorHom X X Y₁ Y₂ (CategoryTheory.CategoryStruct.id X) f = whiskerLeft X Y₁ Y₂ f) _auto✝) (tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ X₂) (Y : C), tensorHom X₁ X₂ Y Y f (CategoryTheory.CategoryStruct.id Y) = whiskerRight X₁ X₂ f Y) _auto✝) (tensor_comp : autoParam (∀ {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂), tensorHom X₁ Z₁ X₂ Z₂ (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (tensorHom X₁ Y₁ X₂ Y₂ f₁ f₂) (tensorHom Y₁ Z₁ Y₂ Z₂ g₁ g₂)) _auto✝) (tensorUnit' : C) (associator : (X Y Z : C) → tensorObj (tensorObj X Y) Z tensorObj X (tensorObj Y Z)) (associator_naturality : autoParam (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃), CategoryTheory.CategoryStruct.comp (tensorHom (tensorObj X₁ X₂) (tensorObj Y₁ Y₂) X₃ Y₃ (tensorHom X₁ Y₁ X₂ Y₂ f₁ f₂) f₃) (associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (associator X₁ X₂ X₃).hom (tensorHom X₁ Y₁ (tensorObj X₂ X₃) (tensorObj Y₂ Y₃) f₁ (tensorHom X₂ Y₂ X₃ Y₃ f₂ f₃))) _auto✝) (leftUnitor : (X : C) → tensorObj tensorUnit' X X) (leftUnitor_naturality : autoParam (∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (tensorHom tensorUnit' tensorUnit' X Y (CategoryTheory.CategoryStruct.id tensorUnit') f) (leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (leftUnitor X).hom f) _auto✝) (rightUnitor : (X : C) → tensorObj X tensorUnit' X) (rightUnitor_naturality : autoParam (∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (tensorHom X Y tensorUnit' tensorUnit' f (CategoryTheory.CategoryStruct.id tensorUnit')) (rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (rightUnitor X).hom f) _auto✝) (pentagon : autoParam (∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (tensorHom (tensorObj (tensorObj W X) Y) (tensorObj W (tensorObj X Y)) Z Z (associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (associator W (tensorObj X Y) Z).hom (tensorHom W W (tensorObj (tensorObj X Y) Z) (tensorObj X (tensorObj Y Z)) (CategoryTheory.CategoryStruct.id W) (associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (associator (tensorObj W X) Y Z).hom (associator W X (tensorObj Y Z)).hom) _auto✝) (triangle : autoParam (∀ (X Y : C), CategoryTheory.CategoryStruct.comp (associator X tensorUnit' Y).hom (tensorHom X X (tensorObj tensorUnit' Y) Y (CategoryTheory.CategoryStruct.id X) (leftUnitor Y).hom) = tensorHom (tensorObj X tensorUnit') X Y Y (rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)) _auto✝) :

                          A constructor for monoidal categories that requires tensorHom instead of whiskerLeft and whiskerRight.

                          Instances For

                            The tensor product expressed as a functor.

                            Instances For

                              The left-associated triple tensor product as a functor.

                              Instances For

                                The right-associated triple tensor product as a functor.

                                Instances For

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

                                  Instances For

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

                                    Instances For

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

                                      TODO: show this is an op-monoidal functor.

                                      Instances For

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

                                        We later show this is a monoidal functor.

                                        Instances For