English
For small C, and X,Y: C ⥤ Type, if C is sifted, then the product comparison map is an isomorphism: (colim X) × (colim Y) ≅ colim (X ⊠ Y).
Русский
Для малой категории C и X,Y: C ⥤ Type, если C ситообразна, то продуктовое сравнение является изоморфизмом: (colim X) × (colim Y) ≅ colim (X ⊠ Y).
LaTeX
$$IsIso (CartesianMonoidalCategory.prodComparison colim X Y)$$
Lean4
/-- 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. -/
theorem factorization_prodComparison_colim :
(HasColimit.isoOfNatIso ((externalProductCompDiagIso _ _).app (X, Y)).symm).hom ≫
colimit.pre (X ⊠ Y) (diag C) ≫
(PreservesColimit₂.isoColimitUncurryWhiskeringLeft₂ X Y <| curriedTensor <| Type u).hom =
CartesianMonoidalCategory.prodComparison colim X Y :=
by
apply colimit.hom_ext
intro j
dsimp [externalProductBifunctor, CartesianMonoidalCategory.prodComparison, externalProductBifunctorCurried,
externalProduct]
cat_disch
