English
If a category has binary coproducts, then it is sifted or empty.
Русский
Если в категории существуют бинарные копроизведения, то она ситообразна или пуста.
LaTeX
$$IsSiftedOrEmpty C$$
Lean4
/-- A category with binary coproducts is sifted or empty. -/
instance [HasBinaryCoproducts C] : IsSiftedOrEmpty C :=
by
constructor
rintro ⟨c₁, c₂⟩
haveI : _root_.Nonempty <| StructuredArrow (c₁, c₂) (diag C) :=
⟨.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂))⟩
apply isConnected_of_zigzag
rintro ⟨_, c, f⟩ ⟨_, c', g⟩
dsimp only [const_obj_obj, diag_obj, prod_Hom] at f g
use [.mk ((coprod.inl : c₁ ⟶ c₁ ⨿ c₂), (coprod.inr : c₂ ⟶ c₁ ⨿ c₂)), .mk (g.fst, g.snd)]
simp only [colimit.cocone_x, diag_obj, Prod.mk.eta, List.isChain_cons_cons, List.isChain_singleton, and_true, ne_eq,
reduceCtorEq, not_false_eq_true, List.getLast_cons, List.cons_ne_self, List.getLast_singleton]
exact
⟨⟨Zag.of_inv <| StructuredArrow.homMk <| coprod.desc f.fst f.snd,
Zag.of_hom <| StructuredArrow.homMk <| coprod.desc g.fst g.snd⟩,
rfl⟩
