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 Mathlib/CategoryTheory/Monoidal/ExternalProduct/Basic.lean 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 bundles 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).

The main way to assert that a given monoidal category structure on a category D arises as a "Day convolution monoidal structure" is given by the typeclass LawfulDayConvolutionMonoidalCategoryStruct C V D, which bundles the data and equations needed to exhibit D as a monoidal full subcategory of C ⥤ V if the latter were to have the Day convolution monoidal structure. The definition monoidalOfLawfulDayConvolutionMonoidalCategoryStruct promotes (under suitable assumptions on V) a LawfulDayConvolutionMonoidalCategoryStruct C V D to a monoidal structure.

References

• nLab page: Day convolution

TODOs (@robin-carlier)

• Type alias for C ⥤ V with a LawfulDayConvolutionMonoidalCategoryStruct.
• 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 properties 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.

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.

@[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.

@[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.

@[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.

instance CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitRightUnit {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G H : Functor C V) [DayConvolution G H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] : (externalProduct F (convolution G H)).IsLeftKanExtension (ExternalProduct.extensionUnitRight (convolution G H) (unit G H) F)

instance CategoryTheory.MonoidalCategory.DayConvolution.instIsLeftKanExtensionProdExternalProductConvolutionExtensionUnitLeftUnit {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] (H : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] : (externalProduct (convolution F G) H).IsLeftKanExtension (ExternalProduct.extensionUnitLeft (convolution F G) (unit F G) 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 H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (C × C × C) (C × C) V).obj ((Functor.id C).prod (tensor C))).comp (coyoneda.obj (Opposite.op (externalProduct F (externalProduct G H)))))).CorepresentableBy (convolution F (convolution G H))

The CorepresentableBy structure asserting that the Type-valued functor Y ↦ (F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ Y) is corepresented by F ⊛ G ⊛ H.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] {Y✝ : Functor C V} : (corepresentableBy₂ F G H).homEquiv = (corepresentableBy F (convolution G H)).homEquiv.trans ((externalProduct F (convolution G H)).homEquivOfIsLeftKanExtension (ExternalProduct.extensionUnitRight (convolution G H) (unit G H) F) (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).obj Y✝))

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] (H : Functor C V) [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft ((C × C) × C) (C × C) V).obj ((tensor C).prod (Functor.id C))).comp (coyoneda.obj (Opposite.op (externalProduct (externalProduct F G) H))))).CorepresentableBy (convolution (convolution F G) H)

The CorepresentableBy structure asserting that the Type-valued functor Y ↦ ((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ Y) is corepresented by (F ⊛ G) ⊛ H.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.corepresentableBy₂'_homEquiv {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] (H : Functor C V) [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] {Y✝ : Functor C V} : (corepresentableBy₂' F G H).homEquiv = (corepresentableBy (convolution F G) H).homEquiv.trans ((externalProduct (convolution F G) H).homEquivOfIsLeftKanExtension (ExternalProduct.extensionUnitLeft (convolution F G) (unit F G) H) (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).obj Y✝))

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

The isomorphism of functors between ((F ⊠ G) ⊠ H ⟶ (tensor C).prod (𝟭 C) ⋙ tensor C ⋙ -) and (F ⊠ G ⊠ H ⟶ (𝟭 C).prod (tensor C) ⋙ tensor C ⋙ -) that corresponds to the associator isomorphism for Day convolution through corepresentableBy₂ and corepresentableBy₂.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G H X : Functor C V) (a✝ : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft ((C × C) × C) (C × C) V).obj ((tensor C).prod (Functor.id C))).comp (coyoneda.obj (Opposite.op (externalProduct (externalProduct F G) H))))).obj X) (X✝ : C × C × C) : ((associatorCorepresentingIso F G H).hom.app X a✝).app X✝ = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X✝.1) (G.obj X✝.2.1) (H.obj X✝.2.2)).inv (CategoryStruct.comp (((prod.associativity C C C).congrLeft.fullyFaithfulFunctor.homEquiv a✝).app X✝) (X.map (MonoidalCategoryStruct.associator X✝.1 X✝.2.1 X✝.2.2).hom))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.associatorCorepresentingIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G H X : Functor C V) (a✝ : (((Functor.whiskeringLeft (C × C × C) C V).obj (((Functor.id C).prod (tensor C)).comp (tensor C))).comp (coyoneda.obj (Opposite.op (externalProduct F (externalProduct G H))))).obj X) (X✝ : (C × C) × C) : ((associatorCorepresentingIso F G H).inv.app X a✝).app X✝ = CategoryStruct.comp (whiskerRight (whiskerRight (F.map ((prod.associativity C C C).unit.app X✝).1.1) (G.obj X✝.1.2)) (H.obj X✝.2)) (CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj X✝.1.1) (G.obj X✝.1.2) (H.obj X✝.2)).hom (CategoryStruct.comp (whiskerLeft (F.obj X✝.1.1) (whiskerRight (G.map ((prod.associativity C C C).unit.app X✝).1.2) (H.obj X✝.2))) (CategoryStruct.comp (whiskerLeft (F.obj X✝.1.1) (whiskerLeft (G.obj X✝.1.2) (H.map ((prod.associativity C C C).unit.app X✝).2))) (CategoryStruct.comp (a✝.app (X✝.1.1, X✝.1.2, X✝.2)) (CategoryStruct.comp (X.map (tensorHom ((prod.associativity C C C).unitInv.app X✝).1.1 (tensorHom ((prod.associativity C C C).unitInv.app X✝).1.2 ((prod.associativity C C C).unitInv.app X✝).2))) (X.map (MonoidalCategoryStruct.associator X✝.1.1 X✝.1.2 X✝.2).inv))))))

def CategoryTheory.MonoidalCategory.DayConvolution.associator {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] (H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] : convolution (convolution F G) H ≅ convolution F (convolution G H)

The associator isomorphism for Day convolution

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_hom_unit_unit {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] (H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] (x y z : C) : CategoryStruct.comp (whiskerRight ((unit F G).app (x, y)) (H.obj z)) (CategoryStruct.comp ((unit (convolution F G) H).app (tensorObj x y, z)) ((associator F G H).hom.app (tensorObj (tensorObj x y) z))) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj x) ((G, H).1.obj (y, z).1) ((G, H).2.obj (y, z).2)).hom (CategoryStruct.comp (whiskerLeft (F.obj x) ((unit G H).app (y, z))) (CategoryStruct.comp ((unit F (convolution G H)).app (x, tensorObj y z)) ((convolution F (convolution G H)).map (MonoidalCategoryStruct.associator (x, tensorObj y z).1 y z).inv)))

Characterizing the forward direction of the associator isomorphism with respect to the unit transformations.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_hom_unit_unit_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] (H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] (x y z : C) {Z : V} (h : (convolution F (convolution G H)).obj (tensorObj (tensorObj x y) z) ⟶ Z) : CategoryStruct.comp (whiskerRight ((unit F G).app (x, y)) (H.obj z)) (CategoryStruct.comp ((unit (convolution F G) H).app (tensorObj x y, z)) (CategoryStruct.comp ((associator F G H).hom.app (tensorObj (tensorObj x y) z)) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj x) (G.obj y) (H.obj z)).hom (CategoryStruct.comp (whiskerLeft (F.obj x) ((unit G H).app (y, z))) (CategoryStruct.comp ((unit F (convolution G H)).app (x, tensorObj y z)) (CategoryStruct.comp ((convolution F (convolution G H)).map (MonoidalCategoryStruct.associator x y z).inv) h)))

Characterizing the forward direction of the associator isomorphism with respect to the unit transformations.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_inv_unit_unit {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] (H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] (x y z : C) : CategoryStruct.comp (whiskerLeft (F.obj x) ((unit G H).app (y, z))) (CategoryStruct.comp ((unit F (convolution G H)).app (x, tensorObj y z)) ((associator F G H).inv.app (tensorObj x (tensorObj y z)))) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj x) (G.obj y) (H.obj z)).inv (CategoryStruct.comp (whiskerRight ((unit F G).app (x, y)) (H.obj z)) (CategoryStruct.comp ((unit (convolution F G) H).app (tensorObj x y, z)) ((convolution (convolution F G) H).map (MonoidalCategoryStruct.associator x y z).hom)))

Characterizing the inverse direction of the associator with respect to the unit transformations

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_inv_unit_unit_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] (H : Functor C V) [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] (x y z : C) {Z : V} (h : (convolution (convolution F G) H).obj (tensorObj x (tensorObj y z)) ⟶ Z) : CategoryStruct.comp (whiskerLeft (F.obj x) ((unit G H).app (y, z))) (CategoryStruct.comp ((unit F (convolution G H)).app (x, tensorObj y z)) (CategoryStruct.comp ((associator F G H).inv.app (tensorObj x (tensorObj y z))) h)) = CategoryStruct.comp (MonoidalCategoryStruct.associator (F.obj x) (G.obj y) (H.obj z)).inv (CategoryStruct.comp (whiskerRight ((unit F G).app (x, y)) (H.obj z)) (CategoryStruct.comp ((unit (convolution F G) H).app (tensorObj x y, z)) (CategoryStruct.comp ((convolution (convolution F G) H).map (MonoidalCategoryStruct.associator x y z).hom) h)))

Characterizing the inverse direction of the associator with respect to the unit transformations

theorem CategoryTheory.MonoidalCategory.DayConvolution.associator_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] {H : Functor C V} [DayConvolution G H] [DayConvolution F (convolution G H)] [DayConvolution (convolution F G) H] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] {F' G' H' : Functor C V} [DayConvolution F' G'] [DayConvolution G' H'] [DayConvolution F' (convolution G' H')] [DayConvolution (convolution F' G') H'] (f : F ⟶ F') (g : G ⟶ G') (h : H ⟶ H') : CategoryStruct.comp (map (map f g) h) (associator F' G' H').hom = CategoryStruct.comp (associator F G H).hom (map f (map g h))

theorem CategoryTheory.MonoidalCategory.DayConvolution.pentagon {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] [∀ (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 × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (H K : Functor C V) [DayConvolution G H] [DayConvolution (convolution F G) H] [DayConvolution F (convolution G H)] [DayConvolution H K] [DayConvolution G (convolution H K)] [DayConvolution (convolution G H) K] [DayConvolution (convolution (convolution F G) H) K] [DayConvolution (convolution F G) (convolution H K)] [DayConvolution (convolution F (convolution G H)) K] [DayConvolution F (convolution G (convolution H K))] [DayConvolution F (convolution (convolution G H) K)] : CategoryStruct.comp (map (associator F G H).hom (CategoryStruct.id K)) (CategoryStruct.comp (associator F (convolution G H) K).hom (map (CategoryStruct.id F) (associator G H K).hom)) = CategoryStruct.comp (associator (convolution F G) H K).hom (associator F G (convolution H K)).hom

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.

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.

instance CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitRightφ {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] : (externalProduct F U).IsLeftKanExtension (ExternalProduct.extensionUnitRight U (φ U) F)

instance CategoryTheory.MonoidalCategory.DayConvolutionUnit.instIsLeftKanExtensionProdDiscretePUnitExternalProductExtensionUnitLeftφ {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] : (externalProduct U F).IsLeftKanExtension (ExternalProduct.extensionUnitLeft U (φ U) F)

def CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (Discrete PUnit.{1} × C) (C × C) V).obj ((Functor.fromPUnit (tensorUnit C)).prod (Functor.id C))).comp (coyoneda.obj (Opposite.op (externalProduct (Functor.fromPUnit (tensorUnit V)) F))))).CorepresentableBy (DayConvolution.convolution U F)

A CorepresentableBy structure that characterizes maps out of U ⊛ F by leveraging the fact that U ⊠ F is a left Kan extension of (fromPUnit 𝟙_ V) ⊠ F.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByLeft_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] {Y✝ : Functor C V} : (corepresentableByLeft U F).homEquiv = ((DayConvolution.convolution U F).homEquivOfIsLeftKanExtension (DayConvolution.unit U F) Y✝).trans ((externalProduct U F).homEquivOfIsLeftKanExtension (ExternalProduct.extensionUnitLeft U (φ U) F) ((tensor C).comp Y✝))

def CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C)))).comp (coyoneda.obj (Opposite.op (externalProduct F (Functor.fromPUnit (tensorUnit V))))))).CorepresentableBy (DayConvolution.convolution F U)

A CorepresentableBy structure that characterizes maps out of F ⊛ U by leveraging the fact that F ⊠ U is a left Kan extension of F ⊠ (fromPUnit 𝟙_ V).

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.corepresentableByRight_homEquiv {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] {Y✝ : Functor C V} : (corepresentableByRight U F).homEquiv = ((DayConvolution.convolution F U).homEquivOfIsLeftKanExtension (DayConvolution.unit F U) Y✝).trans ((externalProduct F U).homEquivOfIsLeftKanExtension (ExternalProduct.extensionUnitRight U (φ U) F) ((tensor C).comp Y✝))

def CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : Functor C V) : ((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (Discrete PUnit.{1} × C) (C × C) V).obj ((Functor.fromPUnit (tensorUnit C)).prod (Functor.id C))).comp (coyoneda.obj (Opposite.op (externalProduct (Functor.fromPUnit (tensorUnit V)) F)))) ≅ coyoneda.obj (Opposite.op F)

The isomorphism of corepresentable functors that defines the left unitor for Day convolution.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F X : Functor C V) (a✝ : (coyoneda.obj (Opposite.op (Functor.fromPUnit (tensorUnit V), F).2)).obj X) (X✝ : Discrete PUnit.{1} × C) : ((leftUnitorCorepresentingIso F).inv.app X a✝).app X✝ = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X✝.2)).hom (CategoryStruct.comp (a✝.app X✝.2) (CategoryStruct.comp (X.map ((prod.leftUnitorEquivalence C).unit.app X✝).2) (CategoryStruct.comp (X.map ((prod.leftUnitorEquivalence C).unitInv.app X✝).2) (X.map (MonoidalCategoryStruct.leftUnitor X✝.2).inv))))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitorCorepresentingIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F X : Functor C V) (a✝ : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (Discrete PUnit.{1} × C) (C × C) V).obj ((Functor.fromPUnit (tensorUnit C)).prod (Functor.id C))).comp (coyoneda.obj (Opposite.op (externalProduct (Functor.fromPUnit (tensorUnit V)) F))))).obj X) (X✝ : C) : ((leftUnitorCorepresentingIso F).hom.app X a✝).app X✝ = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj X✝)).inv (CategoryStruct.comp (((prod.leftUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv a✝).app X✝) (X.map (MonoidalCategoryStruct.leftUnitor X✝).hom))

def CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : Functor C V) : ((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C)))).comp (coyoneda.obj (Opposite.op (externalProduct F (Functor.fromPUnit (tensorUnit V)))))) ≅ coyoneda.obj (Opposite.op F)

