Day functors

In this file, given a monoidal category C and a monoidal category V, we define a basic type synonym DayFunctor C V (denoted C ⊛⥤ D) for the category C ⥤ V and endow it with the monoidal structure coming from Day convolution. Such a setup is necessary as by default, the MonoidalCategory instance on C ⥤ V is the "pointwise" one, where the tensor product of F and G is the functor x ↦ F.obj x ⊗ G.obj x.

TODOs

• Given a LawfulDayConvolutionMonoidalCategoryStruct C V D, show that ι induces a monoidal functor D ⥤ (C ⊛⥤ V).
• Specialize to the case V := Type _, and prove a universal property stating that for every monoidal category W with suitable colimits, colimit-preserving monoidal functors (Cᵒᵖ ⊛⥤ Type u) ⥤ W are equivalent to monoidal functors C ⥤ W. Show that the Yoneda embedding is monoidal.

structure CategoryTheory.MonoidalCategory.DayFunctor (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] : Type (max (max (max u₁ u₂) v₁) v₂)

DayFunctor C V is a type synonym for C ⥤ V, implemented as a one-field structure.

• functor : Functor C V

  the underlying functor.

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

Notation for DayFunctor.

theorem CategoryTheory.MonoidalCategory.DayFunctor.mk_functor {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : Functor C V) : { functor := F }.functor = F

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.functor_mk {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : DayFunctor C V) : { functor := F.functor } = F

structure CategoryTheory.MonoidalCategory.DayFunctor.Hom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F G : DayFunctor C V) : Type (max u₁ v₂)

Morphisms of Day functors are natural transformations of the underlying functors.

• natTrans : F.functor ⟶ G.functor

  the underlying natural transformation

