Braided and symmetric monoidal categories

The basic definitions of braided monoidal categories, and symmetric monoidal categories, as well as braided functors.

Implementation note

We make BraidedCategory another typeclass, but then have SymmetricCategory extend this. The rationale is that we are not carrying any additional data, just requiring a property.

Future work

• Construct the Drinfeld center of a monoidal category as a braided monoidal category.
• Say something about pseudo-natural transformations.

class CategoryTheory.BraidedCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] : Type (max u v)

• braiding : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X
• braiding_naturality : ∀ {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (β_ Y Y').hom = CategoryTheory.CategoryStruct.comp (β_ X X').hom (CategoryTheory.MonoidalCategory.tensorHom g f)
• hexagon_forward : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (β_ X Z).hom))
• hexagon_reverse : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.tensorHom (β_ X Z).hom (CategoryTheory.CategoryStruct.id Y)))

A braided monoidal category is a monoidal category equipped with a braiding isomorphism β_ X Y : X ⊗ Y ≅ Y ⊗ X which is natural in both arguments, and also satisfies the two hexagon identities.

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [self : CategoryTheory.BraidedCategory C] {X : C} {X' : C} {Y : C} {Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Y' Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (CategoryTheory.CategoryStruct.comp (β_ Y Y').hom h) = CategoryTheory.CategoryStruct.comp (β_ X X').hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom g f) h)

theorem CategoryTheory.BraidedCategory.hexagon_reverse_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [self : CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj Z X) Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Z X Y).inv h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ X Z).hom (CategoryTheory.CategoryStruct.id Y)) h))

theorem CategoryTheory.BraidedCategory.hexagon_forward_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [self : CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Y (CategoryTheory.MonoidalCategory.tensorObj Z X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y Z X).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (β_ X Z).hom) h))

def CategoryTheory.termβ_ : Lean.ParserDescr

def CategoryTheory.braidedCategoryOfFaithful {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [CategoryTheory.Faithful F.toFunctor] [CategoryTheory.BraidedCategory D] (β : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X) (w : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y) (F.map (β X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X)) : CategoryTheory.BraidedCategory C

Verifying the axioms for a braiding by checking that the candidate braiding is sent to a braiding by a faithful monoidal functor.

noncomputable def CategoryTheory.braidedCategoryOfFullyFaithful {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [CategoryTheory.Full F.toFunctor] [CategoryTheory.Faithful F.toFunctor] [CategoryTheory.BraidedCategory D] : CategoryTheory.BraidedCategory C

Pull back a braiding along a fully faithful monoidal functor.

We now establish how the braiding interacts with the unitors.

I couldn't find a detailed proof in print, but this is discussed in:

• Proposition 1 of André Joyal and Ross Street, "Braided monoidal categories", Macquarie Math Reports 860081 (1986).
• Proposition 2.1 of André Joyal and Ross Street, "Braided tensor categories" , Adv. Math. 102 (1993), 20–78.
• Exercise 8.1.6 of Etingof, Gelaki, Nikshych, Ostrik, "Tensor categories", vol 25, Mathematical Surveys and Monographs (2015), AMS.

theorem CategoryTheory.braiding_leftUnitor_aux₁ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorUnit C) (CategoryTheory.MonoidalCategory.tensorUnit C) X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) (β_ X (CategoryTheory.MonoidalCategory.tensorUnit C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorUnit C) X (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.CategoryStruct.id X)) (β_ X (CategoryTheory.MonoidalCategory.tensorUnit C)).inv

theorem CategoryTheory.braiding_leftUnitor_aux₂ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ X (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C))) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C))) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C))

@[simp]

theorem CategoryTheory.braiding_leftUnitor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.MonoidalCategory.leftUnitor X).hom = (CategoryTheory.MonoidalCategory.rightUnitor X).hom

theorem CategoryTheory.braiding_rightUnitor_aux₁ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X (CategoryTheory.MonoidalCategory.tensorUnit C) (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ (CategoryTheory.MonoidalCategory.tensorUnit C) X).inv (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorUnit C) X (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom) (β_ (CategoryTheory.MonoidalCategory.tensorUnit C) X).inv

