Hopf problem: homology of x · threefold homology 2

Supporting definitions and proofs for this stage of the six-sphere construction.

def Mathoverflow1973.ThreefoldHomology.BoundaryFirst.latticeCoinvariantMap : Option Elliptic.Kind → Lattice →ₗ[ℤ] Fin 2 → ℤ

The lattice coinvariant map for a cusp or elliptic boundary component.

Equations

• Mathoverflow1973.ThreefoldHomology.BoundaryFirst.latticeCoinvariantMap none = Mathoverflow1973.ThreefoldHomology.BoundaryFirst.cuspCoinvariantMap✝
• Mathoverflow1973.ThreefoldHomology.BoundaryFirst.latticeCoinvariantMap (some j) = Mathoverflow1973.Elliptic.coinvariantMap✝ j

theorem Mathoverflow1973.ThreefoldHomology.BoundaryFirst.latticeCoinvariantMap_surjective (i : Option Elliptic.Kind) : Function.Surjective ⇑(latticeCoinvariantMap i)