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)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- braiding : Π (X Y : C), X ⊗ Y ≅ Y ⊗ X
- braiding_naturality' : (∀ {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'), (f ⊗ g) ≫ (β_ Y Y').hom = (β_ X X').hom ≫ (g ⊗ f)) . "obviously"
- hexagon_forward' : (∀ (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)) . "obviously"
- hexagon_reverse' : (∀ (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)) . "obviously"
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.
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₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(X : C) :
@[simp]
theorem
category_theory.braiding_left_unitor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(X : C) :
theorem
category_theory.braiding_right_unitor_aux₁
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(X : C) :
@[simp]
theorem
category_theory.braiding_right_unitor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(X : C) :
@[class]
structure
category_theory.symmetric_category
(C : Type u)
[category_theory.category C]
[category_theory.monoidal_category C] :
Type (max u v)
- to_braided_category : category_theory.braided_category C
- symmetry' : (∀ (X Y : C), (β_ X Y).hom ≫ (β_ Y X).hom = 𝟙 (X ⊗ Y)) . "obviously"
A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.
See https://stacks.math.columbia.edu/tag/0FFW.
structure
category_theory.lax_braided_functor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
Type (max u₁ u₂ v₁ v₂)
- to_lax_monoidal_functor : category_theory.lax_monoidal_functor C D
- braided' : (∀ (X Y : C), c.to_lax_monoidal_functor.μ X Y ≫ c.to_lax_monoidal_functor.to_functor.map (β_ X Y).hom = (β_ (c.to_lax_monoidal_functor.to_functor.obj X) (c.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ c.to_lax_monoidal_functor.μ Y X) . "obviously"
A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.
@[simp]
theorem
category_theory.lax_braided_functor.id_to_lax_monoidal_functor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C] :
def
category_theory.lax_braided_functor.id
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C] :
The identity lax braided monoidal functor.
@[instance]
def
category_theory.lax_braided_functor.inhabited
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C] :
Equations
@[simp]
theorem
category_theory.lax_braided_functor.comp_to_lax_monoidal_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{E : Type u₃}
[category_theory.category E]
[category_theory.monoidal_category E]
[category_theory.braided_category E]
(F : category_theory.lax_braided_functor C D)
(G : category_theory.lax_braided_functor D E) :
def
category_theory.lax_braided_functor.comp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{E : Type u₃}
[category_theory.category E]
[category_theory.monoidal_category E]
[category_theory.braided_category E]
(F : category_theory.lax_braided_functor C D)
(G : category_theory.lax_braided_functor D E) :
The composition of lax braided monoidal functors.
Equations
- F.comp G = {to_lax_monoidal_functor := {to_functor := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).to_functor, ε := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).ε, μ := (F.to_lax_monoidal_functor ⊗⋙ G.to_lax_monoidal_functor).μ, μ_natural' := _, associativity' := _, left_unitality' := _, right_unitality' := _}, braided' := _}
@[instance]
def
category_theory.lax_braided_functor.category_lax_braided_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
@[simp]
theorem
category_theory.lax_braided_functor.comp_to_nat_trans
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G H : category_theory.lax_braided_functor C D}
{α : F ⟶ G}
{β : G ⟶ H} :
(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans
@[simp]
theorem
category_theory.lax_braided_functor.mk_iso_inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G : category_theory.lax_braided_functor C D}
(i : F.to_lax_monoidal_functor ≅ G.to_lax_monoidal_functor) :
def
category_theory.lax_braided_functor.mk_iso
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G : category_theory.lax_braided_functor C D}
(i : F.to_lax_monoidal_functor ≅ G.to_lax_monoidal_functor) :
F ≅ G
Interpret a natural isomorphism of the underlyling lax monoidal functors as an isomorphism of the lax braided monoidal functors.
Equations
- category_theory.lax_braided_functor.mk_iso i = {hom := i.hom, inv := i.inv, hom_inv_id' := _, inv_hom_id' := _}
@[simp]
theorem
category_theory.lax_braided_functor.mk_iso_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G : category_theory.lax_braided_functor C D}
(i : F.to_lax_monoidal_functor ≅ G.to_lax_monoidal_functor) :
structure
category_theory.braided_functor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
Type (max u₁ u₂ v₁ v₂)
- to_monoidal_functor : category_theory.monoidal_functor C D
- braided' : (∀ (X Y : C), c.to_monoidal_functor.to_lax_monoidal_functor.to_functor.map (β_ X Y).hom = category_theory.is_iso.inv (c.to_monoidal_functor.to_lax_monoidal_functor.μ X Y) ≫ (β_ (c.to_monoidal_functor.to_lax_monoidal_functor.to_functor.obj X) (c.to_monoidal_functor.to_lax_monoidal_functor.to_functor.obj Y)).hom ≫ c.to_monoidal_functor.to_lax_monoidal_functor.μ Y X) . "obviously"
A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.
@[simp]
theorem
category_theory.braided_functor.to_lax_braided_functor_to_lax_monoidal_functor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(F : category_theory.braided_functor C D) :
def
category_theory.braided_functor.to_lax_braided_functor
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
(D : Type u₂)
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
(F : category_theory.braided_functor C D) :
Turn a braided functor into a lax braided functor.
Equations
def
category_theory.braided_functor.id
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C] :
The identity braided monoidal functor.
Equations
@[instance]
def
category_theory.braided_functor.inhabited
(C : Type u₁)
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C] :
Equations
@[simp]
theorem
category_theory.braided_functor.comp_to_monoidal_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{E : Type u₃}
[category_theory.category E]
[category_theory.monoidal_category E]
[category_theory.braided_category E]
(F : category_theory.braided_functor C D)
(G : category_theory.braided_functor D E) :
def
category_theory.braided_functor.comp
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{E : Type u₃}
[category_theory.category E]
[category_theory.monoidal_category E]
[category_theory.braided_category E]
(F : category_theory.braided_functor C D)
(G : category_theory.braided_functor D E) :
The composition of braided monoidal functors.
Equations
- F.comp G = {to_monoidal_functor := {to_lax_monoidal_functor := (F.to_monoidal_functor ⊗⋙ G.to_monoidal_functor).to_lax_monoidal_functor, ε_is_iso := (F.to_monoidal_functor ⊗⋙ G.to_monoidal_functor).ε_is_iso, μ_is_iso := (F.to_monoidal_functor ⊗⋙ G.to_monoidal_functor).μ_is_iso}, braided' := _}
@[instance]
def
category_theory.braided_functor.category_braided_functor
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D] :
@[simp]
theorem
category_theory.braided_functor.comp_to_nat_trans
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G H : category_theory.braided_functor C D}
{α : F ⟶ G}
{β : G ⟶ H} :
(α ≫ β).to_nat_trans = α.to_nat_trans ≫ β.to_nat_trans
@[simp]
theorem
category_theory.braided_functor.mk_iso_hom
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G : category_theory.braided_functor C D}
(i : F.to_monoidal_functor ≅ G.to_monoidal_functor) :
@[simp]
theorem
category_theory.braided_functor.mk_iso_inv
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G : category_theory.braided_functor C D}
(i : F.to_monoidal_functor ≅ G.to_monoidal_functor) :
def
category_theory.braided_functor.mk_iso
{C : Type u₁}
[category_theory.category C]
[category_theory.monoidal_category C]
[category_theory.braided_category C]
{D : Type u₂}
[category_theory.category D]
[category_theory.monoidal_category D]
[category_theory.braided_category D]
{F G : category_theory.braided_functor C 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
- category_theory.braided_functor.mk_iso i = {hom := i.hom, inv := i.inv, hom_inv_id' := _, inv_hom_id' := _}
@[instance]
Equations
- category_theory.comm_monoid_discrete M = id _inst_10
@[instance]
Equations
- category_theory.category_theory.braided_category M = {braiding := λ (X Y : category_theory.discrete M), category_theory.eq_to_iso _, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}
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
- category_theory.discrete.braided_functor F = {to_monoidal_functor := {to_lax_monoidal_functor := (category_theory.discrete.monoidal_functor F).to_lax_monoidal_functor, ε_is_iso := (category_theory.discrete.monoidal_functor F).ε_is_iso, μ_is_iso := (category_theory.discrete.monoidal_functor F).μ_is_iso}, braided' := _}
@[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) :