theorem CategoryTheory.braiding_rightUnitor_aux₂ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) (β_ (CategoryTheory.MonoidalCategory.tensorUnit C) X).hom) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.MonoidalCategory.rightUnitor X).hom) = CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.MonoidalCategory.leftUnitor X).hom

@[simp]

theorem CategoryTheory.braiding_rightUnitor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategory.tensorUnit C) X).hom (CategoryTheory.MonoidalCategory.rightUnitor X).hom = (CategoryTheory.MonoidalCategory.leftUnitor X).hom

@[simp]

theorem CategoryTheory.leftUnitor_inv_braiding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (β_ (CategoryTheory.MonoidalCategory.tensorUnit C) X).hom = (CategoryTheory.MonoidalCategory.rightUnitor X).inv

@[simp]

theorem CategoryTheory.rightUnitor_inv_braiding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (β_ X (CategoryTheory.MonoidalCategory.tensorUnit C)).hom = (CategoryTheory.MonoidalCategory.leftUnitor X).inv

class CategoryTheory.SymmetricCategory (C : Type u) [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] extends CategoryTheory.BraidedCategory : Type (max u v)

• braiding : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X
• braiding_naturality : ∀ {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (β_ Y Y').hom = CategoryTheory.CategoryStruct.comp (β_ X X').hom (CategoryTheory.MonoidalCategory.tensorHom g f)
• hexagon_forward : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ X Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id Y) (β_ X Z).hom))
• hexagon_reverse : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.tensorHom (β_ X Z).hom (CategoryTheory.CategoryStruct.id Y)))
• symmetry : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)

A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.

See https://stacks.math.columbia.edu/tag/0FFW.

@[simp]

theorem CategoryTheory.SymmetricCategory.symmetry_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [self : CategoryTheory.SymmetricCategory C] (X : C) (Y : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (β_ Y X).hom h) = h

structure CategoryTheory.LaxBraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] extends CategoryTheory.LaxMonoidalFunctor : Type (max (max (max u₁ u₂) v₁) v₂)

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
• ε : CategoryTheory.MonoidalCategory.tensorUnit D ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorUnit C)
• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (s.obj X) (s.obj Y) ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
• μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.map f) (s.map g)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X X') (s.map (CategoryTheory.MonoidalCategory.tensorHom f g))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y) (CategoryTheory.CategoryStruct.id (s.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (s.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (s.obj X) (s.obj Y) (s.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Z)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.ε (CategoryTheory.CategoryStruct.id (s.obj X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit C) X) (s.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) s.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorUnit C)) (s.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
• braided : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y) (s.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (s.obj X) (s.obj Y)).hom (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y X)

A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.id_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.LaxBraidedFunctor.id C).toLaxMonoidalFunctor.toFunctor.map f = f

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.id_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : (CategoryTheory.LaxBraidedFunctor.id C).toLaxMonoidalFunctor.toFunctor.obj X = X

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.id_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.LaxBraidedFunctor.id C).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.id_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.LaxBraidedFunctor.id C).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)

def CategoryTheory.LaxBraidedFunctor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.LaxBraidedFunctor C C

The identity lax braided monoidal functor.

instance CategoryTheory.LaxBraidedFunctor.instInhabitedLaxBraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Inhabited (CategoryTheory.LaxBraidedFunctor C C)

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.comp_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.LaxBraidedFunctor C D) (G : CategoryTheory.LaxBraidedFunctor D E) (X : C) : (CategoryTheory.LaxBraidedFunctor.comp F G).toLaxMonoidalFunctor.toFunctor.obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.comp_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.LaxBraidedFunctor C D) (G : CategoryTheory.LaxBraidedFunctor D E) (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.LaxBraidedFunctor.comp F G).toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ G.toLaxMonoidalFunctor (F.obj X) (F.obj Y)) (G.map (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y))

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.comp_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.LaxBraidedFunctor C D) (G : CategoryTheory.LaxBraidedFunctor D E) : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.LaxBraidedFunctor.comp F G).toLaxMonoidalFunctor.toFunctor.map f = G.map (F.map f)

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.comp_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.LaxBraidedFunctor C D) (G : CategoryTheory.LaxBraidedFunctor D E) : (CategoryTheory.LaxBraidedFunctor.comp F G).toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.comp G.ε (G.map F.ε)

