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.
References #
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.
- braiding : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X
The braiding natural isomorphism.
- braiding_naturality_right : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (β_ X Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)
- braiding_naturality_left : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (β_ Y Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Z f)
- hexagon_forward : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).hom))
The first hexagon identity.
- hexagon_reverse : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y))
The second hexagon identity.
Instances
The first hexagon identity.
The second hexagon identity.
The braiding natural isomorphism.
Equations
- CategoryTheory.termβ_ = Lean.ParserDescr.node `CategoryTheory.termβ_ 1024 (Lean.ParserDescr.symbol "β_")
Instances For
Verifying the axioms for a braiding by checking that the candidate braiding is sent to a braiding by a faithful monoidal functor.
Equations
- CategoryTheory.braidedCategoryOfFaithful F β w = { braiding := β, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }
Instances For
Pull back a braiding along a fully faithful monoidal functor.
Equations
- One or more equations did not get rendered due to their size.
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.
A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.
See https://stacks.math.columbia.edu/tag/0FFW.
- braiding : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj X Y ≅ CategoryTheory.MonoidalCategory.tensorObj Y X
- braiding_naturality_right : ∀ (X : C) {Y Z : C} (f : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X f) (β_ X Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Y).hom (CategoryTheory.MonoidalCategory.whiskerRight f X)
- braiding_naturality_left : ∀ {X Y : C} (f : X ⟶ Y) (Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight f Z) (β_ Y Z).hom = CategoryTheory.CategoryStruct.comp (β_ X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Z f)
- hexagon_forward : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom (CategoryTheory.CategoryStruct.comp (β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom (CategoryTheory.MonoidalCategory.associator Y Z X).hom) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Y).hom Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).hom))
- hexagon_reverse : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom (CategoryTheory.MonoidalCategory.associator Z X Y).inv) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (β_ Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y))
- symmetry : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (β_ X Y).hom (β_ Y X).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj X Y)
Instances
A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.
- μ' : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
- μ'_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj X')) (CategoryTheory.Functor.LaxMonoidal.μ' Y X') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X X') (F.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))
- μ'_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X') (F.map f)) (CategoryTheory.Functor.LaxMonoidal.μ' X' Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X' X) (F.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
- associativity' : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ' X Y) (F.obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ' Y Z)) (CategoryTheory.Functor.LaxMonoidal.μ' X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
- left_unitality' : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε' (F.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
- right_unitality' : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) CategoryTheory.Functor.LaxMonoidal.ε') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
- braided : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)
Instances
Equations
- CategoryTheory.Functor.LaxBraided.id = CategoryTheory.Functor.LaxBraided.mk ⋯
Bundled version of lax braided functors.
- obj : C → D
- map_id : ∀ (X : C), self.map (CategoryTheory.CategoryStruct.id X) = CategoryTheory.CategoryStruct.id (self.obj X)
- map_comp : ∀ {X Y Z : C} (f : X ⟶ Y) (g : Y ⟶ Z), self.map (CategoryTheory.CategoryStruct.comp f g) = CategoryTheory.CategoryStruct.comp (self.map f) (self.map g)
- laxBraided : self.LaxBraided
Instances For
Constructor for LaxBraidedFunctor C D
.
Equations
- CategoryTheory.LaxBraidedFunctor.of F = { toFunctor := F, laxBraided := inferInstance }
Instances For
The lax monoidal functor induced by a lax braided functor.
Equations
- F.toLaxMonoidalFunctor = { toFunctor := F.toFunctor, laxMonoidal := inferInstance }
Instances For
Equations
- CategoryTheory.LaxBraidedFunctor.instCategory = CategoryTheory.InducedCategory.category CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor
Constructor for morphisms in the category LaxBraiededFunctor C D
.
Equations
- CategoryTheory.LaxBraidedFunctor.homMk f = { hom := f, isMonoidal := ⋯ }
Instances For
Constructor for isomorphisms in the category LaxBraidedFunctor C D
.
Equations
- CategoryTheory.LaxBraidedFunctor.isoMk e = { hom := CategoryTheory.LaxBraidedFunctor.homMk e.hom, inv := CategoryTheory.LaxBraidedFunctor.homMk e.inv, hom_inv_id := ⋯, inv_hom_id := ⋯ }
Instances For
The forgetful functor from lax braided functors to lax monoidal functors.
Equations
- CategoryTheory.LaxBraidedFunctor.forget = CategoryTheory.inducedFunctor CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor
Instances For
The forgetful functor from lax braided functors to lax monoidal functors is fully faithful.
Equations
- CategoryTheory.LaxBraidedFunctor.fullyFaithfulForget = CategoryTheory.fullyFaithfulInducedFunctor CategoryTheory.LaxBraidedFunctor.toLaxMonoidalFunctor
Instances For
Constructor for isomorphisms between lax braided functors.
Equations
- One or more equations did not get rendered due to their size.
Instances For
A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.
- μ' : (X Y : C) → CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y) ⟶ F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y)
- μ'_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj X')) (CategoryTheory.Functor.LaxMonoidal.μ' Y X') = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X X') (F.map (CategoryTheory.MonoidalCategory.whiskerRight f X'))
- μ'_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X') (F.map f)) (CategoryTheory.Functor.LaxMonoidal.μ' X' Y) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X' X) (F.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f))
- associativity' : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ' X Y) (F.obj Z)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom)) = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ' Y Z)) (CategoryTheory.Functor.LaxMonoidal.μ' X (CategoryTheory.MonoidalCategory.tensorObj Y Z)))
- left_unitality' : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.Functor.LaxMonoidal.ε' (F.obj X)) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' (𝟙_ C) X) (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).hom))
- right_unitality' : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) CategoryTheory.Functor.LaxMonoidal.ε') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ' X (𝟙_ C)) (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).hom))
- δ' : (X Y : C) → F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y) ⟶ CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y)
- δ'_natural_left : ∀ {X Y : C} (f : X ⟶ Y) (X' : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X X') (CategoryTheory.MonoidalCategory.whiskerRight (F.map f) (F.obj X')) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerRight f X')) (CategoryTheory.Functor.OplaxMonoidal.δ' Y X')
- δ'_natural_right : ∀ {X Y : C} (X' : C) (f : X ⟶ Y), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X' X) (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X') (F.map f)) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.whiskerLeft X' f)) (CategoryTheory.Functor.OplaxMonoidal.δ' X' Y)
- oplax_associativity' : ∀ (X Y Z : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' (CategoryTheory.MonoidalCategory.tensorObj X Y) Z) (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.δ' X Y) (F.obj Z)) (CategoryTheory.MonoidalCategory.associator (F.obj X) (F.obj Y) (F.obj Z)).hom) = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.associator X Y Z).hom) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X (CategoryTheory.MonoidalCategory.tensorObj Y Z)) (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) (CategoryTheory.Functor.OplaxMonoidal.δ' Y Z)))
- oplax_left_unitality' : ∀ (X : C), (CategoryTheory.MonoidalCategory.leftUnitor (F.obj X)).inv = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.leftUnitor X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' (𝟙_ C) X) (CategoryTheory.MonoidalCategory.whiskerRight CategoryTheory.Functor.OplaxMonoidal.η' (F.obj X)))
- oplax_right_unitality' : ∀ (X : C), (CategoryTheory.MonoidalCategory.rightUnitor (F.obj X)).inv = CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategory.rightUnitor X).inv) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ' X (𝟙_ C)) (CategoryTheory.MonoidalCategory.whiskerLeft (F.obj X) CategoryTheory.Functor.OplaxMonoidal.η'))
- μ_δ : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.tensorObj (F.obj X) (F.obj Y))
- δ_μ : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.δ F X Y) (CategoryTheory.Functor.LaxMonoidal.μ F X Y) = CategoryTheory.CategoryStruct.id (F.obj (CategoryTheory.MonoidalCategory.tensorObj X Y))
- braided : ∀ (X Y : C), CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.map (β_ X Y).hom) = CategoryTheory.CategoryStruct.comp (β_ (F.obj X) (F.obj Y)).hom (CategoryTheory.Functor.LaxMonoidal.μ F Y X)
Instances
A braided category with a faithful braided functor to a symmetric category is itself symmetric.
Instances For
Equations
- CategoryTheory.Functor.Braided.instId = CategoryTheory.Functor.Braided.mk ⋯
Equations
- One or more equations did not get rendered due to their size.
A multiplicative morphism between commutative monoids gives a braided functor between the corresponding discrete braided monoidal categories.
Swap the second and third objects in (X₁ ⊗ X₂) ⊗ (Y₁ ⊗ Y₂)
. This is used to strength the
tensor product functor from C × C
to C
as a monoidal functor.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The inverse of tensorμ
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The identity functor on C
, viewed as a functor from C
to its
monoidal opposite, upgraded to a braided functor.
Equations
- CategoryTheory.MonoidalOpposite.instBraidedMopFunctor = CategoryTheory.Functor.Braided.mk ⋯
The identity functor on C
, viewed as a functor from the
monoidal opposite of C
to C
, upgraded to a braided functor.
Equations
- CategoryTheory.MonoidalOpposite.instBraidedUnmopFunctor = CategoryTheory.Functor.Braided.mk ⋯
The braided monoidal category obtained from C
by replacing its braiding
β_ X Y : X ⊗ Y ≅ Y ⊗ X
with the inverse (β_ Y X)⁻¹ : X ⊗ Y ≅ Y ⊗ X
.
This corresponds to the automorphism of the braid group swapping
over-crossings and under-crossings.
Equations
- CategoryTheory.reverseBraiding C = { braiding := fun (X Y : C) => (β_ Y X).symm, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }
Instances For
The identity functor from C
to C
, where the codomain is given the
reversed braiding, upgraded to a braided functor.