mathlib documentation


Homological complexes are differential graded objects. #

We verify that a homological_complex indexed by an add_comm_group is essentially the same thing as a differential graded object.

This equivalence is probably not particularly useful in practice; it's here to check that definitions match up as expected.

The functor from differential graded objects to homological complexes.


The functor from homological complexes to differential graded objects.