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)

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.

• braiding : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X

  The braiding natural isomorphism.

• braiding_naturality_right : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (β_ X Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)
• braiding_naturality_left : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (β_ Y Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Z 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.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).hom))

  The first hexagon identity.

• 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.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y))

  The second hexagon identity.

@[simp]

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

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_naturality_right_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [self : CategoryTheory.BraidedCategory C] (X : C) {Y : C} {Z : C} (f : Y ⟶ Z✝) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z✝ X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (CategoryTheory.CategoryStruct.comp (β_ X Z✝).hom h) = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X) 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.whiskerRight (β_ X Y).hom Z✝) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z✝).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z✝).hom) 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.whiskerLeft X (β_ Y Z✝).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z✝ Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z✝).hom Y) h))

def CategoryTheory.termβ_ : Lean.ParserDescr

The braiding natural isomorphism.

Equations

• CategoryTheory.termβ_ = Lean.ParserDescr.node `CategoryTheory.termβ_ 1024 (Lean.ParserDescr.symbol "β_")

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_tensor_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) : (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y) (CategoryTheory.MonoidalCategory.associator Z X Y).hom)))

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_tensor_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) : (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).hom) (CategoryTheory.MonoidalCategory.associator Y Z X).inv)))

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_inv_tensor_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) : (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Z X Y).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).inv Y) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (β_ Y Z).inv) (CategoryTheory.MonoidalCategory.associator X Y Z).inv)))

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_inv_tensor_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) : (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).inv = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y Z X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Y).inv Z) (CategoryTheory.MonoidalCategory.associator X Y Z).hom)))

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_naturality_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [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)

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X : C} {X' : C} {Y : C} {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)

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 (F.toLaxMonoidalFunctor.μ X Y) (F.toPrefunctor.map (β X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)).hom (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.

Equations

• CategoryTheory.braidedCategoryOfFaithful F β w = CategoryTheory.BraidedCategory.mk β

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.

Equations

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

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 (𝟙_ C) (𝟙_ C) X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) (β_ X (𝟙_ C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).hom (𝟙_ C)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom X) (β_ X (𝟙_ 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.whiskerRight (β_ X (𝟙_ C)).hom (𝟙_ C)) (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).hom (𝟙_ C)) = CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.rightUnitor X).hom (𝟙_ C)

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

theorem CategoryTheory.braiding_leftUnitor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : CategoryTheory.CategoryStruct.comp (β_ X (𝟙_ 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 (𝟙_ C) (𝟙_ C)).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ (𝟙_ C) X).inv (𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X (𝟙_ C)).hom (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) (CategoryTheory.MonoidalCategory.rightUnitor X).hom))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (CategoryTheory.MonoidalCategory.rightUnitor (𝟙_ C)).hom) (β_ (𝟙_ 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.whiskerLeft (𝟙_ C) (β_ (𝟙_ C) X).hom) (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) (CategoryTheory.MonoidalCategory.rightUnitor X).hom) = CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) (CategoryTheory.MonoidalCategory.leftUnitor X).hom

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

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

theorem CategoryTheory.braiding_tensorUnit_left_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C) ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ (𝟙_ C) X).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv h)

@[simp]

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

theorem CategoryTheory.leftUnitor_inv_braiding_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X (𝟙_ C) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv (CategoryTheory.CategoryStruct.comp (β_ (𝟙_ C) X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv h

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 (β_ (𝟙_ C) X).hom = (CategoryTheory.MonoidalCategory.rightUnitor X).inv

theorem CategoryTheory.rightUnitor_inv_braiding_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).inv (CategoryTheory.CategoryStruct.comp (β_ X (𝟙_ C)).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv h

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 (𝟙_ C)).hom = (CategoryTheory.MonoidalCategory.leftUnitor X).inv

theorem CategoryTheory.braiding_tensorUnit_right_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (𝟙_ C) X ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ X (𝟙_ C)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).inv h)

@[simp]

theorem CategoryTheory.braiding_tensorUnit_right (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) : (β_ X (𝟙_ C)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor X).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)

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

See .

• braiding : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X
• braiding_naturality_right : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (β_ X Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)
• braiding_naturality_left : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (β_ Y Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Z 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.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft 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.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y))
• symmetry : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)

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

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

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

@[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.toPrefunctor.obj X = X

@[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.toPrefunctor.map f = f

@[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 (𝟙_ C)

@[simp]

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

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.

Equations

• CategoryTheory.LaxBraidedFunctor.id C = let src := CategoryTheory.MonoidalFunctor.id C; CategoryTheory.LaxBraidedFunctor.mk src.toLaxMonoidalFunctor

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

Equations

• CategoryTheory.LaxBraidedFunctor.instInhabitedLaxBraidedFunctor C = { default := CategoryTheory.LaxBraidedFunctor.id C }

@[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.toPrefunctor.map F.ε)

@[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.toPrefunctor.obj X = G.toPrefunctor.obj (F.toPrefunctor.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.LaxBraidedFunctor.comp F G).toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.comp (G.toLaxMonoidalFunctor.μ (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) (G.toPrefunctor.map (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.toPrefunctor.map f = G.toPrefunctor.map (F.toPrefunctor.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.

Equations

• CategoryTheory.LaxBraidedFunctor.comp F G = let src := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor; CategoryTheory.LaxBraidedFunctor.mk src

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)

Equations

• CategoryTheory.LaxBraidedFunctor.categoryLaxBraidedFunctor = CategoryTheory.InducedCategory.category CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor

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), α.toNatTrans.app X = β.toNatTrans.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_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

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

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.

Equations

• CategoryTheory.LaxBraidedFunctor.mkIso i = CategoryTheory.Iso.mk i.hom i.inv

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₂)

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

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

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.

Equations

• CategoryTheory.symmetricCategoryOfFaithful F = CategoryTheory.SymmetricCategory.mk

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

Equations

• CategoryTheory.BraidedFunctor.toLaxBraidedFunctor C D F = CategoryTheory.LaxBraidedFunctor.mk F.toLaxMonoidalFunctor

@[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 (𝟙_ C)

@[simp]

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

@[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.toPrefunctor.obj X = X

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

Equations

• CategoryTheory.BraidedFunctor.id C = let src := CategoryTheory.MonoidalFunctor.id C; CategoryTheory.BraidedFunctor.mk src

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

Equations

• CategoryTheory.BraidedFunctor.instInhabitedBraidedFunctor C = { default := CategoryTheory.BraidedFunctor.id 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) : (CategoryTheory.BraidedFunctor.comp F G).toMonoidalFunctor.toLaxMonoidalFunctor.ε = CategoryTheory.CategoryStruct.comp G.ε (G.toPrefunctor.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.toPrefunctor.map f = G.toPrefunctor.map (F.toPrefunctor.map f)

@[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.toPrefunctor.obj X = G.toPrefunctor.obj (F.toPrefunctor.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) (X : C) (Y : C) : (CategoryTheory.BraidedFunctor.comp F G).toMonoidalFunctor.toLaxMonoidalFunctor.μ X Y = CategoryTheory.CategoryStruct.comp (G.toLaxMonoidalFunctor.μ (F.toPrefunctor.obj X) (F.toPrefunctor.obj Y)) (G.toPrefunctor.map (F.toLaxMonoidalFunctor.μ X Y))

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.

Equations

• CategoryTheory.BraidedFunctor.comp F G = let src := F.toMonoidalFunctor ⊗⋙ G.toMonoidalFunctor; CategoryTheory.BraidedFunctor.mk src

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)

Equations

• CategoryTheory.BraidedFunctor.categoryBraidedFunctor = CategoryTheory.InducedCategory.category CategoryTheory.BraidedFunctor.toMonoidalFunctor

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), α.toNatTrans.app X = β.toNatTrans.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_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

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

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.

Equations

• CategoryTheory.BraidedFunctor.mkIso i = CategoryTheory.Iso.mk i.hom i.inv

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

Equations

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

@[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_μ {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : (CategoryTheory.Discrete.braidedFunctor F).toMonoidalFunctor.toLaxMonoidalFunctor.μ X Y = CategoryTheory.Discrete.eqToHom (_ : F X.as * F Y.as = F (X.as * Y.as))

@[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.toPrefunctor.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.toPrefunctor.obj X).as = F X.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.

Equations

• CategoryTheory.Discrete.braidedFunctor F = let src := CategoryTheory.Discrete.monoidalFunctor F; CategoryTheory.BraidedFunctor.mk src

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.tensorObj X.1 X.2) (CategoryTheory.MonoidalCategory.tensorObj Y.1 Y.2) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X.1 Y.1) (CategoryTheory.MonoidalCategory.tensorObj X.2 Y.2)

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

Equations

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

theorem CategoryTheory.tensor_μ_natural_assoc (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₂) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj Y₁ V₁) (CategoryTheory.MonoidalCategory.tensorObj Y₂ V₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorHom g₁ g₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (Y₁, Y₂) (V₁, V₂)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (U₁, U₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.tensorHom f₁ g₁) (CategoryTheory.MonoidalCategory.tensorHom f₂ g₂)) h)

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_μ_natural_left_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ : C) (Z₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj Y₁ Z₁) (CategoryTheory.MonoidalCategory.tensorObj Y₂ Z₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (Z₁, Z₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.whiskerRight f₁ Z₁) (CategoryTheory.MonoidalCategory.whiskerRight f₂ Z₂)) h)

theorem CategoryTheory.tensor_μ_natural_left (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (Z₁ : C) (Z₂ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂) (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂)) (CategoryTheory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (Z₁, Z₂)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.whiskerRight f₁ Z₁) (CategoryTheory.MonoidalCategory.whiskerRight f₂ Z₂))

theorem CategoryTheory.tensor_μ_natural_right_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (Z₁ : C) (Z₂ : C) {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj Z₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj Z₂ Y₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂) (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (Z₁, Z₂) (Y₁, Y₂)) h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (Z₁, Z₂) (X₁, X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.whiskerLeft Z₁ f₁) (CategoryTheory.MonoidalCategory.whiskerLeft Z₂ f₂)) h)

theorem CategoryTheory.tensor_μ_natural_right (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (Z₁ : C) (Z₂ : C) {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂) (CategoryTheory.MonoidalCategory.tensorHom f₁ f₂)) (CategoryTheory.tensor_μ C (Z₁, Z₂) (Y₁, Y₂)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (Z₁, Z₂) (X₁, X₂)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.whiskerLeft Z₁ f₁) (CategoryTheory.MonoidalCategory.whiskerLeft Z₂ f₂))

theorem CategoryTheory.tensor_left_unitality_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (𝟙_ C, 𝟙_ C) (X₁, X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X₁).hom (CategoryTheory.MonoidalCategory.leftUnitor X₂).hom) h))

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.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (𝟙_ C, 𝟙_ C) (X₁, X₂)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X₁).hom (CategoryTheory.MonoidalCategory.leftUnitor X₂).hom))

theorem CategoryTheory.tensor_right_unitality_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (𝟙_ C, 𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X₁).hom (CategoryTheory.MonoidalCategory.rightUnitor X₂).hom) h))

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.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (𝟙_ C, 𝟙_ C)) (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X₁).hom (CategoryTheory.MonoidalCategory.rightUnitor X₂).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.whiskerRight (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (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.whiskerLeft (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₂)))

theorem CategoryTheory.tensor_associativity_assoc (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) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ (CategoryTheory.MonoidalCategory.tensorObj Y₁ Z₁)) (CategoryTheory.MonoidalCategory.tensorObj X₂ (CategoryTheory.MonoidalCategory.tensorObj Y₂ Z₂)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (CategoryTheory.MonoidalCategory.tensorObj Z₁ Z₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁, CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (Z₁, Z₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator X₁ Y₁ Z₁).hom (CategoryTheory.MonoidalCategory.associator X₂ Y₂ Z₂).hom) h)) = 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.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂))) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, X₂) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Z₁, CategoryTheory.MonoidalCategory.tensorObj Y₂ Z₂)) h))

@[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.toPrefunctor.obj X = CategoryTheory.MonoidalCategory.tensorObj X.1 X.2

@[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.tensorMonoidal C).toLaxMonoidalFunctor.μ X Y = CategoryTheory.tensor_μ C X Y

@[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.toPrefunctor.map f = CategoryTheory.MonoidalCategory.tensorHom f.1 f.2

@[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 (𝟙_ C)).inv

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.

Equations

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

theorem CategoryTheory.leftUnitor_monoidal_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.leftUnitor X₁).hom (CategoryTheory.MonoidalCategory.leftUnitor X₂).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom h))

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 (𝟙_ C, X₁) (𝟙_ C, X₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)) (CategoryTheory.MonoidalCategory.leftUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom)

theorem CategoryTheory.rightUnitor_monoidal_assoc (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj X₁ X₂ ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.rightUnitor X₁).hom (CategoryTheory.MonoidalCategory.rightUnitor X₂).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).hom h))

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₁, 𝟙_ C) (X₂, 𝟙_ C)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom) (CategoryTheory.MonoidalCategory.rightUnitor (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂)).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.whiskerRight (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (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.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.tensor_μ C (X₂, X₃) (Y₂, Y₃))))

theorem CategoryTheory.associator_monoidal_assoc (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) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂, X₃) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂, Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.tensor_μ C (X₁, X₂) (Y₁, Y₂)) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)).hom h)) = 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.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.tensor_μ C (X₂, X₃) (Y₂, Y₃))) h))