Preservation of pointwise left Kan extensions by external products

We prove that if a functor H' : D' ⥤ V is a pointwise left Kan extension of H : D ⥤ V along L : D ⥤ D', and if K : E ⥤ V is any functor such that for any e : E, the functor tensorRight (K.obj e) commutes with colimits of shape CostructuredArrow L d, then the functor H' ⊠ K is a pointwise left kan extension of H ⊠ K along L.prod (𝟭 E).

We also prove a similar criterion to establish that K ⊠ H' is a pointwise left Kan extension of K ⊠ H along (𝟭 E).prod L.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {D : Type u₂} {D' : Type u₃} {E : Type u₄} [Category.{v₂, u₂} D] [Category.{v₃, u₃} D'] [Category.{v₄, u₄} E] {H : Functor D V} {L : Functor D D'} (H' : Functor D' V) (α : H ⟶ L.comp H') (K : Functor E V) : externalProduct H K ⟶ (L.prod (Functor.id E)).comp (externalProduct H' K)

Given an extension α : H ⟶ L ⋙ H', this is the canonical extension H ⊠ K ⟶ L.prod (𝟭 E) ⋙ H' ⊠ K it induces through bifunctoriality of the external product.

@[reducible, inline]

abbrev CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {D : Type u₂} {D' : Type u₃} {E : Type u₄} [Category.{v₂, u₂} D] [Category.{v₃, u₃} D'] [Category.{v₄, u₄} E] {H : Functor D V} {L : Functor D D'} (H' : Functor D' V) (α : H ⟶ L.comp H') (K : Functor E V) : externalProduct K H ⟶ ((Functor.id E).prod L).comp (externalProduct K H')

Given an extension α : H ⟶ L ⋙ H', this is the canonical extension K ⊠ H ⟶ (𝟭 E).prod L ⋙ K ⊠ H' it induces through bifunctoriality of the external product.

def CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionAtExtensionUnitLeft {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {D : Type u₂} {D' : Type u₃} {E : Type u₄} [Category.{v₂, u₂} D] [Category.{v₃, u₃} D'] [Category.{v₄, u₄} E] {H : Functor D V} {L : Functor D D'} (H' : Functor D' V) (α : H ⟶ L.comp H') (K : Functor E V) (d : D') (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E) [Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))] : (Functor.LeftExtension.mk (externalProduct H' K) (extensionUnitLeft H' α K)).IsPointwiseLeftKanExtensionAt (d, e)

If H' : D' ⥤ V is a pointwise left Kan extension along L : D ⥤ D' at (d : D') and if tensoring right with an object preserves colimits in V, then H' ⊠ K : D' × E ⥤ V is a pointwise left Kan extension along L × (𝟭 E) at (d, e) for every e : E.

def CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitLeft {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {D : Type u₂} {D' : Type u₃} {E : Type u₄} [Category.{v₂, u₂} D] [Category.{v₃, u₃} D'] [Category.{v₄, u₄} E] {H : Functor D V} {L : Functor D D'} (H' : Functor D' V) (α : H ⟶ L.comp H') (K : Functor E V) [∀ (d : D') (e : E), Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorRight (K.obj e))] (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension) : (Functor.LeftExtension.mk (externalProduct H' K) (extensionUnitLeft H' α K)).IsPointwiseLeftKanExtension

If H' : D' ⥤ V is a pointwise left Kan extension along L : D ⥤ D', and if tensoring right with an object preserves colimits in V then H' ⊠ K : D' × E ⥤ V is a pointwise left Kan extension along L × (𝟭 E).

def CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionAtExtensionUnitRight {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {D : Type u₂} {D' : Type u₃} {E : Type u₄} [Category.{v₂, u₂} D] [Category.{v₃, u₃} D'] [Category.{v₄, u₄} E] {H : Functor D V} {L : Functor D D'} (H' : Functor D' V) (α : H ⟶ L.comp H') (K : Functor E V) (d : D') (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d) (e : E) [Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))] : (Functor.LeftExtension.mk (externalProduct K H') (extensionUnitRight H' α K)).IsPointwiseLeftKanExtensionAt (e, d)

If H' : D' ⥤ V is a pointwise left Kan extension along L : D ⥤ D' at d : D' and if tensoring left with an object preserves colimits in V, then K ⊠ H' : D' × E ⥤ V is a pointwise left Kan extension along (𝟭 E) × L at (e, d) for every e.

def CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitRight {V : Type u₁} [Category.{v₁, u₁} V] [MonoidalCategory V] {D : Type u₂} {D' : Type u₃} {E : Type u₄} [Category.{v₂, u₂} D] [Category.{v₃, u₃} D'] [Category.{v₄, u₄} E] {H : Functor D V} {L : Functor D D'} (H' : Functor D' V) (α : H ⟶ L.comp H') (K : Functor E V) [∀ (d : D') (e : E), Limits.PreservesColimitsOfShape (CostructuredArrow L d) (tensorLeft (K.obj e))] (P : (Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension) : (Functor.LeftExtension.mk (externalProduct K H') (extensionUnitRight H' α K)).IsPointwiseLeftKanExtension

If H' : D' ⥤ V is a pointwise left Kan extension along L : D ⥤ D' and if tensoring left with an object preserves colimits in V, then K ⊠ H' : D' × E ⥤ V is a pointwise left Kan extension along (𝟭 E) × L.