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

  The braiding natural isomorphism.

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

  The first hexagon identity.

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

  The second hexagon identity.

@[simp]

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

@[simp]

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

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

The first hexagon identity.

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

The second hexagon identity.

@[simp]

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

@[simp]

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

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

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

def CategoryTheory.termβ_ : Lean.ParserDescr

The braiding natural isomorphism.

Equations

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

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

@[simp]

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

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[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 : C} {Z : C} (f : Y ⟶ Z✝) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj Z✝ X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (CategoryTheory.CategoryStruct.comp (β_ Z✝ X).inv h) = CategoryTheory.CategoryStruct.comp (β_ Y X).inv (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f X) 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 : C} {Z : C} (f : Y ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (β_ Z X).inv = CategoryTheory.CategoryStruct.comp (β_ Y X).inv (CategoryTheory.MonoidalCategory.whiskerRight f X)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

theorem CategoryTheory.BraidedCategory.yang_baxter' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X : C) (Y : C) (Z : C) : CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Y).hom Z) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).hom) (CategoryTheory.MonoidalCategory.whiskerRight (β_ Y Z).hom X)) = CategoryTheory.monoidalComp (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X Y) Z)) (CategoryTheory.monoidalComp (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategory.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.monoidalComp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y) (CategoryTheory.MonoidalCategory.whiskerLeft Z (β_ X Y).hom))) (CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.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 : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.associator X Y Z).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫ CategoryTheory.MonoidalCategory.associator Y X Z ≪≫ CategoryTheory.MonoidalCategory.whiskerLeftIso Y (β_ X Z) ≪≫ (CategoryTheory.MonoidalCategory.associator Y Z X).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ Y Z) X ≪≫ CategoryTheory.MonoidalCategory.associator Z Y X = CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫ (CategoryTheory.MonoidalCategory.associator X Z Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y ≪≫ CategoryTheory.MonoidalCategory.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 : C) (Y : C) (Z : C) : CategoryTheory.MonoidalCategory.associator X Y Z ≪≫ β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z) ≪≫ CategoryTheory.MonoidalCategory.associator Y Z X = CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Y) Z ≪≫ CategoryTheory.MonoidalCategory.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 : C) (Y : C) (Z : C) : (CategoryTheory.MonoidalCategory.associator X Y Z).symm ≪≫ β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z ≪≫ (CategoryTheory.MonoidalCategory.associator Z X Y).symm = CategoryTheory.MonoidalCategory.whiskerLeftIso X (β_ Y Z) ≪≫ (CategoryTheory.MonoidalCategory.associator X Z Y).symm ≪≫ CategoryTheory.MonoidalCategory.whiskerRightIso (β_ X Z) Y

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

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

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

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

def CategoryTheory.braidedCategoryOfFaithful {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] (F : CategoryTheory.MonoidalFunctor C D) [F.Faithful] [CategoryTheory.BraidedCategory D] (β : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X) (w : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (F.μ X Y) (F.map (β X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (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.MonoidalFunctor C D) [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.MonoidalCategory.associator (𝟙_ C) (𝟙_ C) X).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (𝟙_ C) (β_ X (𝟙_ C)).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (𝟙_ C) X (𝟙_ C)).inv (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor X).hom (𝟙_ C)))) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.MonoidalCategory.leftUnitor (𝟙_ C)).hom X) (β_ X (𝟙_ C)).inv

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

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

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

@[simp]

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

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

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

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

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

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

@[simp]

theorem CategoryTheory.SymmetricCategory.symmetry {C : Type u} : ∀ {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.SymmetricCategory C] (X Y : C), CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)

