Day convolution is closed

Let C be a monoidal category and V a monoidal closed category in which every functor Cᵒᵖ ⥤ C ⥤ V has an end. Then the Day convolution monoidal structure on C ⊛⥤ V is closed: the internal hom [F, G] is the functor c ↦ ∫_j [F j, G (j ⊗ c)].

Mathlib's DayConvolutionInternalHom F G H records that H is such an end, and constructs from it the evaluation F ⊛ H ⟶ G, the coevaluation G ⟶ [F, F ⊛ G] and their triangle identities. We choose the ends functorially through endFunctor, so that [F, -] is a functor, check that it satisfies DayConvolutionInternalHom, and assemble the evaluation and coevaluation into an adjunction tensorLeft F ⊣ [F, -]. This turns the construction of Mathlib's CategoryTheory.MonoidalCategory.DayConvolution.Closed into an actual MonoidalClosed instance on C ⊛⥤ V.

Main definitions

• DayFunctor.internalHom F: the internal hom functor [F, -] for Day convolution.
• DayFunctor.dayConvolutionInternalHom F G: [F, G] is an internal hom of F and G in the sense of DayConvolutionInternalHom.
• DayFunctor.internalHomAdjunction F: the adjunction tensorLeft F ⊣ [F, -].
• DayFunctor.monoidalClosed: the MonoidalClosed instance on C ⊛⥤ V.

Main statements

• DayFunctor.η_app_comp_ev_natTrans_app: the evaluation F ⊗ [F, G] ⟶ G, restricted along the Day convolution unit, is the uncurried end projection.
• DayFunctor.coev_natTrans_app_comp_π: the coevaluation G ⟶ [F, F ⊗ G], followed by an end projection, is the curried Day convolution unit.

References

• B. Day, On closed categories of functors, Reports of the Midwest Category Seminar IV, Lecture Notes in Math. 137 (1970), 1–38.

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.internalHom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) : Functor (DayFunctor C V) (DayFunctor C V)

The internal hom functor [F, -] for the Day convolution product: the functor G ↦ [F, G] with [F, G].obj c = ∫_j [F j, G (j ⊗ c)].

theorem CategoryTheory.MonoidalCategory.DayFunctor.internalHom_obj_functor_obj {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) (c : C) : (F.internalHom.obj G).functor.obj c = Limits.end_ (((dayConvolutionInternalHomDiagramFunctor F.functor).obj G.functor).obj c)

The value of [F, G] at c is the end ∫_j [F j, G (j ⊗ c)].

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) (c j : C) : (F.internalHom.obj G).functor.obj c ⟶ (ihom (F.functor.obj j)).obj (G.functor.obj (tensorObj j c))

The projection [F, G].obj c ⟶ [F j, G (j ⊗ c)] from the end.

theorem CategoryTheory.MonoidalCategory.DayFunctor.π_hom_ext {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] {F G : DayFunctor C V} {c : C} {X : V} {f g : X ⟶ (F.internalHom.obj G).functor.obj c} (h : ∀ (j : C), CategoryStruct.comp f (F.π G c j) = CategoryStruct.comp g (F.π G c j)) : f = g

Morphisms into [F, G].obj c are determined by their composites with the projections.

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] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] {F G : DayFunctor C V} {c : C} {X : V} {f g : X ⟶ (F.internalHom.obj G).functor.obj c} : f = g ↔ ∀ (j : C), CategoryStruct.comp f (F.π G c j) = CategoryStruct.comp g (F.π G c j)

theorem CategoryTheory.MonoidalCategory.DayFunctor.π_comp_ihom_map {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) (c : C) {i j : C} (f : i ⟶ j) : CategoryStruct.comp (F.π G c i) ((ihom (F.functor.obj i)).map (G.functor.map (whiskerRight f c))) = CategoryStruct.comp (F.π G c j) ((MonoidalClosed.pre (F.functor.map f)).app (G.functor.obj (tensorObj j c)))

The projections out of [F, G].obj c form a wedge.

