Coproducts of finitely supported families

A family of objects with only finitely many nonzero members has a coproduct when its finite subfamily has a coproduct. The colimit cocone uses that subfamily's coproduct and zero maps from objects outside its support.

Main result

• CategoryTheory.Limits.hasCoproduct_of_finite_support constructs the coproduct of the full family from its finite support.

Implementation notes

The finite subfamily supplies the apex. Its coproduct inclusions are extended by zero maps outside the support, where IsZero makes every cocone leg unique. An empty support is allowed.

References

This extends Mathlib's CategoryTheory.Limits.HasCoproduct and CategoryTheory.Limits.Cofan APIs for a finitely supported family.

theorem CategoryTheory.Limits.hasCoproduct_of_finite_support {C : Type u} [Category.{v, u} C] [HasZeroMorphisms C] {I : Type w} (X : I → C) (s : Finset I) [HasCoproduct fun (i : ↥s) => X ↑i] (hzero : ∀ i ∉ s, IsZero (X i)) : HasCoproduct X

Extend the coproduct cocone of a finite subfamily by zero maps on all other indices. The IsZero hypothesis makes those other cocone legs unique, so the extended cocone is colimiting, even when the finite support is empty.