Hopf problem: homology of x · threefold homology 3 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.ThreefoldHomologyFinitenessAlgebra.subsingleton_of_exact
{B H C : Type u}
[AddCommGroup B]
[AddCommGroup H]
[AddCommGroup C]
[Module ℤ B]
[Module ℤ H]
[Module ℤ C]
(f : B →ₗ[ℤ] H)
(g : H →ₗ[ℤ] C)
(h : Function.Exact ⇑f ⇑g)
[Subsingleton B]
[Subsingleton C]
: