Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitLeft

{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) →
                            CategoryTheory.MonoidalCategory.externalProduct H K ⟶
                              (L.prod (CategoryTheory.Functor.id E)).comp
                                (CategoryTheory.MonoidalCategory.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.

Defined in

Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Cited by

10 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category