Reeb's sphere theorem

Reeb's theorem (Milnor, Morse Theory, Theorem 4.1): if a compact manifold M of dimension n carries a Morse function with exactly two critical points, then M is homeomorphic to the sphere Sⁿ. The conclusion is a homeomorphism, not a diffeomorphism: Milnor's exotic 7-spheres carry such functions.

The two critical points are the global minimum x₀ and the global maximum x₁ of f. Following Milnor, for small r > 0 the sublevel {f ≤ f x₀ + r²} and the superlevel {f ≥ f x₁ - r²} are closed discs, by the Morse lemma at the nondegenerate extrema (TauCeti.IsManifoldNondegenerateCriticalPoint.exists_sublevel_homeomorph_closedBall), and the band between them contains no critical point, so the sublevel {f ≤ f x₁ - r²} is homeomorphic to the small disc {f ≤ f x₀ + r²} by a homeomorphism carrying boundary level onto boundary level (TauCeti.exists_sublevelHomeomorph). So M is the union of two closed discs meeting along their boundary spheres, which is a sphere (TauCeti.nonempty_homeomorph_sphere_of_union_closedBall).

If f x₀ = f x₁ the function is constant, every point is a critical point, so M has exactly two points, and a nondegenerate critical point that is both a local minimum and a local maximum forces n = 0. Then M is the two-point sphere S⁰; no connectedness or dimension hypothesis is needed.

Main results

• TauCeti.IsMorse.nonempty_homeomorph_sphere_of_totalCriticalCount_eq_two: Reeb's theorem.

References

• J. Milnor, Morse Theory, Annals of Mathematics Studies 51, Princeton University Press, 1963, Theorem 4.1.
• G. Reeb, Sur les points singuliers d'une forme de Pfaff complètement intégrable ou d'une fonction numérique, C. R. Acad. Sci. Paris 222 (1946), 847–849.

theorem TauCeti.IsMorse.nonempty_homeomorph_sphere_of_totalCriticalCount_eq_two {E : Type u_1} {H : Type u_2} {M : Type u_3} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [TopologicalSpace H] {I : ModelWithCorners ℝ E H} [I.Boundaryless] [TopologicalSpace M] [ChartedSpace H M] [IsManifold I (↑⊤) M] [T2Space M] [CompactSpace M] {f : M → ℝ} (hf : IsMorse I f) (h2 : totalCriticalCount I f = 2) : Nonempty (M ≃ₜ ↑(Metric.sphere 0 1))

Reeb's theorem (Milnor, Morse Theory, Theorem 4.1). A compact boundaryless manifold modelled on a real vector space of dimension n which carries a Morse function with exactly two critical points is homeomorphic to the sphere Sⁿ.