colim_preservesLimits_pair_of_sSifted

English

The comparison map for the colimit factors through the standard product comparison map via a natural isomorphism given by external product constructions.

Русский

Сравнение для колима факторизуется через стандартное сравнение произведений, полученное с помощью внешнего произведения.

LaTeX

$$HasColimit.isoOfNatIso ((externalProductCompDiagIso _ _).app (X, Y)).symm ≫ colimit.pre (X ⊠ Y) (diag C) ≫ (PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y ...).hom = CartesianMonoidalCategory.prodComparison colim X Y$$

Lean4

instance colim_preservesLimits_pair_of_sSifted {X Y : C ⥤ Type u} : PreservesLimit (pair X Y) colim :=
  preservesLimit_pair_of_isIso_prodComparison _ _ _

Похожие утверждения