theorem CategoryTheory.MonoidalCategory.DayFunctor.π_comp_ihom_map_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) (c : C) {i j : C} (f : i ⟶ j) {Z : V} (h : (ihom (F.functor.obj i)).obj (G.functor.obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp (F.π G c i) (CategoryStruct.comp ((ihom (F.functor.obj i)).map (G.functor.map (whiskerRight f c))) h) = CategoryStruct.comp (F.π G c j) (CategoryStruct.comp ((MonoidalClosed.pre (F.functor.map f)).app (G.functor.obj (tensorObj j c))) h)

The projections out of [F, G].obj c form a wedge.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.map_natTrans_app_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) {c c' : C} (f : c ⟶ c') (j : C) : CategoryStruct.comp ((F.internalHom.obj G).functor.map f) (F.π G c' j) = CategoryStruct.comp (F.π G c j) ((ihom (F.functor.obj j)).map (G.functor.map (whiskerLeft j f)))

The functoriality of [F, G] in the variable c, along the projections.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.map_natTrans_app_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) {c c' : C} (f : c ⟶ c') (j : C) {Z : V} (h : (ihom (F.functor.obj j)).obj (G.functor.obj (tensorObj j c')) ⟶ Z) : CategoryStruct.comp ((F.internalHom.obj G).functor.map f) (CategoryStruct.comp (F.π G c' j) h) = CategoryStruct.comp (F.π G c j) (CategoryStruct.comp ((ihom (F.functor.obj j)).map (G.functor.map (whiskerLeft j f))) h)

The functoriality of [F, G] in the variable c, along the projections.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.internalHom_map_natTrans_app_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) {G G' : DayFunctor C V} (g : G ⟶ G') (c j : C) : CategoryStruct.comp ((F.internalHom.map g).natTrans.app c) (F.π G' c j) = CategoryStruct.comp (F.π G c j) ((ihom (F.functor.obj j)).map (g.natTrans.app (tensorObj j c)))

The functoriality of [F, -], along the projections.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.internalHom_map_natTrans_app_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) {G G' : DayFunctor C V} (g : G ⟶ G') (c j : C) {Z : V} (h : (ihom (F.functor.obj j)).obj (G'.functor.obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp ((F.internalHom.map g).natTrans.app c) (CategoryStruct.comp (F.π G' c j) h) = CategoryStruct.comp (F.π G c j) (CategoryStruct.comp ((ihom (F.functor.obj j)).map (g.natTrans.app (tensorObj j c))) h)

The functoriality of [F, -], along the projections.

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.dayConvolutionInternalHom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F G : DayFunctor C V) : DayConvolutionInternalHom F.functor G.functor (F.internalHom.obj G).functor

[F, G] is an internal hom of F and G for Day convolution in the sense of Mathlib's DayConvolutionInternalHom: its values are ends, with the projections π.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.dayConvolutionInternalHom_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] {F : DayFunctor C V} (G : DayFunctor C V) (c j : C) : (F.dayConvolutionInternalHom G).π c j = F.π G c j

The projections of dayConvolutionInternalHom F G are the end projections π.

theorem CategoryTheory.MonoidalCategory.DayFunctor.dayConvolutionInternalHom_map {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) {G G' : DayFunctor C V} (g : G ⟶ G') : (F.dayConvolutionInternalHom G).map g.natTrans (F.dayConvolutionInternalHom G') = (F.internalHom.map g).natTrans

The morphism of internal homs that Mathlib's DayConvolutionInternalHom.map induces from a morphism g : G ⟶ G' is the image of g under the functor [F, -].

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.ev {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) : tensorObj F (F.internalHom.obj G) ⟶ G

The evaluation F ⊗ [F, G] ⟶ G of the Day convolution internal hom.

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.coev {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) : G ⟶ F.internalHom.obj (tensorObj F G)

The coevaluation G ⟶ [F, F ⊗ G] of the Day convolution internal hom.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_ev_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) (x y : C) : CategoryStruct.comp ((F.η (F.internalHom.obj G)).app (x, y)) ((F.ev G).natTrans.app (tensorObj x y)) = MonoidalClosed.uncurry (F.π G y x)

