English
For a coproduct cocone c over f, Sigma.desc c.inj is an isomorphism if and only if c is a colimit.
Русский
Для копроизведения кофакона c над f, Sigma.desc c.inj является изоморфизмом тогда и только тогда, когда c является колимитом.
LaTeX
$$IsIso\bigl(\Sigma.desc c.inj\bigr) \iff Nonempty(IsColimit c)$$
Lean4
theorem isColimit_iff_isIso_sigmaDesc {f : β → C} [HasCoproduct f] (c : Cofan f) :
IsIso (Sigma.desc c.inj) ↔ Nonempty (IsColimit c) :=
by
refine ⟨fun h ↦ ⟨isColimitOfIsIsoSigmaDesc c⟩, fun ⟨hc⟩ ↦ ?_⟩
have : IsIso (((coproductIsCoproduct f).coconePointUniqueUpToIso hc).hom ≫ hc.desc c) := by simp; infer_instance
convert this
ext
simp only [colimit.ι_desc, mk_pt, mk_ι_app, IsColimit.coconePointUniqueUpToIso, coproductIsCoproduct,
colimit.cocone_x, Functor.mapIso_hom, IsColimit.uniqueUpToIso_hom, Cocones.forget_map,
IsColimit.descCoconeMorphism_hom, IsColimit.ofIsoColimit_desc, Cocones.ext_inv_hom, Iso.refl_inv,
colimit.isColimit_desc, Category.id_comp, IsColimit.desc_self, Category.comp_id]
rfl
