# 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 #

class CategoryTheory.BraidedCategory (C : Type u) :
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.

Instances
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_naturality_right {C : Type u} [self : ] (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_naturality_left {C : Type u} [self : ] {X : C} {Y : C} (f : X Y) (Z : C) :

The first hexagon identity.

The second hexagon identity.

@[simp]
theorem CategoryTheory.BraidedCategory.braiding_naturality_left_assoc {C : Type u} [self : ] {X : C} {Y : C} (f : X Y) (Z : C) {Z : C} (h : ) :
=
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_naturality_right_assoc {C : Type u} [self : ] (X : C) {Y : C} {Z : C} (f : Y Z✝) {Z : C} (h : ) :

The braiding natural isomorphism.

Equations
Instances For
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_naturality_assoc {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (f : X Y) (g : X' Y') {Z : C} (h : ) :
=
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_naturality {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (f : X Y) (g : X' Y') :
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_right_assoc {C : Type u} (X : C) {Y : C} {Z : C} (f : Y Z✝) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_right {C : Type u} (X : C) {Y : C} {Z : C} (f : Y Z) :
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_left_assoc {C : Type u} {X : C} {Y : C} (f : X Y) (Z : C) {Z : C} (h : ) :
=
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_left {C : Type u} {X : C} {Y : C} (f : X Y) (Z : C) :
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_inv_naturality_assoc {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (f : X Y) (g : X' Y') {Z : C} (h : ) :
=
@[simp]
theorem CategoryTheory.BraidedCategory.braiding_inv_naturality {C : Type u} {X : C} {X' : C} {Y : C} {Y' : C} (f : X Y) (g : X' Y') :
theorem CategoryTheory.BraidedCategory.yang_baxter_iso {C : Type u} (X : C) (Y : C) (Z : C) :
theorem CategoryTheory.BraidedCategory.hexagon_forward_iso {C : Type u} (X : C) (Y : C) (Z : C) :
theorem CategoryTheory.BraidedCategory.hexagon_reverse_iso {C : Type u} (X : C) (Y : C) (Z : C) :
.symm ≪≫ ≪≫ .symm = ≪≫
def CategoryTheory.braidedCategoryOfFaithful {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Faithful] (β : ) (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)) :

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

Equations
• = { braiding := β, braiding_naturality_right := , braiding_naturality_left := , hexagon_forward := , hexagon_reverse := }
Instances For
noncomputable def CategoryTheory.braidedCategoryOfFullyFaithful {C : Type u_1} {D : Type u_2} [] [] (F : ) [F.Full] [F.Faithful] :

Pull back a braiding along a fully faithful monoidal functor.

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

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_assoc (C : Type u₁) [] (X : C) {Z : C} (h : X Z) :
theorem CategoryTheory.braiding_rightUnitor_assoc (C : Type u₁) [] (X : C) {Z : C} (h : X Z) :
theorem CategoryTheory.braiding_tensorUnit_left_assoc (C : Type u₁) [] (X : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.braiding_tensorUnit_left (C : Type u₁) [] (X : C) :
(β_ (𝟙_ C) X).hom =
theorem CategoryTheory.braiding_inv_tensorUnit_left_assoc (C : Type u₁) [] (X : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.braiding_inv_tensorUnit_left (C : Type u₁) [] (X : C) :
(β_ (𝟙_ C) X).inv =
theorem CategoryTheory.leftUnitor_inv_braiding_assoc (C : Type u₁) [] (X : C) {Z : C} (h : ) :
theorem CategoryTheory.rightUnitor_inv_braiding_assoc (C : Type u₁) [] (X : C) {Z : C} (h : ) :
theorem CategoryTheory.braiding_tensorUnit_right_assoc (C : Type u₁) [] (X : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.braiding_tensorUnit_right (C : Type u₁) [] (X : C) :
(β_ X (𝟙_ C)).hom =
theorem CategoryTheory.braiding_inv_tensorUnit_right_assoc (C : Type u₁) [] (X : C) {Z : C} (h : ) :
@[simp]
theorem CategoryTheory.braiding_inv_tensorUnit_right (C : Type u₁) [] (X : C) :
(β_ X (𝟙_ C)).inv =
class CategoryTheory.SymmetricCategory (C : Type u) extends :
Type (max u v)

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

Instances
@[simp]
theorem CategoryTheory.SymmetricCategory.symmetry {C : Type u} [self : ] (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.SymmetricCategory.symmetry_assoc {C : Type u} [self : ] (X : C) (Y : C) {Z : C} (h : ) :
theorem CategoryTheory.SymmetricCategory.braiding_swap_eq_inv_braiding {C : Type u₁} [] (X : C) (Y : C) :
(β_ Y X).hom = (β_ X Y).inv
structure CategoryTheory.LaxBraidedFunctor (C : Type u₁) [] (D : Type u₂) [] extends :
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.

Instances For
theorem CategoryTheory.LaxBraidedFunctor.braided {C : Type u₁} [] {D : Type u₂} [] (self : ) (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₁) [] (X : C) (Y : C) :
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.id_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), f = f
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.id_obj (C : Type u₁) [] (X : C) :
X = X
@[simp]

The identity lax braided monoidal functor.

Equations
• = let __src := ; { toLaxMonoidalFunctor := __src.toLaxMonoidalFunctor, braided := }
Instances For
Equations
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.comp_μ {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (X : C) (Y : C) :
(F.comp G) X Y = CategoryTheory.CategoryStruct.comp (G (F.obj X) (F.obj Y)) (G.map (F X Y))
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.comp_ε {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
(F.comp G) = CategoryTheory.CategoryStruct.comp G (G.map F)
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.comp_map {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
∀ {X Y : C} (f : X Y), (F.comp G).map f = G.map (F.map f)
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.comp_obj {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (X : C) :
(F.comp G).obj X = G.obj (F.obj X)

The composition of lax braided monoidal functors.

Equations
• F.comp G = let __src := F.toLaxMonoidalFunctor ⊗⋙ G.toLaxMonoidalFunctor; { toLaxMonoidalFunctor := __src, braided := }
Instances For
Equations
theorem CategoryTheory.LaxBraidedFunctor.ext' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {α : F G} {β : F G} (w : ∀ (X : C), α.app X = β.app X) :
α = β
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.comp_toNatTrans {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } {α : F G} {β : G H} :
.toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mkIso_inv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (i : F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor) :
= i.inv
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mkIso_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (i : F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor) :
= i.hom
def CategoryTheory.LaxBraidedFunctor.mkIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (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
• = { hom := i.hom, inv := i.inv, hom_inv_id := , inv_hom_id := }
Instances For
structure CategoryTheory.BraidedFunctor (C : Type u₁) [] (D : Type u₂) [] extends :
Type (max (max (max u₁ u₂) v₁) v₂)

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

Instances For
@[simp]
theorem CategoryTheory.BraidedFunctor.braided {C : Type u₁} [] {D : Type u₂} [] (self : ) (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} [] [] (F : ) [F.Faithful] :

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

Equations
Instances For
@[simp]
theorem CategoryTheory.BraidedFunctor.toLaxBraidedFunctor_toLaxMonoidalFunctor (C : Type u₁) [] (D : Type u₂) [] (F : ) :
.toLaxMonoidalFunctor = F.toLaxMonoidalFunctor

Turn a braided functor into a lax braided functor.

Equations
• = { toLaxMonoidalFunctor := F.toLaxMonoidalFunctor, braided := }
Instances For
@[simp]
theorem CategoryTheory.BraidedFunctor.id_obj (C : Type u₁) [] (X : C) :
.obj X = X
@[simp]
theorem CategoryTheory.BraidedFunctor.id_μ (C : Type u₁) [] (X : C) (Y : C) :
@[simp]
@[simp]
theorem CategoryTheory.BraidedFunctor.id_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), .map f = f

The identity braided monoidal functor.

Equations
• = let __src := ; { toMonoidalFunctor := __src, braided := }
Instances For
Equations
• = { default := }
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_μ {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (X : C) (Y : C) :
(F.comp 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₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
∀ {X Y : C} (f : X Y), (F.comp G).map f = G.map (F.map f)
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_obj {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (X : C) :
(F.comp G).obj X = G.obj (F.obj X)
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_ε {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
(F.comp G) = CategoryTheory.CategoryStruct.comp G (G.map F)
def CategoryTheory.BraidedFunctor.comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :

The composition of braided monoidal functors.

Equations
• F.comp G = let __src := F.toMonoidalFunctor ⊗⋙ G.toMonoidalFunctor; { toMonoidalFunctor := __src, braided := }
Instances For
instance CategoryTheory.BraidedFunctor.categoryBraidedFunctor {C : Type u₁} [] {D : Type u₂} [] :
Equations
theorem CategoryTheory.BraidedFunctor.ext' {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {α : F G} {β : F G} (w : ∀ (X : C), α.app X = β.app X) :
α = β
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_toNatTrans {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } {H : } {α : F G} {β : G H} :
.toNatTrans = CategoryTheory.CategoryStruct.comp α.toNatTrans β.toNatTrans
@[simp]
theorem CategoryTheory.BraidedFunctor.mkIso_inv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (i : F.toMonoidalFunctor G.toMonoidalFunctor) :
= i.inv
@[simp]
theorem CategoryTheory.BraidedFunctor.mkIso_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (i : F.toMonoidalFunctor G.toMonoidalFunctor) :
= i.hom
def CategoryTheory.BraidedFunctor.mkIso {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (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
• = { hom := i.hom, inv := i.inv, hom_inv_id := , inv_hom_id := }
Instances For
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_map {M : Type u} [] {N : Type u} [] (F : M →* N) :
∀ {X Y : } (f : X Y),
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_ε {M : Type u} [] {N : Type u} [] (F : M →* N) :
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_μ {M : Type u} [] {N : Type u} [] (F : M →* N) (X : ) (Y : ) :
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_obj_as {M : Type u} [] {N : Type u} [] (F : M →* N) (X : ) :
().as = F X.as
def CategoryTheory.Discrete.braidedFunctor {M : Type u} [] {N : Type u} [] (F : M →* N) :

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

Equations
• = let __src := ; { toMonoidalFunctor := __src, braided := }
Instances For
def CategoryTheory.tensor_μ (C : Type u₁) [] (X : C × C) (Y : C × C) :

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

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem CategoryTheory.tensor_μ_natural_assoc (C : Type u₁) [] {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 : ) :
theorem CategoryTheory.tensor_μ_natural (C : Type u₁) [] {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₂) :
theorem CategoryTheory.tensor_μ_natural_left_assoc (C : Type u₁) [] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (Z₁ : C) (Z₂ : C) {Z : C} (h : ) :
theorem CategoryTheory.tensor_μ_natural_left (C : Type u₁) [] {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (Z₁ : C) (Z₂ : C) :
theorem CategoryTheory.tensor_μ_natural_right_assoc (C : Type u₁) [] (Z₁ : C) (Z₂ : C) {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) {Z : C} (h : ) :
theorem CategoryTheory.tensor_μ_natural_right (C : Type u₁) [] (Z₁ : C) (Z₂ : C) {X₁ : C} {X₂ : C} {Y₁ : C} {Y₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) :
theorem CategoryTheory.tensor_left_unitality_assoc (C : Type u₁) [] (X₁ : C) (X₂ : C) {Z : C} (h : ) :
theorem CategoryTheory.tensor_right_unitality_assoc (C : Type u₁) [] (X₁ : C) (X₂ : C) {Z : C} (h : ) :
@[simp]
@[simp]
@[simp]
theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_toFunctor_map (C : Type u₁) [] {X : C × C} {Y : C × C} (f : X Y) :
.map f =
@[simp]
theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_μ (C : Type u₁) [] (X : C × C) (Y : C × C) :
X Y =

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.
Instances For
theorem CategoryTheory.leftUnitor_monoidal_assoc (C : Type u₁) [] (X₁ : C) (X₂ : C) {Z : C} (h : ) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂)) ()
theorem CategoryTheory.leftUnitor_monoidal (C : Type u₁) [] (X₁ : C) (X₂ : C) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (𝟙_ C, X₁) (𝟙_ C, X₂)) ()
theorem CategoryTheory.rightUnitor_monoidal_assoc (C : Type u₁) [] (X₁ : C) (X₂ : C) {Z : C} (h : ) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C)) ()
theorem CategoryTheory.rightUnitor_monoidal (C : Type u₁) [] (X₁ : C) (X₂ : C) :
= CategoryTheory.CategoryStruct.comp (CategoryTheory.tensor_μ C (X₁, 𝟙_ C) (X₂, 𝟙_ C)) ()
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.op_braiding (C : Type u₁) [] (X : C) (Y : C) :
(β_ X Y).op = β_ () ()
@[simp]
theorem CategoryTheory.unop_braiding (C : Type u₁) [] (X : Cᵒᵖ) (Y : Cᵒᵖ) :
(β_ X Y).unop = β_ () ()
@[simp]
theorem CategoryTheory.op_hom_braiding (C : Type u₁) [] (X : C) (Y : C) :
(β_ X Y).hom.op = (β_ () ()).hom
@[simp]
theorem CategoryTheory.unop_hom_braiding (C : Type u₁) [] (X : Cᵒᵖ) (Y : Cᵒᵖ) :
(β_ X Y).hom.unop = (β_ () ()).hom
@[simp]
theorem CategoryTheory.op_inv_braiding (C : Type u₁) [] (X : C) (Y : C) :
(β_ X Y).inv.op = (β_ () ()).inv
@[simp]
theorem CategoryTheory.unop_inv_braiding (C : Type u₁) [] (X : Cᵒᵖ) (Y : Cᵒᵖ) :
(β_ X Y).inv.unop = (β_ () ()).inv
Equations
• One or more equations did not get rendered due to their size.
@[simp]
theorem CategoryTheory.MonoidalOpposite.mop_braiding (C : Type u₁) [] (X : C) (Y : C) :
(β_ X Y).mop = β_ { unmop := Y } { unmop := X }
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmop_braiding (C : Type u₁) [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) :
(β_ X Y).unmop = β_ Y.unmop X.unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.mop_hom_braiding (C : Type u₁) [] (X : C) (Y : C) :
(β_ X Y).hom.mop = (β_ { unmop := Y } { unmop := X }).hom
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmop_hom_braiding (C : Type u₁) [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) :
(β_ X Y).hom.unmop = (β_ Y.unmop X.unmop).hom
@[simp]
theorem CategoryTheory.MonoidalOpposite.mop_inv_braiding (C : Type u₁) [] (X : C) (Y : C) :
(β_ X Y).inv.mop = (β_ { unmop := Y } { unmop := X }).inv
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmop_inv_braiding (C : Type u₁) [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) :
(β_ X Y).inv.unmop = (β_ Y.unmop X.unmop).inv
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopBraidedFunctor_obj_unmop (C : Type u₁) [] (unmop : C) :
( unmop).unmop = unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopBraidedFunctor_μ_unmop (C : Type u₁) [] (X : C) (Y : C) :
.unmop = (β_ Y X).hom
@[simp]
theorem CategoryTheory.MonoidalOpposite.mopBraidedFunctor_map_unmop (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), .unmop = f
@[simp]

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.
Instances For
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopBraidedFunctor_obj (C : Type u₁) [] (self : Cᴹᵒᵖ) :
= self.unmop
@[simp]
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopBraidedFunctor_map (C : Type u₁) [] :
∀ {X Y : Cᴹᵒᵖ} (f : X Y), = f.unmop
@[simp]
theorem CategoryTheory.MonoidalOpposite.unmopBraidedFunctor_μ (C : Type u₁) [] (X : Cᴹᵒᵖ) (Y : Cᴹᵒᵖ) :
= (β_ X.unmop Y.unmop).hom

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.
Instances For
@[reducible, inline]

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
• = { braiding := fun (X Y : C) => (β_ Y X).symm, braiding_naturality_right := , braiding_naturality_left := , hexagon_forward := , hexagon_reverse := }
Instances For
theorem CategoryTheory.SymmetricCategory.reverseBraiding_eq (C : Type u₁) [] :
= CategoryTheory.SymmetricCategory.toBraidedCategory

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

Equations
• = { toMonoidalFunctor := , braided := }
Instances For