Day convolution on Type-valued functor categories

Mathlib equips the type synonym C ⊛⥤ V (MonoidalCategory.DayFunctor) with the Day-convolution monoidal structure, subject to instance hypotheses: existence of the relevant pointwise left Kan extensions and preservation of colimits of the relevant costructured-arrow shapes by tensorLeft/tensorRight in V. For V := Type v and C a small monoidal category all of these hold via instances that Mathlib already provides (Type v is monoidal closed and braided, so both tensoring functors are left adjoints and preserve all colimits, and Type v has all small colimits); the imports of Closed.Types and Closed.Braided above are exactly what makes them synthesise.

What Mathlib does not provide is a braided (or symmetric) structure on C ⊛⥤ V: Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided constructs the braiding and proves the hexagons at the level of individual DayConvolution structures on plain functors, but never assembles them into a BraidedCategory (C ⊛⥤ V) instance. This file performs that assembly, at the same generality as Mathlib's MonoidalCategory (C ⊛⥤ V) instance, and records the acceptance tests for V := Type v at the bottom.

The Mathlib imports above are deliberate exceptions to the RS.Common.MathlibDeps funnel: the Day-convolution modules are not reachable from it.

@[instance_reducible]

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

The underlying functor of a tensor product in C ⊛⥤ V is a Day convolution of the underlying functors. Local instance: Mathlib advises against registering DayConvolution instances globally.

Equations

• RS.dayConv F G = CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution C V (CategoryTheory.MonoidalCategory.DayFunctor C V) F G

@[instance_reducible]

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

Right-nested triple Day convolutions, phrased so that instance search finds them behind the ⊛ notation.

Equations

• RS.dayConv₂ F G H = RS.dayConv F (CategoryTheory.MonoidalCategoryStruct.tensorObj G H)

@[instance_reducible]

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

Left-nested triple Day convolutions, phrased so that instance search finds them behind the ⊛ notation.

Equations

• RS.dayConv₂' F G H = RS.dayConv (CategoryTheory.MonoidalCategoryStruct.tensorObj F G) H

theorem RS.natTrans_tensorHom {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [∀ (F G : CategoryTheory.Functor C V), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct F G)] [(CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] {F F' G G' : CategoryTheory.MonoidalCategory.DayFunctor C V} (f : F ⟶ F') (g : G ⟶ G') : (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).natTrans = CategoryTheory.MonoidalCategory.DayConvolution.map f.natTrans g.natTrans

The underlying natural transformation of a tensor product of morphisms of C ⊛⥤ V is the induced morphism of Day convolutions.

theorem RS.natTrans_whiskerLeft {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [∀ (F G : CategoryTheory.Functor C V), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct F G)] [(CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (F : CategoryTheory.MonoidalCategory.DayFunctor C V) {G H : CategoryTheory.MonoidalCategory.DayFunctor C V} (g : G ⟶ H) : (CategoryTheory.MonoidalCategoryStruct.whiskerLeft F g).natTrans = CategoryTheory.MonoidalCategory.DayConvolution.map (CategoryTheory.CategoryStruct.id F.functor) g.natTrans

Left whiskering in C ⊛⥤ V, read off on underlying natural transformations.

theorem RS.natTrans_whiskerRight {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [∀ (F G : CategoryTheory.Functor C V), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct F G)] [(CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] {F G : CategoryTheory.MonoidalCategory.DayFunctor C V} (f : F ⟶ G) (H : CategoryTheory.MonoidalCategory.DayFunctor C V) : (CategoryTheory.MonoidalCategoryStruct.whiskerRight f H).natTrans = CategoryTheory.MonoidalCategory.DayConvolution.map f.natTrans (CategoryTheory.CategoryStruct.id H.functor)

Right whiskering in C ⊛⥤ V, read off on underlying natural transformations.

theorem RS.natTrans_associator {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [∀ (F G : CategoryTheory.Functor C V), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct F G)] [(CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (F G H : CategoryTheory.MonoidalCategory.DayFunctor C V) : (CategoryTheory.MonoidalCategoryStruct.associator F G H).hom.natTrans = (CategoryTheory.MonoidalCategory.DayConvolution.associator F.functor G.functor H.functor).hom

The associator of C ⊛⥤ V, read off on underlying natural transformations.

theorem RS.natTrans_associator_inv {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [CategoryTheory.Category.{v₂, u₂} V] [CategoryTheory.MonoidalCategory C] [CategoryTheory.MonoidalCategory V] [∀ (F G : CategoryTheory.Functor C V), (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension (CategoryTheory.MonoidalCategory.externalProduct F G)] [(CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorLeft v)] [∀ (v : V) (d : C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.Functor.id C).prod (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))) d) (CategoryTheory.MonoidalCategory.tensorRight v)] [∀ (v : V) (d : C × C), CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d) (CategoryTheory.MonoidalCategory.tensorRight v)] (F G H : CategoryTheory.MonoidalCategory.DayFunctor C V) : (CategoryTheory.MonoidalCategoryStruct.associator F G H).inv.natTrans = (CategoryTheory.MonoidalCategory.DayConvolution.associator F.functor G.functor H.functor).inv

Inverse form of RS.natTrans_associator.

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

The braiding on C ⊛⥤ V, inherited from the Day-convolution braiding of the underlying functors.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

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

The Day-convolution monoidal structure on C ⊛⥤ V is braided when C and V are. This discharges, for the type synonym, what Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided proves at the level of individual convolutions.

Equations

• RS.dayFunctorBraided = { braiding := RS.dayFunctorBraiding, braiding_naturality_right := ⋯, braiding_naturality_left := ⋯, hexagon_forward := ⋯, hexagon_reverse := ⋯ }

@[instance_reducible]

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

The Day-convolution monoidal structure on C ⊛⥤ V is symmetric when C and V are, via DayConvolution.symmetry.

Equations

• RS.dayFunctorSymmetric = { toBraidedCategory := inferInstance, symmetry := ⋯ }