def CategoryTheory.LaxBraidedFunctor.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.LaxBraidedFunctor C D) (G : CategoryTheory.LaxBraidedFunctor D E) : CategoryTheory.LaxBraidedFunctor C E

The composition of lax braided monoidal functors.

instance CategoryTheory.LaxBraidedFunctor.categoryLaxBraidedFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.LaxBraidedFunctor C D)

theorem CategoryTheory.LaxBraidedFunctor.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.LaxBraidedFunctor C D} {G : CategoryTheory.LaxBraidedFunctor C D} {α : F ⟶ G} {β : F ⟶ G} (w : ∀ (X : C), α.app X = β.app X) : α = β

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.comp_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.LaxBraidedFunctor C D} {G : CategoryTheory.LaxBraidedFunctor C D} {H : CategoryTheory.LaxBraidedFunctor C D} {α : F ⟶ G} {β : G ⟶ H} : (CategoryTheory.CategoryStruct.comp α β).toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mkIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.LaxBraidedFunctor C D} {G : CategoryTheory.LaxBraidedFunctor C D} (i : F.toLaxMonoidalFunctor ≅ G.toLaxMonoidalFunctor) : (CategoryTheory.LaxBraidedFunctor.mkIso i).hom = i.hom

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.mkIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.LaxBraidedFunctor C D} {G : CategoryTheory.LaxBraidedFunctor C D} (i : F.toLaxMonoidalFunctor ≅ G.toLaxMonoidalFunctor) : (CategoryTheory.LaxBraidedFunctor.mkIso i).inv = i.inv

def CategoryTheory.LaxBraidedFunctor.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.LaxBraidedFunctor C D} {G : CategoryTheory.LaxBraidedFunctor C D} (i : F.toLaxMonoidalFunctor ≅ G.toLaxMonoidalFunctor) : F ≅ G

Interpret a natural isomorphism of the underlying lax monoidal functors as an isomorphism of the lax braided monoidal functors.

structure CategoryTheory.BraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] extends CategoryTheory.MonoidalFunctor : Type (max (max (max u₁ u₂) v₁) v₂)

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (s.obj X ⟶ s.obj Y)
• map_id : ∀ (X : C), s.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (s.obj X)
• map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), s.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (s.map f) (s.map g)
• ε : CategoryTheory.MonoidalCategory.tensorUnit D ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorUnit C)
• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (s.obj X) (s.obj Y) ⟶ s.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
• μ_natural : ∀ {X Y X' Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (s.map f) (s.map g)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Y') = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X X') (s.map (CategoryTheory.MonoidalCategory.tensorHom f g))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y) (CategoryTheory.CategoryStruct.id (s.obj Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (s.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (s.obj X) (s.obj Y) (s.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y Z)) (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom s.ε (CategoryTheory.CategoryStruct.id (s.obj X))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor (CategoryTheory.MonoidalCategory.tensorUnit C) X) (s.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (s.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (s.obj X)) s.ε) (CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X (CategoryTheory.MonoidalCategory.tensorUnit C)) (s.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
• ε_isIso : CategoryTheory.IsIso s.ε
• μ_isIso : ∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y)
• braided : ∀ (X Y : C), s.map (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor X Y)) (CategoryTheory.CategoryStruct.comp (β_ (s.obj X) (s.obj Y)).hom (CategoryTheory.LaxMonoidalFunctor.μ s.toLaxMonoidalFunctor Y X))

A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.

def CategoryTheory.symmetricCategoryOfFaithful {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory C] [CategoryTheory.SymmetricCategory D] (F : CategoryTheory.BraidedFunctor C D) [CategoryTheory.Faithful F.toFunctor] : CategoryTheory.SymmetricCategory C

A braided category with a faithful braided functor to a symmetric category is itself symmetric.

@[simp]