@[simp]

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

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

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

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

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (self.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)
• ε : 𝟙_ D ⟶ self.obj (𝟙_ C)
• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (self.obj X) (self.obj Y) ⟶ self.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
• μ_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X')) (self.μ Y X') = CategoryTheory.CategoryStruct.comp (self.μ X X') (self.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))
• μ_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f)) (self.μ X' Y) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.μ X Y) (self.obj Z)) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.μ Y Z)) (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.ε (self.obj X)) (CategoryTheory.CategoryStruct.comp (self.μ (𝟙_ C) X) (self.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) self.ε) (CategoryTheory.CategoryStruct.comp (self.μ X (𝟙_ C)) (self.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
• braided : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (self.μ X Y) (self.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (self.obj X) (self.obj Y)).hom (self.μ Y X)

theorem CategoryTheory.LaxBraidedFunctor.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] (self : CategoryTheory.LaxBraidedFunctor C D) (X : C) (Y : C) : CategoryTheory.CategoryStruct.comp (self.μ X Y) (self.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (self.obj X) (self.obj Y)).hom (self.μ Y X)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The identity lax braided monoidal functor.

Equations

• CategoryTheory.LaxBraidedFunctor.id C = { toLaxMonoidalFunctor := (CategoryTheory.MonoidalFunctor.id C).toLaxMonoidalFunctor, braided := ⋯ }

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

Equations

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The composition of lax braided monoidal functors.

Equations

• F.comp G = { toLaxMonoidalFunctor := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor, braided := ⋯ }

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.LaxBraidedFunctor.mkIso i = { hom := i.hom, inv := i.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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

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

• obj : C → D
• map : {X Y : C} → (X ⟶ Y) → (self.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)
• ε : 𝟙_ D ⟶ self.obj (𝟙_ C)
• μ : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (self.obj X) (self.obj Y) ⟶ self.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
• μ_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.map f) (self.obj X')) (self.μ Y X') = CategoryTheory.CategoryStruct.comp (self.μ X X') (self.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))
• μ_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X') (self.map f)) (self.μ X' Y) = CategoryTheory.CategoryStruct.comp (self.μ X' X) (self.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
• associativity : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (self.μ X Y) (self.obj Z)) (CategoryTheory.CategoryStruct.comp (self.μ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (self.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (self.obj X) (self.obj Y) (self.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) (self.μ Y Z)) (self.μ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
• left_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight self.ε (self.obj X)) (CategoryTheory.CategoryStruct.comp (self.μ (𝟙_ C) X) (self.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
• right_unitality : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (self.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (self.obj X) self.ε) (CategoryTheory.CategoryStruct.comp (self.μ X (𝟙_ C)) (self.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
• ε_isIso : CategoryTheory.IsIso self.ε
• μ_isIso : ∀ (X Y : C), CategoryTheory.IsIso (self.μ X Y)
• braided : ∀ (X Y : C), self.map (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (self.μ X Y)) (CategoryTheory.CategoryStruct.comp (β_ (self.obj X) (self.obj Y)).hom (self.μ Y X))

@[simp]

theorem CategoryTheory.BraidedFunctor.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] (self : CategoryTheory.BraidedFunctor C D) (X : C) (Y : C) : self.map (β_ X Y).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.inv (self.μ X Y)) (CategoryTheory.CategoryStruct.comp (β_ (self.obj X) (self.obj Y)).hom (self.μ Y X))

def CategoryTheory.symmetricCategoryOfFaithful {C : Type u_1} {D : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} D] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory D] [CategoryTheory.BraidedCategory C] [CategoryTheory.SymmetricCategory D] (F : CategoryTheory.BraidedFunctor C D) [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 ⋯

@[simp]

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

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

Turn a braided functor into a lax braided functor.

Equations

• CategoryTheory.BraidedFunctor.toLaxBraidedFunctor C D F = { toLaxMonoidalFunctor := F.toLaxMonoidalFunctor, braided := ⋯ }

@[simp]

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

@[simp]

theorem CategoryTheory.BraidedFunctor.id_μ (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ (x x_1 : C), (CategoryTheory.BraidedFunctor.id C).μ x x_1 = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj x x_1)

@[simp]

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

@[simp]

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

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

The identity braided monoidal functor.

Equations

• CategoryTheory.BraidedFunctor.id C = { toMonoidalFunctor := CategoryTheory.MonoidalFunctor.id C, braided := ⋯ }

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

Equations

• CategoryTheory.BraidedFunctor.instInhabited C = { default := CategoryTheory.BraidedFunctor.id C }

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

The composition of braided monoidal functors.

Equations

• CategoryTheory.BraidedFunctor.comp C D E F G = { toMonoidalFunctor := F.toMonoidalFunctor ⊗⋙ G.toMonoidalFunctor, braided := ⋯ }

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

Equations

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• CategoryTheory.BraidedFunctor.mkIso C D i = { hom := i.hom, inv := i.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }

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.

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

theorem CategoryTheory.Discrete.braidedFunctor_μ {M : Type u} [CommMonoid M] {N : Type u} [CommMonoid N] (F : M →* N) (X : CategoryTheory.Discrete M) (Y : CategoryTheory.Discrete M) : (CategoryTheory.Discrete.braidedFunctor F).μ X Y = CategoryTheory.Discrete.eqToHom ⋯

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

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

Equations

• CategoryTheory.Discrete.braidedFunctor F = { toMonoidalFunctor := CategoryTheory.Discrete.monoidalFunctor F, braided := ⋯ }

def CategoryTheory.tensor_μ {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂) ⟶ CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.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.

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

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

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

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

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

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

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

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

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

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

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

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

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

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

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

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

theorem CategoryTheory.associator_monoidal_assoc {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (X₁ : C) (X₂ : C) (X₃ : C) (Y₁ : C) (Y₂ : C) (Y₃ : C) {Z : C} (h : CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ (CategoryTheory.MonoidalCategory.tensorObj X₁ X₂) X₃ (CategoryTheory.MonoidalCategory.tensorObj Y₁ Y₂) Y₃) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.tensor_μ X₁ X₂ Y₁ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.MonoidalCategory.tensorObj X₂ Y₂) (CategoryTheory.MonoidalCategory.tensorObj X₃ Y₃)).hom h)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom (CategoryTheory.MonoidalCategory.associator X₁ X₂ X₃).hom (CategoryTheory.MonoidalCategory.associator Y₁ Y₂ Y₃).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ X₁ (CategoryTheory.MonoidalCategory.tensorObj X₂ X₃) Y₁ (CategoryTheory.MonoidalCategory.tensorObj Y₂ Y₃)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (CategoryTheory.MonoidalCategory.tensorObj X₁ Y₁) (CategoryTheory.tensor_μ 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 : C) (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 : Cᵒᵖ) (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 : C) (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 : Cᵒᵖ) (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 : C) (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 : Cᵒᵖ) (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 : C) (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 : Cᴹᵒᵖ) (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 : C) (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 : Cᴹᵒᵖ) (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 : C) (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 : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) : (β_ X Y).inv.unmop = (β_ Y.unmop X.unmop).inv

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopBraidedFunctor_ε_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : (CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).ε.unmop = CategoryTheory.CategoryStruct.id (𝟙_ C)

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopBraidedFunctor_map_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : C} (f : X ⟶ Y), ((CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).map f).unmop = f

