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

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_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))

@[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✝ β

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 coresponsds to the associator isomorphism for Day convolution through corepresentableBy₂ and corepresentableBy₂.

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

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

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 asociator 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)))

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

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_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))

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

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_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))

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

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)

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

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