Direct Sums are coproducts

Stream: Is there code for X?

[Robin Carlier]

Algebra.DirectSum.Module defines the direct sum of a family of modules over a ring, and Algebra.Category.ModuleCatshows a lot of properties of the category of Modules over a Ring, but I didn’t find in there a proof that the direct sum constructed in Algebra.DirectSum.Moduleis a coproduct in the categorical sense. Is this somewhere else?

[Johan Commelin]

It is quite likely that this is missing...

[Adam Topaz]

are you looking for the universal property, or some coproduct cocone whose conepoint is defeq to a direct sum? We certainly have the first thing, but probably not the second.

[Adam Topaz]

If you look at docs#DirectSum.toModule and the surrounding API, that's essentially the universal property.

[Robin Carlier]

I was more looking for the second, in order to use some "Preserves colimits hence commutes with direct sums" kind of argument. I ended up doing it by hand.