mathlib documentation

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

@[class]

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} [category_theory.category C] [category_theory.monoidal_category C] [c : 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} [category_theory.category C] [category_theory.monoidal_category C] [c : 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'

We now establish how the braiding interacts with the unitors.

I couldn't find a detailed proof in print, but this is discussed in:

@[class]

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

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

Instances
@[simp]

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

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

Equations

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

Equations