Hopf problem: cusp fibre · cusp central homology 2 #
Supporting definitions and proofs for this stage of the six-sphere construction.
noncomputable def
Mathoverflow1973.CuspCentralHomology.Suspension.liftFromSurjection
{A : Type u_1}
{B : Type u_2}
{S : Type u_3}
{Z : Type u_4}
(q : A → B)
(hq : Function.Surjective q)
(F : S × A → Z)
(p : S × B)
:
Z
A choice-based lift of a function along a surjection in its second coordinate.
Equations
- Mathoverflow1973.CuspCentralHomology.Suspension.liftFromSurjection q hq F p = F (p.1, Function.surjInv hq p.2)
Instances For
theorem
Mathoverflow1973.CuspCentralHomology.Suspension.liftFromSurjection_continuous_mo1973_4393
{A : Type u_1}
{B : Type u_2}
{S : Type u_3}
{Z : Type u_4}
[TopologicalSpace A]
[TopologicalSpace B]
[TopologicalSpace S]
[TopologicalSpace Z]
[LocallyCompactSpace S]
(q : A → B)
(hq : Topology.IsQuotientMap q)
(F : S × A → Z)
(hF : ∀ (s : S) (a b : A), q a = q b → F (s, a) = F (s, b))
(hcont : Continuous F)
:
Continuous (liftFromSurjection q ⋯ F)