# mathlibdocumentation

category_theory.monoidal.braided

# 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 braided_monoidal_category another typeclass, but then have symmetric_monoidal_category extend this. The rationale is that we are not carrying any additional data, just requiring a property.

## Future work #

• Construct the Drinfeld center of a monoidal category as a braided monoidal category.
• Say something about pseudo-natural transformations.
@[class]
structure category_theory.braided_category (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 category_theory.braided_category.braiding_naturality {C : Type u} [self : category_theory.braided_category C] {X X' Y Y' : C} (f : X Y) (g : X' Y') :
(f g) (β_ Y Y').hom = (β_ X X').hom (g f)
@[simp]
theorem category_theory.braided_category.braiding_naturality_assoc {C : Type u} [self : category_theory.braided_category C] {X X' Y Y' : C} (f : X Y) (g : X' Y') {X'_1 : C} (f' : Y' Y X'_1) :
(f g) (β_ Y Y').hom f' = (β_ X X').hom (g f) f'
theorem category_theory.braided_category.hexagon_forward {C : Type u} [self : category_theory.braided_category C] (X Y Z : C) :
(α_ X Y Z).hom (β_ X (Y Z)).hom (α_ Y Z X).hom = ((β_ X Y).hom 𝟙 Z) (α_ Y X Z).hom (𝟙 Y (β_ X Z).hom)
theorem category_theory.braided_category.hexagon_reverse {C : Type u} [self : category_theory.braided_category C] (X Y Z : C) :
(α_ X Y Z).inv (β_ (X Y) Z).hom (α_ Z X Y).inv = (𝟙 X (β_ Y Z).hom) (α_ X Z Y).inv ((β_ X Z).hom 𝟙 Y)

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 category_theory.braiding_left_unitor_aux₁ (C : Type u₁) (X : C) :
(α_ (𝟙_ C) (𝟙_ C) X).hom (𝟙 (𝟙_ C) (β_ X (𝟙_ C)).inv) (α_ (𝟙_ C) X (𝟙_ C)).inv ((λ_ X).hom 𝟙 (𝟙_ C)) = ((λ_ (𝟙_ C)).hom 𝟙 X) (β_ X (𝟙_ C)).inv
theorem category_theory.braiding_left_unitor_aux₂ (C : Type u₁) (X : C) :
((β_ X (𝟙_ C)).hom 𝟙 (𝟙_ C)) ((λ_ X).hom 𝟙 (𝟙_ C)) = ((ρ_ X).hom 𝟙 (𝟙_ C))
@[simp]
theorem category_theory.braiding_left_unitor (C : Type u₁) (X : C) :
(β_ X (𝟙_ C)).hom (λ_ X).hom = (ρ_ X).hom
theorem category_theory.braiding_right_unitor_aux₁ (C : Type u₁) (X : C) :
(α_ X (𝟙_ C) (𝟙_ C)).inv ((β_ (𝟙_ C) X).inv 𝟙 (𝟙_ C)) (α_ (𝟙_ C) X (𝟙_ C)).hom (𝟙 (𝟙_ C) (ρ_ X).hom) = (𝟙 X (ρ_ (𝟙_ C)).hom) (β_ (𝟙_ C) X).inv
theorem category_theory.braiding_right_unitor_aux₂ (C : Type u₁) (X : C) :
(𝟙 (𝟙_ C) (β_ (𝟙_ C) X).hom) (𝟙 (𝟙_ C) (ρ_ X).hom) = (𝟙 (𝟙_ C) (λ_ X).hom)
@[simp]
theorem category_theory.braiding_right_unitor (C : Type u₁) (X : C) :
(β_ (𝟙_ C) X).hom (ρ_ X).hom = (λ_ X).hom
@[class]
structure category_theory.symmetric_category (C : Type u)  :
Type (max u v)

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

Instances
@[simp]
theorem category_theory.symmetric_category.symmetry {C : Type u} [self : category_theory.symmetric_category C] (X Y : C) :
(β_ X Y).hom (β_ Y X).hom = 𝟙 (X Y)
@[simp]
theorem category_theory.symmetric_category.symmetry_assoc {C : Type u} [self : category_theory.symmetric_category C] (X Y : C) {X' : C} (f' : X Y X') :
(β_ X Y).hom (β_ Y X).hom f' = f'
structure category_theory.lax_braided_functor (C : Type u₁) (D : Type u₂)  :
Type (max u₁ u₂ v₁ v₂)

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

@[simp]

The identity lax braided monoidal functor.

Equations
@[instance]
Equations
@[simp]
def category_theory.lax_braided_functor.comp {C : Type u₁} {D : Type u₂} {E : Type u₃}  :

The composition of lax braided monoidal functors.

Equations
@[instance]
Equations
@[simp]
theorem category_theory.lax_braided_functor.comp_to_nat_trans {C : Type u₁} {D : Type u₂} {F G H : D} {α : F G} {β : G H} :
β).to_nat_trans =
@[simp]
theorem category_theory.lax_braided_functor.mk_iso_inv {C : Type u₁} {D : Type u₂} {F G : D}  :
def category_theory.lax_braided_functor.mk_iso {C : Type u₁} {D : Type u₂} {F G : D}  :
F G

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

Equations
@[simp]
theorem category_theory.lax_braided_functor.mk_iso_hom {C : Type u₁} {D : Type u₂} {F G : D}  :
structure category_theory.braided_functor (C : Type u₁) (D : Type u₂)  :
Type (max u₁ u₂ v₁ v₂)

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

@[simp]
theorem category_theory.braided_functor.braided {C : Type u₁} {D : Type u₂} (self : D) (X Y : C) :
@[simp]

Turn a braided functor into a lax braided functor.

Equations

The identity braided monoidal functor.

Equations
@[simp]
@[instance]
Equations
@[simp]
theorem category_theory.braided_functor.comp_to_monoidal_functor {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : D) (G : E) :
def category_theory.braided_functor.comp {C : Type u₁} {D : Type u₂} {E : Type u₃} (F : D) (G : E) :

The composition of braided monoidal functors.

Equations
@[instance]
Equations
@[simp]
theorem category_theory.braided_functor.comp_to_nat_trans {C : Type u₁} {D : Type u₂} {F G H : D} {α : F G} {β : G H} :
β).to_nat_trans =
@[simp]
theorem category_theory.braided_functor.mk_iso_hom {C : Type u₁} {D : Type u₂} {F G : D} (i : F.to_monoidal_functor G.to_monoidal_functor) :
@[simp]
theorem category_theory.braided_functor.mk_iso_inv {C : Type u₁} {D : Type u₂} {F G : D} (i : F.to_monoidal_functor G.to_monoidal_functor) :
def category_theory.braided_functor.mk_iso {C : Type u₁} {D : Type u₂} {F G : D} (i : F.to_monoidal_functor G.to_monoidal_functor) :
F G

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

Equations
@[instance]
Equations
• = id _inst_10
@[instance]
Equations
def category_theory.discrete.braided_functor {M : Type u} [comm_monoid M] {N : Type u} [comm_monoid N] (F : M →* N) :

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

Equations
@[simp]
theorem category_theory.discrete.braided_functor_to_monoidal_functor {M : Type u} [comm_monoid M] {N : Type u} [comm_monoid N] (F : M →* N) :