English
For a family f: α → C with a coproduct, one can form a canonical cocone from the coproduct ∐ f to the diagram liftToFinsetObj (Discrete.functor f) indexed by finite subsets of α. The legs are given by the universal property via Sigma-descending maps.
Русский
Для семейства f: α → C с существующим копроизводом можно образовать канонический коаксон от coproduct ∐ f к диаграмме liftToFinsetObj (Discrete.functor f), индексируемой конечными подмножествами α. Ребра задаются через универсальность посредством отображений типа Sigma-desc.
LaTeX
$$$$ \text{finiteSubcoproductsCocone}(f) \;:\; \mathrm{Cocone}(\mathrm{liftToFinsetObj}(\mathrm{Discrete.functor}\ f)) \;,\quad \mathrm{pt}=\coprod f,\; \iota_S=\Sigma\text{.desc}(\lambda s,\ \Sigma\iota f\_s). $$$$
Lean4
/-- The converse of the construction in `liftToFinsetColimitCocone`: we can form a cocone on the
coproduct of `f` whose legs are the coproducts over the finite subsets of `α`. -/
@[simps!]
def finiteSubcoproductsCocone (f : α → C) [HasCoproduct f] : Cocone (liftToFinsetObj (Discrete.functor f))
where
pt := ∐ f
ι := { app S := Sigma.desc fun s => Sigma.ι f _ }
