Hopf problem: recognition · smale 10 #
Supporting definitions and proofs for this stage of the six-sphere construction.
theorem
Mathoverflow1973.Smale.HomologyTransport.exact_of_equivalences
{R : Type u_1}
{A : Type u_2}
{B : Type u_3}
{C : Type u_4}
{A' : Type u_5}
{B' : Type u_6}
{C' : Type u_7}
[Ring R]
[AddCommGroup A]
[Module R A]
[AddCommGroup B]
[Module R B]
[AddCommGroup C]
[Module R C]
[AddCommGroup A']
[Module R A']
[AddCommGroup B']
[Module R B']
[AddCommGroup C']
[Module R C']
(eA : A ≃ₗ[R] A')
(eB : B ≃ₗ[R] B')
(eC : C ≃ₗ[R] C')
(f : A →ₗ[R] B)
(g : B →ₗ[R] C)
(f' : A' →ₗ[R] B')
(g' : B' →ₗ[R] C')
(hf : ∀ (a : A), f' (eA a) = eB (f a))
(hg : ∀ (b : B), g' (eB b) = eC (g b))
(hexact : f.range = g.ker)
: