Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionExtensionUnitLeft

{V : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {D : Type u₂} →
        {D' : Type u₃} →
          {E : Type u₄} →
            [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} D'] →
                [inst_4 : CategoryTheory.Category.{v₄, u₄} E] →
                  {H : CategoryTheory.Functor D V} →
                    {L : CategoryTheory.Functor D D'} →
                      (H' : CategoryTheory.Functor D' V) →
                        (α : H ⟶ L.comp H') →
                          (K : CategoryTheory.Functor E V) →
                            [∀ (d : D') (e : E),
                                  CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow L d)
                                    (CategoryTheory.MonoidalCategory.tensorRight (K.obj e))] →
                              (CategoryTheory.Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtension →
                                (CategoryTheory.Functor.LeftExtension.mk
                                    (CategoryTheory.MonoidalCategory.externalProduct H' K)
                                    (CategoryTheory.MonoidalCategory.ExternalProduct.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).

Defined in

Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Cited by

2 results in Mathlib

Foundations

Depth 52 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Limits.PreservesColimitsOfShape