The isomorphism of corepresentable functors that defines the right unitor for Day convolution.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_inv_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F X : Functor C V) (a✝ : (coyoneda.obj (Opposite.op (F, Functor.fromPUnit (tensorUnit V)).1)).obj X) (X✝ : C × Discrete PUnit.{1}) : ((rightUnitorCorepresentingIso F).inv.app X a✝).app X✝ = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X✝.1)).hom (CategoryStruct.comp (a✝.app X✝.1) (CategoryStruct.comp (X.map ((prod.rightUnitorEquivalence C).unit.app X✝).1) (CategoryStruct.comp (X.map ((prod.rightUnitorEquivalence C).unitInv.app X✝).1) (X.map (MonoidalCategoryStruct.rightUnitor X✝.1).inv))))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitorCorepresentingIso_hom_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F X : Functor C V) (a✝ : (((Functor.whiskeringLeft (C × C) C V).obj (tensor C)).comp (((Functor.whiskeringLeft (C × Discrete PUnit.{1}) (C × C) V).obj ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C)))).comp (coyoneda.obj (Opposite.op (externalProduct F (Functor.fromPUnit (tensorUnit V))))))).obj X) (X✝ : C) : ((rightUnitorCorepresentingIso F).hom.app X a✝).app X✝ = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj X✝)).inv (CategoryStruct.comp (((prod.rightUnitorEquivalence C).congrLeft.fullyFaithfulFunctor.homEquiv a✝).app X✝) (X.map (MonoidalCategoryStruct.rightUnitor X✝).hom))

def CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] : DayConvolution.convolution U F ≅ F

The left unitor isomorphism for Day convolution.

def CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] : DayConvolution.convolution F U ≅ F

The right unitor isomorphism for Day convolution.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] (y : C) : CategoryStruct.comp (whiskerRight can (F.obj y)) (CategoryStruct.comp ((DayConvolution.unit U F).app (tensorUnit C, y)) ((leftUnitor U F).hom.app (tensorObj (tensorUnit C) y))) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj y)).hom (F.map (MonoidalCategoryStruct.leftUnitor y).inv)

Characterizing the forward direction of leftUnitor via the universal maps.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_hom_unit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] (y : C) {Z : V} (h : F.obj (tensorObj (tensorUnit C) y) ⟶ Z) : CategoryStruct.comp (whiskerRight can (F.obj y)) (CategoryStruct.comp ((DayConvolution.unit U F).app (tensorUnit C, y)) (CategoryStruct.comp ((leftUnitor U F).hom.app (tensorObj (tensorUnit C) y)) h)) = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj y)).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.leftUnitor y).inv) h)

Characterizing the forward direction of leftUnitor via the universal maps.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] (x : C) : (leftUnitor U F).inv.app x = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj x)).inv (CategoryStruct.comp (whiskerRight can (F.obj x)) (CategoryStruct.comp ((DayConvolution.unit U F).app (tensorUnit C, x)) ((DayConvolution.convolution U F).map (MonoidalCategoryStruct.leftUnitor x).hom)))

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_inv_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] (x : C) {Z : V} (h : (DayConvolution.convolution U F).obj x ⟶ Z) : CategoryStruct.comp ((leftUnitor U F).inv.app x) h = CategoryStruct.comp (MonoidalCategoryStruct.leftUnitor (F.obj x)).inv (CategoryStruct.comp (whiskerRight can (F.obj x)) (CategoryStruct.comp ((DayConvolution.unit U F).app (tensorUnit C, x)) (CategoryStruct.comp ((DayConvolution.convolution U F).map (MonoidalCategoryStruct.leftUnitor x).hom) h)))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] {F : Functor C V} [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] {G : Functor C V} [DayConvolution U G] (f : F ⟶ G) : CategoryStruct.comp (DayConvolution.map (CategoryStruct.id U) f) (leftUnitor U G).hom = CategoryStruct.comp (leftUnitor U F).hom f

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.leftUnitor_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] {F : Functor C V} [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [DayConvolution U F] {G : Functor C V} [DayConvolution U G] (f : F ⟶ G) {Z : Functor C V} (h : G ⟶ Z) : CategoryStruct.comp (DayConvolution.map (CategoryStruct.id U) f) (CategoryStruct.comp (leftUnitor U G).hom h) = CategoryStruct.comp (leftUnitor U F).hom (CategoryStruct.comp f h)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] (x : C) : CategoryStruct.comp (whiskerLeft (F.obj x) can) (CategoryStruct.comp ((DayConvolution.unit F U).app (x, tensorUnit C)) ((rightUnitor U F).hom.app (tensorObj x (tensorUnit C)))) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj x)).hom (F.map (MonoidalCategoryStruct.rightUnitor x).inv)

Characterizing the forward direction of rightUnitor via the universal maps.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_hom_unit_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] (x : C) {Z : V} (h : F.obj (tensorObj x (tensorUnit C)) ⟶ Z) : CategoryStruct.comp (whiskerLeft (F.obj x) can) (CategoryStruct.comp ((DayConvolution.unit F U).app (x, tensorUnit C)) (CategoryStruct.comp ((rightUnitor U F).hom.app (tensorObj x (tensorUnit C))) h)) = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj x)).hom (CategoryStruct.comp (F.map (MonoidalCategoryStruct.rightUnitor x).inv) h)

