# Documentation

Mathlib.CategoryTheory.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 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.
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_assoc {C : Type u} [self : ] {X : C} {X' : C} {Y : C} {Y' : C} (f : X Y) (g : X' Y') {Z : C} (h : ) :
=
theorem CategoryTheory.BraidedCategory.hexagon_reverse_assoc {C : Type u} [self : ] (X : C) (Y : C) (Z : C) {Z : C} :
theorem CategoryTheory.BraidedCategory.hexagon_forward_assoc {C : Type u} [self : ] (X : C) (Y : C) (Z : C) {Z : C} :
Instances For
def CategoryTheory.braidedCategoryOfFaithful {C : Type u_1} {D : Type u_2} [] [] (F : ) [CategoryTheory.Faithful F.toFunctor] (β : ) (w : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y) (F.map (β X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor Y X)) :

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

Instances For
noncomputable def CategoryTheory.braidedCategoryOfFullyFaithful {C : Type u_1} {D : Type u_2} [] [] (F : ) [CategoryTheory.Full F.toFunctor] [CategoryTheory.Faithful F.toFunctor] :

Pull back a braiding along a fully faithful monoidal functor.

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.
@[simp]
theorem CategoryTheory.braiding_leftUnitor (C : Type u₁) [] (X : C) :
@[simp]
theorem CategoryTheory.braiding_rightUnitor (C : Type u₁) [] (X : C) :
@[simp]
theorem CategoryTheory.leftUnitor_inv_braiding (C : Type u₁) [] (X : C) :
@[simp]
theorem CategoryTheory.rightUnitor_inv_braiding (C : Type u₁) [] (X : C) :
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_assoc {C : Type u} [self : ] (X : C) (Y : C) {Z : C} (h : ) :
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
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.id_map (C : Type u₁) [] :
∀ {X Y : C} (f : X Y), ().toLaxMonoidalFunctor.toFunctor.map f = f
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.id_obj (C : Type u₁) [] (X : C) :
().toLaxMonoidalFunctor.toFunctor.obj X = X
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.id_μ (C : Type u₁) [] (X : C) (Y : C) :
CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y =
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.id_ε (C : Type u₁) [] :
().toLaxMonoidalFunctor =

The identity lax braided monoidal functor.

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

The composition of lax braided monoidal functors.

Instances For
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_hom {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (i : F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor) :
= i.hom
@[simp]
theorem CategoryTheory.LaxBraidedFunctor.mkIso_inv {C : Type u₁} [] {D : Type u₂} [] {F : } {G : } (i : F.toLaxMonoidalFunctor G.toLaxMonoidalFunctor) :
= i.inv
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.

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
def CategoryTheory.symmetricCategoryOfFaithful {C : Type u_1} {D : Type u_2} [] [] (F : ) [CategoryTheory.Faithful F.toFunctor] :

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

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.

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

The identity braided monoidal functor.

Instances For
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_μ {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (X : C) (Y : C) :
CategoryTheory.LaxMonoidalFunctor.μ ().toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.CategoryStruct.comp (CategoryTheory.LaxMonoidalFunctor.μ G.toLaxMonoidalFunctor (F.obj X) (F.obj Y)) (G.map (CategoryTheory.LaxMonoidalFunctor.μ F.toLaxMonoidalFunctor X Y))
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_obj {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) (X : C) :
().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X = G.obj (F.obj X)
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_ε {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
().toMonoidalFunctor.toLaxMonoidalFunctor = CategoryTheory.CategoryStruct.comp G (G.map F)
@[simp]
theorem CategoryTheory.BraidedFunctor.comp_map {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :
∀ {X Y : C} (f : X Y), ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = G.map (F.map f)
def CategoryTheory.BraidedFunctor.comp {C : Type u₁} [] {D : Type u₂} [] {E : Type u₃} [] (F : ) (G : ) :

The composition of braided monoidal functors.

Instances For
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.

Instances For
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_ε {M : Type u} [] {N : Type u} [] (F : M →* N) :
().toMonoidalFunctor.toLaxMonoidalFunctor = CategoryTheory.Discrete.eqToHom (_ : 1 = F 1)
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_map {M : Type u} [] {N : Type u} [] (F : M →* N) :
∀ {X Y : } (f : X Y), ().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.map f = CategoryTheory.Discrete.eqToHom (_ : F X.as = F Y.as)
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_obj_as {M : Type u} [] {N : Type u} [] (F : M →* N) (X : ) :
(().toMonoidalFunctor.toLaxMonoidalFunctor.toFunctor.obj X).as = F X.as
@[simp]
theorem CategoryTheory.Discrete.braidedFunctor_μ {M : Type u} [] {N : Type u} [] (F : M →* N) (X : ) (Y : ) :
CategoryTheory.LaxMonoidalFunctor.μ ().toMonoidalFunctor.toLaxMonoidalFunctor X Y = CategoryTheory.Discrete.eqToHom (_ : F X.as * F Y.as = F (X.as * Y.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.

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.

Instances For
theorem CategoryTheory.tensor_μ_def₁ (C : Type u₁) [] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) :
theorem CategoryTheory.tensor_μ_def₂ (C : Type u₁) [] (X₁ : C) (X₂ : C) (Y₁ : C) (Y₂ : C) :
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_left_unitality (C : Type u₁) [] (X₁ : C) (X₂ : C) :
theorem CategoryTheory.tensor_right_unitality (C : Type u₁) [] (X₁ : C) (X₂ : C) :
@[simp]
theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_ε (C : Type u₁) [] :
().toLaxMonoidalFunctor =
@[simp]
theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_toFunctor_obj (C : Type u₁) [] (X : C × C) :
().toLaxMonoidalFunctor.toFunctor.obj X =
@[simp]
theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_toFunctor_map (C : Type u₁) [] {X : C × C} {Y : C × C} (f : X Y) :
().toLaxMonoidalFunctor.toFunctor.map f =
@[simp]
theorem CategoryTheory.tensorMonoidal_toLaxMonoidalFunctor_μ (C : Type u₁) [] (X : C × C) (Y : C × C) :
CategoryTheory.LaxMonoidalFunctor.μ ().toLaxMonoidalFunctor X Y =

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

Instances For
theorem CategoryTheory.leftUnitor_monoidal (C : Type u₁) [] (X₁ : C) (X₂ : C) :
theorem CategoryTheory.rightUnitor_monoidal (C : Type u₁) [] (X₁ : C) (X₂ : C) :