The braided and symmetric Day convolution monoidal structures on `C ⊛⥤ V` #

For braided monoidal categories C and V, Mathlib constructs the Day convolution braiding DayConvolution.braiding F G : F ⊛ G ≅ G ⊛ F of two functors F G : C ⥤ V admitting Day convolutions, and proves its naturality, both hexagon identities and, when C and V are symmetric, its symmetry. Mathlib also equips the type synonym C ⊛⥤ V of C ⥤ V with the Day convolution monoidal structure. This file combines the two: under the same existence and colimit-preservation hypotheses as Mathlib's MonoidalCategory (C ⊛⥤ V), it makes C ⊛⥤ V a braided monoidal category when C and V are braided, and a symmetric monoidal category when they are symmetric.

The transfer goes through the faithful functor ι : (C ⊛⥤ V) ⥤ C ⥤ V of a lawful Day convolution monoidal structure, which Mathlib proves carries tensor products of morphisms and associators to their Day convolution counterparts; the corresponding statements for whiskerings and inverse associators are in TauCeti.CategoryTheory.Monoidal.DayConvolution.Basic.

The main application is the symmetric monoidal category of symmetric sequences, Day convolution along the block sum of the finite-bijection groupoid, over which symmetric spectra are modules.

Main definitions #

DayFunctor.braiding F G: the Day convolution braiding F ⊗ G ≅ G ⊗ F in C ⊛⥤ V.
The instances BraidedCategory (C ⊛⥤ V) and SymmetricCategory (C ⊛⥤ V).

Main statements #

DayFunctor.η_app_comp_braiding_hom_natTrans_app: the braiding is characterised by its restriction along the Day convolution unit η F G, where it is the braiding of V followed by η G F and the braiding of C.

References #

B. Day, On closed categories of functors, Reports of the Midwest Category Seminar IV, Lecture Notes in Math. 137 (1970), 1-38.

source

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.braiding {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [BraidedCategory C] [BraidedCategory V] (F G : DayFunctor C V) :

tensorObj F G ≅ tensorObj G F

The Day convolution braiding F ⊗ G ≅ G ⊗ F of Day functors: Mathlib's DayConvolution.braiding of the underlying functors.

Instances For

source

@[instance_reducible]

noncomputable instance CategoryTheory.MonoidalCategory.DayFunctor.braidedCategory {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [BraidedCategory C] [BraidedCategory V] :

BraidedCategory (DayFunctor C V)

source

theorem CategoryTheory.MonoidalCategory.DayFunctor.braiding_eq {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [BraidedCategory C] [BraidedCategory V] (F G : DayFunctor C V) :

β_ F G = F.braiding G

The braiding of the instance BraidedCategory (C ⊛⥤ V) is DayFunctor.braiding.

source

theorem CategoryTheory.MonoidalCategory.DayFunctor.ι_map_braiding_hom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [BraidedCategory C] [BraidedCategory V] (F G : DayFunctor C V) :

(LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).map (β_ F G).hom = (DayConvolution.braiding ((LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).obj F) ((LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).obj G)).hom

ι carries the braiding of Day functors to Mathlib's Day convolution braiding.

source

theorem CategoryTheory.MonoidalCategory.DayFunctor.ι_map_braiding_inv {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [BraidedCategory C] [BraidedCategory V] (F G : DayFunctor C V) :

(LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).map (β_ F G).inv = (DayConvolution.braiding ((LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).obj F) ((LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).obj G)).inv

ι carries the inverse braiding of Day functors to Mathlib's inverse Day convolution braiding.

source

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_braiding_hom_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] [BraidedCategory C] [BraidedCategory V] (F G : DayFunctor C V) (x y : C) :

CategoryStruct.comp ((F.η G).app (x, y)) ((β_ F G).hom.natTrans.app (tensorObj x y)) = CategoryStruct.comp (β_ ((G.functor, F.functor).2.obj (y, x).2) ((G.functor, F.functor).1.obj (y, x).1)).hom (CategoryStruct.comp ((G.η F).app (y, x)) ((tensorObj G F).functor.map (β_ y x).hom))

The braiding of Day functors restricted along the Day convolution unit η F G: at (x, y) it is the braiding of V, followed by η G F at (y, x) and the action of G ⊗ F on the braiding of C.

source

@[simp]