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.

class CategoryTheory.MonoidalCoherence {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) : Type v

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.

def CategoryTheory.MonoidalCategory.«term⊗𝟙» : Lean.ParserDescr

Notation for identities up to unitors and associators.

Equations

• CategoryTheory.MonoidalCategory.«term⊗𝟙» = Lean.ParserDescr.node `CategoryTheory.MonoidalCategory.term⊗𝟙 1024 (Lean.ParserDescr.symbol " ⊗𝟙 ")

@[reducible, inline]

abbrev CategoryTheory.monoidalIso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] : X ≅ Y

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

Equations

• CategoryTheory.monoidalIso X Y = CategoryTheory.MonoidalCoherence.iso

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

• CategoryTheory.monoidalComp f g = CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.MonoidalCoherence.iso.hom g)

def CategoryTheory.MonoidalCategory.«term_⊗≫_» : Lean.TrailingParserDescr

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.

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

• CategoryTheory.monoidalIsoComp f g = f ≪≫ CategoryTheory.MonoidalCoherence.iso ≪≫ g

def CategoryTheory.MonoidalCategory.«term_≪⊗≫_» : Lean.TrailingParserDescr

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.

@[simp]

theorem CategoryTheory.MonoidalCoherence.refl_iso {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.MonoidalCoherence.iso = CategoryTheory.Iso.refl X

instance CategoryTheory.MonoidalCoherence.refl {C : Type u} [CategoryTheory.Category.{v, u} C] (X : C) : CategoryTheory.MonoidalCoherence X X

Equations

• CategoryTheory.MonoidalCoherence.refl X = { 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

instance CategoryTheory.MonoidalCoherence.whiskerLeft {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence Y Z] : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X Y) (CategoryTheory.MonoidalCategory.tensorObj X Z)

Equations

• CategoryTheory.MonoidalCoherence.whiskerLeft X Y Z = { 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

instance CategoryTheory.MonoidalCoherence.whiskerRight {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence X Y] : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X Z) (CategoryTheory.MonoidalCategory.tensorObj Y Z)

Equations

• CategoryTheory.MonoidalCoherence.whiskerRight X Y Z = { iso := CategoryTheory.MonoidalCategory.whiskerRightIso CategoryTheory.MonoidalCoherence.iso Z }

@[simp]

theorem CategoryTheory.MonoidalCoherence.tensor_right_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence (𝟙_ C) Y] : CategoryTheory.MonoidalCoherence.iso = (CategoryTheory.MonoidalCategory.rightUnitor X).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso X CategoryTheory.MonoidalCoherence.iso

instance CategoryTheory.MonoidalCoherence.tensor_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence (𝟙_ C) Y] : CategoryTheory.MonoidalCoherence X (CategoryTheory.MonoidalCategory.tensorObj X Y)

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCoherence.tensor_right'_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence Y (𝟙_ C)] : CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCategory.whiskerLeftIso X CategoryTheory.MonoidalCoherence.iso ≪≫ CategoryTheory.MonoidalCategory.rightUnitor X

instance CategoryTheory.MonoidalCoherence.tensor_right' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence Y (𝟙_ C)] : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X Y) X

Equations

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

@[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

instance CategoryTheory.MonoidalCoherence.left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X) Y

Equations

• CategoryTheory.MonoidalCoherence.left X Y = { 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

instance CategoryTheory.MonoidalCoherence.left' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] : CategoryTheory.MonoidalCoherence X (CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) Y)

Equations

• CategoryTheory.MonoidalCoherence.left' X Y = { 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

instance CategoryTheory.MonoidalCoherence.right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C)) Y

Equations

• CategoryTheory.MonoidalCoherence.right X Y = { 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

instance CategoryTheory.MonoidalCoherence.right' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) [CategoryTheory.MonoidalCoherence X Y] : CategoryTheory.MonoidalCoherence X (CategoryTheory.MonoidalCategory.tensorObj Y (𝟙_ C))

Equations

• CategoryTheory.MonoidalCoherence.right' X Y = { iso := CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategory.rightUnitor Y).symm }

@[simp]

theorem CategoryTheory.MonoidalCoherence.assoc_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) (W : C) [CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) W] : CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCategory.associator X Y Z ≪≫ CategoryTheory.MonoidalCoherence.iso

instance CategoryTheory.MonoidalCoherence.assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (X : C) (Y : C) (Z : C) (W : C) [CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) W] : CategoryTheory.MonoidalCoherence (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) W

Equations

• CategoryTheory.MonoidalCoherence.assoc X Y Z W = { iso := CategoryTheory.MonoidalCategory.associator X Y Z ≪≫ CategoryTheory.MonoidalCoherence.iso }

@[simp]

theorem CategoryTheory.MonoidalCoherence.assoc'_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence W (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))] : CategoryTheory.MonoidalCoherence.iso = CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategory.associator X Y Z).symm

instance CategoryTheory.MonoidalCoherence.assoc' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] (W : C) (X : C) (Y : C) (Z : C) [CategoryTheory.MonoidalCoherence W (CategoryTheory.MonoidalCategory.tensorObj X (CategoryTheory.MonoidalCategory.tensorObj Y Z))] : CategoryTheory.MonoidalCoherence W (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)

Equations

• CategoryTheory.MonoidalCoherence.assoc' W X Y Z = { iso := CategoryTheory.MonoidalCoherence.iso ≪≫ (CategoryTheory.MonoidalCategory.associator X Y Z).symm }

@[simp]

theorem CategoryTheory.monoidalComp_refl {C : Type u} [CategoryTheory.Category.{v, u} C] {X : C} {Y : C} {Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : CategoryTheory.monoidalComp f g = CategoryTheory.CategoryStruct.comp f g