mathlib3

8c75ef35 - feat(algebra/homology/opposite): add opposite complexes (#18144)

feat(algebra/homology/opposite): add opposite complexes (#18144) The opposite of the category of chain complexes with objects in $V$ is equivalent to the category of cochain complexes of objects in $V^{op}.$ Moreover, the opposite of the homology of a chain complex is isomorphic to the cohomology of the corresponding cochain complex of objects in $V^{op}.$ We prove this more generally, for any complex shape.