Commit 2021-04-09 12:24 fe5d6604View on Github →
feat(algebra/category/Module): arbitrary colimits (#7099)
This is just the "semi-automated" construction of arbitrary colimits in the category or
R-modules, following the same model as for
We already have finite colimits from the
abelian instance. One could also give definitionally nicer colimits as quotients of finitely supported functions. But this is better than nothing!