Internal homs for day convolution

Given a category V that is monoidal closed, a category C that is monoidal, a functor C ⥤ V, and given the data of suitable day convolutions and suitable ends of profunctors c c₁ c₂ ↦ ihom (F c₁) (·.obj (c₂ ⊗ c)), we prove that the data of the units of the left Kan extensions that define day convolutions and the data of the canonical morphisms to the aforementioned ends can be organised as data that exhibit F as monoidal closed in C ⥤ V for the Day convolution monoidal structure.

TODOs

• When LawfulDayConvolutionMonoidalStruct (#26820) lands, transport the constructions here to produce actual CategoryTheory.MonoidalClosed instances.

def CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F : Functor C V) : Functor (Functor C V) (Functor C (Functor Cᵒᵖ (Functor C V)))

Given F : C ⥤ V, this is the functor G ↦ c c₁ c₂ ↦ ihom (F c₁) (G.obj (c₂ ⊗ c)). The internal hom functor for Day convolution [F, -] is naturally isomorphic to the functor G ↦ c ↦ end_ (c₁ c₂ ↦ ihom (F c₁) (G.obj (c₂ ⊗ c))), hence this definition.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_obj {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F G : Functor C V) (c : C) (X : Cᵒᵖ) (X✝ : C) : ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj X).obj X✝ = (ihom (F.obj (Opposite.unop X))).obj (G.obj (tensorObj X✝ c))

@[simp]

theorem CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_map_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F G : Functor C V) (c : C) {X✝ Y✝ : Cᵒᵖ} (f : X✝ ⟶ Y✝) (X : C) : ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).map f).app X = (MonoidalClosed.pre (F.map f.unop)).app (G.obj (tensorObj X c))

@[simp]

theorem CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_map_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F G : Functor C V) {c c' : C} (f : c ⟶ c') (X : Cᵒᵖ) (c✝ : C) : ((((dayConvolutionInternalHomDiagramFunctor F).obj G).map f).app X).app c✝ = (ihom (F.obj (Opposite.unop X))).map (G.map (whiskerLeft c✝ f))

@[simp]

theorem CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_map_app_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F : Functor C V) {G G' : Functor C V} (η : G ⟶ G') (c : C) (X : Cᵒᵖ) (c✝ : C) : ((((dayConvolutionInternalHomDiagramFunctor F).map η).app c).app X).app c✝ = (ihom (F.obj (Opposite.unop X))).map (η.app (tensorObj c✝ c))

@[simp]

theorem CategoryTheory.MonoidalCategory.dayConvolutionInternalHomDiagramFunctor_obj_obj_obj_map {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F G : Functor C V) (c : C) (X : Cᵒᵖ) {X✝ Y✝ : C} (f : X✝ ⟶ Y✝) : ((((dayConvolutionInternalHomDiagramFunctor F).obj G).obj c).obj X).map f = (ihom (F.obj (Opposite.unop X))).map (G.map (whiskerRight f c))

structure CategoryTheory.MonoidalCategory.DayConvolutionInternalHom {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] (F G H : Functor C V) : Type (max (max (max u₁ u₂) v₁) v₂)

DayConvolutionInternalHom F G H asserts that H is the value at G of an internal hom functor of F for the Day convolution monoidal structure. This is phrased as the data of a limit CategoryTheory.Wedge (i.e an end) on internalHomDiagramFunctor F|>.obj G|>.obj c and c, with tip (H.obj G).obj c and a compatibility condition asserting that the functoriality of H identifies to the functoriality of ends.

• π (c j : C) : H.obj c ⟶ (ihom (F.obj j)).obj (G.obj (tensorObj j c))

  The canonical projections maps

• hπ (c : C) ⦃i j : C⦄ (f : i ⟶ j) : CategoryStruct.comp (self.π c i) ((ihom (F.obj i)).map (G.map (whiskerRight f c))) = CategoryStruct.comp (self.π c j) ((MonoidalClosed.pre (F.map f)).app (G.obj (tensorObj j c)))

  The projections maps assemble into a wedge.

