The symmetric monoidal structure on a category with chosen finite products. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
theorem
category_theory.monoidal_of_chosen_finite_products.braiding_naturality
{C : Type u}
[category_theory.category C]
(ℬ : Π (X Y : C), category_theory.limits.limit_cone (category_theory.limits.pair X Y))
{X X' Y Y' : C}
(f : X ⟶ Y)
(g : X' ⟶ Y') :
category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ f g ≫ (category_theory.limits.binary_fan.braiding (ℬ Y Y').is_limit (ℬ Y' Y).is_limit).hom = (category_theory.limits.binary_fan.braiding (ℬ X X').is_limit (ℬ X' X).is_limit).hom ≫ category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ g f
theorem
category_theory.monoidal_of_chosen_finite_products.hexagon_forward
{C : Type u}
[category_theory.category C]
(ℬ : Π (X Y : C), category_theory.limits.limit_cone (category_theory.limits.pair X Y))
(X Y Z : C) :
(category_theory.limits.binary_fan.associator_of_limit_cone ℬ X Y Z).hom ≫ (category_theory.limits.binary_fan.braiding (ℬ X (category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ Y Z)).is_limit (ℬ (category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ Y Z) X).is_limit).hom ≫ (category_theory.limits.binary_fan.associator_of_limit_cone ℬ Y Z X).hom = category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ (category_theory.limits.binary_fan.braiding (ℬ X Y).is_limit (ℬ Y X).is_limit).hom (𝟙 Z) ≫ (category_theory.limits.binary_fan.associator_of_limit_cone ℬ Y X Z).hom ≫ category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ (𝟙 Y) (category_theory.limits.binary_fan.braiding (ℬ X Z).is_limit (ℬ Z X).is_limit).hom
theorem
category_theory.monoidal_of_chosen_finite_products.hexagon_reverse
{C : Type u}
[category_theory.category C]
(ℬ : Π (X Y : C), category_theory.limits.limit_cone (category_theory.limits.pair X Y))
(X Y Z : C) :
(category_theory.limits.binary_fan.associator_of_limit_cone ℬ X Y Z).inv ≫ (category_theory.limits.binary_fan.braiding (ℬ (category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ X Y) Z).is_limit (ℬ Z (category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ X Y)).is_limit).hom ≫ (category_theory.limits.binary_fan.associator_of_limit_cone ℬ Z X Y).inv = category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ (𝟙 X) (category_theory.limits.binary_fan.braiding (ℬ Y Z).is_limit (ℬ Z Y).is_limit).hom ≫ (category_theory.limits.binary_fan.associator_of_limit_cone ℬ X Z Y).inv ≫ category_theory.monoidal_of_chosen_finite_products.tensor_hom ℬ (category_theory.limits.binary_fan.braiding (ℬ X Z).is_limit (ℬ Z X).is_limit).hom (𝟙 Y)
theorem
category_theory.monoidal_of_chosen_finite_products.symmetry
{C : Type u}
[category_theory.category C]
(ℬ : Π (X Y : C), category_theory.limits.limit_cone (category_theory.limits.pair X Y))
(X Y : C) :
(category_theory.limits.binary_fan.braiding (ℬ X Y).is_limit (ℬ Y X).is_limit).hom ≫ (category_theory.limits.binary_fan.braiding (ℬ Y X).is_limit (ℬ X Y).is_limit).hom = 𝟙 (category_theory.monoidal_of_chosen_finite_products.tensor_obj ℬ X Y)
def
category_theory.symmetric_of_chosen_finite_products
{C : Type u}
[category_theory.category C]
(𝒯 : category_theory.limits.limit_cone (category_theory.functor.empty C))
(ℬ : Π (X Y : C), category_theory.limits.limit_cone (category_theory.limits.pair X Y)) :
The monoidal structure coming from finite products is symmetric.
Equations
- category_theory.symmetric_of_chosen_finite_products 𝒯 ℬ = {to_braided_category := {braiding := λ (X Y : category_theory.monoidal_of_chosen_finite_products.monoidal_of_chosen_finite_products_synonym 𝒯 ℬ), category_theory.limits.binary_fan.braiding (ℬ X Y).is_limit (ℬ Y X).is_limit, braiding_naturality' := _, hexagon_forward' := _, hexagon_reverse' := _}, symmetry' := _}