Characterizing the forward direction of rightUnitor via the universal maps.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] (x : C) : (rightUnitor U F).inv.app x = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj x)).inv (CategoryStruct.comp (whiskerLeft (F.obj x) can) (CategoryStruct.comp ((DayConvolution.unit F U).app (x, tensorUnit C)) ((DayConvolution.convolution F U).map (MonoidalCategoryStruct.rightUnitor x).hom)))

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] (F : Functor C V) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] (x : C) {Z : V} (h : (DayConvolution.convolution F U).obj x ⟶ Z) : CategoryStruct.comp ((rightUnitor U F).inv.app x) h = CategoryStruct.comp (MonoidalCategoryStruct.rightUnitor (F.obj x)).inv (CategoryStruct.comp (whiskerLeft (F.obj x) can) (CategoryStruct.comp ((DayConvolution.unit F U).app (x, tensorUnit C)) (CategoryStruct.comp ((DayConvolution.convolution F U).map (MonoidalCategoryStruct.rightUnitor x).hom) h)))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] {F : Functor C V} [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] {G : Functor C V} [DayConvolution G U] (f : F ⟶ G) : CategoryStruct.comp (DayConvolution.map f (CategoryStruct.id U)) (rightUnitor U G).hom = CategoryStruct.comp (rightUnitor U F).hom f

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (U : Functor C V) [DayConvolutionUnit U] {F : Functor C V} [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [DayConvolution F U] {G : Functor C V} [DayConvolution G U] (f : F ⟶ G) {Z : Functor C V} (h : G ⟶ Z) : CategoryStruct.comp (DayConvolution.map f (CategoryStruct.id U)) (CategoryStruct.comp (rightUnitor U G).hom h) = CategoryStruct.comp (rightUnitor U F).hom (CategoryStruct.comp f h)

theorem CategoryTheory.MonoidalCategory.DayConvolution.triangle {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory 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)] (F G U : Functor C V) [DayConvolutionUnit U] [DayConvolution F U] [DayConvolution U G] [DayConvolution F (convolution U G)] [DayConvolution (convolution F U) G] [DayConvolution F G] : CategoryStruct.comp (associator F U G).hom (map (CategoryStruct.id F) (DayConvolutionUnit.leftUnitor U G).hom) = map (DayConvolutionUnit.rightUnitor U F).hom (CategoryStruct.id G)

class CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] : Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)

The class DayConvolutionMonoidalCategory C V D bundles the necessary data to turn a monoidal category D into a monoidal full subcategory of a category of functors C ⥤ V endowed with a Day convolution monoidal structure. The design of this class is to bundle a fully faithful functor into C ⥤ V with left extensions on its values representing the fact that it maps tensors products in D to Day convolutions, and furthermore ask that this data is "lawful", i.e that once realized in the functor category, the objects behave like the corresponding ones in the category C ⥤ V.

• ι : Functor D (Functor C V)

  a functor that interprets element of D as functors C ⥤ V

