Homotopies

Extensions of Mathlib's Homotopy between chain maps: homotopies on the summands of a coproduct of complexes assemble to a homotopy on the coproduct, complexes of vector spaces split noncanonically as their homology, and explicit finite cohomology presentations record chosen finite homotopy splittings.