# 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 of this typeclass
Instances of other typeclasses for category_theory.braided_category
• category_theory.braided_category.has_sizeof_inst
@[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)
theorem category_theory.braided_category.hexagon_reverse_assoc {C : Type u} [self : category_theory.braided_category C] (X Y Z : C) {X' : C} (f' : (Z X) Y X') :
(α_ X Y Z).inv (β_ (X Y) Z).hom (α_ Z X Y).inv f' = (𝟙 X (β_ Y Z).hom) (α_ X Z Y).inv ((β_ X Z).hom 𝟙 Y) f'
theorem category_theory.braided_category.hexagon_forward_assoc {C : Type u} [self : category_theory.braided_category C] (X Y Z : C) {X' : C} (f' : Y Z X X') :
(α_ X Y Z).hom (β_ X (Y Z)).hom (α_ Y Z X).hom f' = ((β_ X Y).hom 𝟙 Z) (α_ Y X Z).hom (𝟙 Y (β_ X Z).hom) f'
def category_theory.braided_category_of_faithful {C : Type u_1} {D : Type u_2} (F : D) (β : Π (X Y : C), X Y Y X) (w : ∀ (X Y : C), Y F.to_lax_monoidal_functor.to_functor.map (β X Y).hom = .hom X) :

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

Equations

Pull back a braiding along a fully faithful monoidal functor.

Equations

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
@[simp]
theorem category_theory.left_unitor_inv_braiding (C : Type u₁) (X : C) :
(λ_ X).inv (β_ (𝟙_ C) X).hom = (ρ_ X).inv
@[simp]
theorem category_theory.right_unitor_inv_braiding (C : Type u₁) (X : C) :
(ρ_ X).inv (β_ X (𝟙_ C)).hom = (λ_ X).inv
@[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 of this typeclass
Instances of other typeclasses for category_theory.symmetric_category
• category_theory.symmetric_category.has_sizeof_inst
@[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.

Instances for category_theory.lax_braided_functor
@[simp]

The identity lax braided monoidal functor.

Equations
@[protected, 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
@[protected, 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.

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

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

Equations
@[simp]

Turn a braided functor into a lax braided functor.

Equations

The identity braided monoidal functor.

Equations
@[simp]
@[protected, 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
@[protected, 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
@[protected, 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) :
def category_theory.tensor_μ (C : Type u₁) (X Y : C × C) :

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

Equations
theorem category_theory.tensor_μ_def₁ (C : Type u₁) (X₁ X₂ Y₁ Y₂ : C) :
(X₁, X₂) (Y₁, Y₂) (α_ X₁ Y₁ (X₂ Y₂)).hom (𝟙 X₁ (α_ Y₁ X₂ Y₂).inv) = (α_ X₁ X₂ (Y₁ Y₂)).hom (𝟙 X₁ (α_ X₂ Y₁ Y₂).inv) (𝟙 X₁ (β_ X₂ Y₁).hom 𝟙 Y₂)
theorem category_theory.tensor_μ_def₂ (C : Type u₁) (X₁ X₂ Y₁ Y₂ : C) :
(𝟙 X₁ (α_ X₂ Y₁ Y₂).hom) (α_ X₁ X₂ (Y₁ Y₂)).inv (X₁, X₂) (Y₁, Y₂) = (𝟙 X₁ (β_ X₂ Y₁).hom 𝟙 Y₂) (𝟙 X₁ (α_ Y₁ X₂ Y₂).hom) (α_ X₁ Y₁ (X₂ Y₂)).inv
theorem category_theory.tensor_μ_natural (C : Type u₁) {X₁ X₂ Y₁ Y₂ U₁ U₂ V₁ V₂ : C} (f₁ : X₁ Y₁) (f₂ : X₂ Y₂) (g₁ : U₁ V₁) (g₂ : U₂ V₂) :
((f₁ f₂) g₁ g₂) (Y₁, Y₂) (V₁, V₂) = (X₁, X₂) (U₁, U₂) ((f₁ g₁) f₂ g₂)
theorem category_theory.tensor_left_unitality (C : Type u₁) (X₁ X₂ : C) :
(λ_ (X₁ X₂)).hom = ((λ_ (𝟙_ C)).inv 𝟙 (X₁ X₂)) (𝟙_ C _inst_2, 𝟙_ C _inst_2) (X₁, X₂) ((λ_ X₁).hom (λ_ X₂).hom)
theorem category_theory.tensor_right_unitality (C : Type u₁) (X₁ X₂ : C) :
(ρ_ (X₁ X₂)).hom = (𝟙 (X₁ X₂) (λ_ (𝟙_ C)).inv) (X₁, X₂) (𝟙_ C _inst_2, 𝟙_ C _inst_2) ((ρ_ X₁).hom (ρ_ X₂).hom)
theorem category_theory.tensor_associativity_aux (C : Type u₁) (W X Y Z : C) :
((β_ W X).hom 𝟙 (Y Z)) (α_ X W (Y Z)).hom (𝟙 X (α_ W Y Z).inv) (𝟙 X (β_ (W Y) Z).hom) (𝟙 X (α_ Z W Y).inv) = (𝟙 (W X) (β_ Y Z).hom) (α_ (W X) Z Y).inv ((α_ W X Z).hom 𝟙 Y) ((β_ W (X Z)).hom 𝟙 Y) ((α_ X Z W).hom 𝟙 Y) (α_ X (Z W) Y).hom
theorem category_theory.tensor_associativity (C : Type u₁) (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
(X₁, X₂) (Y₁, Y₂) 𝟙 (Z₁ Z₂)) (X₁ Y₁, X₂ Y₂) (Z₁, Z₂) ((α_ X₁ Y₁ Z₁).hom (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ X₂) (Y₁ Y₂) (Z₁ Z₂)).hom (𝟙 (X₁ X₂) (Y₁, Y₂) (Z₁, Z₂)) (X₁, X₂) (Y₁ Z₁, Y₂ Z₂)
@[simp]
theorem category_theory.tensor_monoidal_to_lax_monoidal_functor_μ (C : Type u₁) (X Y : C × C) :

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

Equations
@[simp]
@[simp]
theorem category_theory.left_unitor_monoidal (C : Type u₁) (X₁ X₂ : C) :
(λ_ X₁).hom (λ_ X₂).hom = (𝟙_ C _inst_2, X₁) (𝟙_ C _inst_2, X₂) ((λ_ (𝟙_ C)).hom 𝟙 (X₁ X₂)) (λ_ (X₁ X₂)).hom
theorem category_theory.right_unitor_monoidal (C : Type u₁) (X₁ X₂ : C) :
(ρ_ X₁).hom (ρ_ X₂).hom = (X₁, 𝟙_ C _inst_2) (X₂, 𝟙_ C _inst_2) (𝟙 (X₁ X₂) (λ_ (𝟙_ C)).hom) (ρ_ (X₁ X₂)).hom
theorem category_theory.associator_monoidal_aux (C : Type u₁) (W X Y Z : C) :
(𝟙 W (β_ X (Y Z)).hom) (𝟙 W (α_ Y Z X).hom) (α_ W Y (Z X)).inv ((β_ W Y).hom 𝟙 (Z X)) = (α_ W X (Y Z)).inv (α_ (W X) Y Z).inv ((β_ (W X) Y).hom 𝟙 Z) ((α_ Y W X).inv 𝟙 Z) (α_ (Y W) X Z).hom (𝟙 (Y W) (β_ X Z).hom)
theorem category_theory.associator_monoidal (C : Type u₁) (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
(X₁ X₂, X₃) (Y₁ Y₂, Y₃) (X₁, X₂) (Y₁, Y₂) 𝟙 (X₃ Y₃)) (α_ (X₁ Y₁) (X₂ Y₂) (X₃ Y₃)).hom = ((α_ X₁ X₂ X₃).hom (α_ Y₁ Y₂ Y₃).hom) (X₁, X₂ X₃) (Y₁, Y₂ Y₃) (𝟙 (X₁ Y₁) (X₂, X₃) (Y₂, Y₃))