With Anders Mörtberg we started a library on finitely presented modules and prove it forms an abelian category.
This work is described in this preprint (prior to corrections, accepted for publication in the proceedings of ITP 2014).
We define finitely presented modules and morphisms between them, including the identity and zero morphisms, together with operations on morphisms: multiplication (i.e. composition), addition, negation, kernel and cokernel. We also prove that the class of finitely presented modules together with the class of module morphisms forms an abelian category.
The sources are here. (md5sum 467e308ced46f7d960597e69a4ce8f54)
You can install them by hand and through opam (package fpmods from the experimental opam Coq repository).
Note about a problem we encountered during the development:
When writing this library, we first used a coercion from morphisms to matrices in order to avoid redefining arithmetic operations (0,1,+,-,*m). However this proved to be a poor mathematical design choice as we could then write inconsistent morphism composition: we could compose morphisms M → N and N’ → P, when the number of generators of N was the same as the number of generator of N’ but with N different from N’. It led us to write meaningless statement (w.r.t. module theory) that we detected only when using them…
