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.

References

• [Pavel Etingof, Shlomo Gelaki, Dmitri Nikshych, Victor Ostrik, Tensor categories][egno15]

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.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X

  The braiding natural isomorphism.

• braiding_naturality_right (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_ X Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
• braiding_naturality_left {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (β_ Y Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
• hexagon_forward (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom))

  The first hexagon identity.

• hexagon_reverse (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y))

  The second hexagon identity.

@[simp]

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

@[simp]

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

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

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_ Z X).inv = CategoryTheory.CategoryStruct.comp (β_ Y X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)

@[simp]

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

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (β_ Z Y).inv = CategoryTheory.CategoryStruct.comp (β_ Z X).inv (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)

@[simp]

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

@[simp]

theorem CategoryTheory.BraidedCategory.braiding_inv_naturality {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g) (β_ Y' Y).inv = CategoryTheory.CategoryStruct.comp (β_ X' X).inv (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)

@[simp]

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

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

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

theorem CategoryTheory.BraidedCategory.yang_baxter' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : C) : CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y Z).hom X)) = CategoryTheory.monoidalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)) (CategoryTheory.monoidalComp (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (β_ X Y).hom))) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Z Y) X)))

theorem CategoryTheory.BraidedCategory.yang_baxter_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫ CategoryTheory.MonoidalCategoryStruct.associator Y X Z ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z) ≪≫ (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ Y Z) X ≪≫ CategoryTheory.MonoidalCategoryStruct.associator Z Y X = CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫ (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y ≪≫ CategoryTheory.MonoidalCategoryStruct.associator Z X Y ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Z (β_ X Y)

theorem CategoryTheory.BraidedCategory.hexagon_forward_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : C) : CategoryTheory.MonoidalCategoryStruct.associator X Y Z ≪≫ β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z) ≪≫ CategoryTheory.MonoidalCategoryStruct.associator Y Z X = CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫ CategoryTheory.MonoidalCategoryStruct.associator Y X Z ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z)

theorem CategoryTheory.BraidedCategory.hexagon_reverse_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y Z : C) : (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).symm ≪≫ β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z ≪≫ (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).symm = CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫ (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y

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

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

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

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

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.Functor C D) [F.Monoidal] [F.Faithful] [CategoryTheory.BraidedCategory D] (β : (X Y : C) → CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) (w : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F 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 = { braiding := β, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }

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.Functor C D) [F.Monoidal] [F.Full] [F.Faithful] [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.MonoidalCategoryStruct.associator (𝟙_ C) (𝟙_ C) X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (𝟙_ C) (β_ X (𝟙_ C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (𝟙_ C) X (𝟙_ C)).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom (𝟙_ C)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.whiskerRight (β_ X (𝟙_ C)).hom (𝟙_ C)) (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom (𝟙_ C)) = CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom (𝟙_ C)

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.MonoidalCategoryStruct.leftUnitor X).hom = (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom

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.MonoidalCategoryStruct.leftUnitor X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom h

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

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.MonoidalCategoryStruct.rightUnitor X).hom = (CategoryTheory.MonoidalCategoryStruct.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.MonoidalCategoryStruct.rightUnitor X).hom h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom 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.MonoidalCategoryStruct.leftUnitor X).hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv

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.MonoidalCategoryStruct.tensorObj X (𝟙_ C) ⟶ Z) : CategoryTheory.CategoryStruct.comp (β_ (𝟙_ C) X).hom h = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv h)

@[simp]

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

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

@[simp]

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

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

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

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

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

• braiding (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y ≅ CategoryTheory.MonoidalCategoryStruct.tensorObj Y X
• braiding_naturality_right (X : C) {Y Z : C} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) (β_ X Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X)
• braiding_naturality_left {X Y : C} (f : X ⟶ Y) (Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z) (β_ Y Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z f)
• hexagon_forward (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom))
• hexagon_reverse (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y))
• symmetry (X Y : C) : CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)

@[simp]

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

theorem CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] (X Y : C) : (β_ Y X).hom = (β_ X Y).inv

