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.

  • iso : X Y

    A monoidal structural isomorphism between two objects.

Instances

    Notation for identities up to unitors and associators.

    Equations
    Instances For
      @[reducible, inline]

      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_iso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.Iso.refl X
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.whiskerLeft_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence Y Z] :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCategory.whiskerLeftIso X CategoryTheory.MonoidalCoherence.iso
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.whiskerRight_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence X Y] :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCategory.whiskerRightIso CategoryTheory.MonoidalCoherence.iso Z
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.left_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCategory.leftUnitor X ≪≫ CategoryTheory.MonoidalCoherence.iso
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.left'_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategory.leftUnitor Y).symm
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.right_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCategory.rightUnitor X ≪≫ CategoryTheory.MonoidalCoherence.iso
                @[simp]
                theorem CategoryTheory.MonoidalCoherence.right'_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] :
                CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategory.rightUnitor Y).symm