Theorems · Definition · category theory

CategoryTheory.MonoidalCategory.ExternalProduct.extensionUnitRight

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

Defined in

Mathlib.CategoryTheory.Monoidal.ExternalProduct.KanExtension

Cited by

9 results in Mathlib

Foundations

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

Assumes

CategoryTheory.CategoryCategoryTheory.MonoidalCategoryCategoryTheory.CategoryCategoryTheory.CategoryCategoryTheory.Category