We define a chain complex in
V as a differential
ℤ-graded object in
This is fancy language for the obvious definition, and it seems we can use it straightforwardly:
example (C : chain_complex V) : C.X 5 ⟶ C.X 6 := C.d 5
homological_complex V b for
b : β is a (co)chain complex graded by
with differential in grading
(We use the somewhat cumbersome
homological_complex to avoid the name conflict with
A convenience lemma for morphisms of cochain complexes, picking out one component of the commutation relation.
The forgetful functor from cochain complexes to graded objects, forgetting the differential.