The symmetric monoidal structure on a category with chosen finite products.

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.braiding_naturality {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') : CategoryStruct.comp (tensorHom ℬ f g) (Limits.BinaryFan.braiding (ℬ Y Y').isLimit (ℬ Y' Y).isLimit).hom = CategoryStruct.comp (Limits.BinaryFan.braiding (ℬ X X').isLimit (ℬ X' X).isLimit).hom (tensorHom ℬ g f)

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_forward {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y Z : C) : CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).hom (CategoryStruct.comp (Limits.BinaryFan.braiding (ℬ X (tensorObj ℬ Y Z)).isLimit (ℬ (tensorObj ℬ Y Z) X).isLimit).hom (Limits.BinaryFan.associatorOfLimitCone ℬ Y Z X).hom) = CategoryStruct.comp (tensorHom ℬ (Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (CategoryStruct.id Z)) (CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ Y X Z).hom (tensorHom ℬ (CategoryStruct.id Y) (Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom))

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.hexagon_reverse {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y Z : C) : CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ X Y Z).inv (CategoryStruct.comp (Limits.BinaryFan.braiding (ℬ (tensorObj ℬ X Y) Z).isLimit (ℬ Z (tensorObj ℬ X Y)).isLimit).hom (Limits.BinaryFan.associatorOfLimitCone ℬ Z X Y).inv) = CategoryStruct.comp (tensorHom ℬ (CategoryStruct.id X) (Limits.BinaryFan.braiding (ℬ Y Z).isLimit (ℬ Z Y).isLimit).hom) (CategoryStruct.comp (Limits.BinaryFan.associatorOfLimitCone ℬ X Z Y).inv (tensorHom ℬ (Limits.BinaryFan.braiding (ℬ X Z).isLimit (ℬ Z X).isLimit).hom (CategoryStruct.id Y)))

theorem CategoryTheory.MonoidalOfChosenFiniteProducts.symmetry {C : Type u} [Category.{v, u} C] (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) (X Y : C) : CategoryStruct.comp (Limits.BinaryFan.braiding (ℬ X Y).isLimit (ℬ Y X).isLimit).hom (Limits.BinaryFan.braiding (ℬ Y X).isLimit (ℬ X Y).isLimit).hom = CategoryStruct.id (tensorObj ℬ X Y)

def CategoryTheory.symmetricOfChosenFiniteProducts {C : Type u} [Category.{v, u} C] (𝒯 : Limits.LimitCone (Functor.empty C)) (ℬ : (X Y : C) → Limits.LimitCone (Limits.pair X Y)) : SymmetricCategory (MonoidalOfChosenFiniteProducts.MonoidalOfChosenFiniteProductsSynonym 𝒯 ℬ)

The monoidal structure coming from finite products is symmetric.

Equations

• CategoryTheory.symmetricOfChosenFiniteProducts 𝒯 ℬ = CategoryTheory.SymmetricCategory.mk ⋯