Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.ExternalProduct.isPointwiseLeftKanExtensionAtExtensionUnitLeft

{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') →
                              (CategoryTheory.Functor.LeftExtension.mk H' α).IsPointwiseLeftKanExtensionAt d →
                                (e : E) →
                                  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.CostructuredArrow L d)
                                        (CategoryTheory.MonoidalCategory.tensorRight (K.obj e))] →
                                    (CategoryTheory.Functor.LeftExtension.mk
                                          (CategoryTheory.MonoidalCategory.externalProduct H' K)
                                          (CategoryTheory.MonoidalCategory.ExternalProduct.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.

Defined in

Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Cited by

0 results in Mathlib

Foundations

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

Assumes

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