Documentation

Mathlib.Tactic.CategoryTheory.MonoidalComp

Monoidal composition ⊗≫ (composition up to associators) #

We provide f ⊗≫ g, the monoidalComp operation, which automatically inserts associators and unitors as needed to make the target of f match the source of g.

Example #

Suppose we have a braiding morphism R X Y : X ⊗ Y ⟶ Y ⊗ X in a monoidal category, and that we want to define the morphism with the type V₁ ⊗ V₂ ⊗ V₃ ⊗ V₄ ⊗ V₅ ⟶ V₁ ⊗ V₃ ⊗ V₂ ⊗ V₄ ⊗ V₅ that transposes the second and third components by R V₂ V₃. How to do this? The first guess would be to use the whiskering operators and , and define the morphism as V₁ ◁ R V₂ V₃ ▷ V₄ ▷ V₅. However, this morphism has the type V₁ ⊗ ((V₂ ⊗ V₃) ⊗ V₄) ⊗ V₅ ⟶ V₁ ⊗ ((V₃ ⊗ V₂) ⊗ V₄) ⊗ V₅, which is not what we need. We should insert suitable associators. The desired associators can, in principle, be defined by using the primitive three-components associator α_ X Y Z : (X ⊗ Y) ⊗ Z ≅ X ⊗ (Y ⊗ Z) as a building block, but writing down actual definitions are quite tedious, and we usually don't want to see them.

The monoidal composition ⊗≫ is designed to solve such a problem. In this case, we can define the desired morphism as 𝟙 _ ⊗≫ V₁ ◁ R V₂ V₃ ▷ V₄ ▷ V₅ ⊗≫ 𝟙 _, where the first and the second 𝟙 _ are completed as 𝟙 (V₁ ⊗ V₂ ⊗ V₃ ⊗ V₄ ⊗ V₅) and 𝟙 (V₁ ⊗ V₃ ⊗ V₂ ⊗ V₄ ⊗ V₅), respectively.

A typeclass carrying a choice of monoidal structural isomorphism between two objects. Used by the ⊗≫ monoidal composition operator, and the coherence tactic.

  • hom : X Y

    A monoidal structural isomorphism between two objects.

  • isIso : CategoryTheory.IsIso CategoryTheory.MonoidalCoherence.hom
Instances
    theorem CategoryTheory.MonoidalCoherence.isIso {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} [self : CategoryTheory.MonoidalCoherence X Y] :
    CategoryTheory.IsIso CategoryTheory.MonoidalCoherence.hom

    Notation for identities up to unitors and associators.

    Equations
    Instances For

      Construct an isomorphism between two objects in a monoidal category out of unitors and associators.

      Equations
      Instances For
        def CategoryTheory.monoidalComp {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} [CategoryTheory.MonoidalCoherence X Y] (f : W X) (g : Y Z) :
        W Z

        Compose two morphisms in a monoidal category, inserting unitors and associators between as necessary.

        Equations
        Instances For

          Compose two morphisms in a monoidal category, inserting unitors and associators between as necessary.

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            def CategoryTheory.monoidalIsoComp {C : Type u} [CategoryTheory.Category.{v, u} C] {W : C} {X : C} {Y : C} {Z : C} [CategoryTheory.MonoidalCoherence X Y] (f : W X) (g : Y Z) :
            W Z

            Compose two isomorphisms in a monoidal category, inserting unitors and associators between as necessary.

            Equations
            Instances For

              Compose two isomorphisms in a monoidal category, inserting unitors and associators between as necessary.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.refl_hom {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
                CategoryTheory.MonoidalCoherence.hom = CategoryTheory.CategoryStruct.id X
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.whiskerLeft_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence Y Z] :
                CategoryTheory.MonoidalCoherence.hom = CategoryTheory.MonoidalCategory.whiskerLeft X CategoryTheory.MonoidalCoherence.hom
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.whiskerRight_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence X Y] :
                CategoryTheory.MonoidalCoherence.hom = CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.MonoidalCoherence.hom Z