mathlib documentation

algebra.homology.differential_object

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.

Equations

The functor from homological complexes to differential graded objects.

Equations