mathlib documentation


(Co)homology groups for complexes

We setup that part of the theory of homology groups which works in any category with kernels and images.

We define the homology groups themselves, and show that they induce maps on kernels.

Under the additional assumption that our category has equalizers and functorial images, we construct induced morphisms on images and functorial induced morphisms in homology.

Chains and cochains

Throughout we work with complexes graded by an arbitrary [add_comm_group β], with a differential with grading b : β. Thus we're simultaneously doing homology and cohomology groups (and in future, e.g., enabling computing homologies for successive pages of spectral sequences).

At the end of the file we set up abbreviations cohomology and graded_cohomology, so that when you're working with a C : cochain_complex V, you can write C.cohomology i rather than the confusing C.homology i.

The map induced by a chain map between the kernels of the differentials.


The kernels of the differentials of a complex form a β-graded object.


A morphism of complexes induces a morphism on the images of the differentials in every degree.

The connecting morphism from the image of d i to the kernel of d (i ± 1).


We now set up abbreviations so that you can write C.cohomology i or (graded_cohomology V).map f, etc., when C is a cochain complex.