Checking exactness of a complex of complexes pointwise

Stream: Is there code for X?

[Michał Mrugała]

Is there a way to check that a complex of complexes is exact by checking exactness at every index? I want to show that if G is a group, the functor mapping G to its inhomogeneous (co)chain complex is exact using this.

[Kevin Buzzard]

Is docs#groupCohomology.map_cochainsFunctor_shortExact not good enough for you?

[Michał Mrugała]

It definitely is, thank you!

[Michał Mrugała]

However, here is the next step I could use checking pointwise. I now want to deduce exactness of the Tate complex functor by quoting exactness of inhomogeneous (co)chains.

[Andrew Yang]

perhaps docs#HomologicalComplex.preservesLimitsOfShape_of_eval ?