Chain complexes
We define a chain complex in V as a differential ℤ-graded object in V.
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
We define the forgetful functor to ℤ-graded objects, and show that
chain_complex V is concrete when V is, and V has coproducts.
A homological_complex V b for b : β is a (co)chain complex graded by β,
with differential in grading b.
(We use the somewhat cumbersome homological_complex to avoid the name conflict with ℂ.)
A chain complex in V is "just" a differential ℤ-graded object in V,
with differential graded -1.
A cochain complex in V is "just" a differential ℤ-graded object in V,
with differential graded +1.
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.