theorem CategoryTheory.BraidedFunctor.toLaxBraidedFunctor_toLaxMonoidalFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.BraidedFunctor C D) : (CategoryTheory.BraidedFunctor.toLaxBraidedFunctor C D F).toLaxMonoidalFunctor = F.toLaxMonoidalFunctor

def CategoryTheory.BraidedFunctor.toLaxBraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (D : Type u₂) [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] (F : CategoryTheory.BraidedFunctor C D) : CategoryTheory.LaxBraidedFunctor C D

Turn a braided functor into a lax braided functor.

@[simp]

theorem CategoryTheory.BraidedFunctor.id_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.BraidedFunctor.id C).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorUnit C)

@[simp]

theorem CategoryTheory.BraidedFunctor.id_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : (CategoryTheory.BraidedFunctor.id C).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X = X

@[simp]

theorem CategoryTheory.BraidedFunctor.id_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.BraidedFunctor.id C).toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)

@[simp]

theorem CategoryTheory.BraidedFunctor.id_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.BraidedFunctor.id C).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = f

def CategoryTheory.BraidedFunctor.id (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedFunctor C C

The identity braided monoidal functor.

instance CategoryTheory.BraidedFunctor.instInhabitedBraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : Inhabited (CategoryTheory.BraidedFunctor C C)

@[simp]

theorem CategoryTheory.BraidedFunctor.comp_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.BraidedFunctor C D) (G : CategoryTheory.BraidedFunctor D E) (X : C) (Y : C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.BraidedFunctor.comp F G).toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ G.toLaxMonoidalFunctor (F.obj X) (F.obj Y)) (G.map (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y))

@[simp]

theorem CategoryTheory.BraidedFunctor.comp_obj {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.BraidedFunctor C D) (G : CategoryTheory.BraidedFunctor D E) (X : C) : (CategoryTheory.BraidedFunctor.comp F G).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X = G.obj (F.obj X)

@[simp]

theorem CategoryTheory.BraidedFunctor.comp_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.BraidedFunctor C D) (G : CategoryTheory.BraidedFunctor D E) : (CategoryTheory.BraidedFunctor.comp F G).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.comp G.ε (G.map F.ε)

@[simp]

theorem CategoryTheory.BraidedFunctor.comp_map {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.BraidedFunctor C D) (G : CategoryTheory.BraidedFunctor D E) : ∀ {X Y : C} (f : X ⟶ Y), (CategoryTheory.BraidedFunctor.comp F G).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = G.map (F.map f)

def CategoryTheory.BraidedFunctor.comp {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {E : Type u₃} [CategoryTheory.Category.{v₃, u₃} E] [CategoryTheory.MonoidalCategory E] [CategoryTheory.BraidedCategory E] (F : CategoryTheory.BraidedFunctor C D) (G : CategoryTheory.BraidedFunctor D E) : CategoryTheory.BraidedFunctor C E

The composition of braided monoidal functors.

instance CategoryTheory.BraidedFunctor.categoryBraidedFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] : CategoryTheory.Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (CategoryTheory.BraidedFunctor C D)

theorem CategoryTheory.BraidedFunctor.ext' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.BraidedFunctor C D} {G : CategoryTheory.BraidedFunctor C D} {α : F ⟶ G} {β : F ⟶ G} (w : ∀ (X : C), α.app X = β.app X) : α = β

@[simp]

theorem CategoryTheory.BraidedFunctor.comp_toNatTrans {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.BraidedFunctor C D} {G : CategoryTheory.BraidedFunctor C D} {H : CategoryTheory.BraidedFunctor C D} {α : F ⟶ G} {β : G ⟶ H} : (CategoryTheory.CategoryStruct.comp α β).toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans

@[simp]

theorem CategoryTheory.BraidedFunctor.mkIso_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.BraidedFunctor C D} {G : CategoryTheory.BraidedFunctor C D} (i : F.toMonoidalFunctor ≅ G.toMonoidalFunctor) : (CategoryTheory.BraidedFunctor.mkIso i).inv = i.inv

@[simp]