@[simp]

theorem CategoryTheory.MonoidalOpposite.mopBraidedFunctor_obj_unmop (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (unmop : C) : ((CategoryTheory.MonoidalOpposite.mopBraidedFunctor C).obj unmop).unmop = unmop

@[simp]

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

def CategoryTheory.MonoidalOpposite.mopBraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedFunctor C Cᴹᵒᵖ

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

Equations

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

@[simp]

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

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopBraidedFunctor_map (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : ∀ {X Y : Cᴹᵒᵖ} (f : X ⟶ Y), (CategoryTheory.MonoidalOpposite.unmopBraidedFunctor C).map f = f.unmop

@[simp]

theorem CategoryTheory.MonoidalOpposite.unmopBraidedFunctor_obj (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] (self : Cᴹᵒᵖ) : (CategoryTheory.MonoidalOpposite.unmopBraidedFunctor C).obj self = self.unmop

@[simp]

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

def CategoryTheory.MonoidalOpposite.unmopBraidedFunctor (C : Type u₁) [CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.MonoidalCategory C] [CategoryTheory.BraidedCategory C] : CategoryTheory.BraidedFunctor Cᴹᵒᵖ C

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

Equations

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

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

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 = { toMonoidalFunctor := CategoryTheory.MonoidalFunctor.id C, braided := ⋯ }