Day convolution monoidal structure

Given functors F G : C ⥤ V between two monoidal categories, this file defines a typeclass DayConvolution on functors F G that contains a functor F ⊛ G, as well as the required data to exhibit F ⊛ G as a pointwise left Kan extension of F ⊠ G (see CategoryTheory/Monoidal/ExternalProduct for the definition) along the tensor product of C. Such a functor is called a Day convolution of F and G, and although we do not show it yet, this operation defines a monoidal structure on C ⥤ V.

We also define a typeclass DayConvolutionUnit on a functor U : C ⥤ V that bundle the data required to make it a unit for the Day convolution monoidal structure: said data is that of a map 𝟙_ V ⟶ U.obj (𝟙_ C) that exhibits U as a pointwise left Kan extension of fromPUnit (𝟙_ V) along fromPUnit (𝟙_ C).

References

• nLab page: Day convolution

TODOs (@robin-carlier)

• Define associators and unitors, prove the pentagon and triangle identities.
• Braided/symmetric case.
• Case where V is closed.
• Define a typeclass DayConvolutionMonoidalCategory extending MonoidalCategory
• Characterization of lax monoidal functors out of a day convolution monoidal category.
• Case V = Type u and its universal property.

class CategoryTheory.MonoidalCategory.DayConvolution {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) : Type (max (max (max u₁ u₂) v₁) v₂)

A DayConvolution structure on functors F G : C ⥤ V is the data of a functor F ⊛ G : C ⥤ V, along with a unit F ⊠ G ⟶ tensor C ⋙ F ⊛ G that exhibits this functor as a pointwise left Kan extension of F ⊠ G along tensor C. This is a class used to prove various property of such extensions, but registering global instances of this class is probably a bad idea.

• convolution : Functor C V

  The chosen convolution between the functors. Denoted F ⊛ G.

• unit : externalProduct F G ⟶ (tensor C).comp (convolution F G)

  The chosen convolution between the functors.

• isPointwiseLeftKanExtensionUnit : (Functor.LeftExtension.mk (convolution F G) (unit F G)).IsPointwiseLeftKanExtension

  The transformation unit exhibits F ⊛ G as a pointwise left Kan extension of F ⊠ G along tensor C.

def CategoryTheory.MonoidalCategory.DayConvolution.«term_⊛_» : Lean.TrailingParserDescr

A notation for the Day convolution of two functors.

Equations

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

instance CategoryTheory.MonoidalCategory.DayConvolution.leftKanExtension {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] : (convolution F G).IsLeftKanExtension (unit F G)

def CategoryTheory.MonoidalCategory.DayConvolution.uniqueUpToIso {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} (h h' : DayConvolution F G) : convolution F G ≅ convolution F G

Two day convolution structures on the same functors gives an isomorphic functor.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} (h h' : DayConvolution F G) : CategoryStruct.comp (unit F G) ((tensor C).whiskerLeft (h.uniqueUpToIso h').hom) = unit F G

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_hom_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} (h h' : DayConvolution F G) {Z : Functor (C × C) V} (h✝ : (tensor C).comp (convolution F G) ⟶ Z) : CategoryStruct.comp (unit F G) (CategoryStruct.comp ((tensor C).whiskerLeft (h.uniqueUpToIso h').hom) h✝) = CategoryStruct.comp (unit F G) h✝

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_inv {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} (h h' : DayConvolution F G) : CategoryStruct.comp (unit F G) ((tensor C).whiskerLeft (h.uniqueUpToIso h').inv) = unit F G

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_uniqueUpToIso_inv_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} (h h' : DayConvolution F G) {Z : Functor (C × C) V} (h✝ : (tensor C).comp (convolution F G) ⟶ Z) : CategoryStruct.comp (unit F G) (CategoryStruct.comp ((tensor C).whiskerLeft (h.uniqueUpToIso h').inv) h✝) = CategoryStruct.comp (unit F G) h✝

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_naturality {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] {x x' y y' : C} (f : x ⟶ x') (g : y ⟶ y') : CategoryStruct.comp (tensorHom (F.map f) (G.map g)) ((unit F G).app (x', y')) = CategoryStruct.comp ((unit F G).app (x, y)) ((convolution F G).map (tensorHom f g))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] {x x' y y' : C} (f : x ⟶ x') (g : y ⟶ y') {Z : V} (h : (convolution F G).obj ((tensor C).obj (x', y')) ⟶ Z) : CategoryStruct.comp (tensorHom (F.map f) (G.map g)) (CategoryStruct.comp ((unit F G).app (x', y')) h) = CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((convolution F G).map (tensorHom f g)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.whiskerRight_comp_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] {x x' : C} (y : C) (f : x ⟶ x') : CategoryStruct.comp (whiskerRight (F.map f) (G.obj y)) ((unit F G).app (x', y)) = CategoryStruct.comp ((unit F G).app (x, y)) ((convolution F G).map (whiskerRight f y))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.whiskerRight_comp_unit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] {x x' : C} (y : C) (f : x ⟶ x') {Z : V} (h : (convolution F G).obj ((tensor C).obj (x', y)) ⟶ Z) : CategoryStruct.comp (whiskerRight (F.map f) (G.obj y)) (CategoryStruct.comp ((unit F G).app (x', y)) h) = CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((convolution F G).map (whiskerRight f y)) h)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.whiskerLeft_comp_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] (x : C) {y y' : C} (g : y ⟶ y') : CategoryStruct.comp (whiskerLeft (F.obj x) (G.map g)) ((unit F G).app (x, y')) = CategoryStruct.comp ((unit F G).app (x, y)) ((convolution F G).map (whiskerLeft x g))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.whiskerLeft_comp_unit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] (x : C) {y y' : C} (g : y ⟶ y') {Z : V} (h : (convolution F G).obj ((tensor C).obj (x, y')) ⟶ Z) : CategoryStruct.comp (whiskerLeft (F.obj x) (G.map g)) (CategoryStruct.comp ((unit F G).app (x, y')) h) = CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((convolution F G).map (whiskerLeft x g)) h)

