Homological complexes are differential graded objects. #
We verify that a HomologicalComplex
indexed by an AddCommGroup
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.
We first prove some results about differential graded objects.
Porting note: after the port, move these to their own file.
Since eqToHom
only preserves the fact that X.X i = X.X j
but not i = j
, this definition
is used to aid the simplifier.
Instances For
The functor from differential graded objects to homological complexes.
Instances For
The functor from homological complexes to differential graded objects.
Instances For
The unit isomorphism for dgoEquivHomologicalComplex
.
Instances For
The counit isomorphism for dgoEquivHomologicalComplex
.
Instances For
The category of differential graded objects in V
is equivalent
to the category of homological complexes in V
.