Hopf problem: homology of x · threefold homology 4 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.ThreefoldHomologyTopDegreeAlgebra.surjective_of_columnIso
{A : Type u_1}
{B : Type u_2}
{D : Type u_3}
[AddCommGroup A]
[AddCommGroup B]
[AddCommGroup D]
[Module ℤ A]
[Module ℤ B]
[Module ℤ D]
[Module ℤ (A × B)]
(F : A × B →ₗ[ℤ] D)
(f : A →ₗ[ℤ] D)
(e : B ≃ₗ[ℤ] D)
(hF : ∀ (a : A) (b : B), F (a, b) = f a + e b)
: