Theorems · Theorem · category theory

CategoryTheory.IsSifted.factorization_prodComparison_colim

∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] (X Y : CategoryTheory.Functor C (Type u)),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          ((CategoryTheory.MonoidalCategory.externalProductCompDiagIso C (Type u)).app (X, Y)).symm).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.pre (CategoryTheory.MonoidalCategory.externalProduct X Y)
          (CategoryTheory.Functor.diag C))
        (CategoryTheory.Limits.PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y
            (CategoryTheory.MonoidalCategory.curriedTensor (Type u))).hom) =
    CategoryTheory.CartesianMonoidalCategory.prodComparison CategoryTheory.Limits.colim X Y

Through the isomorphisms PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ and externalProductCompDiagIso, the comparison map colimit.pre (X ⊠ Y) (diag C) identifies with the product comparison map for the colimit functor.

Defined in

Mathlib.CategoryTheory.Limits.Sifted

Cited by

0 results in Mathlib

Foundations

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

Assumes

CategoryTheory.SmallCategory