instance CategoryTheory.MonoidalCategory.DayFunctor.instCategory {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] : Category.{max u₁ v₂, max (max (max u₂ u₁) v₂) v₁} (DayFunctor C V)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.comp_natTrans {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {X✝ Y✝ Z✝ : DayFunctor C V} (α : X✝.Hom Y✝) (β : Y✝.Hom Z✝) : (CategoryStruct.comp α β).natTrans = CategoryStruct.comp α.natTrans β.natTrans

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.id_natTrans {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (x : DayFunctor C V) : (CategoryStruct.id x).natTrans = CategoryStruct.id x.functor

theorem CategoryTheory.MonoidalCategory.DayFunctor.hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : DayFunctor C V} {α β : F ⟶ G} (h : α.natTrans = β.natTrans) : α = β

theorem CategoryTheory.MonoidalCategory.DayFunctor.hom_ext_iff {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {F G : DayFunctor C V} {α β : F ⟶ G} : α = β ↔ α.natTrans = β.natTrans

def CategoryTheory.MonoidalCategory.DayFunctor.equiv (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] : DayFunctor C V ≌ Functor C V

The tautological equivalence of categories between C ⥤ V and C ⊛⥤ V.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_map (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {X✝ Y✝ : DayFunctor C V} (α : X✝ ⟶ Y✝) : (equiv C V).functor.map α = α.natTrans

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_obj_functor (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : Functor C V) : ((equiv C V).inverse.obj F).functor = F

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_functor_obj (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (F : DayFunctor C V) : (equiv C V).functor.obj F = F.functor

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (X : Functor C V) : (equiv C V).counitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_unitIso_inv_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (X : DayFunctor C V) : (equiv C V).unitIso.inv.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_unitIso_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (X : DayFunctor C V) : (equiv C V).unitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_counitIso_hom_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] (X : Functor C V) : (equiv C V).counitIso.hom.app X = CategoryStruct.id X

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.equiv_inverse_map_natTrans (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] {X✝ Y✝ : Functor C V} (α : X✝ ⟶ Y✝) : ((equiv C V).inverse.map α).natTrans = α

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

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ι_map {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {X✝ Y✝ : DayFunctor C V} (α : X✝ ⟶ Y✝) : (LawfulDayConvolutionMonoidalCategoryStruct.ι C V (DayFunctor C V)).map α = α.natTrans

@[simp]

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

def CategoryTheory.MonoidalCategory.DayFunctor.η {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G : DayFunctor C V) : externalProduct F.functor G.functor ⟶ (tensor C).comp (tensorObj F G).functor

The unit transformation exhibiting (F ⊗ G).functor as a left Kan extension of F.functor ⊠ G.functor along tensor C.

instance CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionProdFunctorTensorObjη {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G : DayFunctor C V) : (tensorObj F G).functor.IsLeftKanExtension (F.η G)

theorem CategoryTheory.MonoidalCategory.DayFunctor.tensor_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G H : DayFunctor C V} {α β : tensorObj F G ⟶ H} (h : ∀ (x y : C), CategoryStruct.comp ((F.η G).app (x, y)) (α.natTrans.app (tensorObj x y)) = CategoryStruct.comp ((F.η G).app (x, y)) (β.natTrans.app (tensorObj x y))) : α = β

def CategoryTheory.MonoidalCategory.DayFunctor.tensorDesc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G H : DayFunctor C V} (α : externalProduct F.functor G.functor ⟶ (tensor C).comp H.functor) : tensorObj F G ⟶ H

A natural transformation F.functor ⊠ G.functor ⟶ tensor C ⋙ H.functor defines a morphism F ⨂ G ⟶ H.

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDec {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G H : DayFunctor C V} (α : externalProduct F.functor G.functor ⟶ (tensor C).comp H.functor) : CategoryStruct.comp (F.η G) ((tensor C).whiskerLeft (tensorDesc α).natTrans) = α

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDesc_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G H : DayFunctor C V} (α : externalProduct F.functor G.functor ⟶ (tensor C).comp H.functor) (x y : C) : CategoryStruct.comp ((F.η G).app (x, y)) ((tensorDesc α).natTrans.app (tensorObj x y)) = α.app (x, y)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_comp_tensorDesc_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F G H : DayFunctor C V} (α : externalProduct F.functor G.functor ⟶ (tensor C).comp H.functor) (x y : C) {Z : V} (h : H.functor.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((F.η G).app (x, y)) (CategoryStruct.comp ((tensorDesc α).natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (α.app (x, y)) h

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

An abstract isomorphism between (F ⊗ G).functor and the generic pointwise left Kan extension of F.functor ⊠ G.functor along the

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_comp_isoPointwiseLeftKanExtension_hom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G : DayFunctor C V) (x y : C) : CategoryStruct.comp ((F.η G).app (x, y)) ((F.isoPointwiseLeftKanExtension G).hom.app (tensorObj x y)) = Limits.colimit.ι ((CostructuredArrow.proj (tensor C) (tensorObj x y)).comp (externalProduct F.functor G.functor)) (CostructuredArrow.mk (CategoryStruct.id (tensorObj x y)))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ι_comp_isoPointwiseLeftKanExtension_inv {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (F G : DayFunctor C V) (x y : C) : CategoryStruct.comp (Limits.colimit.ι ((CostructuredArrow.proj (tensor C) (tensorObj x y)).comp (externalProduct F.functor G.functor)) (CostructuredArrow.mk (CategoryStruct.id (tensorObj x y)))) ((F.isoPointwiseLeftKanExtension G).inv.app (tensorObj x y)) = (F.η G).app (x, y)

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

The canonical map 𝟙_ V ⟶ (𝟙_ (C ⊛⥤ V)).functor.obj (𝟙_ C) that exhibits (𝟙_ (C ⊛⥤ V)).functor as a Day convolution unit.

def CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] : Functor.fromPUnit (tensorUnit V) ⟶ (Functor.fromPUnit (tensorUnit C)).comp (tensorUnit (DayFunctor C V)).functor

The reinterpretation of ν as a natural transformation.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.νNatTrans_app (C : Type u₁) [Category.{v₁, u₁} C] (V : Type u₂) [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] (x✝ : Discrete PUnit.{1}) : (νNatTrans C V).app x✝ = ν C V

instance CategoryTheory.MonoidalCategory.DayFunctor.instIsLeftKanExtensionDiscretePUnitFunctorTensorUnitνNatTrans {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] : (tensorUnit (DayFunctor C V)).functor.IsLeftKanExtension (νNatTrans C V)

theorem CategoryTheory.MonoidalCategory.DayFunctor.unit_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F : DayFunctor C V} {α β : tensorUnit (DayFunctor C V) ⟶ F} (h : CategoryStruct.comp (ν C V) (α.natTrans.app (tensorUnit C)) = CategoryStruct.comp (ν C V) (β.natTrans.app (tensorUnit C))) : α = β

def CategoryTheory.MonoidalCategory.DayFunctor.unitDesc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F : DayFunctor C V} (φ : tensorUnit V ⟶ F.functor.obj (tensorUnit C)) : tensorUnit (DayFunctor C V) ⟶ F

Given F : C ⊛⥤ V, a morphism 𝟙_ V ⟶ F.functor.obj (𝟙_ C) induces a (unique) morphism 𝟙_ (C ⊛⥤ V) ⟶ F.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_unitDesc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F : DayFunctor C V} (φ : tensorUnit V ⟶ F.functor.obj (tensorUnit C)) : CategoryStruct.comp (ν C V) ((unitDesc φ).natTrans.app (tensorUnit C)) = φ

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_unitDesc_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [hasDayConvolution : ∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [hasDayConvolutionUnit : (Functor.fromPUnit (tensorUnit C)).HasPointwiseLeftKanExtension (Functor.fromPUnit (tensorUnit V))] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (tensor C) d) (tensorRight v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorLeft v)] [∀ (v : V) (d : C), Limits.PreservesColimitsOfShape (CostructuredArrow (Functor.fromPUnit (tensorUnit C)) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((Functor.id C).prod (Functor.fromPUnit (tensorUnit C))) d) (tensorRight v)] [∀ (v : V) (d : C × C), Limits.PreservesColimitsOfShape (CostructuredArrow ((tensor C).prod (Functor.id C)) d) (tensorRight v)] {F : DayFunctor C V} (φ : tensorUnit V ⟶ F.functor.obj (tensorUnit C)) {Z : V} (h : F.functor.obj (tensorUnit C) ⟶ Z) : CategoryStruct.comp (ν C V) (CategoryStruct.comp ((unitDesc φ).natTrans.app (tensorUnit C)) h) = CategoryStruct.comp φ h