# 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

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.

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

Instances
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]

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₂)
• to_monoidal_functor :
• braided' : (∀ (X Y : C), . "obviously"

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

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

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} :
(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] :

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