On Friday 22/11/2013, at 10h30, in room Byron Beige,
Speaker: Cyril Cohen.
Joint work with: Anders Mortberg.
Title: A Coq formalization of finitely presented modules.
Abstract:
The use of vector spaces in homology theory does not give as precise
information as with modules. A generalization to finitely presented modules
covers computable Z-homology, which gives finer-grained topological invariants.
We formalize a construction of finitely presented modules over coherent and
strongly discrete rings and discuss its properties. This formalization gives
basic building blocks that lead to a clean definition of homology groups.
