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.
@[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.
Instances
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.
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] :
The composition of braided monoidal functors.
Equations
- F.comp G = {to_monoidal_functor := {to_lax_monoidal_functor := (F.to_monoidal_functor.comp G.to_monoidal_functor).to_lax_monoidal_functor, ε_is_iso := (F.to_monoidal_functor.comp G.to_monoidal_functor).ε_is_iso, μ_is_iso := (F.to_monoidal_functor.comp G.to_monoidal_functor).μ_is_iso}, braided' := _}