class CategoryTheory.Functor.LaxBraided {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.Functor C D) extends F.LaxMonoidal : Type (max u₁ v₂)

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

• ε' : 𝟙_ D ⟶ F.obj (𝟙_ C)
• μ' (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
• μ'_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryTheory.Functor.LaxMonoidal.μ' Y X') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X X') (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
• μ'_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryTheory.Functor.LaxMonoidal.μ' X' Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X' X) (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
• associativity' (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ' X Y) (F.obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ' Y Z)) (CategoryTheory.Functor.LaxMonoidal.μ' X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
• left_unitality' (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε' (F.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))
• right_unitality' (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) CategoryTheory.Functor.LaxMonoidal.ε') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))
• braided (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)

theorem CategoryTheory.Functor.LaxBraided.braided_assoc {C : Type u₁} {inst✝ : CategoryTheory.Category.{v₁, u₁} C} {inst✝¹ : CategoryTheory.MonoidalCategory C} {inst✝² : CategoryTheory.BraidedCategory C} {D : Type u₂} {inst✝³ : CategoryTheory.Category.{v₂, u₂} D} {inst✝⁴ : CategoryTheory.MonoidalCategory D} {inst✝⁵ : CategoryTheory.BraidedCategory D} {F : CategoryTheory.Functor C D} [self : F.LaxBraided] (X Y : C) {Z : D} (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (CategoryTheory.CategoryStruct.comp (F.map (β_ X Y).hom) h) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y X) h)

instance CategoryTheory.Functor.LaxBraided.id {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.Functor.id C).LaxBraided

Equations

• CategoryTheory.Functor.LaxBraided.id = CategoryTheory.Functor.LaxBraided.mk ⋯

instance CategoryTheory.Functor.LaxBraided.instComp {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.Functor C D) (G : CategoryTheory.Functor D E) [F.LaxBraided] [G.LaxBraided] : (F.comp G).LaxBraided

Equations

• CategoryTheory.Functor.LaxBraided.instComp F G = CategoryTheory.Functor.LaxBraided.mk ⋯

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.Functor C D : Type (max (max (max u₁ u₂) v₁) v₂)

Bundled version of lax braided functors.

• obj : C → D
• map {X Y : C} : (X ⟶ Y) → (self.obj X ⟶ self.obj Y)
• map_id (X : C) : self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
• map_comp {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z) : self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
• laxBraided : self.LaxBraided

def CategoryTheory.LaxBraidedFunctor.of {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.Functor C D) [F.LaxBraided] : CategoryTheory.LaxBraidedFunctor C D

Constructor for LaxBraidedFunctor C D.

Equations

• CategoryTheory.LaxBraidedFunctor.of F = { toFunctor := F, laxBraided := inferInstance }

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.of_toFunctor {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.Functor C D) [F.LaxBraided] : (CategoryTheory.LaxBraidedFunctor.of F).toFunctor = F

def CategoryTheory.LaxBraidedFunctor.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.LaxBraidedFunctor C D) : CategoryTheory.LaxMonoidalFunctor C D

The lax monoidal functor induced by a lax braided functor.

Equations

• F.toLaxMonoidalFunctor = { toFunctor := F.toFunctor, laxMonoidal := inferInstance }

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor_toFunctor {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) : F.toLaxMonoidalFunctor.toFunctor = F.toFunctor

instance CategoryTheory.LaxBraidedFunctor.instCategory {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.instCategory = CategoryTheory.InducedCategory.category CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.id_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) : (CategoryTheory.CategoryStruct.id F).hom = CategoryTheory.CategoryStruct.id F.toLaxMonoidalFunctor.toFunctor

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.comp_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 G H : CategoryTheory.LaxBraidedFunctor C D} (α : F ⟶ G) (β : G ⟶ H) : (CategoryTheory.CategoryStruct.comp α β).hom = CategoryTheory.CategoryStruct.comp α.hom β.hom

