Hopf problem: cusp fibre · cusp central homology 4

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

theorem Mathoverflow1973.CuspCentralHomology.coprod_surjective_of_exact_section {A : Type u_1} {B : Type u_2} {T : Type u_3} [AddCommGroup A] [AddCommGroup B] [AddCommGroup T] [Module ℤ A] [Module ℤ B] [Module ℤ T] (i : A →ₗ[ℤ] B) (p : B →ₗ[ℤ] T) (s : T →ₗ[ℤ] B) (hexact : i.range = p.ker) (hps : ∀ (t : T), p (s t) = t) : Function.Surjective ⇑(i.coprod s)