Formality of complexes of vector spaces

This file constructs the zero-differential homology model of a cochain complex of vector spaces and a noncanonical homotopy equivalence to that model.

The construction is deliberately coefficient-side and unbounded. It uses choice to split each space of cycles into boundaries and representatives and to choose preimages of boundaries under the preceding differential. No naturality in the complex is claimed. Finite support and finite-dimensionality play no role here; packaging a finite cohomology presentation is a downstream consumer.

noncomputable def CochainComplex.homotopyEquivHomologyModel {k : Type u} [DivisionRing k] (K : CochainComplex (ModuleCat k) ℤ) : HomotopyEquiv K K.homologyModel

Every unbounded cochain complex of vector spaces is noncanonically homotopy equivalent to its zero-differential homology model.

This construction is not natural in K: it records choices of homology representatives and boundary preimages.

Equations

• One or more equations did not get rendered due to their size.