theorem CategoryTheory.BraidedFunctor.mkIso_hom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.BraidedFunctor C D} {G : CategoryTheory.BraidedFunctor C D} (i : F.toMonoidalFunctor ≅ G.toMonoidalFunctor) : (CategoryTheory.BraidedFunctor.mkIso i).hom = i.hom

def CategoryTheory.BraidedFunctor.mkIso {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory D] {F : CategoryTheory.BraidedFunctor C D} {G : CategoryTheory.BraidedFunctor C D} (i : F.toMonoidalFunctor ≅ G.toMonoidalFunctor) : F ≅ G

Interpret a natural isomorphism of the underlying monoidal functors as an isomorphism of the braided monoidal functors.

instance CategoryTheory.instBraidedCategoryDiscreteDiscreteCategoryMonoidalToMonoid (M : Type u) [CommMonoid M] : CategoryTheory.BraidedCategory (CategoryTheory.Discrete M)

@[simp]

theorem CategoryTheory.Discrete.braidedFunctor_ε {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) : (CategoryTheory.Discrete.braidedFunctor F).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.Discrete.eqToHom (_ : 1 = ↑F 1)

@[simp]

theorem CategoryTheory.Discrete.braidedFunctor_map {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) : ∀ {X Y : CategoryTheory.Discrete M} (f : X ⟶ Y), (CategoryTheory.Discrete.braidedFunctor F).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.Discrete.eqToHom (_ : ↑F X.as = ↑F Y.as)

@[simp]

theorem CategoryTheory.Discrete.braidedFunctor_obj_as {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) (X : CategoryTheory.Discrete M) : ((CategoryTheory.Discrete.braidedFunctor F).toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X).as = ↑F X.as

@[simp]

theorem CategoryTheory.Discrete.braidedFunctor_μ {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.Discrete.braidedFunctor F).toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.Discrete.eqToHom (_ : ↑F X.as * ↑F Y.as = ↑F (X.as * Y.as))

def CategoryTheory.Discrete.braidedFunctor {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) : CategoryTheory.BraidedFunctor (CategoryTheory.Discrete M) (CategoryTheory.Discrete N)

A multiplicative morphism between commutative monoids gives a braided functor between the corresponding discrete braided monoidal categories.

def CategoryTheory.tensor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C × C) (Y : C × C) : CategoryTheory.MonoidalCategory.tensorObj ((CategoryTheory.MonoidalCategory.tensor C).obj X) ((CategoryTheory.MonoidalCategory.tensor C).obj Y) ⟶ (CategoryTheory.MonoidalCategory.tensor C).obj (CategoryTheory.MonoidalCategory.tensorObj X Y)

The strength of the tensor product functor from C × C to C.

theorem CategoryTheory.tensor_μ_def₁ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ Y₁ (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂)).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.MonoidalCategory.associator Y₁ X₂ Y₂).inv)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.MonoidalCategory.associator X₂ Y₁ Y₂).inv) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.MonoidalCategory.tensorHom (β_ X₂ Y₁).hom (CategoryTheory.CategoryStruct.id Y₂))))

theorem CategoryTheory.tensor_μ_def₂ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.MonoidalCategory.associator X₂ Y₁ Y₂).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X₁ X₂ (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂)).inv (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.MonoidalCategory.tensorHom (β_ X₂ Y₁).hom (CategoryTheory.CategoryStruct.id Y₂))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X₁) (CategoryTheory.MonoidalCategory.associator Y₁ X₂ Y₂).hom) (CategoryTheory.MonoidalCategory.associator X₁ Y₁ (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂)).inv)

theorem CategoryTheory.tensor_μ_natural (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} {U₁ : C} {U₂ : C} {V₁ : C} {V₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : U₁ ⟶ V₁) (g₂ : U₂ ⟶ V₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)) (CategoryTheory.tensor_μ C (Y₁, Y₂) (V₁, V₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (U₁, U₂)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ g₁) (CategoryTheory.MonoidalCategory.tensorHom f₂ g₂))

theorem CategoryTheory.tensor_left_unitality (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) : (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorUnit C, CategoryTheory.MonoidalCategory.tensorUnit C) (X₁, X₂)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X₁).hom (CategoryTheory.MonoidalCategory.leftUnitor X₂).hom))

