mathlib3 documentation

category_theory.monoidal.braided

Braided and symmetric monoidal categories #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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 #

@[class]

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} [category_theory.category C] [category_theory.monoidal_category C] [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} [category_theory.category C] [category_theory.monoidal_category C] [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_reverse_assoc {C : Type u} [category_theory.category C] [category_theory.monoidal_category C] [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} [category_theory.category C] [category_theory.monoidal_category C] [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'

We now establish how the braiding interacts with the unitors.

I couldn't find a detailed proof in print, but this is discussed in:

@[class]

A symmetric monoidal category is a braided monoidal category for which the braiding is symmetric.

See https://stacks.math.columbia.edu/tag/0FFW.

Instances of this typeclass
Instances of other typeclasses for category_theory.symmetric_category
  • category_theory.symmetric_category.has_sizeof_inst

A lax braided functor between braided monoidal categories is a lax monoidal functor which preserves the braiding.

Instances for category_theory.lax_braided_functor

Interpret a natural isomorphism of the underlyling lax monoidal functors as an isomorphism of the lax braided monoidal functors.

Equations

A braided functor between braided monoidal categories is a monoidal functor which preserves the braiding.

Instances for category_theory.braided_functor

Interpret a natural isomorphism of the underlyling monoidal functors as an isomorphism of the braided monoidal functors.

Equations

A multiplicative morphism between commutative monoids gives a braided functor between the corresponding discrete braided monoidal categories.

Equations
theorem category_theory.tensor_μ_def₁ (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ Y₁ Y₂ : C) :
category_theory.tensor_μ 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₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ Y₁ Y₂ : C) :
(𝟙 X₁ (α_ X₂ Y₁ Y₂).hom) (α_ X₁ X₂ (Y₁ Y₂)).inv category_theory.tensor_μ C (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₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] {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₂) category_theory.tensor_μ C (Y₁, Y₂) (V₁, V₂) = category_theory.tensor_μ C (X₁, X₂) (U₁, U₂) ((f₁ g₁) f₂ g₂)
theorem category_theory.tensor_left_unitality (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :
(λ_ (X₁ X₂)).hom = ((λ_ (𝟙_ C)).inv 𝟙 (X₁ X₂)) category_theory.tensor_μ C (𝟙_ C _inst_2, 𝟙_ C _inst_2) (X₁, X₂) ((λ_ X₁).hom (λ_ X₂).hom)
theorem category_theory.tensor_right_unitality (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :
(ρ_ (X₁ X₂)).hom = (𝟙 (X₁ X₂) (λ_ (𝟙_ C)).inv) category_theory.tensor_μ C (X₁, X₂) (𝟙_ C _inst_2, 𝟙_ C _inst_2) ((ρ_ X₁).hom (ρ_ X₂).hom)
theorem category_theory.tensor_associativity_aux (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (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₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) :
(category_theory.tensor_μ C (X₁, X₂) (Y₁, Y₂) 𝟙 (Z₁ Z₂)) category_theory.tensor_μ C (X₁ Y₁, X₂ Y₂) (Z₁, Z₂) ((α_ X₁ Y₁ Z₁).hom (α_ X₂ Y₂ Z₂).hom) = (α_ (X₁ X₂) (Y₁ Y₂) (Z₁ Z₂)).hom (𝟙 (X₁ X₂) category_theory.tensor_μ C (Y₁, Y₂) (Z₁, Z₂)) category_theory.tensor_μ C (X₁, X₂) (Y₁ Z₁, Y₂ Z₂)
theorem category_theory.left_unitor_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :
(λ_ X₁).hom (λ_ X₂).hom = category_theory.tensor_μ C (𝟙_ C _inst_2, X₁) (𝟙_ C _inst_2, X₂) ((λ_ (𝟙_ C)).hom 𝟙 (X₁ X₂)) (λ_ (X₁ X₂)).hom
theorem category_theory.right_unitor_monoidal (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ : C) :
(ρ_ X₁).hom (ρ_ X₂).hom = category_theory.tensor_μ C (X₁, 𝟙_ C _inst_2) (X₂, 𝟙_ C _inst_2) (𝟙 (X₁ X₂) (λ_ (𝟙_ C)).hom) (ρ_ (X₁ X₂)).hom
theorem category_theory.associator_monoidal_aux (C : Type u₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (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₁) [category_theory.category C] [category_theory.monoidal_category C] [category_theory.braided_category C] (X₁ X₂ X₃ Y₁ Y₂ Y₃ : C) :
category_theory.tensor_μ C (X₁ X₂, X₃) (Y₁ Y₂, Y₃) (category_theory.tensor_μ C (X₁, X₂) (Y₁, Y₂) 𝟙 (X₃ Y₃)) (α_ (X₁ Y₁) (X₂ Y₂) (X₃ Y₃)).hom = ((α_ X₁ X₂ X₃).hom (α_ Y₁ Y₂ Y₃).hom) category_theory.tensor_μ C (X₁, X₂ X₃) (Y₁, Y₂ Y₃) (𝟙 (X₁ Y₁) category_theory.tensor_μ C (X₂, X₃) (Y₂, Y₃))