theorem CategoryTheory.LaxBraidedFunctor.comp_hom_assoc {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 G H : CategoryTheory.LaxBraidedFunctor C D} (α : F ⟶ G) (β : G ⟶ H) {Z : CategoryTheory.Functor C D} (h : H.toLaxMonoidalFunctor.toFunctor ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp α β).hom h = CategoryTheory.CategoryStruct.comp α.hom (CategoryTheory.CategoryStruct.comp β.hom h)

theorem CategoryTheory.LaxBraidedFunctor.hom_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 G : CategoryTheory.LaxBraidedFunctor C D} {α β : F ⟶ G} (h : α.hom = β.hom) : α = β

def CategoryTheory.LaxBraidedFunctor.homMk {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 G : CategoryTheory.LaxBraidedFunctor C D} (f : F.toFunctor ⟶ G.toFunctor) [CategoryTheory.NatTrans.IsMonoidal f] : F ⟶ G

Constructor for morphisms in the category LaxBraiededFunctor C D.

Equations

• CategoryTheory.LaxBraidedFunctor.homMk f = { hom := f, isMonoidal := ⋯ }

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.homMk_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 G : CategoryTheory.LaxBraidedFunctor C D} (f : F.toFunctor ⟶ G.toFunctor) [CategoryTheory.NatTrans.IsMonoidal f] : (CategoryTheory.LaxBraidedFunctor.homMk f).hom = f

def CategoryTheory.LaxBraidedFunctor.isoMk {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 G : CategoryTheory.LaxBraidedFunctor C D} (e : F.toFunctor ≅ G.toFunctor) [CategoryTheory.NatTrans.IsMonoidal e.hom] : F ≅ G

Constructor for isomorphisms in the category LaxBraidedFunctor C D.

Equations

• CategoryTheory.LaxBraidedFunctor.isoMk e = { hom := CategoryTheory.LaxBraidedFunctor.homMk e.hom, inv := CategoryTheory.LaxBraidedFunctor.homMk e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.isoMk_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 G : CategoryTheory.LaxBraidedFunctor C D} (e : F.toFunctor ≅ G.toFunctor) [CategoryTheory.NatTrans.IsMonoidal e.hom] : (CategoryTheory.LaxBraidedFunctor.isoMk e).hom = CategoryTheory.LaxBraidedFunctor.homMk e.hom

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.isoMk_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 G : CategoryTheory.LaxBraidedFunctor C D} (e : F.toFunctor ≅ G.toFunctor) [CategoryTheory.NatTrans.IsMonoidal e.hom] : (CategoryTheory.LaxBraidedFunctor.isoMk e).inv = CategoryTheory.LaxBraidedFunctor.homMk e.inv

def CategoryTheory.LaxBraidedFunctor.forget {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.Functor (CategoryTheory.LaxBraidedFunctor C D) (CategoryTheory.LaxMonoidalFunctor C D)

The forgetful functor from lax braided functors to lax monoidal functors.

Equations

• CategoryTheory.LaxBraidedFunctor.forget = CategoryTheory.inducedFunctor CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.forget_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] {X✝ Y✝ : CategoryTheory.InducedCategory (CategoryTheory.LaxMonoidalFunctor C D) CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor} (f : X✝ ⟶ Y✝) : CategoryTheory.LaxBraidedFunctor.forget.map f = f

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.forget_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] (F : CategoryTheory.LaxBraidedFunctor C D) : CategoryTheory.LaxBraidedFunctor.forget.obj F = F.toLaxMonoidalFunctor

def CategoryTheory.LaxBraidedFunctor.fullyFaithfulForget {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.LaxBraidedFunctor.forget.FullyFaithful

The forgetful functor from lax braided functors to lax monoidal functors is fully faithful.

Equations

• CategoryTheory.LaxBraidedFunctor.fullyFaithfulForget = CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor

def CategoryTheory.LaxBraidedFunctor.isoOfComponents {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 G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by aesop_cat) (unit : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by aesop_cat) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y) (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by aesop_cat) : F ≅ G

