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.

Simp-normal form for morphisms #

Rewriting involving associators and unitors could be very complicated. We try to ease this complexity by putting carefully chosen simp lemmas that rewrite any morphisms into the simp-normal form defined below. Rewriting into simp-normal form is especially useful in preprocessing performed by the coherence tactic.

The simp-normal form of morphisms is defined to be an expression that has the minimal number of parentheses. More precisely,

  1. it is a composition of morphisms like f₁ ≫ f₂ ≫ f₃ ≫ f₄ ≫ f₅ such that each fᵢ is either a structural morphisms (morphisms made up only of identities, associators, unitors) or non-structural morphisms, and
  2. each non-structural morphism in the composition is of the form X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅, where each Xᵢ is a object that is not the identity or a tensor and f is a non-structural morphisms that is not the identity or a composite.

Note that X₁ ◁ X₂ ◁ X₃ ◁ f ▷ X₄ ▷ X₅ is actually X₁ ◁ (X₂ ◁ (X₃ ◁ ((f ▷ X₄) ▷ X₅))).

Currently, the simp lemmas don't rewrite 𝟙 X ⊗ f and f ⊗ 𝟙 Y into X ◁ f and f ▷ Y, respectively, since it requires a huge refactoring. We hope to add these simp lemmas soon.

References #

Auxiliary structure to carry only the data fields of (and provide notation for) MonoidalCategory.

Instances

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

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For

      Notation for the whiskerLeft operator of monoidal categories

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        Notation for the whiskerRight operator of monoidal categories

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            Notation for tensorUnit, the two-sided identity of

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For

              Used to ensure that 𝟙_ notation is used, as the ascription makes this not automatic.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

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

                Equations
                Instances For

                  Notation for the leftUnitor: 𝟙_C ⊗ X ≃ X

                  Equations
                  Instances For

                    Notation for the rightUnitor: X ⊗ 𝟙_C ≃ X

                    Equations
                    Instances For

                      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
                        @[simp]
                        theorem CategoryTheory.MonoidalCategory.tensor_comp {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [self : CategoryTheory.MonoidalCategory C] {X₁ : C} {Y₁ : C} {Z₁ : C} {X₂ : C} {Y₂ : C} {Z₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : Y₁ Z₁) (g₂ : Y₂ Z₂) :

                        Composition of tensor products is tensor product of compositions: (f₁ ⊗ g₁) ∘ (f₂ ⊗ g₂) = (f₁ ∘ f₂) ⊗ (g₁ ⊗ g₂)

                        Naturality of the associator isomorphism: (f₁ ⊗ f₂) ⊗ f₃ ≃ f₁ ⊗ (f₂ ⊗ f₃)

                        Naturality of the left unitor, commutativity of 𝟙_ C ⊗ X ⟶ 𝟙_ C ⊗ Y ⟶ Y and 𝟙_ C ⊗ X ⟶ X ⟶ Y

                        Naturality of the right unitor: commutativity of X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y and X ⊗ 𝟙_ C ⟶ X ⟶ Y

                        The left whiskering of an isomorphism is an isomorphism.

                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For

                          The right whiskering of an isomorphism is an isomorphism.

                          Equations
                          • One or more equations did not get rendered due to their size.
                          Instances For
                            @[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') :
                            @[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') :

                            The tensor product of two isomorphisms is an isomorphism.

                            Equations
                            Instances For

                              Notation for tensorIso, the tensor product of isomorphisms

                              Equations
                              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.

                                @[reducible, inline]
                                abbrev CategoryTheory.MonoidalCategory.ofTensorHom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategoryStruct C] (tensor_id : autoParam (∀ (X₁ X₂ : C), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) _auto✝) (id_tensorHom : autoParam (∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ Y₂), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f = CategoryTheory.MonoidalCategory.whiskerLeft X f) _auto✝) (tensorHom_id : autoParam (∀ {X₁ X₂ : C} (f : X₁ X₂) (Y : C), CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.MonoidalCategory.whiskerRight 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₂), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁) (CategoryTheory.CategoryStruct.comp f₂ g₂) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)) _auto✝) (associator_naturality : autoParam (∀ {X₁ X₂ X₃ Y₁ Y₂ Y₃ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (f₃ : X₃ Y₃), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) f₃) (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategory.tensorHom f₁ (CategoryTheory.MonoidalCategory.tensorHom f₂ f₃))) _auto✝) (leftUnitor_naturality : autoParam (∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (𝟙_ C)) f) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom f) _auto✝) (rightUnitor_naturality : autoParam (∀ {X Y : C} (f : X Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id (𝟙_ C))) (CategoryTheory.MonoidalCategory.rightUnitor Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom f) _auto✝) (pentagon : autoParam (∀ (W X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).hom (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom) _auto✝) (triangle : autoParam (∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (𝟙_ C) Y).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.leftUnitor Y).hom) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.id Y)) _auto✝) :

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

                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  The tensor product expressed as a functor.

                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    The left-associated triple tensor product as a functor.

                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      The right-associated triple tensor product as a functor.

                                      Equations
                                      • One or more equations did not get rendered due to their size.
                                      Instances For

                                        The tensor product bifunctor C ⥤ C ⥤ C of a monoidal category.

                                        Equations
                                        • One or more equations did not get rendered due to their size.
                                        Instances For
                                          @[reducible, inline]

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

                                          TODO: show this is an op-monoidal functor.

                                          Equations
                                          Instances For