12 The spherical space form theorem
This is the terminal node. The route reaches it without proving the geometrization conjecture, which matters a great deal for how much has to be formalized.
Let \(M\) be a closed \(3\)-manifold whose fundamental group is a free product of finite groups and infinite cyclic groups. Then \(M\) admits no locally separating \(\mathbb {R}P^2\), so a Ricci flow with surgery exists for all positive time, and it becomes extinct after some \(T {\lt} \infty \): the time-slices \(M_t\) are empty for \(t \ge T\). (Morgan–Tian Theorem 0.4, proved in Chapter 18.)
Carries a third PDE prerequisite. Morgan–Tian follow Perelman’s third preprint and route the proof through the curve-shrinking flow (18.4), yet another geometric flow with its own existence and regularity theory. Chapter 18 is seven sections and largely self-contained analysis.
A closed \(3\)-manifold whose fundamental group is a free product of finite groups and infinite cyclic groups is a connected sum of spherical space forms, copies of \(S^2 \times S^1\), and copies of the non-orientable \(S^2\)-bundle over \(S^1\). (Morgan–Tian Theorem 0.1, deduced from 0.3 and 0.4 by downward induction on the surgery times.)
A closed \(3\)-manifold with finite fundamental group admits a metric of constant positive sectional curvature, and is therefore diffeomorphic to \(S^3/\Gamma \) for a finite \(\Gamma \subset SO(4)\) acting freely.
A finite group is in particular a free product of finite groups, so Theorem 131 applies. An \(S^2 \times S^1\) summand would contribute a \(\mathbb {Z}\) factor and a connected sum of two non-trivial groups is infinite, so with \(\pi _1\) finite exactly one spherical summand survives.
A simply connected closed \(3\)-manifold is diffeomorphic to \(S^3\). The case \(\Gamma = 1\).
Mathlib already states this, unproved, in Mathlib/Geometry/Manifold/PoincareConjecture.lean. It is the only node on this road that Lean has so far looked at.