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…


This page was last updated at 2014-12-01 03:52:16 +0100
This site is compiled with nanoc and hosted by Cr@ns

Warning: fopen(index.log): failed to open stream: Permission denied in /home/cohen/www/work/fpmods/index.php on line 99

Warning: fwrite() expects parameter 1 to be resource, bool given in /home/cohen/www/work/fpmods/index.php on line 100

Warning: Use of undefined constant REMOTE_HOST - assumed 'REMOTE_HOST' (this will throw an Error in a future version of PHP) in /home/cohen/www/work/fpmods/index.php on line 101

Notice: Undefined index: REMOTE_HOST in /home/cohen/www/work/fpmods/index.php on line 101

Warning: Use of undefined constant REMOTE_ADDR - assumed 'REMOTE_ADDR' (this will throw an Error in a future version of PHP) in /home/cohen/www/work/fpmods/index.php on line 101

Warning: fwrite() expects parameter 1 to be resource, bool given in /home/cohen/www/work/fpmods/index.php on line 101

Warning: fclose() expects parameter 1 to be resource, bool given in /home/cohen/www/work/fpmods/index.php on line 102