• convolutionExtensionUnit (d d' : D) : externalProduct ((ι C V D).obj d) ((ι C V D).obj d') ⟶ (tensor C).comp ((ι C V D).obj (tensorObj d d'))

  a natural transformation ι.obj d ⊠ ι.obj d' ⟶ tensor C ⋙ ι.obj (d ⊗ d')

• isPointwiseLeftKanExtensionConvolutionExtensionUnit (d d' : D) : (Functor.LeftExtension.mk ((ι C V D).obj (tensorObj d d')) (convolutionExtensionUnit C V d d')).IsPointwiseLeftKanExtension

  convolutionUnitUnit exhibits ι.obj (d ⊗ d') as a left Ken extension of ι.obj d ⊠ ι.obj d' along tensor C.

• unitUnit : tensorUnit V ⟶ ((ι C V D).obj (tensorUnit D)).obj (tensorUnit C)

  a map 𝟙_ V ⟶ (ι.obj <| 𝟙_ D).obj (𝟙_ C), that we think of as defining a natural transformation fromPUnit.{0} (𝟙_ V) ⟶ Functor.fromPUnit.{0} (𝟙_ C) ⋙ (ι.obj <| 𝟙_ D).

• isPointwiseLeftKanExtensionUnitUnit : (Functor.LeftExtension.mk ((ι C V D).obj (tensorUnit D)) { app := fun (x : Discrete PUnit.{1}) => unitUnit C V D, naturality := ⋯ }).IsPointwiseLeftKanExtension

  the natural transformation induced by unitUnit exhibits (ι.obj <| 𝟙_ D).obj (𝟙_ C) as a left Kan extension of fromPUnit.{0} (𝟙_ V) as a along fromPUnit.{0} (𝟙_ C).

• faithful_ι : (ι C V D).Faithful

  The field ι interprets an element of D as a functor C ⥤ V.

• convolutionExtensionUnit_comp_ι_map_tensorHom_app {d₁ d₂ d₁' d₂' : D} (f₁ : d₁ ⟶ d₁') (f₂ : d₂ ⟶ d₂') (x y : C) : CategoryStruct.comp ((convolutionExtensionUnit C V d₁ d₂).app (x, y)) (((ι C V D).map (tensorHom f₁ f₂)).app (tensorObj x y)) = CategoryStruct.comp (tensorHom (((ι C V D).map f₁).app x) (((ι C V D).map f₂).app y)) ((convolutionExtensionUnit C V d₁' d₂').app (x, y))
• convolutionExtensionUnit_comp_ι_map_whiskerLeft_app (d₁ : D) {d₂ d₂' : D} (f₂ : d₂ ⟶ d₂') (x y : C) : CategoryStruct.comp ((convolutionExtensionUnit C V d₁ d₂).app (x, y)) (((ι C V D).map (whiskerLeft d₁ f₂)).app (tensorObj x y)) = CategoryStruct.comp (whiskerLeft (((ι C V D).obj d₁).obj x) (((ι C V D).map f₂).app y)) ((convolutionExtensionUnit C V d₁ d₂').app (x, y))
• convolutionExtensionUnit_comp_ι_map_whiskerRight_app {d₁ d₁' : D} (f₁ : d₁ ⟶ d₁') (d₂ : D) (x y : C) : CategoryStruct.comp ((convolutionExtensionUnit C V d₁ d₂).app (x, y)) (((ι C V D).map (whiskerRight f₁ d₂)).app (tensorObj x y)) = CategoryStruct.comp (whiskerRight (((ι C V D).map f₁).app x) (((ι C V D).obj d₂).obj y)) ((convolutionExtensionUnit C V d₁' d₂).app (x, y))
• associator_hom_unit_unit (d d' d'' : D) (x y z : C) : CategoryStruct.comp (whiskerRight ((convolutionExtensionUnit C V d d').app (x, y)) (((ι C V D).obj d'').obj z)) (CategoryStruct.comp ((convolutionExtensionUnit C V (tensorObj d d') d'').app (tensorObj x y, z)) (((ι C V D).map (associator d d' d'').hom).app (tensorObj (tensorObj x y) z))) = CategoryStruct.comp (associator (((ι C V D).obj d).obj x) (((ι C V D).obj d', (ι C V D).obj d'').1.obj (y, z).1) (((ι C V D).obj d', (ι C V D).obj d'').2.obj (y, z).2)).hom (CategoryStruct.comp (whiskerLeft (((ι C V D).obj d).obj x) ((convolutionExtensionUnit C V d' d'').app (y, z))) (CategoryStruct.comp ((convolutionExtensionUnit C V d (tensorObj d' d'')).app (x, tensorObj y z)) (((ι C V D).obj (tensorObj d (tensorObj d' d''))).map (associator (x, tensorObj y z).1 y z).inv)))
• leftUnitor_hom_unit_app (d : D) (y : C) : CategoryStruct.comp (whiskerRight (unitUnit C V D) (((ι C V D).obj d).obj y)) (CategoryStruct.comp ((convolutionExtensionUnit C V (tensorUnit D) d).app (tensorUnit C, y)) (((ι C V D).map (leftUnitor d).hom).app (tensorObj (tensorUnit C) y))) = CategoryStruct.comp (leftUnitor (((ι C V D).obj d).obj y)).hom (((ι C V D).obj d).map (leftUnitor y).inv)
• rightUnitor_hom_unit_app (d : D) (y : C) : CategoryStruct.comp (whiskerLeft (((ι C V D).obj d).obj y) (unitUnit C V D)) (CategoryStruct.comp ((convolutionExtensionUnit C V d (tensorUnit D)).app (y, tensorUnit C)) (((ι C V D).map (rightUnitor d).hom).app (tensorObj y (tensorUnit C)))) = CategoryStruct.comp (rightUnitor (((ι C V D).obj d).obj y)).hom (((ι C V D).obj d).map (rightUnitor y).inv)

def CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d d' : D) : DayConvolution ((ι C V D).obj d) ((ι C V D).obj d')

In a LawfulDayConvolutionMonoidalCategoryStruct, ι.obj (d ⊗ d') is a Day convolution of (ι C V).obj d and (ι C V).d'.

def CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution₂ (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d d' d'' : D) : DayConvolution ((ι C V D).obj d) (DayConvolution.convolution ((ι C V D).obj d') ((ι C V D).obj d''))

In a LawfulDayConvolutionMonoidalCategoryStruct, ι.obj (d ⊗ d' ⊗ d'') is a (triple) Day convolution of (ι C V).obj d, (ι C V).obj d' and (ι C V).obj d''.

def CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution₂' (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d d' d'' : D) : DayConvolution (DayConvolution.convolution ((ι C V D).obj d) ((ι C V D).obj d')) ((ι C V D).obj d'')

In a LawfulDayConvolutionMonoidalCategoryStruct, ι.obj ((d ⊗ d') ⊗ d'') is a (triple) Day convolution of (ι C V).obj d, (ι C V).obj d' and (ι C V).obj d''.

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_tensorHom_hom_eq_tensorHom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') : (ι C V D).map (tensorHom f f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_associator_hom_eq_associator_hom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d d' d'' : D) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] : (ι C V D).map (associator d d' d'').hom = (DayConvolution.associator ((ι C V D).obj d) ((ι C V D).obj d') ((ι C V D).obj d'')).hom

def CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolutionUnit (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] : DayConvolutionUnit ((ι C V D).obj (tensorUnit D))

In a LawfulDayConvolutionMonoidalCategoryStruct, ι.obj (𝟙_ D) is a Day convolution unit.

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_leftUnitor_hom_eq_leftUnitor_hom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] : (ι C V D).map (leftUnitor d).hom = (DayConvolutionUnit.leftUnitor ((ι C V D).obj (tensorUnit D)) ((ι C V D).obj d)).hom

theorem CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι_map_rightUnitor_hom_eq_rightUnitor_hom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] (d : D) [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] : (ι C V D).map (rightUnitor d).hom = (DayConvolutionUnit.rightUnitor ((ι C V D).obj (tensorUnit D)) ((ι C V D).obj d)).hom

def CategoryTheory.MonoidalCategory.monoidalOfLawfulDayConvolutionMonoidalCategoryStruct (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [MonoidalCategoryStruct D] [LawfulDayConvolutionMonoidalCategoryStruct C V D] [∀ (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)] : MonoidalCategory D

We can promote a LawfulDayConvolutionMonoidalCategoryStruct to a monoidal category, note that every non-prop data is already here, so this is just about showing that they satisfy the axioms of a monoidal category.

In what follows, we give a constructor for LawfulDayConvolutionMonoidalCategoryStruct that does not assume a pre-existing MonoidalCategoryStruct and builds one from the data of suitable convolutions, while giving definitional control over as many parameters as we can.

class CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] : Type (max (max (max (max (max u₁ u₂) u₃) v₁) v₂) v₃)

An InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D bundles the core data needed to construct a full LawfulDayConvolutionMonoidalCategoryStructCore. We are making this a class so that it can act as a "proxy" for inferring DayConvolution instances (which is all the more important that we are modifying the instances given in the constructor to get better ones defeq-wise). As this object is purely about the internals of definitions of Day convolutions monoidal structures, it is advised to not register this class globally.

• ι : Functor D (Functor C V)

  A functor that interprets elements of D as functors C ⥤ V.

• fullyFaithulι : (ι C V D).FullyFaithful

  The functor ι is fully faithful.

• tensorObj : D → D → D

  Candidate function for the tensor product of objects.

• convolutions' (d d' : D) : DayConvolution ((ι C V D).obj d) ((ι C V D).obj d')

  First candidate Day convolutions between objects. Note that the name here is primed as in fact, we will use the other fields in this class to produce convolutions with more controlled defeq properties.

• tensorObjIsoConvolution (d d' : D) : (ι C V D).obj (tensorObj C V d d') ≅ DayConvolution.convolution ((ι C V D).obj d) ((ι C V D).obj d')

  Isomorphisms that exhibits the essential image of ι as closed under day convolution.

• convolutionUnitApp (d d' : D) (x y : C) : MonoidalCategoryStruct.tensorObj (((ι C V D).obj d).obj x) (((ι C V D).obj d').obj y) ⟶ ((ι C V D).obj (tensorObj C V d d')).obj (MonoidalCategoryStruct.tensorObj x y)

  Candidate component of units for the LawfulDayConvolutionMonoidalCategoryStruct, this defaults to the ones deduced by convolutions' and tensorObjIsoConvolution.

• convolutionUnitApp_eq (d d' : D) (x y : C) : convolutionUnitApp V d d' x y = CategoryStruct.comp ((DayConvolution.unit ((ι C V D).obj d) ((ι C V D).obj d')).app (x, y)) ((tensorObjIsoConvolution C V d d').inv.app (MonoidalCategoryStruct.tensorObj x y))

  Lawfulness of convolutionUnitApp.

• tensorHom {d₁ d₂ d₁' d₂' : D} : (d₁ ⟶ d₂) → (d₁' ⟶ d₂') → (tensorObj C V d₁ d₁' ⟶ tensorObj C V d₂ d₂')

  Candidate tensorHom. This defaults to the one that corresponds to DayConvolution.map through convolutions'.

• tensorHom_eq {d₁ d₂ d₁' d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') : (ι C V D).map (tensorHom f f') = CategoryStruct.comp (tensorObjIsoConvolution C V d₁ d₁').hom (CategoryStruct.comp (DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')) (tensorObjIsoConvolution C V d₂ d₂').inv)

  Lawfulness of tensorHom.

• tensorUnit : D

  Candidate tensor unit.

• tensorUnitConvolutionUnit : DayConvolutionUnit ((ι C V D).obj (tensorUnit C V D))

  DayConvolutionUnit structure on the candidate.

def CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.convolutions (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {D : Type u₃} [Category.{v₃, u₃} D] [InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] (d d' : D) : DayConvolution ((ι C V D).obj d) ((ι C V D).obj d')

With the data of chosen isomorphic objects to given day convolutions, and provably equal unit maps through these isomorphisms, we can transform a given family of Day convolutions to one with convolutions definitionally equals to the given objects, and component of units definitionally equal to the provided map family.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mkMonoidalCategoryStruct (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] [∀ (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 (MonoidalCategoryStruct.tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (tensorLeft v)] : MonoidalCategoryStruct D

Given a fully faithful functor ι : C ⥤ V ⥤ D, a family of Day convolutions, candidate functions for tensorObj and tensorHom, suitable isomorphisms ι.obj (tensorObj d d') ≅ ι.obj (tensorObj d) ⊛ ι.obj (tensorObj d') that behave in a lawful way with respect to the chosen Day convolutions, we can construct a MonoidalCategoryStruct on D.

theorem CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.id_tensorHom (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] [∀ (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 (MonoidalCategoryStruct.tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (tensorLeft v)] (x : D) {y y' : D} (f : y ⟶ y') : MonoidalCategoryStruct.tensorHom (CategoryStruct.id x) f = whiskerLeft x f

theorem CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.tensorHom_id (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] [∀ (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 (MonoidalCategoryStruct.tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (tensorLeft v)] {x x' : D} (f : x ⟶ x') (y : D) : MonoidalCategoryStruct.tensorHom f (CategoryStruct.id y) = whiskerRight f y

theorem CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ι_map_tensorHom_eq (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] [∀ (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 (MonoidalCategoryStruct.tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (tensorLeft v)] {d₁ d₁' d₂ d₂' : D} (f : d₁ ⟶ d₂) (f' : d₁' ⟶ d₂') : (ι C V D).map (MonoidalCategoryStruct.tensorHom f f') = DayConvolution.map ((ι C V D).map f) ((ι C V D).map f')

def CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.mkLawfulDayConvolutionMonoidalCategoryStruct (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (D : Type u₃) [Category.{v₃, u₃} D] [InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D] [∀ (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 (MonoidalCategoryStruct.tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)) d) (tensorLeft v)] : LawfulDayConvolutionMonoidalCategoryStruct C V D

The monoidal category struct constructed in DayConvolution.mkMonoidalCategoryStruct extends to a LawfulDayConvolutionMonoidalCategoryStruct.

noncomputable def CategoryTheory.MonoidalCategory.InducedLawfulDayConvolutionMonoidalCategoryStructCore.ofHasDayConvolutions {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {D : Type u₃} [Category.{v₃, u₃} D] (ι : Functor D (Functor C V)) (ffι : ι.FullyFaithful) [hasDayConvolution : ∀ (d d' : D), (tensor C).HasPointwiseLeftKanExtension (externalProduct (ι.obj d) (ι.obj d'))] (essImageDayConvolution : ∀ (d d' : D), ι.essImage ((tensor C).pointwiseLeftKanExtension (externalProduct (ι.obj d) (ι.obj d')))) [hasDayConvolutionUnit : (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V))] (essImageDayConvolutionUnit : ι.essImage ((Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit C)).pointwiseLeftKanExtension (Functor.fromPUnit (MonoidalCategoryStruct.tensorUnit V)))) : InducedLawfulDayConvolutionMonoidalCategoryStructCore C V D

Given a fully faithful functor ι : D ⥤ C ⥤ V and mere existence of Day convolutions of ι.obj d and ι.obj d' such that the convolution remains in the essential image of ι, construct an InducedLawfulDayConvolutionMonoidalCategoryStructCore by letting all other data be the generic ones from the HasPointwiseLeftKanExtension API.

noncomputable def CategoryTheory.MonoidalCategory.monoidalOfHasDayConvolutions {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {D : Type u₃} [Category.{v₃, u₃} D] (ι : Functor D (Functor C V)) (ffι : ι.FullyFaithful) [hasDayConvolution : ∀ (d d' : D), (tensor C).HasPointwiseLeftKanExtension (externalProduct (ι.obj d) (ι.obj d'))] (essImageDayConvolution : ∀ (d d' : D), ι.essImage ((tensor C).pointwiseLeftKanExtension (externalProduct (ι.obj d) (ι.obj d')))) [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] (essImageDayConvolutionUnit : ι.essImage ((Functor.fromPUnit (tensorUnit C)).pointwiseLeftKanExtension (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)] : MonoidalCategory D

Under suitable assumptions on existence of relevant Kan extensions and preservation of relevant colimits by the tensor product of V, we can define a MonoidalCategory D from the data of a fully faithful functor ι : D ⥤ C ⥤ V whose essential image contains a Day convolution unit and is stable under binary Day convolutions.

noncomputable def CategoryTheory.MonoidalCategory.lawfulDayConvolutionMonoidalCategoryStructOfHasDayConvolutions {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {D : Type u₃} [Category.{v₃, u₃} D] (ι : Functor D (Functor C V)) (ffι : ι.FullyFaithful) [hasDayConvolution : ∀ (d d' : D), (tensor C).HasPointwiseLeftKanExtension (externalProduct (ι.obj d) (ι.obj d'))] (essImageDayConvolution : ∀ (d d' : D), ι.essImage ((tensor C).pointwiseLeftKanExtension (externalProduct (ι.obj d) (ι.obj d')))) [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] (essImageDayConvolutionUnit : ι.essImage ((Functor.fromPUnit (tensorUnit C)).pointwiseLeftKanExtension (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)] : LawfulDayConvolutionMonoidalCategoryStruct C V D

The monoidal category constructed via monoidalOfHasDayConvolutions has a canonical LawfulDayConvolutionMonoidalCategoryStruct C V D.