• isLimitWedge (c : C) : Limits.IsLimit (Limits.Wedge.mk (H.obj c) (self.π c) ⋯)

  The wedge defined by π and hπ is a limit wedge, i.e H.obj c is an end of internalHomDiagramFunctor F G|>.obj c.

• map_comp_π {c c' : C} (f : c ⟶ c') (j : C) : CategoryStruct.comp (H.map f) (self.π c' j) = CategoryStruct.comp (self.π c j) ((ihom (F.obj j)).map (G.map (whiskerLeft j f)))

  The functoriality of H.obj G identifies (through Wedge.IsLimit.hom_ext) with the functoriality on ends induced by functoriality of internalHomDiagramFunctor F|>.obj G.

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} (self : DayConvolutionInternalHom F G H) {c c' : C} (f : c ⟶ c') (j : C) {Z : V} (h : (ihom (F.obj j)).obj (G.obj (tensorObj j c')) ⟶ Z) : CategoryStruct.comp (H.map f) (CategoryStruct.comp (self.π c' j) h) = CategoryStruct.comp (self.π c j) (CategoryStruct.comp ((ihom (F.obj j)).map (G.map (whiskerLeft j f))) h)

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.hπ_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} (self : DayConvolutionInternalHom F G H) (c : C) ⦃i j : C⦄ (f : i ⟶ j) {Z : V} (h : (ihom (F.obj i)).obj (G.obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp (self.π c i) (CategoryStruct.comp ((ihom (F.obj i)).map (G.map (whiskerRight f c))) h) = CategoryStruct.comp (self.π c j) (CategoryStruct.comp ((MonoidalClosed.pre (F.map f)).app (G.obj (tensorObj j c))) h)

def CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} (ℌ : DayConvolutionInternalHom F G H) {G' H' : Functor C V} (f : G ⟶ G') (ℌ' : DayConvolutionInternalHom F G' H') : H ⟶ H'

If we have a map G ⟶ G' and a DayConvolutionInternalHom F G' H', then there is a unique map H ⟶ H' induced by functoriality of ends and functoriality of internalHomDiagramFunctor F.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} (ℌ : DayConvolutionInternalHom F G H) {G' H' : Functor C V} (f : G ⟶ G') (ℌ' : DayConvolutionInternalHom F G' H') (c j : C) : CategoryStruct.comp ((ℌ.map f ℌ').app c) (ℌ'.π c j) = CategoryStruct.comp (ℌ.π c j) ((ihom (F.obj j)).map (f.app (tensorObj j c)))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.map_app_comp_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} (ℌ : DayConvolutionInternalHom F G H) {G' H' : Functor C V} (f : G ⟶ G') (ℌ' : DayConvolutionInternalHom F G' H') (c j : C) {Z : V} (h : (ihom (F.obj j)).obj (G'.obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp ((ℌ.map f ℌ').app c) (CategoryStruct.comp (ℌ'.π c j) h) = CategoryStruct.comp (ℌ.π c j) (CategoryStruct.comp ((ihom (F.obj j)).map (f.app (tensorObj j c))) h)

def CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} [DayConvolution F H] (ℌ : DayConvolutionInternalHom F G H) : DayConvolution.convolution F H ⟶ G

Given ℌ : DayConvolutionInternalHom F H, if we think of H.obj G as the internal hom [F, G], then this is the transformation corresponding to the component at G of the "evaluation" natural morphism F ⊛ [F, _] ⟶ 𝟭.

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} [DayConvolution F H] (ℌ : DayConvolutionInternalHom F G H) (x y : C) : CategoryStruct.comp ((DayConvolution.unit F H).app (x, y)) (ℌ.ev_app.app (tensorObj x y)) = MonoidalClosed.uncurry (ℌ.π y x)

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.unit_app_ev_app_app_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} [DayConvolution F H] (ℌ : DayConvolutionInternalHom F G H) (x y : C) {Z : V} (h : G.obj (tensorObj x y) ⟶ Z) : CategoryStruct.comp ((DayConvolution.unit F H).app (x, y)) (CategoryStruct.comp (ℌ.ev_app.app (tensorObj x y)) h) = CategoryStruct.comp (MonoidalClosed.uncurry (ℌ.π y x)) h

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.ev_naturality_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F G H : Functor C V} [DayConvolution F H] (ℌ : DayConvolutionInternalHom F G H) {G' H' : Functor C V} (ℌ' : DayConvolutionInternalHom F G' H') [DayConvolution F H'] (η : G ⟶ G') : CategoryStruct.comp (DayConvolution.map (CategoryStruct.id F) (ℌ.map η ℌ')) ℌ'.ev_app = CategoryStruct.comp ℌ.ev_app η

def CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F H G : Functor C V} [DayConvolution F G] (ℌ : DayConvolutionInternalHom F (DayConvolution.convolution F G) H) : G ⟶ H

Given ℌ : DayConvolutionInternalHom F H, if we think of H.obj G as the internal hom [F, G], then this is the transformation corresponding to the component at G of the "coevaluation" natural morphism 𝟭 ⟶ [F, F ⊛ _].

Equations

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

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F H G : Functor C V} [DayConvolution F G] (ℌ : DayConvolutionInternalHom F (DayConvolution.convolution F G) H) (c j : C) : CategoryStruct.comp (ℌ.coev_app.app c) (ℌ.π c j) = MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))

@[simp]

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_app_π_assoc {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F H G : Functor C V} [DayConvolution F G] (ℌ : DayConvolutionInternalHom F (DayConvolution.convolution F G) H) (c j : C) {Z : V} (h : (ihom (F.obj j)).obj ((DayConvolution.convolution F G).obj (tensorObj j c)) ⟶ Z) : CategoryStruct.comp (ℌ.coev_app.app c) (CategoryStruct.comp (ℌ.π c j) h) = CategoryStruct.comp (MonoidalClosed.curry ((DayConvolution.unit F G).app (j, c))) h

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.coev_naturality_app {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F H G : Functor C V} [DayConvolution F G] (ℌ : DayConvolutionInternalHom F (DayConvolution.convolution F G) H) {G' H' : Functor C V} [DayConvolution F G'] (η : G ⟶ G') (ℌ' : DayConvolutionInternalHom F (DayConvolution.convolution F G') H') : CategoryStruct.comp η ℌ'.coev_app = CategoryStruct.comp ℌ.coev_app (ℌ.map (DayConvolution.map (CategoryStruct.id F) η) ℌ')

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.left_triangle_components {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F H : Functor C V} (G : Functor C V) [DayConvolution F G] (ℌ : DayConvolutionInternalHom F (DayConvolution.convolution F G) H) [DayConvolution F H] : CategoryStruct.comp (DayConvolution.map (CategoryStruct.id F) ℌ.coev_app) ℌ.ev_app = CategoryStruct.id (DayConvolution.convolution F G)

theorem CategoryTheory.MonoidalCategory.DayConvolutionInternalHom.right_triangle_components {C : Type u₁} [Category.{v₁, u₁} C] {V : Type u₂} [Category.{v₂, u₂} V] [MonoidalCategory C] [MonoidalCategory V] [MonoidalClosed V] {F H : Functor C V} (G : Functor C V) [DayConvolution F H] (ℌ : DayConvolutionInternalHom F G H) {H' : Functor C V} (ℌ' : DayConvolutionInternalHom F (DayConvolution.convolution F H) H') : CategoryStruct.comp ℌ'.coev_app (ℌ'.map ℌ.ev_app ℌ) = CategoryStruct.id H