Constructor for isomorphisms between lax braided functors.

Equations

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

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.isoOfComponents_hom_hom_app {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 G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by aesop_cat) (unit : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by aesop_cat) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y) (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by aesop_cat) (X : C) : (CategoryTheory.LaxBraidedFunctor.isoOfComponents e ⋯ unit tensor).hom.hom.app X = (e X).hom

@[simp]

theorem CategoryTheory.LaxBraidedFunctor.isoOfComponents_inv_hom_app {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 G : CategoryTheory.LaxBraidedFunctor C D} (e : (X : C) → F.obj X ≅ G.obj X) (naturality : ∀ {X Y : C} (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (F.map f) (e Y).hom = CategoryTheory.CategoryStruct.comp (e X).hom (G.map f) := by aesop_cat) (unit : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F.toFunctor) (e (𝟙_ C)).hom = CategoryTheory.Functor.LaxMonoidal.ε G.toFunctor := by aesop_cat) (tensor : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F.toFunctor X Y) (e (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (e X).hom (e Y).hom) (CategoryTheory.Functor.LaxMonoidal.μ G.toFunctor X Y) := by aesop_cat) (X : C) : (CategoryTheory.LaxBraidedFunctor.isoOfComponents e ⋯ unit tensor).inv.hom.app X = (e X).inv

class CategoryTheory.Functor.Braided {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.Functor C D) extends F.Monoidal, F.LaxBraided : Type (max u₁ v₂)

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

• ε' : 𝟙_ D ⟶ F.obj (𝟙_ C)
• μ' (X Y : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
• μ'_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) (CategoryTheory.Functor.LaxMonoidal.μ' Y X') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X X') (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))
• μ'_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) (CategoryTheory.Functor.LaxMonoidal.μ' X' Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X' X) (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f))
• associativity' (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ' X Y) (F.obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ' Y Z)) (CategoryTheory.Functor.LaxMonoidal.μ' X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
• left_unitality' (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε' (F.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).hom))
• right_unitality' (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) CategoryTheory.Functor.LaxMonoidal.ε') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom))
• η' : F.obj (𝟙_ C) ⟶ 𝟙_ D
• δ' (X Y : C) : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y)
• δ'_natural_left {X Y : C} (f : X ⟶ Y) (X' : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X X') (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X')) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X')) (CategoryTheory.Functor.OplaxMonoidal.δ' Y X')
• δ'_natural_right {X Y : C} (X' : C) (f : X ⟶ Y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X' X) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X') (F.map f)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X' f)) (CategoryTheory.Functor.OplaxMonoidal.δ' X' Y)
• oplax_associativity' (X Y Z : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ' X Y) (F.obj Z)) (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ' Y Z)))
• oplax_left_unitality' (X : C) : (CategoryTheory.MonoidalCategoryStruct.leftUnitor (F.obj X)).inv = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' (𝟙_ C) X) (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.Functor.OplaxMonoidal.η' (F.obj X)))
• oplax_right_unitality' (X : C) : (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X (𝟙_ C)) (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) CategoryTheory.Functor.OplaxMonoidal.η'))
• ε_η : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.ε F) (CategoryTheory.Functor.OplaxMonoidal.η F) = CategoryTheory.CategoryStruct.id (𝟙_ D)
• η_ε : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) (CategoryTheory.Functor.LaxMonoidal.ε F) = CategoryTheory.CategoryStruct.id (F.obj (𝟙_ C))
• μ_δ (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj X) (F.obj Y))
• δ_μ (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (CategoryTheory.Functor.LaxMonoidal.μ F X Y) = CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
• braided (X Y : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)

@[simp]

theorem CategoryTheory.Functor.map_braiding {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.Functor C D) (X Y : C) [F.Braided] : F.map (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X))

theorem CategoryTheory.Functor.map_braiding_assoc {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.Functor C D) (X Y : C) [F.Braided] {Z : D} (h : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj Y X) ⟶ Z) : CategoryTheory.CategoryStruct.comp (F.map (β_ X Y).hom) h = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F Y X) h))

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.Functor C D) [F.Braided] [F.Faithful] : 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 ⋯