def CategoryTheory.MonoidalCategory.DayConvolution.map {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} [DayConvolution F G] {F' G' : Functor C V} [DayConvolution F' G'] (f : F ⟶ F') (g : G ⟶ G') : convolution F G ⟶ convolution F' G'

The morphism between day convolutions (provided they exist) induced by a pair of morphisms.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} [DayConvolution F G] {F' G' : Functor C V} [DayConvolution F' G'] (f : F ⟶ F') (g : G ⟶ G') (x y : C) : CategoryStruct.comp ((unit F G).app (x, y)) ((map f g).app (tensorObj x y)) = CategoryStruct.comp (tensorHom (f.app x) (g.app y)) ((unit F' G').app (x, y))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.unit_app_map_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : Functor C V} [DayConvolution F G] {F' G' : Functor C V} [DayConvolution F' G'] (f : F ⟶ F') (g : G ⟶ G') (x y : C) {Z : V} (h : (convolution F' G').obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((map f g).app (tensorObj x y)) h) = CategoryStruct.comp (tensorHom (f.app x) (g.app y)) (CategoryStruct.comp ((unit F' G').app (x, y)) h)

def CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (coyoneda.obj (Opposite.op (externalProduct F G)))).CorepresentableBy (convolution F G)

The universal property of left Kan extensions characterizes the functor corepresented by F ⊛ G.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_symm_apply {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] {Y✝ : Functor C V} (β : externalProduct F G ⟶ (tensor C).comp Y✝) : (corepresentableBy F G).homEquiv.symm β = (convolution F G).descOfIsLeftKanExtension (unit F G) Y✝ β

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy_homEquiv_apply_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] {Y✝ : Functor C V} (β : convolution F G ⟶ Y✝) (X : C × C) : ((corepresentableBy F G).homEquiv β).app X = CategoryStruct.comp ((unit F G).app X) (β.app (tensorObj X.1 X.2))

theorem CategoryTheory.MonoidalCategory.DayConvolution.convolution_hom_ext_at {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : Functor C V) [DayConvolution F G] (c : C) {v : V} {f g : (convolution F G).obj c ⟶ v} (h : ∀ {x y : C} (u : tensorObj x y ⟶ c), CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((convolution F G).map u) f) = CategoryStruct.comp ((unit F G).app (x, y)) (CategoryStruct.comp ((convolution F G).map u) g)) : f = g

Use the fact that (F ⊛ G).obj c is a colimit to characterize morphisms out of it at a point.

class CategoryTheory.MonoidalCategory.DayConvolutionUnit {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : Functor C V) : Type (max (max (max u₁ u₂) v₁) v₂)

A DayConvolutionUnit structure on a functor C ⥤ V is the data of a pointwise left Kan extension of fromPUnit (𝟙_ V) along fromPUnit (𝟙_ C). Again, this is made a class to ease proofs when constructing DayConvolutionMonoidalCategory structures, but one should avoid registering it globally.

• can : tensorUnit V ⟶ F.obj (tensorUnit C)

  A "canonical" structure map 𝟙_ V ⟶ F.obj (𝟙_ C) that defines a natural transformation fromPUnit (𝟙_ V) ⟶ fromPUnit (𝟙_ C) ⋙ F.

• isPointwiseLeftKanExtensionCan : (Functor.LeftExtension.mk F { app := fun (x : Discrete PUnit.{1}) => can, naturality := ⋯ }).IsPointwiseLeftKanExtension

  The canonical map 𝟙_ V ⟶ F.obj (𝟙_ C) exhibits F as a pointwise left kan extension of fromPUnit.{0} 𝟙_ V along fromPUnit.{0} 𝟙_ C.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] : Functor.fromPUnit (tensorUnit V) ⟶ (Functor.fromPUnit (tensorUnit C)).comp U

A shorthand for the natural transformation of functors out of PUnit defined by the canonical morphism 𝟙_ V ⟶ U.obj (𝟙_ C) when U is a unit for Day convolution.

Equations

• CategoryTheory.MonoidalCategory.DayConvolutionUnit.φ U = { app := fun (x : CategoryTheory.Discrete PUnit.{1}) => CategoryTheory.MonoidalCategory.DayConvolutionUnit.can, naturality := ⋯ }

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] {c : C} {v : V} {g h : U.obj c ⟶ v} (e : ∀ (f : tensorUnit C ⟶ c), CategoryStruct.comp can (CategoryStruct.comp (U.map f) g) = CategoryStruct.comp can (CategoryStruct.comp (U.map f) h)) : g = h

Since a convolution unit is a pointwise left Kan extension, maps out of it at any object are uniquely characterized.