The symmetric monoidal structure on a category with chosen finite products. #
theorem
CategoryTheory.MonoidalOfChosenFiniteProducts.braiding_naturality
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y))
{X : C}
{X' : C}
{Y : C}
{Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y')
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ f g)
(CategoryTheory.Limits.BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom
(CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ g f)
theorem
CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_forward
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y))
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.BinaryFan.braiding
(ℬ X (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z)).isLimit
(ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ Y Z) X).isLimit).hom
(CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ
(CategoryTheory.Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom
(CategoryTheory.CategoryStruct.id Z))
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Y X Z).hom
(CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id Y)
(CategoryTheory.Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom))
theorem
CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_reverse
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y))
(X : C)
(Y : C)
(Z : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).inv
(CategoryTheory.CategoryStruct.comp
(CategoryTheory.Limits.BinaryFan.braiding
(ℬ (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y) Z).isLimit
(ℬ Z (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y)).isLimit).hom
(CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) = CategoryTheory.CategoryStruct.comp
(CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ (CategoryTheory.CategoryStruct.id X)
(CategoryTheory.Limits.BinaryFan.braiding (ℬ Y Z).isLimit (ℬ Z Y).isLimit).hom)
(CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.associatorOfLimitCone ℬ X Z Y).inv
(CategoryTheory.MonoidalOfChosenFiniteProducts.tensorHom ℬ
(CategoryTheory.Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom
(CategoryTheory.CategoryStruct.id Y)))
theorem
CategoryTheory.MonoidalOfChosenFiniteProducts.symmetry
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y))
(X : C)
(Y : C)
:
CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom
(CategoryTheory.Limits.BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom = CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalOfChosenFiniteProducts.tensorObj ℬ X Y)
def
CategoryTheory.symmetricOfChosenFiniteProducts
{C : Type u}
[CategoryTheory.Category.{v, u} C]
(𝒯 : CategoryTheory.Limits.LimitCone (CategoryTheory.Functor.empty C))
(ℬ : (X Y : C) → CategoryTheory.Limits.LimitCone (CategoryTheory.Limits.pair X Y))
:
The monoidal structure coming from finite products is symmetric.