The evaluation F ⊗ [F, G] ⟶ G, restricted along the Day convolution unit, is the uncurried projection from the end.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_ev_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) (x y : C) {Z : V} (h : G.functor.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((F.η (F.internalHom.obj G)).app (x, y)) (CategoryStruct.comp ((F.ev G).natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (MonoidalClosed.uncurry (F.π G y x)) h

The evaluation F ⊗ [F, G] ⟶ G, restricted along the Day convolution unit, is the uncurried projection from the end.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.coev_natTrans_app_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) (c j : C) : CategoryStruct.comp ((F.coev G).natTrans.app c) (F.π (tensorObj F G) c j) = MonoidalClosed.curry ((F.η G).app (j, c))

The coevaluation G ⟶ [F, F ⊗ G], followed by a projection from the end, is the curried Day convolution unit.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.coev_natTrans_app_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) (c j : C) {Z : V} (h : (ihom (F.functor.obj j)).obj ((tensorObj F G).functor.obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp ((F.coev G).natTrans.app c) (CategoryStruct.comp (F.π (tensorObj F G) c j) h) = CategoryStruct.comp (MonoidalClosed.curry ((F.η G).app (j, c))) h

The coevaluation G ⟶ [F, F ⊗ G], followed by a projection from the end, is the curried Day convolution unit.

theorem CategoryTheory.MonoidalCategory.DayFunctor.coev_naturality {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G G' : DayFunctor C V} (g : G ⟶ G') : CategoryStruct.comp g (F.coev G') = CategoryStruct.comp (F.coev G) (F.internalHom.map (whiskerLeft F g))

The coevaluation G ⟶ [F, F ⊗ G] is natural in G.

theorem CategoryTheory.MonoidalCategory.DayFunctor.coev_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G G' : DayFunctor C V} (g : G ⟶ G') {Z : DayFunctor C V} (h : F.internalHom.obj (tensorObj F G') ⟶ Z) : CategoryStruct.comp g (CategoryStruct.comp (F.coev G') h) = CategoryStruct.comp (F.coev G) (CategoryStruct.comp (F.internalHom.map (whiskerLeft F g)) h)

The coevaluation G ⟶ [F, F ⊗ G] is natural in G.

theorem CategoryTheory.MonoidalCategory.DayFunctor.ev_naturality {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G G' : DayFunctor C V} (g : G ⟶ G') : CategoryStruct.comp (whiskerLeft F (F.internalHom.map g)) (F.ev G') = CategoryStruct.comp (F.ev G) g

The evaluation F ⊗ [F, G] ⟶ G is natural in G.

theorem CategoryTheory.MonoidalCategory.DayFunctor.ev_naturality_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G G' : DayFunctor C V} (g : G ⟶ G') {Z : DayFunctor C V} (h : G' ⟶ Z) : CategoryStruct.comp (whiskerLeft F (F.internalHom.map g)) (CategoryStruct.comp (F.ev G') h) = CategoryStruct.comp (F.ev G) (CategoryStruct.comp g h)

The evaluation F ⊗ [F, G] ⟶ G is natural in G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.whiskerLeft_coev_comp_ev {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) : CategoryStruct.comp (whiskerLeft F (F.coev G)) (F.ev (tensorObj F G)) = CategoryStruct.id (tensorObj F G)

The first triangle identity: F ⊗ G ⟶ F ⊗ [F, F ⊗ G] ⟶ F ⊗ G is the identity.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.whiskerLeft_coev_comp_ev_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) {Z : DayFunctor C V} (h : tensorObj F G ⟶ Z) : CategoryStruct.comp (whiskerLeft F (F.coev G)) (CategoryStruct.comp (F.ev (tensorObj F G)) h) = h

The first triangle identity: F ⊗ G ⟶ F ⊗ [F, F ⊗ G] ⟶ F ⊗ G is the identity.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.coev_comp_internalHom_map_ev {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) : CategoryStruct.comp (F.coev (F.internalHom.obj G)) (F.internalHom.map (F.ev G)) = CategoryStruct.id (F.internalHom.obj G)

The second triangle identity: [F, G] ⟶ [F, F ⊗ [F, G]] ⟶ [F, G] is the identity.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.coev_comp_internalHom_map_ev_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) {Z : DayFunctor C V} (h : F.internalHom.obj G ⟶ Z) : CategoryStruct.comp (F.coev (F.internalHom.obj G)) (CategoryStruct.comp (F.internalHom.map (F.ev G)) h) = h