instance CategoryTheory.Functor.Braided.instId {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.Functor.id C).Braided

Equations

• CategoryTheory.Functor.Braided.instId = CategoryTheory.Functor.Braided.mk ⋯

instance CategoryTheory.Functor.Braided.instComp {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.Functor C D) (G : CategoryTheory.Functor D E) [F.Braided] [G.Braided] : (F.comp G).Braided

Equations

• CategoryTheory.Functor.Braided.instComp F G = CategoryTheory.Functor.Braided.mk ⋯

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

Equations

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

instance CategoryTheory.Discrete.monoidalFunctorBraided {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) : (CategoryTheory.Discrete.monoidalFunctor F).Braided

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

Equations

• CategoryTheory.Discrete.monoidalFunctorBraided F = CategoryTheory.Functor.Braided.mk ⋯

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

Swap the second and third objects in (X₁ ⊗ X₂) ⊗ (Y₁ ⊗ Y₂). This is used to strength 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.

def CategoryTheory.MonoidalCategory.tensorδ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)

The inverse of tensorμ.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorμ_tensorδ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂))

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorμ_tensorδ_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂) h) = h

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorδ_tensorμ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂) (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂))

@[simp]

theorem CategoryTheory.MonoidalCategory.tensorδ_tensorμ_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorδ X₁ X₂ Y₁ Y₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) h) = h

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

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

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

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

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

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

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

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

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

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

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

theorem CategoryTheory.MonoidalCategory.tensor_associativity_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Z₁)) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₁ Z₂) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom) h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ Z₁ Z₂)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Z₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂)) h))

instance CategoryTheory.MonoidalCategory.tensorMonoidal {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.MonoidalCategory.tensor C).Monoidal

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.MonoidalCategory.tensor C) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).inv

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.MonoidalCategory.tensor C) = (CategoryTheory.MonoidalCategoryStruct.leftUnitor (𝟙_ C)).hom

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C × C) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.MonoidalCategory.tensor C) X Y = CategoryTheory.MonoidalCategory.tensorμ X.1 X.2 Y.1 Y.2

@[simp]

theorem CategoryTheory.MonoidalCategory.tensor_δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C × C) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalCategory.tensor C) X Y = CategoryTheory.MonoidalCategory.tensorδ X.1 X.2 Y.1 Y.2

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

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

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

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

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

theorem CategoryTheory.MonoidalCategory.associator_monoidal_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂) X₃ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂) Y₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategoryStruct.tensorObj X₃ Y₃)).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategoryStruct.associator Y₁ Y₂ Y₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ X₃) Y₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorμ X₂ X₃ Y₂ Y₃)) h))

instance CategoryTheory.instBraidedCategoryOpposite {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory Cᵒᵖ

Equations

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

@[simp]

theorem CategoryTheory.op_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).op = β_ (Opposite.op Y) (Opposite.op X)

@[simp]

theorem CategoryTheory.unop_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᵒᵖ) : (β_ X Y).unop = β_ (Opposite.unop Y) (Opposite.unop X)

@[simp]

theorem CategoryTheory.op_hom_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).hom.op = (β_ (Opposite.op Y) (Opposite.op X)).hom

@[simp]

theorem CategoryTheory.unop_hom_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᵒᵖ) : (β_ X Y).hom.unop = (β_ (Opposite.unop Y) (Opposite.unop X)).hom

@[simp]

theorem CategoryTheory.op_inv_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).inv.op = (β_ (Opposite.op Y) (Opposite.op X)).inv

@[simp]

theorem CategoryTheory.unop_inv_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᵒᵖ) : (β_ X Y).inv.unop = (β_ (Opposite.unop Y) (Opposite.unop X)).inv

instance CategoryTheory.MonoidalOpposite.instBraiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory Cᴹᵒᵖ

Equations

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

@[simp]

