Tag: homology

Nov 22 2013

Séminaire Marelle : A Coq formalization of finitely presented modules.

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.