theorem CategoryTheory.tensor_right_unitality (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) : (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (CategoryTheory.MonoidalCategory.tensorUnit C, CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X₁).hom (CategoryTheory.MonoidalCategory.rightUnitor X₂).hom))

theorem CategoryTheory.tensor_associativity_aux (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (W : C) (X : C) (Y : C) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ W X).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y Z))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X W (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.associator W Y Z).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (β_ (CategoryTheory.MonoidalCategory.tensorObj W Y) Z).hom) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id X) (CategoryTheory.MonoidalCategory.associator Z W Y).inv)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj W X)) (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Z Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator W X Z).hom (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ W (CategoryTheory.MonoidalCategory.tensorObj X Z)).hom (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator X Z W).hom (CategoryTheory.CategoryStruct.id Y)) (CategoryTheory.MonoidalCategory.associator X (CategoryTheory.MonoidalCategory.tensorObj Z W) Y).hom))))

theorem CategoryTheory.tensor_associativity (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) (Z₁ : C) (Z₂ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁, CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (Z₁, Z₂)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator X₁ Y₁ Z₁).hom (CategoryTheory.MonoidalCategory.associator X₂ Y₂ Z₂).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂) (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂))) (CategoryTheory.tensor_μ C (X₁, X₂) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Z₁, CategoryTheory.MonoidalCategory.tensorObj Y₂ Z₂)))

@[simp]

theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_ε (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.tensorMonoidal C).toLaxMonoidalFunctor.ε = (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).inv

@[simp]

theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_toFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C × C) : (CategoryTheory.tensorMonoidal C).toLaxMonoidalFunctor.toFunctor.obj X = CategoryTheory.MonoidalCategory.tensorObj X.fst X.snd

@[simp]

theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_toFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : C × C} {Y : C × C} (f : X ⟶ Y) : (CategoryTheory.tensorMonoidal C).toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.MonoidalCategory.tensorHom f.fst f.snd

@[simp]

theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C × C) (Y : C × C) : CategoryTheory.LaxMonoidalFunctor.μ (CategoryTheory.tensorMonoidal C).toLaxMonoidalFunctor X Y = CategoryTheory.tensor_μ C X Y

def CategoryTheory.tensorMonoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.MonoidalFunctor (C × C) C

The tensor product functor from C × C to C as a monoidal functor.

theorem CategoryTheory.leftUnitor_monoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X₁).hom (CategoryTheory.MonoidalCategory.leftUnitor X₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorUnit C, X₁) (CategoryTheory.MonoidalCategory.tensorUnit C, X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂))) (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom)

theorem CategoryTheory.rightUnitor_monoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) : CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X₁).hom (CategoryTheory.MonoidalCategory.rightUnitor X₂).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, CategoryTheory.MonoidalCategory.tensorUnit C) (X₂, CategoryTheory.MonoidalCategory.tensorUnit C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorUnit C)).hom) (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom)

theorem CategoryTheory.associator_monoidal_aux (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (W : C) (X : C) (Y : C) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id W) (CategoryTheory.MonoidalCategory.associator Y Z X).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W Y (CategoryTheory.MonoidalCategory.tensorObj Z X)).inv (CategoryTheory.MonoidalCategory.tensorHom (β_ W Y).hom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Z X))))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator W X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj W X) Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (β_ (CategoryTheory.MonoidalCategory.tensorObj W X) Y).hom (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator Y W X).inv (CategoryTheory.CategoryStruct.id Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj Y W) X Z).hom (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj Y W)) (β_ X Z).hom)))))

theorem CategoryTheory.associator_monoidal (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (X₃ : C) (Y₁ : C) (Y₂ : C) (Y₃ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂, X₃) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂, Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃))) (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, CategoryTheory.MonoidalCategory.tensorObj X₂ X₃) (Y₁, CategoryTheory.MonoidalCategory.tensorObj Y₂ Y₃)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁)) (CategoryTheory.tensor_μ C (X₂, X₃) (Y₂, Y₃))))