CategoryTheory.BraidedCategory.braiding_naturality
theorem CategoryTheory.BraidedCategory.braiding_naturality :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.BraidedCategory C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y'),
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorHom f g) (β_ Y Y').hom =
CategoryTheory.CategoryStruct.comp (β_ X X').hom (CategoryTheory.MonoidalCategory.tensorHom g f)
This theorem, `CategoryTheory.BraidedCategory.braiding_naturality`, states that in a braided category, the braiding (symbolized by `β`) behaves naturally with respect to morphisms. Specifically, given any category `C` which is also a monoidal and braided category and objects `X, X', Y, Y'` in `C`, for any morphisms `f: X ⟶ Y` and `g: X' ⟶ Y'`, the composition of morphisms denoted by `CategoryTheory.CategoryStruct.comp`, the tensor product of `f` and `g` followed by the braiding on `Y` and `Y'` is equal to the braiding on `X` and `X'` followed by the tensor product of `g` and `f`. The symbol `β_ Y Y'.hom` represents the braiding of `Y` and `Y'` while `β_ X X'.hom` represents the braiding of `X` and `X'`. The tensor product of morphisms is indicated by `CategoryTheory.MonoidalCategory.tensorHom`. This theorem captures one of the core properties of braiding in braided monoidal categories.
More concisely: In a braided monoidal category, the braiding is natural with respect to morphisms, that is, for objects X, X', Y, Y' and morphisms f : X ⟶ Y and g : X' ⟶ Y', the composition of g ⊗ f and β\_Y Y'.hom is equal to β\_X X'.hom ⊗ f g.
|
CategoryTheory.braiding_tensorUnit_left
theorem CategoryTheory.braiding_tensorUnit_left :
∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.BraidedCategory C] (X : C),
(β_ (𝟙_ C) X).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.leftUnitor X).hom
(CategoryTheory.MonoidalCategory.rightUnitor X).inv
The theorem `CategoryTheory.braiding_tensorUnit_left` states that for any type `C` which forms a Category, a Monoidal Category, and a Braided Category, and for any `X` of type `C`, the homomorphism of the braiding of the tensor unit and `X` is equal to the composition of the homomorphism of the left unitor of `X` and the inverse of the homomorphism of the right unitor of `X`.
In other words, in the context of category theory, a braiding of the tensor unit and another object `X` in a braided monoidal category `C` is equivalent to the composition of certain natural transformations associated with `X` (left and right unitors).
More concisely: In a braided monoidal category, the braiding of the tensor unit and an object X is equivalent to the composition of X's left unitor homomorphism and the inverse of its right unitor homomorphism.
|
CategoryTheory.braiding_leftUnitor
theorem CategoryTheory.braiding_leftUnitor :
∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.BraidedCategory C] (X : C),
CategoryTheory.CategoryStruct.comp (β_ X (𝟙_ C)).hom (CategoryTheory.MonoidalCategory.leftUnitor X).hom =
(CategoryTheory.MonoidalCategory.rightUnitor X).hom
This theorem states that for any category `C` that has both a monoidal and braided structure, for any object `X` in `C`, the composition of the morphism associated with the braiding of `X` and the unit object of `C`, and the morphism associated with the left unitor of `X`, is equal to the morphism associated with the right unitor of `X`. In simpler terms, it says that a certain diagram commutes in a braided monoidal category: following one path (first braiding, then applying the left unitor) gets you to the same result as if you took the other path (applying the right unitor directly).
More concisely: In a braided monoidal category, for any object X, the composition of the morphism associated with the braiding of X and the unit object's left unitor morphism is equal to the morphism associated with X's right unitor.
|
CategoryTheory.BraidedCategory.braiding_tensor_left
theorem CategoryTheory.BraidedCategory.braiding_tensor_left :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
(β_ (CategoryTheory.MonoidalCategory.tensorObj X Y) Z).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft X (β_ Y Z).hom)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Z Y).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Z).hom Y)
(CategoryTheory.MonoidalCategory.associator Z X Y).hom)))
This theorem is part of the Category Theory and it states that, for any braided monoidal category `C` and any three objects `X`, `Y`, and `Z` in `C`, the braiding morphism from the tensor product of `X` and `Y` with `Z` to `Z` tensor `X` tensor `Y` is equal to the composition of several other morphisms.
Specifically, the composition starts with the associator from `X` tensor `Y` tensor `Z` to `X` tensor `(Y tensor Z)`, then applies the braiding morphism from `Y` tensor `Z` to `Z` tensor `Y` (which is 'whiskered' with `X`), reverses the associator from `X` tensor `Z` tensor `Y` to `(X tensor Z) tensor Y`, applies the braiding morphism from `X` tensor `Z` to `Z` tensor `X` (which is 'whiskered' with `Y`), and finally applies the associator from `Z` tensor `X` tensor `Y` to `(Z tensor X) tensor Y`.
In mathematical terms, this means that the braiding operation is compatible with the tensor product and the associativity of the category, making it a key property of the structure of braided monoidal categories.
More concisely: In a braided monoidal category, the braiding morphism between any three objects is equal to the composition of the associator and the braiding morphisms in reverse order, followed by the reversed associator.
|
CategoryTheory.BraidedCategory.hexagon_forward
theorem CategoryTheory.BraidedCategory.hexagon_forward :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[self : CategoryTheory.BraidedCategory C] (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))
In the context of a braided monoidal category `C`, the first hexagon identity theorem articulates a specific equality of morphism compositions for arbitrary objects `X`, `Y`, and `Z` in `C`. It states that the composition of three morphisms - the associator of `X`, `Y`, and `Z`, the braiding of `X` with the tensor of `Y` and `Z`, and the associator of `Y`, `Z`, and `X` - is equal to the composition of three other morphisms - the braiding of `X` and `Y` whiskered right with `Z`, the associator of `Y`, `X`, and `Z`, and the tensor of `Y` with the braiding of `X` and `Z` whiskered left. This theorem is a fundamental part of the structure of a braided monoidal category.
More concisely: In a braided monoidal category, the composition of the associator of X, Y, and Z, the braiding of X with Y whiskered right with Z, the associator of Y, X, and Z, and the tensor of Y with the braiding of X and Z whiskered left is equal to the composition of the braiding of X and Y, the associator of Y, X, and Z, and the associator of X, Y, and Z.
|
CategoryTheory.BraidedCategory.braiding_tensor_right
theorem CategoryTheory.BraidedCategory.braiding_tensor_right :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
(β_ X (CategoryTheory.MonoidalCategory.tensorObj Y Z)).hom =
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator X Y Z).inv
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerRight (β_ X Y).hom Z)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.associator Y X Z).hom
(CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.whiskerLeft Y (β_ X Z).hom)
(CategoryTheory.MonoidalCategory.associator Y Z X).inv)))
The theorem `CategoryTheory.BraidedCategory.braiding_tensor_right` states that for any type `C` which has a category structure, a monoidal category structure, and a braided category structure, and for any three objects `X`, `Y`, and `Z` in `C`, the braiding of `X` with the tensor product of `Y` and `Z` is equal to a specific composition of morphisms that involve associators, whiskering, and other braiding operations. This composition involves first inverting the associator of `X`, `Y`, and `Z`, then whisking the braiding of `X` and `Y` on the right with `Z`, then applying the associator of `Y`, `X`, and `Z`, then whisking the braiding of `X` and `Z` on the left with `Y`, and finally inverting the associator of `Y`, `Z`, and `X`. This theorem is a part of the mathematical structure known as "braided monoidal categories" which play a key role in many areas of mathematics and theoretical physics, including knot theory and quantum field theory.
More concisely: In a braided monoidal category, the braiding of objects X, Y, and Z is equal to the composition of whiskering the braiding of X and Y on the right with Z, associators, and whiskering the braiding of X and Z on the left with Y, inverted associators.
|
CategoryTheory.BraidedCategory.hexagon_reverse
theorem CategoryTheory.BraidedCategory.hexagon_reverse :
∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
[self : CategoryTheory.BraidedCategory C] (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))
This theorem, often referred to as the "second hexagon identity," is a foundational result in the theory of braided categories. It is stated for any category `C` that is not only a category in the usual sense, but also has the additional structure of a monoidal category and a braided category. Given three objects `X`, `Y`, and `Z` in this category, the theorem compares two different ways of "reassociating" a triple tensor product `X ⊗ Y ⊗ Z`. More specifically, it states that doing an associator, followed by a braiding, and then another associator, is the same as doing a braiding, followed by an associator, and then another braiding. This identity is a key part of the definition of a braided category, and plays a central role in many of its properties.
More concisely: In a braided monoidal category, the order of applying associators and braids is interchangeable in the reassociation of triple tensor products.
|