instIsIsoObjFunctorTypeColimTensorObjProdComparison

English

If C is small and IsSifted, then prodComparison is an isomorphism.

Русский

Если C малая и ситообразна, то prodComparison является изоморфизмом.

LaTeX

$$IsIso (CartesionMonoidalCategory.prodComparison colim X Y)$$

Lean4

/-- If `C` is sifted, the canonical product comparison map for the `colim` functor
`(C ⥤ Type) ⥤ Type` is an isomorphism. -/
instance : IsIso (CartesianMonoidalCategory.prodComparison colim X Y) :=
  by
  rw [← factorization_prodComparison_colim]
  infer_instance

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