isSiftedOrEmpty_of_colim_preservesBinaryProducts

English

If C has binary coproducts, then C is sifted or empty.

Русский

Если C имеет бинарные копроизведения, то C ситообразна или пуста.

LaTeX

$$IsSiftedOrEmpty C$$

Lean4

/-- If the `colim` functor `(C ⥤ Type) ⥤ Type` preserves binary products, then `C` is sifted or
empty. -/
theorem isSiftedOrEmpty_of_colim_preservesBinaryProducts
    [PreservesLimitsOfShape (Discrete WalkingPair) (colim : (C ⥤ Type u) ⥤ Type u)] : IsSiftedOrEmpty C :=
  by
  apply final_of_colimit_comp_coyoneda_iso_pUnit
  rintro ⟨c₁, c₂⟩
  calc
    colimit <| diag C ⋙ coyoneda.obj (op (c₁, c₂))
    _ ≅ colimit <| _ ⋙ (coyoneda.obj _) ⊠ (coyoneda.obj _) := (HasColimit.isoOfNatIso <| isoWhiskerLeft _ <| .refl _)
    _ ≅ colimit (_ ⊗ _) := (HasColimit.isoOfNatIso <| .refl _)
    _ ≅ (colimit _) ⊗ (colimit _) := (CartesianMonoidalCategory.prodComparisonIso colim _ _)
    _ ≅ PUnit ⊗ PUnit := ((Coyoneda.colimitCoyonedaIso _) ⊗ᵢ (Coyoneda.colimitCoyonedaIso _))
    _ ≅ PUnit := λ_ _

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