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]

                        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

                        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

                            The tensor product of two isomorphisms is an isomorphism.

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

                              Notation for tensorIso, the tensor product of isomorphisms

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                theorem CategoryTheory.MonoidalCategory.tensor_dite {C : Type u} [𝒞 : CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] {P : Prop} [Decidable P] {W X Y 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 X Y 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 : ∀ (X₁ X₂ : C), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.CategoryStruct.id X₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) := by aesop_cat) (id_tensorHom : ∀ (X : C) {Y₁ Y₂ : C} (f : Y₁ Y₂), CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) f = CategoryTheory.MonoidalCategory.whiskerLeft X f := by aesop_cat) (tensorHom_id : ∀ {X₁ X₂ : C} (f : X₁ X₂) (Y : C), CategoryTheory.MonoidalCategory.tensorHom f (CategoryTheory.CategoryStruct.id Y) = CategoryTheory.MonoidalCategory.whiskerRight f Y := by aesop_cat) (tensor_comp : ∀ {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₂) := by aesop_cat) (associator_naturality : ∀ {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₃)) := by aesop_cat) (leftUnitor_naturality : ∀ {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 := by aesop_cat) (rightUnitor_naturality : ∀ {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 := by aesop_cat) (pentagon : ∀ (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 := by aesop_cat) (triangle : ∀ (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) := by aesop_cat) :

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

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

                                            We later show this is a monoidal functor.

                                            Equations
                                            Instances For