English
For a diagram f: α → C with HasFiniteCoproducts, the finite-subcoproducts cocone built from liftToFinsetObj (Discrete.functor f) is a colimit cocone (i.e., its universal property holds).
Русский
Для диаграммы f: α → C с конечными копроизводами, коаксонка конечных подпкопроизведений, построенная из liftToFinsetObj (Discrete.functor f), является колимитной коаксоной.
LaTeX
$$$$ \mathrm{isColimitFiniteSubproductsCocone}(f):\; \text{IsColimit}(\mathrm{finiteSubcoproductsCocone}\ f). $$$$
Lean4
/-- The cocone `finiteSubcoproductsCocone` is a colimit cocone. -/
def isColimitFiniteSubproductsCocone (f : α → C) [HasColimitsOfShape (Finset (Discrete α)) C] [HasCoproduct f] :
IsColimit (finiteSubcoproductsCocone f) :=
IsColimit.ofIsoColimit (colimit.isColimit _)
(Cocones.ext
(IsColimit.coconePointUniqueUpToIso (liftToFinsetColimitCocone (Discrete.functor f)).isColimit
(colimit.isColimit _) :)
(by
intro S
simp only [liftToFinsetObj_obj, Discrete.functor_obj_eq_as, finiteSubcoproductsCocone_pt, colimit.cocone_x,
Functor.const_obj_obj, colimit.cocone_ι, finiteSubcoproductsCocone_ι_app]
ext j
rw [← Category.assoc]
convert
IsColimit.comp_coconePointUniqueUpToIso_hom (liftToFinsetColimitCocone (Discrete.functor f)).isColimit
(colimit.isColimit _) j
· simp [← colimit.w (liftToFinsetObj _) (homOfLE (x := { j.1 }) (y := S) (by simp))]
· simp))