theorem CategoryTheory.MonoidalOpposite.mop_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).mop = β_ { unmop := Y } { unmop := X }

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmop_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ) : (β_ X Y).unmop = β_ Y.unmop X.unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.mop_hom_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).hom.mop = (β_ { unmop := Y } { unmop := X }).hom

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmop_hom_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ) : (β_ X Y).hom.unmop = (β_ Y.unmop X.unmop).hom

@[simp]

theorem CategoryTheory.MonoidalOpposite.mop_inv_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : (β_ X Y).inv.mop = (β_ { unmop := Y } { unmop := X }).inv

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmop_inv_braiding {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ) : (β_ X Y).inv.unmop = (β_ Y.unmop X.unmop).inv

instance CategoryTheory.MonoidalOpposite.instMonoidalMopFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.mopFunctor C).Monoidal

Equations

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

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopFunctor_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.mopFunctor C) = CategoryTheory.CategoryStruct.id (𝟙_ Cᴹᵒᵖ)

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopFunctor_η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.mopFunctor C) = CategoryTheory.CategoryStruct.id ((CategoryTheory.mopFunctor C).obj (𝟙_ C))

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopFunctor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.mopFunctor C) X Y = (β_ { unmop := X } { unmop := Y }).hom

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopFunctor_δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : C) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.mopFunctor C) X Y = (β_ { unmop := X } { unmop := Y }).inv

instance CategoryTheory.MonoidalOpposite.instMonoidalUnmopFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.unmopFunctor C).Monoidal

Equations

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

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopFunctor_ε {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.unmopFunctor C) = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopFunctor_η {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.Functor.OplaxMonoidal.η (CategoryTheory.unmopFunctor C) = CategoryTheory.CategoryStruct.id ((CategoryTheory.unmopFunctor C).obj (𝟙_ Cᴹᵒᵖ))

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopFunctor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ) : CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.unmopFunctor C) X Y = (β_ X.unmop Y.unmop).hom

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopFunctor_δ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X Y : Cᴹᵒᵖ) : CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.unmopFunctor C) X Y = (β_ X.unmop Y.unmop).inv

instance CategoryTheory.MonoidalOpposite.instBraidedMopFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.mopFunctor C).Braided

The identity functor on C, viewed as a functor from C to its monoidal opposite, upgraded to a braided functor.

Equations

• CategoryTheory.MonoidalOpposite.instBraidedMopFunctor = CategoryTheory.Functor.Braided.mk ⋯

instance CategoryTheory.MonoidalOpposite.instBraidedUnmopFunctor {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.unmopFunctor C).Braided

The identity functor on C, viewed as a functor from the monoidal opposite of C to C, upgraded to a braided functor.

Equations

• CategoryTheory.MonoidalOpposite.instBraidedUnmopFunctor = CategoryTheory.Functor.Braided.mk ⋯

@[reducible, inline]

abbrev CategoryTheory.reverseBraiding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedCategory C

The braided monoidal category obtained from C by replacing its braiding β_ X Y : X ⊗ Y ≅ Y ⊗ X with the inverse (β_ Y X)⁻¹ : X ⊗ Y ≅ Y ⊗ X. This corresponds to the automorphism of the braid group swapping over-crossings and under-crossings.

Equations

• CategoryTheory.reverseBraiding C = { braiding := fun (X Y : C) => (β_ Y X).symm, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }

theorem CategoryTheory.SymmetricCategory.reverseBraiding_eq (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [i : CategoryTheory.SymmetricCategory C] : CategoryTheory.reverseBraiding C = CategoryTheory.SymmetricCategory.toBraidedCategory

def CategoryTheory.SymmetricCategory.equivReverseBraiding (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.SymmetricCategory C] : (CategoryTheory.Functor.id C).Braided

The identity functor from C to C, where the codomain is given the reversed braiding, upgraded to a braided functor.

Equations

• CategoryTheory.SymmetricCategory.equivReverseBraiding C = CategoryTheory.Functor.Braided.mk ⋯