The second triangle identity: [F, G] ⟶ [F, F ⊗ [F, G]] ⟶ [F, G] is the identity.

noncomputable def CategoryTheory.MonoidalCategory.DayFunctor.internalHomAdjunction {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] : tensorLeft F ⊣ F.internalHom

The Day convolution product with F is left adjoint to the internal hom functor [F, -].

@[instance_reducible]

noncomputable instance CategoryTheory.MonoidalCategory.DayFunctor.monoidalClosed {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] : MonoidalClosed (DayFunctor C V)

Day convolution with values in a monoidal closed category with ends is monoidal closed, with internal hom [F, G].obj c = ∫_j [F j, G (j ⊗ c)].

theorem CategoryTheory.MonoidalCategory.DayFunctor.ihom_eq_internalHom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] : ihom F = F.internalHom

The internal hom of C ⊛⥤ V is internalHom.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ihom_ev_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) : (ihom.ev F).app G = F.ev G

The evaluation of the monoidal closed structure on C ⊛⥤ V is ev.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.ihom_coev_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] (G : DayFunctor C V) : (ihom.coev F).app G = F.coev G

The coevaluation of the monoidal closed structure on C ⊛⥤ V is coev.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.curry_natTrans_app_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G H : DayFunctor C V} (f : tensorObj F G ⟶ H) (c j : C) : CategoryStruct.comp ((MonoidalClosed.curry f).natTrans.app c) (F.π H c j) = MonoidalClosed.curry (CategoryStruct.comp ((F.η G).app (j, c)) (f.natTrans.app (tensorObj j c)))

The curried morphism G ⟶ [F, H] of f : F ⊗ G ⟶ H, followed by a projection from the end, is the curried restriction of f along the Day convolution unit.

theorem CategoryTheory.MonoidalCategory.DayFunctor.curry_natTrans_app_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G H : DayFunctor C V} (f : tensorObj F G ⟶ H) (c j : C) {Z : V} (h : (ihom (F.functor.obj j)).obj (H.functor.obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp (CategoryStruct.comp ((MonoidalClosed.curry f).natTrans.app c) (F.π H c j)) h = CategoryStruct.comp (MonoidalClosed.curry (CategoryStruct.comp ((F.η G).app (j, c)) (f.natTrans.app (tensorObj j c)))) h

The curried morphism G ⟶ [F, H] of f : F ⊗ G ⟶ H, followed by a projection from the end, is the curried restriction of f along the Day convolution unit.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_uncurry_natTrans_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G H : DayFunctor C V} (g : G ⟶ F.internalHom.obj H) (x y : C) : CategoryStruct.comp ((F.η G).app (x, y)) ((MonoidalClosed.uncurry g).natTrans.app (tensorObj x y)) = MonoidalClosed.uncurry (CategoryStruct.comp (g.natTrans.app y) (F.π H y x))

The uncurried morphism F ⊗ G ⟶ H of g : G ⟶ [F, H], restricted along the Day convolution unit, is the uncurried composite of g with a projection from the end.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayFunctor.η_app_comp_uncurry_natTrans_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] [∀ (F : Functor Cᵒᵖ (Functor C V)), Limits.HasEnd F] (F : DayFunctor C V) [∀ (F G : Functor C V), (tensor C).HasPointwiseLeftKanExtension (externalProduct F G)] [(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)] {G H : DayFunctor C V} (g : G ⟶ F.internalHom.obj H) (x y : C) {Z : V} (h : H.functor.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((F.η G).app (x, y)) (CategoryStruct.comp ((MonoidalClosed.uncurry g).natTrans.app (tensorObj x y)) h) = CategoryStruct.comp (MonoidalClosed.uncurry (CategoryStruct.comp (g.natTrans.app y) (F.π H y x))) h

The uncurried morphism F ⊗ G ⟶ H of g : G ⟶ [F, H], restricted along the Day convolution unit, is the uncurried composite of g with a projection from the end.