Skip to content
The Lumenary
Research pathwaysResearch (graduate background) 130 min

Low-dimensional topology: 3- and 4-manifolds

In dimension 3 every closed manifold is built from geometric pieces; in dimension 4 the smooth and the topological worlds come apart — and both facts are invisible from any other dimension.

Formally verified · 12 LeanComputationally tested · 2 PythonAI-drafted · awaiting human reviewMathematically reviewed: Awaiting human review
MotivationH

Why dimensions 3 and 4 are different

The generalised Poincaré conjecture asks: is every closed nn-manifold homotopy equivalent to the sphere SnS^n actually homeomorphic to it? The answer is yes in every dimension, but the proofs tell a strange story.

  • For n≥5n \ge 5 Stephen Smale proved it in 1961 by cancelling handles, a method he developed into the h-cobordism theorem (1962). The key step, the Whitney trick, removes pairs of intersection points of 2-dimensional discs by pushing one disc across an embedded 2-disc; in dimension 5 and above there is room to make that disc embedded.
  • For n=4n = 4 there is not quite room. Michael Freedman (1982) found a way round it in the topological category — and Simon Donaldson's gauge theory (from 1983) showed that in the smooth category the h-cobordism theorem fails. Whether every smooth 4-manifold homotopy equivalent to S4S^4 is diffeomorphic to it is still unknown.
  • For n=3n = 3 the problem resisted all topological methods. Grigori Perelman solved it in 2002–2003 by proving William Thurston's geometrisation conjecture, using Richard Hamilton's Ricci flow: a geometric, analytic proof of a topological statement.

So dimensions 3 and 4 are where "low-dimensional" topology lives. In dimension 3, geometry rules: every closed 3-manifold decomposes into pieces carrying one of eight homogeneous geometries, most of them hyperbolic, and for hyperbolic manifolds the topology determines the geometry completely. In dimension 4, the topological and smooth worlds split: there are topological 4-manifolds with no smooth structure, pairs that are homeomorphic but not diffeomorphic, and uncountably many smooth structures on R4\R^4 — while Rn\R^n has exactly one for every n≠4n \ne 4.

This lesson is an orientation: how to build and compute with 3-manifolds, what geometrisation says, how intersection forms organise 4-manifolds, and what is known and open.

IntuitionH

Building 3-manifolds by gluing

A solid torus S1×D2S^1 \times D^2 has a boundary torus with two special curves: the meridian μ\mu, which bounds a disc inside, and a longitude λ\lambda, which runs once along. Take two solid tori and glue their boundary tori together by a homeomorphism. What you get depends only on where the meridian of the first goes:

  • meridian to longitude: the 3-sphere S3S^3 (think of S3⊂C2S^3 \subset \C^2 as {∣z1∣≤∣z2∣}∪{∣z1∣≥∣z2∣}\{|z_1| \le |z_2|\} \cup \{|z_1| \ge |z_2|\});
  • meridian to meridian: S1×S2S^1 \times S^2;
  • meridian to a curve winding pp times along and qq times around: the lens space L(p,q)L(p, q).
μλ
Schematic of a solid torus. The meridian (red) bounds a disc inside; the longitude (gold) runs once around the hole. Gluing two solid tori along their boundaries, or removing a solid torus around a knot and gluing it back differently (Dehn surgery), is how most 3-manifolds in this lesson are built.

Two generalisations give every closed orientable 3-manifold. Heegaard splittings glue two handlebodies of genus gg (solid "pretzels") along their boundary surfaces. Dehn surgery removes a solid torus neighbourhood of a knot in S3S^3 and glues it back with the meridian sent to a different curve. A computation of the fundamental group is then a computation with the gluing curves.

In dimension 4 the basic invariant is algebraic: two surfaces in a closed oriented 4-manifold meet in finitely many points, counted with signs, and these counts form a symmetric integer matrix — the intersection form. Much of 4-manifold topology is the question of which matrices occur, and for which manifolds.

DefinitionsH

Definitions

All manifolds are compact, connected and orientable unless said otherwise.

Definition— handlebody and Heegaard splitting

A handlebody of genus gg is a regular neighbourhood of a connected graph with first Betti number gg in R3\R^3 — a ball with gg solid handles attached; its boundary is a closed surface of genus gg. A Heegaard splitting of a closed 3-manifold MM is a decomposition M=V1∪ΣV2M = V_1 \cup_\Sigma V_2 into two handlebodies of the same genus with V1∩V2=∂V1=∂V2=ΣV_1 \cap V_2 = \partial V_1 = \partial V_2 = \Sigma. The least such genus is the Heegaard genus of MM.

Definition— lens space

For coprime integers p≥2p \ge 2 and qq, the lens space L(p,q)L(p, q) is the quotient of S3={(z1,z2)∈C2:∣z1∣2+∣z2∣2=1}S^3 = \{(z_1, z_2) \in \C^2 : |z_1|^2 + |z_2|^2 = 1\} by the free action of Z/p\Z/p generated by (z1,z2)↦(ζz1,ζqz2)(z_1, z_2) \mapsto (\zeta z_1, \zeta^q z_2), ζ=e2πi/p\zeta = e^{2\pi i/p}. It has a genus-1 Heegaard splitting, obtained by gluing two solid tori with the meridian of one sent to a curve of homology class pλ+qμp\lambda + q\mu on the other. (Conventions for the signs differ between books.) L(2,1)=RP3L(2, 1) = \R P^3.

Definition— Dehn surgery

Let K⊂S3K \subset S^3 be a knot with closed tubular neighbourhood N(K)N(K), meridian μ\mu and Seifert longitude λ\lambda (null-homologous in the complement). For coprime p,qp, q, the p/qp/q-surgery on KK is

Sp/q3(K)=(S3∖int⁡N(K))∪h(S1×D2),S^3_{p/q}(K) = \big(S^3 \setminus \operatorname{int} N(K)\big) \cup_h (S^1 \times D^2),

where hh sends the meridian {pt}×∂D2\{\mathrm{pt}\} \times \partial D^2 of the new solid torus to a curve of class pμ+qλp\mu + q\lambda. Surgery on a link is done component by component; integral surgery (q=1q = 1) on a link LL is described by a framed link, an integer for each component, and its linking matrix Λ\Lambda has the framings on the diagonal and pairwise linking numbers off it.

Definition— geometric 3-manifold, hyperbolic 3-manifold

A model geometry is a simply connected homogeneous Riemannian manifold XX with a group of isometries acting transitively with compact stabilisers, maximal among such groups, and admitting a quotient of finite volume. A 3-manifold is geometric if its interior is X/ΓX/\Gamma for a model geometry XX and a discrete group Γ\Gamma of isometries acting freely. A hyperbolic 3-manifold is one with a complete Riemannian metric of constant sectional curvature −1-1; equivalently M=H3/ΓM = \mathbb{H}^3/\Gamma for a torsion-free discrete subgroup Γ⊂PSL(2,C)≅Isom+(H3)\Gamma \subset \mathrm{PSL}(2, \C) \cong \mathrm{Isom}^+(\mathbb{H}^3).

Definition— intersection form; exotic smooth structure

For a closed oriented 4-manifold XX the intersection form is the symmetric bilinear form QX(a,b)=⟨a⌣b,[X]⟩Q_X(a, b) = \langle a \smile b, [X] \rangle on H2(X;Z)/torsionH^2(X; \Z)/\text{torsion}; for classes represented by embedded oriented surfaces it counts their intersection points with signs. By Poincaré duality it is unimodular (its matrix has determinant ±1\pm 1). Its invariants are the rank b2b_2, the signature σ\sigma (number of positive minus negative eigenvalues) and the parity (even if Q(a,a)Q(a, a) is always even). Two smooth manifolds that are homeomorphic but not diffeomorphic are exotic copies of each other.

Worked examplesH

Examples

Example— Spherical space forms and the Poincaré homology sphere

The quotient S3/ΓS^3/\Gamma by a finite subgroup Γ⊂SO(4)\Gamma \subset \mathrm{SO}(4) acting freely is a spherical 3-manifold: lens spaces (Γ\Gamma cyclic), prism manifolds, and the Poincaré homology sphere Σ=S3/I∗\Sigma = S^3/I^*, where I∗I^* is the binary icosahedral group of order 120. Poincaré found it in 1904 as a counterexample to his own first conjecture: H∗(Σ)≅H∗(S3)H_*(\Sigma) \cong H_*(S^3) but π1(Σ)≅I∗\pi_1(\Sigma) \cong I^* is not trivial. It has several other descriptions: the dodecahedral space (opposite faces of a dodecahedron glued with a π/5\pi/5 twist), the Brieskorn sphere Σ(2,3,5)={z12+z23+z35=0}∩S5\Sigma(2,3,5) = \{z_1^2 + z_2^3 + z_3^5 = 0\} \cap S^5, −1-1-surgery on the left-handed trefoil, and the boundary of the E8E_8 plumbing (see the computation below).

Example— $H_1$ of a surgery

For any knot KK, H1(S3∖N(K))≅ZH_1(S^3 \setminus N(K)) \cong \Z is generated by the meridian μ\mu, and the Seifert longitude λ\lambda is null-homologous there. Gluing in the solid torus kills the class of pμ+qλp\mu + q\lambda, that is p[μ]p[\mu]. Hence

H1(Sp/q3(K))≅Z/pH_1\big(S^3_{p/q}(K)\big) \cong \Z/p

for every knot. In particular every ±1/n\pm 1/n-surgery gives a homology sphere, and 00-surgery on the unknot gives S1×S2S^1 \times S^2. For integral surgery on a framed link, H1≅coker⁡ΛH_1 \cong \operatorname{coker} \Lambda, so ∣H1∣=∣det⁡Λ∣|H_1| = |\det \Lambda| when det⁡Λ≠0\det \Lambda \ne 0.

Example— Hyperbolic knot complements

The complement of the figure-eight knot is hyperbolic: Robert Riley (1975) found a discrete faithful representation of its group into PSL(2,Z[ω])\mathrm{PSL}(2, \Z[\omega]), ω=e2πi/3\omega = e^{2\pi i/3}, and Thurston showed it is the union of two regular ideal hyperbolic tetrahedra, with volume 2.02988…2.02988\ldots — the smallest volume of a cusped orientable hyperbolic 3-manifold (Cao–Meyerhoff, 2001). The complement of the trefoil is not hyperbolic: it is Seifert fibred, with geometry SL(2,R)~\widetilde{\mathrm{SL}(2,\R)}. Thurston proved that a knot complement is hyperbolic unless the knot is a torus knot or a satellite knot. The closed orientable hyperbolic 3-manifold of smallest volume is the Weeks manifold, of volume 0.9427…0.9427\ldots (Gabai–Meyerhoff–Milley, 2009).

Example— Simply connected 4-manifolds and their forms

CP2\C P^2 has form ⟨1⟩\langle 1 \rangle; S2×S2S^2 \times S^2 has the hyperbolic form H=(0110)H = \begin{pmatrix} 0 & 1 \\ 1 & 0 \end{pmatrix} (even, signature 0); CP2#CP2‾\C P^2 \# \overline{\C P^2} has ⟨1⟩⊕⟨−1⟩\langle 1 \rangle \oplus \langle -1 \rangle (odd, signature 0); the K3 surface {z04+z14+z24+z34=0}⊂CP3\{z_0^4 + z_1^4 + z_2^4 + z_3^4 = 0\} \subset \C P^3 has 2(−E8)⊕3H2(-E_8) \oplus 3H: rank 22, signature −16-16, even. Here E8E_8 is the Cartan matrix of the Lie algebra e8\mathfrak{e}_8, an even, positive definite, unimodular form of rank 8.

ProofH

Central theorems

Theorem— Theorem 1 (Heegaard splittings exist)

Every closed orientable 3-manifold MM has a Heegaard splitting.

Proof

By Moise's theorem (1952) MM has a triangulation. Let V1V_1 be a regular neighbourhood of its 1-skeleton T(1)T^{(1)}: a union of balls around the vertices and solid tubes along the edges. Since MM is orientable and T(1)T^{(1)} is connected, V1V_1 is a handlebody of genus g=1−χ(T(1))=E−V+1g = 1 - \chi(T^{(1)}) = E - V + 1. Its complement V2=M∖int⁡V1V_2 = M \setminus \operatorname{int} V_1 is a regular neighbourhood of the dual 1-skeleton (a vertex at the centre of each tetrahedron and an edge through each triangle): each tetrahedron minus the neighbourhood of its edges retracts onto a neighbourhood of its centre and the four segments to its faces. So V2V_2 is also a handlebody, and ∂V1=∂V2\partial V_1 = \partial V_2 forces equal genus.

∎

Theorem— Theorem 2 (Lickorish 1962, Wallace 1960)

Every closed orientable 3-manifold is obtained by integral surgery on a link in S3S^3; one may even take every component unknotted with framing ±1\pm 1.

Proof sketch. Two Heegaard splittings of the same genus differ by a homeomorphism of the Heegaard surface. Comparing MM with the standard genus-gg splitting of S3S^3, MM is determined by an element of the mapping class group of the surface. Lickorish proved that this group is generated by Dehn twists along finitely many explicit curves, and each Dehn twist can be realised by a ±1\pm1-surgery on a pushed-in copy of its curve. A full proof is in Rolfsen's Knots and Links, Chapter 9.

Theorem— Proposition 3 (lens spaces)

π1(L(p,q))≅Z/p\pi_1(L(p, q)) \cong \Z/p, so H1(L(p,q))≅Z/pH_1(L(p, q)) \cong \Z/p, and all lens spaces with the same pp have the same homology groups.

Proof

Write L(p,q)=V2∪hV1L(p, q) = V_2 \cup_h V_1 with V1,V2V_1, V_2 solid tori and hh sending the meridian μ1\mu_1 of V1V_1 to a curve cc of class pλ2+qμ2p\lambda_2 + q\mu_2 on ∂V2\partial V_2. V1V_1 is a 2-handle attached along cc (a thickened meridian disc) followed by a 3-ball. By the Seifert–van Kampen theorem, attaching a 2-handle along cc adds the relation [c]=1[c] = 1, and attaching a 3-ball changes nothing. In π1(V2)≅Z=⟨λ2⟩\pi_1(V_2) \cong \Z = \langle \lambda_2 \rangle the meridian μ2\mu_2 is trivial, so [c]=λ2p[c] = \lambda_2^p, and π1(L(p,q))≅⟨λ2∣λ2p⟩≅Z/p\pi_1(L(p, q)) \cong \langle \lambda_2 \mid \lambda_2^p \rangle \cong \Z/p. Since this group is abelian, H1≅π1H_1 \cong \pi_1; Poincaré duality gives H2=0H_2 = 0 and H3=ZH_3 = \Z.

∎

Theorem— Theorem 4 (classification of lens spaces)

Let p≥2p \ge 2 and q,q′q, q' be coprime to pp.

  1. (Reidemeister 1935, Brody 1960.) L(p,q)≅L(p,q′)L(p, q) \cong L(p, q') (homeomorphic) if and only if q′≡±q±1(modp)q' \equiv \pm q^{\pm 1} \pmod p.
  2. (Whitehead 1941.) L(p,q)≃L(p,q′)L(p, q) \simeq L(p, q') (homotopy equivalent) if and only if qq′≡±n2(modp)qq' \equiv \pm n^2 \pmod p for some integer nn.

The homeomorphism invariant is Reidemeister torsion, built from the chain complex of the universal cover twisted by characters of Z/p\Z/p; it is the first invariant in topology that is not a homotopy invariant. Arithmetic now does the topology:

Theorem— Corollary 5

L(7,1)L(7, 1) and L(7,2)L(7, 2) are homotopy equivalent but not homeomorphic. L(5,1)L(5, 1) and L(5,2)L(5, 2) have isomorphic fundamental groups and homology, but are not homotopy equivalent.

Proof

Modulo 7: 1⋅2=2≡321 \cdot 2 = 2 \equiv 3^2, but 2≢±1=±1±12 \not\equiv \pm 1 = \pm 1^{\pm1}. Modulo 5: the squares of units are 11 and 4≡−14 \equiv -1, so ±n2∈{1,4}\pm n^2 \in \{1, 4\}, and 1⋅2=21 \cdot 2 = 2 is not among them. Apply Theorem 4. (Both congruence computations are checked in Lean below.)

∎

Theorem— Theorem 6 (geometrisation; Thurston's conjecture, proved by Perelman 2002–2003)

Every closed orientable 3-manifold MM decomposes canonically:

  1. (Kneser 1929, Milnor 1962.) MM is a connected sum of prime 3-manifolds, uniquely up to order.
  2. (Jaco–Shalen, Johannson 1979.) Each prime MM contains a minimal collection of disjoint incompressible tori, unique up to isotopy, cutting it into pieces that are Seifert fibred or atoroidal.
  3. (Perelman.) Each piece is geometric, with one of the eight Thurston geometries
S3,E3,H3,S2×R,H2×R,SL(2,R)~,Nil,Sol.S^3,\quad \mathbb{E}^3,\quad \mathbb{H}^3,\quad S^2 \times \R,\quad \mathbb{H}^2 \times \R,\quad \widetilde{\mathrm{SL}(2, \R)},\quad \mathrm{Nil},\quad \mathrm{Sol}.

Consequences: elliptisation (a closed 3-manifold with finite fundamental group is spherical, S3/ΓS^3/\Gamma), and in particular the Poincaré conjecture (a closed simply connected 3-manifold is homeomorphic to S3S^3); and hyperbolisation (a closed prime atoroidal 3-manifold with infinite fundamental group is hyperbolic). Six of the eight geometries describe Seifert fibred spaces, Sol describes torus bundles with Anosov monodromy, and H3\mathbb{H}^3 is the generic case. The proof is a tour de force of geometric analysis (see geometric analysis): Ricci flow with surgery, Perelman's entropy and non-collapsing, and the analysis of singularities; complete expositions are by Morgan–Tian and by Kleiner–Lott.

Theorem— Theorem 7 (Mostow rigidity 1968; Prasad 1973)

If MM and NN are complete hyperbolic manifolds of finite volume and dimension n≥3n \ge 3, every isomorphism π1(M)≅π1(N)\pi_1(M) \cong \pi_1(N) is induced by an isometry M→NM \to N.

So for hyperbolic 3-manifolds, geometric quantities — volume, lengths of closed geodesics — are topological invariants. In dimension 2 this fails completely: a closed surface of genus g≥2g \ge 2 has a (6g−6)(6g - 6)-dimensional Teichmüller space of hyperbolic metrics.

Theorem— Theorem 8 (four-manifolds: Whitehead–Milnor, Freedman 1982, Rokhlin 1952, Donaldson 1983)

Let XX be a closed, simply connected 4-manifold with intersection form QQ.

  1. (Whitehead 1949, Milnor 1958.) The homotopy type of XX is determined by QQ up to isomorphism.
  2. (Freedman.) Every unimodular symmetric form is the intersection form of a closed simply connected topological 4-manifold. For QQ even this manifold is unique up to homeomorphism; for QQ odd there are exactly two, distinguished by the Kirby–Siebenmann invariant, and at most one of them is smoothable.
  3. (Rokhlin.) If XX is smooth and QQ is even, then σ(Q)≡0(mod16)\sigma(Q) \equiv 0 \pmod{16}.
  4. (Donaldson.) If XX is smooth and QQ is definite, then Q≅±(⟨1⟩⊕⋯⊕⟨1⟩)Q \cong \pm(\langle 1 \rangle \oplus \cdots \oplus \langle 1 \rangle) over Z\Z.

Theorem— Proposition 9 (the E₈ form)

The E8E_8 form is even, unimodular and positive definite, of signature 8.

Proof

Its diagonal entries are all 2 and it is symmetric, so x⊤E8x=∑i2xi2+2∑i<j(E8)ijxixjx^\top E_8 x = \sum_i 2x_i^2 + 2\sum_{i < j} (E_8)_{ij} x_i x_j is even. Its determinant is 1 (by row reduction, or see the Lean below). Completing squares,

60 x⊤E8x=30(2x0−x2)2+30(2x1−x3)2+10(3x2−2x3)2+2(5x3−6x4)2+3(4x4−5x5)2+5(3x5−4x6)2+10(2x6−3x7)2+30x7260\, x^\top E_8 x = 30(2x_0 - x_2)^2 + 30(2x_1 - x_3)^2 + 10(3x_2 - 2x_3)^2 + 2(5x_3 - 6x_4)^2 + 3(4x_4 - 5x_5)^2 + 5(3x_5 - 4x_6)^2 + 10(2x_6 - 3x_7)^2 + 30x_7^2

(with the labelling of the nodes used in Mathlib, where node 3 is the branch point). If this vanishes then x7=0x_7 = 0, then x6=0x_6 = 0, and so on back to x0=0x_0 = 0. So the form is positive definite and its signature is its rank, 8.

∎

Theorem— Corollary 10 (a topological 4-manifold with no smooth structure)

There is a closed simply connected topological 4-manifold (Freedman's E8E_8-manifold) that admits no smooth structure.

Proof

By Freedman's theorem there is a closed simply connected topological 4-manifold with form E8E_8. If it were smooth, Rokhlin's theorem would force 16∣σ=816 \mid \sigma = 8, which is false (Donaldson's theorem gives a second obstruction, since E8E_8 is definite but not diagonalisable: a diagonal form ±⟨1⟩⊕8\pm\langle 1 \rangle^{\oplus 8} is odd).

∎

The same reasoning applied to E8⊕E8E_8 \oplus E_8 (signature 16, so Rokhlin is silent) needs Donaldson. And combining Freedman with Donaldson produces exotic R4\R^4s: smooth manifolds homeomorphic but not diffeomorphic to R4\R^4 (found in the early 1980s by combining the work of Freedman and Donaldson, with explicit constructions by Gompf); Taubes (1987) showed there are uncountably many. For n≠4n \ne 4, Rn\R^n has a unique smooth structure.

ExplanationH

The landscape: what is known and what is open

Established in dimension 3. Geometrisation (Perelman). The virtual Haken and virtual fibring conjectures: every closed hyperbolic 3-manifold has a finite cover that fibres over the circle (Agol 2013, building on Wise, Kahn–Markovic and Haglund–Wise). Tameness (Agol; Calegari–Gabai, 2006) and the ending lamination theorem (Minsky; Brock–Canary–Minsky), which together describe hyperbolic 3-manifolds with finitely generated fundamental group. Algorithmic results: the homeomorphism problem for closed orientable 3-manifolds is decidable (a consequence of geometrisation, written out by Kuperberg, 2019), unknot recognition is decidable (Haken, 1961) and lies in NP (Hass–Lagarias–Pippenger, 1999).

Established in dimension 4. Freedman's classification of simply connected topological 4-manifolds; Donaldson's theorems from Yang–Mills instantons; Seiberg–Witten theory (1994), which simplified and extended them; Furuta's 10/8 theorem (2001): a smooth closed spin 4-manifold with σ≠0\sigma \ne 0 has b2≥108∣σ∣+2b_2 \ge \tfrac{10}{8}|\sigma| + 2, later sharpened by Hopkins, Lin, Shi and Xu using equivariant stable homotopy theory (see stable homotopy theory); many exotic structures on closed manifolds (Donaldson, 1987: the Dolgachev surface is homeomorphic but not diffeomorphic to CP2#9CP2‾\C P^2 \# 9\overline{\C P^2}).

Open problems.

  • The smooth 4-dimensional Poincaré conjecture: is every smooth homotopy 4-sphere diffeomorphic to S4S^4? Equivalently, does S4S^4 have an exotic smooth structure? Likewise open for CP2\C P^2 and S2×S2S^2 \times S^2.
  • The 11/8 conjecture (Matsumoto, 1982): a smooth closed spin 4-manifold has b2≥118∣σ∣b_2 \ge \tfrac{11}{8}|\sigma|. The K3 surface (b2=22b_2 = 22, σ=−16\sigma = -16) shows it would be sharp.
  • The L-space conjecture (Boyer–Gordon–Watson, 2013; Juhász): for an irreducible rational homology 3-sphere, having left-orderable fundamental group, admitting a co-oriented taut foliation, and not being a Heegaard Floer L-space are equivalent.
  • The volume conjecture (Kashaev; H. and J. Murakami): the hyperbolic volume of a knot complement is determined by the growth of coloured Jones polynomials.
  • Whether unknot recognition can be done in polynomial time.

A note on what "low-dimensional" leaves out. Dimensions n≥5n \ge 5 are governed by surgery theory (Browder, Novikov, Sullivan, Wall), which reduces classification to homotopy theory and algebra; there the Poincaré conjecture was solved first.

Formal mathematicsF

What Lean can say: spheres, congruences and the E₈ lattice

Mathlib has smooth manifolds and knows that spheres are among them:

three_sphere_isManifoldLean 4Applies a library theoremFormally verified
/-- The unit sphere `S³ = {x ∈ ℝ⁴ : ‖x‖ = 1}` is an analytic (in particular smooth) manifold of
dimension 3, with charts given by stereographic projection. This is Mathlib's instance
`EuclideanSpace.instIsManifoldSphere`. By Perelman's theorem it is the only closed, simply
connected 3-manifold up to homeomorphism (and, in dimension 3, up to diffeomorphism). -/
theorem three_sphere_isManifold :
    IsManifold (𝓡 3) ω (sphere (0 : EuclideanSpace ℝ (Fin 4)) 1) :=
  inferInstance
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

It has no 3-manifold topology (no Heegaard splittings, Dehn surgery, Reidemeister torsion or hyperbolic 3-manifolds) and no 4-manifold theory, so Theorems 4, 6, 7 and 8 are far out of reach. What can be formalised is the arithmetic those theorems reduce questions to. The two classification criteria for lens spaces, as relations on (Z/p)×(\Z/p)^\times:

LensHomeoRelLean 4Formally verified
/-- The **Reidemeister–Brody relation** on residues coprime to `p`: `q' ≡ ±q` or `qq' ≡ ±1`
(mod `p`), i.e. `q' ∈ {q, −q, q⁻¹, −q⁻¹}`. By the classification of lens spaces (Reidemeister
1935 for the combinatorial version, Brody 1960 for homeomorphism), `L(p, q)` and `L(p, q')` are
homeomorphic exactly when this relation holds. -/
def LensHomeoRel (q q' : (ZMod p)ˣ) : Prop :=
  q' = q ∨ q' = -q ∨ q' = q⁻¹ ∨ q' = -q⁻¹
Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
LensHomotopyRelLean 4Formally verified
/-- The **Whitehead relation**: `qq' ≡ ±n²` (mod `p`) for some unit `n`. By J. H. C. Whitehead
(1941), `L(p, q)` and `L(p, q')` are homotopy equivalent exactly when this relation holds. -/
def LensHomotopyRel (q q' : (ZMod p)ˣ) : Prop :=
  ∃ n : (ZMod p)ˣ, q * q' = n ^ 2 ∨ q * q' = -(n ^ 2)
Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

The homeomorphism criterion is an equivalence relation (as it must be, if Theorem 4 is true), and it implies the homotopy criterion (as it must, since homeomorphic spaces are homotopy equivalent) — a consistency check on the theorem's statement:

lensHomeoRel_equivalenceLean 4Proved here from basic factsFormally verified
/-- The Reidemeister–Brody relation is an equivalence relation. The set `{q, −q, q⁻¹, −q⁻¹}` is the
orbit of `q` under the Klein four-group generated by negation and inversion (which commute), so
each case of transitivity is an identity such as `(−q)⁻¹ = −q⁻¹` or `(q⁻¹)⁻¹ = q`. -/
theorem lensHomeoRel_equivalence : Equivalence (LensHomeoRel (p := p)) where
  refl q := Or.inl rfl
  symm := by
    intro q q' h
    rcases h with rfl | rfl | rfl | rfl
    · exact Or.inl rfl
    · exact Or.inr (Or.inl (neg_neg q).symm)
    · exact Or.inr (Or.inr (Or.inl (inv_inv q).symm))
    · refine Or.inr (Or.inr (Or.inr ?_))
      rw [inv_neg, neg_neg, inv_inv]
  trans := by
    intro q q' q'' h₁ h₂
    unfold LensHomeoRel at *
    rcases h₁ with rfl | rfl | rfl | rfl <;> rcases h₂ with rfl | rfl | rfl | rfl <;>
      simp [inv_neg]
Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
lensHomotopyRel_of_lensHomeoRelLean 4Proved here from basic factsFormally verified
/-- Homeomorphic lens spaces are homotopy equivalent, at the level of the criteria: if
`q' ∈ {±q, ±q⁻¹}` then `qq'` is `±q²` or `±1 = ±1²`, a square up to sign. -/
theorem lensHomotopyRel_of_lensHomeoRel {q q' : (ZMod p)ˣ} (h : LensHomeoRel q q') :
    LensHomotopyRel q q' := by
  rcases h with h | h | h | h <;> rw [h]
  · exact ⟨q, Or.inl (sq q).symm⟩
  · exact ⟨q, Or.inr (by rw [mul_neg, sq])⟩
  · exact ⟨1, Or.inl (by simp)⟩
  · exact ⟨1, Or.inr (by simp)⟩
Axioms used: propext, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

The congruences of Corollary 5, checked by decide:

lens_sevenLean 4Proved here from basic factsFormally verified
/-- **`L(7, 1)` and `L(7, 2)`**: the Whitehead relation holds (`1 · 2 ≡ 3²` mod 7) but the
Reidemeister–Brody relation fails (`2 ∉ {±1}` mod 7). With the classification theorems, these two
lens spaces are homotopy equivalent but not homeomorphic. Checked by `decide` over the six
units of `ZMod 7`. -/
theorem lens_seven :
    LensHomotopyRel (p := 7) 1 (ZMod.unitOfCoprime 2 (by norm_num)) ∧
      ¬ LensHomeoRel (p := 7) 1 (ZMod.unitOfCoprime 2 (by norm_num)) := by
  unfold LensHomotopyRel LensHomeoRel
  decide
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
lens_fiveLean 4Proved here from basic factsFormally verified
/-- **`L(5, 1)` and `L(5, 2)`**: the Whitehead relation fails, since `1 · 2 = 2` is not `±n²`
modulo 5 (the squares of units are `1` and `4 = −1`). With Whitehead's theorem: two closed
3-manifolds with the same fundamental group `ℤ/5` and the same homology groups that are not even
homotopy equivalent. -/
theorem lens_five :
    ¬ LensHomotopyRel (p := 5) 1 (ZMod.unitOfCoprime 2 (by norm_num)) := by
  unfold LensHomotopyRel
  decide
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
lens_five_fourLean 4Proved here from basic factsFormally verified
/-- **`L(5, 1)` and `L(5, 4)`** satisfy the Reidemeister–Brody relation, because `4 ≡ −1`
(mod 5); indeed `L(p, q)` and `L(p, −q)` are always homeomorphic, by a homeomorphism that
reverses orientation. -/
theorem lens_five_four : LensHomeoRel (p := 5) 1 (ZMod.unitOfCoprime 4 (by norm_num)) := by
  unfold LensHomeoRel
  decide
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

Proposition 9, in full. Mathlib defines the Cartan matrix E8E_8 and evaluates its determinant; evenness follows from a general lemma, and positive definiteness from the completed squares of the human proof:

even_form_of_even_diagLean 4Proved here from basic factsFormally verified
/-- **Even forms.** If `A` is a symmetric integer matrix whose diagonal entries are even, then
`xᵀAx` is even for every integer vector `x`. Proof: write `A = D + U + Uᵀ` with `D` diagonal and
`U` strictly upper triangular; then `xᵀAx = xᵀDx + 2·xᵀUx`, and `xᵀDx = Σ Aᵢᵢ xᵢ²` is even. For
the intersection form of a closed simply connected 4-manifold, "even" is equivalent to the
second Stiefel–Whitney class vanishing (the manifold is spin). -/
theorem even_form_of_even_diag {n : ℕ} (A : Matrix (Fin n) (Fin n) ℤ) (hA : A.IsSymm)
    (hdiag : ∀ i, Even (A i i)) (x : Fin n → ℤ) : Even (x ⬝ᵥ (A *ᵥ x)) := by
  classical
  let U : Matrix (Fin n) (Fin n) ℤ := Matrix.of fun i j => if i < j then A i j else 0
  let D : Matrix (Fin n) (Fin n) ℤ := Matrix.diagonal fun i => A i i
  have hsplit : A = D + U + Uᵀ := by
    ext i j
    simp only [D, U, Matrix.add_apply, Matrix.diagonal_apply, Matrix.transpose_apply,
      Matrix.of_apply]
    rcases lt_trichotomy i j with h | rfl | h
    · simp [h, h.ne, not_lt.mpr h.le]
    · simp
    · simp [h, h.ne', not_lt.mpr h.le]
      exact hA.apply j i
  have hU : x ⬝ᵥ (Uᵀ *ᵥ x) = x ⬝ᵥ (U *ᵥ x) := by
    rw [dotProduct_mulVec, vecMul_transpose, dotProduct_comm]
  have hD : Even (x ⬝ᵥ (D *ᵥ x)) := by
    simp only [D, mulVec_diagonal, dotProduct]
    refine Finset.even_sum _ fun i _ => ?_
    obtain ⟨k, hk⟩ := hdiag i
    exact ⟨x i * k * x i, by rw [hk]; ring⟩
  rw [hsplit, add_mulVec, add_mulVec, dotProduct_add, dotProduct_add, hU, add_assoc]
  exact hD.add ⟨x ⬝ᵥ (U *ᵥ x), rfl⟩
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
e8_evenLean 4Proved here from basic factsFormally verified
/-- The **E₈ form** — the Cartan matrix of the exceptional Lie algebra `e₈`, Mathlib's
`CartanMatrix.E 8` — is even: `xᵀE₈x ∈ 2ℤ` for all `x ∈ ℤ⁸`. It is symmetric with `2`s on the
diagonal (`CartanMatrix.E_isSymm`, `CartanMatrix.E_diag`), so `even_form_of_even_diag` applies.
Freedman showed that there is a closed simply connected *topological* 4-manifold with
intersection form E₈; Rokhlin's theorem shows it has no smooth structure. -/
theorem e8_even (x : Fin 8 → ℤ) : Even (x ⬝ᵥ (CartanMatrix.E 8 *ᵥ x)) :=
  even_form_of_even_diag _ (CartanMatrix.E_isSymm 8)
    (fun i => ⟨1, by rw [CartanMatrix.E_diag]; rfl⟩) x
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
e8_unimodularLean 4Applies a library theoremFormally verified
/-- The E₈ form is **unimodular**: its determinant is `1`, so it is the intersection form of a
closed 4-manifold that could exist by Poincaré duality. This is Mathlib's
`CartanMatrix.E₈_det`, proved by a determinant-evaluation tactic. -/
theorem e8_unimodular : (CartanMatrix.E 8).det = 1 :=
  CartanMatrix.E₈_det
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor
e8_posDefLean 4Proved here from basic factsFormally verified
/-- The E₈ form is **positive definite**: `xᵀE₈x > 0` for every non-zero `x ∈ ℤ⁸`. Proof by
completing squares (the `LDLᵀ` decomposition, cleared of denominators):
`60·xᵀE₈x = 30(2x₀ − x₂)² + 30(2x₁ − x₃)² + 10(3x₂ − 2x₃)² + 2(5x₃ − 6x₄)² + 3(4x₄ − 5x₅)²
+ 5(3x₅ − 4x₆)² + 10(2x₆ − 3x₇)² + 30x₇²`. If the form vanished, every square would vanish,
and back-substitution from `x₇ = 0` gives `x = 0`. Together with `e8_even` and
`e8_unimodular`: E₈ is an even, unimodular, positive definite form of rank 8 — so its
signature is 8, which is not divisible by 16. -/
theorem e8_posDef (x : Fin 8 → ℤ) (hx : x ≠ 0) : 0 < x ⬝ᵥ (CartanMatrix.E 8 *ᵥ x) := by
  have hQ : x ⬝ᵥ (CartanMatrix.E 8 *ᵥ x) =
      2 * x 0 ^ 2 - 2 * x 0 * x 2 + 2 * x 1 ^ 2 - 2 * x 1 * x 3 + 2 * x 2 ^ 2 - 2 * x 2 * x 3
        + 2 * x 3 ^ 2 - 2 * x 3 * x 4 + 2 * x 4 ^ 2 - 2 * x 4 * x 5 + 2 * x 5 ^ 2
        - 2 * x 5 * x 6 + 2 * x 6 ^ 2 - 2 * x 6 * x 7 + 2 * x 7 ^ 2 := by
    rw [CartanMatrix.E_eight_eq]
    simp [Matrix.mulVec, dotProduct, Fin.sum_univ_eight]
    ring
  rw [hQ]
  by_contra hle
  push Not at hle
  have s0 := sq_nonneg (2 * x 0 - x 2)
  have s1 := sq_nonneg (2 * x 1 - x 3)
  have s2 := sq_nonneg (3 * x 2 - 2 * x 3)
  have s3 := sq_nonneg (5 * x 3 - 6 * x 4)
  have s4 := sq_nonneg (4 * x 4 - 5 * x 5)
  have s5 := sq_nonneg (3 * x 5 - 4 * x 6)
  have s6 := sq_nonneg (2 * x 6 - 3 * x 7)
  have s7 := sq_nonneg (x 7)
  have z7 : x 7 = 0 := pow_eq_zero_iff two_ne_zero |>.mp (by linarith)
  have z6 : x 6 = 0 := by
    have : (2 * x 6 - 3 * x 7) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  have z5 : x 5 = 0 := by
    have : (3 * x 5 - 4 * x 6) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  have z4 : x 4 = 0 := by
    have : (4 * x 4 - 5 * x 5) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  have z3 : x 3 = 0 := by
    have : (5 * x 3 - 6 * x 4) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  have z2 : x 2 = 0 := by
    have : (3 * x 2 - 2 * x 3) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  have z1 : x 1 = 0 := by
    have : (2 * x 1 - x 3) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  have z0 : x 0 = 0 := by
    have : (2 * x 0 - x 2) ^ 2 = 0 := by linarith
    have := pow_eq_zero_iff two_ne_zero |>.mp this
    omega
  apply hx
  ext i
  fin_cases i <;> assumption
Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/LowDimensionalTopology.leanTry it in the Lean web editor

What is not formalised. Everything topological: that these congruences classify lens spaces, the existence of the E8E_8-manifold (Freedman), and the obstructions of Rokhlin and Donaldson. Those statements live in the prose, attributed to their authors.

ComputationC

Lens spaces and intersection forms by machine

The first experiment applies Theorem 4 to every lens space with p≤15p \le 15, counting homeomorphism and homotopy classes, and computes the moduli that enter the Reidemeister torsion: they differ for L(7,1)L(7, 1) and L(7,2)L(7, 2) and agree for L(7,2)L(7, 2) and L(7,4)L(7, 4).

Lens spaces: homeomorphism versus homotopy, by arithmeticPythonExact computationExhaustive finite checkNumerical approximationComputationally tested
"""Lens spaces: when are L(p, q) and L(p, q') the same?

Every lens space L(p, q) has fundamental group Z/p and the same homology, so
algebraic topology's first tools cannot tell them apart. The classification
reduces the question to arithmetic modulo p:

* homeomorphic  <=> q' = +-q or q q' = +-1 (mod p)
  (Reidemeister 1935, piecewise-linear; Brody 1960, homeomorphism);
* homotopy equivalent <=> q q' = +-n^2 (mod p) for some n
  (J. H. C. Whitehead 1941).

We count the classes of both relations exhaustively for small p, find the
first pairs that are homotopy equivalent but not homeomorphic, and compute the
moduli |(z^k - 1)(z^(kr) - 1)|, z = exp(2 pi i / p), qr = 1 (mod p), which
appear in the Reidemeister torsion, the invariant that tells them apart.
"""

import cmath
import math

def units(p):
    """Residues 1 <= q < p coprime to p."""
    return [q for q in range(1, p) if math.gcd(q, p) == 1]

def inverse(q, p):
    """Inverse of q modulo p."""
    return pow(q, -1, p)

def homeomorphic(p, q, r):
    """Reidemeister-Brody criterion: r = +-q or r = +-q^(-1) (mod p)."""
    qi = inverse(q, p)
    return r % p in {q % p, -q % p, qi, -qi % p}

def homotopy_equivalent(p, q, r):
    """Whitehead's criterion: q r = +-n^2 (mod p) for some unit n."""
    squares = {n * n % p for n in units(p)}
    return q * r % p in squares or -q * r % p in squares

def classes(p, relation):
    """Partition the units mod p into classes of an equivalence relation."""
    out = []
    for q in units(p):
        for c in out:
            if relation(p, c[0], q):
                c.append(q)
                break
        else:
            out.append([q])
    return out

def torsion_moduli(p, q):
    """Sorted moduli |(z^k - 1)(z^(k r) - 1)| for k = 1..p-1, rounded."""
    r = inverse(q, p)
    z = [cmath.exp(2j * math.pi * k / p) for k in range(p)]
    vals = [abs((z[k] - 1) * (z[k * r % p] - 1)) for k in range(1, p)]
    return sorted(round(v, 6) for v in vals)

def main():
    print("Lens spaces L(p, q), 0 < q < p, gcd(p, q) = 1 (all have pi_1 = Z/p)")
    print("  p  units  homeomorphism classes  homotopy classes")
    surprises = []
    for p in range(2, 16):
        h = classes(p, homeomorphic)
        e = classes(p, homotopy_equivalent)
        print(f"{p:3d}  {len(units(p)):5d}  {len(h):21d}  {len(e):16d}")
        for q in units(p):
            for r in units(p):
                if q < r and homotopy_equivalent(p, q, r) and \
                        not homeomorphic(p, q, r):
                    surprises.append((p, q, r))
    print(f"{len(surprises)} pairs (p <= 15) are homotopy equivalent but not "
          "homeomorphic; the first:")
    print("  " + ", ".join(f"L({p},{q}) ~ L({p},{r})"
                           for p, q, r in surprises[:3]))
    print(f"L(5,1), L(5,2) homotopy equivalent? {homotopy_equivalent(5, 1, 2)}")
    print()
    print("Torsion moduli |(z^k - 1)(z^(kr) - 1)|, k = 1..6, for p = 7:")
    for q in (1, 2, 4):
        print(f"  L(7,{q}): " + " ".join(f"{v:.4f}" for v in torsion_moduli(7, q)))
    print("L(7,2) and L(7,4) agree (4 = 2^(-1) mod 7); L(7,1) differs.")
    print()
    print("Epistemic status: the class counts are exact and exhaustive for the")
    print("arithmetic criteria with p <= 15. That these criteria classify lens")
    print("spaces up to homeomorphism and homotopy equivalence is the theorem of")
    print("Reidemeister, Brody and Whitehead, cited and not verified here. The")
    print("torsion moduli are floating-point values, illustrating why the torsion")
    print("distinguishes L(7,1) from L(7,2); they are not a proof.")

if __name__ == "__main__":
    main()
Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The second computes the invariants of intersection forms exactly — rank, signature by diagonalisation over Q\Q (Sylvester's law of inertia), determinant and parity — and records what Freedman, Rokhlin and Donaldson say about each form. It also computes ∣H1∣=∣det⁡Λ∣|H_1| = |\det \Lambda| for some surgeries, including the E8E_8 plumbing, whose boundary is the Poincaré homology sphere.

Intersection forms: E8, Rokhlin, Freedman and DonaldsonPythonExact computationComputationally tested
"""Intersection forms of 4-manifolds: rank, signature, parity, determinant.

The intersection form of a closed simply connected 4-manifold is a symmetric
unimodular integer matrix (determinant +-1). We compute, exactly:

* the determinant and the signature (by diagonalising the form by congruence
  over the rationals; Sylvester's law of inertia says the signs of the
  diagonal entries do not depend on how we do it);
* the parity (even if every diagonal entry is even, as for E8);

and apply three theorems that the computation itself cannot prove:
Freedman (1982): every unimodular form is the form of a closed simply
connected topological 4-manifold; Rokhlin (1952): if a smooth one has an even
form, the signature is divisible by 16; Donaldson (1983): if a smooth one has
a definite form, the form is diagonal (+-1's) after a change of basis.
We also compute |det| of linking matrices of framed links, which is the order
of H_1 of the 3-manifold obtained by integral surgery (infinite if det = 0).
"""

from fractions import Fraction

E8_EDGES = [(0, 2), (1, 3), (2, 3), (3, 4), (4, 5), (5, 6), (6, 7)]

def e8():
    """The E8 form (Cartan matrix, same labelling as Mathlib's CartanMatrix.E 8)."""
    m = [[2 if i == j else 0 for j in range(8)] for i in range(8)]
    for i, j in E8_EDGES:
        m[i][j] = m[j][i] = -1
    return m

def direct_sum(*blocks):
    """Block-diagonal sum of square integer matrices."""
    n = sum(len(b) for b in blocks)
    m = [[0] * n for _ in range(n)]
    k = 0
    for b in blocks:
        for i, row in enumerate(b):
            for j, v in enumerate(row):
                m[k + i][k + j] = v
        k += len(b)
    return m

def scale(m, c):
    """The matrix c * m."""
    return [[c * v for v in row] for row in m]

H = [[0, 1], [1, 0]]

def diagonalise(m):
    """Diagonal entries of a rational congruence diagonalisation P^T M P."""
    a = [[Fraction(v) for v in row] for row in m]
    n = len(a)
    diag = []
    for i in range(n):
        if a[i][i] == 0:
            j = next((j for j in range(i + 1, n) if a[j][j] != 0), None)
            if j is None:
                j = next((j for j in range(i + 1, n) if a[i][j] != 0), None)
                if j is not None:  # replace e_i by e_i + e_j
                    for k in range(n):
                        a[i][k] += a[j][k]
                    for k in range(n):
                        a[k][i] += a[k][j]
            else:
                a[i], a[j] = a[j], a[i]
                for row in a:
                    row[i], row[j] = row[j], row[i]
        p = a[i][i]
        diag.append(p)
        if p == 0:
            continue
        for r in range(i + 1, n):
            f = a[r][i] / p
            for k in range(n):
                a[r][k] -= f * a[i][k]
            for k in range(n):
                a[k][r] -= f * a[k][i]
    return diag

def invariants(m):
    """(rank, signature, determinant, even?) of a symmetric integer matrix."""
    d = diagonalise(m)
    det = Fraction(1)
    for v in d:
        det *= v
    sig = sum(1 for v in d if v > 0) - sum(1 for v in d if v < 0)
    even = all(m[i][i] % 2 == 0 for i in range(len(m)))
    return len(m), sig, int(det), even

FORMS = [
    ("<1>        (CP^2)", [[1]]),
    ("<1>+<-1>   (CP^2 # -CP^2)", [[1, 0], [0, -1]]),
    ("H          (S^2 x S^2)", H),
    ("E8", e8()),
    ("E8+E8", direct_sum(e8(), e8())),
    ("2(-E8)+3H  (K3 surface)", direct_sum(scale(e8(), -1), scale(e8(), -1),
                                           H, H, H)),
]

def main():
    print("form                         rank  sign  det  parity  smooth?")
    for name, m in FORMS:
        rank, sig, det, even = invariants(m)
        definite = abs(sig) == rank
        if even and sig % 16:
            verdict = "no (Rokhlin)"
        elif even and definite:
            verdict = "no (Donaldson)"
        else:
            verdict = "yes"
        parity = "even" if even else "odd"
        print(f"{name:27s} {rank:5d} {sig:5d} {det:4d}  {parity:6s}  {verdict}")
    print("Freedman: each form above is realised by a topological manifold.")
    print()
    print("Integral surgery on a framed link: |H_1| = |det(linking matrix)|")
    links = [("0-surgery on the unknot", [[0]]),
             ("5-surgery on the unknot (L(5,1))", [[5]]),
             ("Hopf link, framings 2 and 3", [[2, 1], [1, 3]]),
             ("E8 plumbing, framings -2", scale(e8(), -1))]
    for name, m in links:
        det = invariants(m)[2]
        order = "infinite (S^1 x S^2)" if det == 0 else str(abs(det))
        print(f"  {name:34s} |H_1| = {order}")
    print("The last is the Poincare homology sphere: H_1 = 0, yet pi_1 has")
    print("order 120 (the binary icosahedral group).")
    print()
    print("Epistemic status: the ranks, signatures, determinants and parities")
    print("are exact rational computations. The 'smooth?' column applies the")
    print("theorems of Rokhlin and Donaldson, and the existence statement is")
    print("Freedman's theorem; none of these is proved by this program, and")
    print("'yes' only means these obstructions do not apply (each such form is")
    print("in fact realised by a smooth manifold, named in the first column).")

if __name__ == "__main__":
    main()
Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.
Explore

Explore: knots, tori and hyperbolic triangles

Knot complements. The trefoil and the figure-eight knot are the two simplest non-trivial knots. Tricolourability shows the trefoil is knotted; but the deeper difference is geometric: the figure-eight complement is hyperbolic, the trefoil complement is Seifert fibred. Surgery on either produces infinitely many 3-manifolds.

Colouring knots with three colours

Both are knotted; only the figure-eight knot has a hyperbolic complement.

????

Click an arc to change its colour (or focus it and press Enter, or 1, 2, 3). An arc runs from one under-crossing to the next.

colour 1 (terracotta, circle)colour 2 (violet, triangle)colour 3 (teal, square)
Figure-eight knot4₁
Crossings in this diagram
4
Crossing number (fewest possible)
4

Arcs coloured: 0 of 4.

Why this rule? Any two diagrams of the same knot are related by three kinds of local moves, the Reidemeister moves: adding or removing a twist, sliding one strand over another, and sliding a strand past a crossing. Each move turns a valid colouring with two or more colours into another one.

The figure-eight knot cannot be tricoloured — just like the unknot. Yet it is knotted, as other invariants (such as the Jones polynomial) prove. When an invariant gives the same answer for two knots it proves nothing: invariants can fail to tell knots apart.

So tricolourability is a knot invariant: if one diagram of a knot can be tricoloured, every diagram of it can. A plain circle has just one arc, so the unknot cannot be tricoloured.

The Heegaard torus. A genus-1 Heegaard surface is a torus; the lens space is determined by which curve on it bounds a disc on the other side. The square with opposite sides glued is that torus: a loop running pp times across one way and qq times the other is the curve along which the meridian disc is glued.

The Heegaard surface of a lens space

Walk around the torus: the two directions are the meridian and the longitude of a solid torus.

abab

Keys: ↑ forward, ↓ back, ← and → turn, Space walks or stops. You can also drag it.

Torusa b a⁻¹ b⁻¹
Orientable
Yes
Euler characteristic
χ = 0

Gluing turns the 4 corners into V = 1, the 4 sides into E = 2 and the square into F = 1: V − E + F = 1 − 2 + 1 = 0

Same way round as at the start.

Sides crossed so far: 0

Opposite sides are glued with arrows pointing the same way. Walk off the right side and you come back on the left, the same way round. However it walks, the flatlander is never mirrored: the torus is orientable.

Hyperbolic geometry, one dimension down. Thurston's insight was that most 3-manifolds are hyperbolic. In H2\mathbb{H}^2, triangles have angle sum less than π\pi and area equal to the defect; the same happens in H3\mathbb{H}^3, where the regular ideal tetrahedron — all vertices at infinity — has volume 1.01494…1.01494\ldots, and two of them make the figure-eight knot complement.

Curvature −1 and curvature +1

Two of Thurston's eight geometries are built on these: ℍ³ and S³.

21.8°24.3°28.3°ABC

Poincaré disk model: the sides are arcs of circles that meet the boundary at right angles (dashed: each side extended). The boundary circle is infinitely far away.

  • ∠A21.8°
  • ∠B24.3°
  • ∠C28.3°

∠A + ∠B + ∠C = 74.4°

Angle defect (180° − sum)
105.6° = 1.843 rad
Area (curvature −1), measured numerically
1.843

π − (∠A + ∠B + ∠C) = AreaIn the hyperbolic plane with curvature −1, the defect in radians equals the area. The area is computed separately, by numerical integration.

∠A + ∠B + ∠C − π = K · Area

Flat planeK = 0∠A+∠B+∠C = 180°
SphereK = 1/R²∠A+∠B+∠C > 180°
Hyperbolic planeK = −1∠A+∠B+∠C < 180°

This is a first glimpse of the Gauss–Bonnet theorem: for a triangle whose sides are geodesics (shortest paths), the angle sum minus π equals the total curvature inside it. Here the curvature K is the same everywhere; on other surfaces you add up (integrate) K over the area.

Exercises

Exercises

1. Low-dimensional topology: 3- and 4-manifolds

Warm-upHuman

Let KK be the figure-eight knot. What is the order of H1(S7/33(K))H_1\big(S^3_{7/3}(K)\big), the first homology of 7/37/3-surgery on KK?

2. Low-dimensional topology: 3- and 4-manifolds

Warm-upHuman

Integral surgery on the Hopf link (two unknots with linking number 11) with framings 33 and 44 gives a lens space. What is the order of its first homology group?

3. Low-dimensional topology: 3- and 4-manifolds

CoreHuman

For which qq is L(11,q)L(11, q) homeomorphic to L(11,2)L(11, 2)? (Choose all that apply.)

Choose all that apply

4. Low-dimensional topology: 3- and 4-manifolds

CoreHuman

Rokhlin's theorem: if a closed smooth simply connected 4-manifold has an even intersection form, its signature is divisible by 16. Which example shows that the smoothness hypothesis cannot be dropped?

Choose one

5. Low-dimensional topology: 3- and 4-manifolds

CoreHuman

Which of these statements follow from the geometrisation theorem? (Choose all that apply.)

Choose all that apply

6. Low-dimensional topology: 3- and 4-manifolds

CoreFormal

The Lean theorem lens_seven proves LensHomotopyRel (p := 7) 1 2 ∧ ¬ LensHomeoRel (p := 7) 1 2 (with 2 as a unit of ZMod 7). What exactly has been machine-checked?

Choose one

7. Low-dimensional topology: 3- and 4-manifolds

StretchHuman

A closed smooth simply connected 4-manifold with even, indefinite intersection form has form ±(aE8⊕bH)\pm\big(a E_8 \oplus b H\big) with a≥0a \ge 0, b≥1b \ge 1, and signature ±8a\pm 8a. By Rokhlin's theorem, what is the smallest positive value of aa that can occur?

8. Low-dimensional topology: 3- and 4-manifolds

StretchHuman

Which statement is a consequence of Mostow rigidity?

Choose one

9. Low-dimensional topology: 3- and 4-manifolds

CoreComputational

Write lens_classes(p) returning the number of homeomorphism classes of lens spaces L(p,q)L(p, q) with 0<q<p0 < q < p and gcd⁡(p,q)=1\gcd(p, q) = 1, using the criterion L(p,q)≅L(p,q′)  ⟺  q′≡±q±1(modp)L(p, q) \cong L(p, q') \iff q' \equiv \pm q^{\pm 1} \pmod p. (In Python, pow(q, -1, p) is the inverse of qq modulo pp.)

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.
Common misconceptionsH

Common misconceptions

Misconception

"The Poincaré conjecture was the last big open problem in 3-manifold topology." Geometrisation transformed the field, and Agol's theorem settled several more central questions, but much remains open: the L-space conjecture, the volume conjecture, the complexity of recognising the unknot, and many questions about hyperbolic 3-manifolds and their volumes. And in dimension 4, the smooth Poincaré conjecture is wide open.

Misconception

"Manifold theory works the same way in every dimension." It does not. Surfaces are classified by genus and orientability; dimension 3 is governed by geometry (geometrisation); dimension 4 is the only one in which topological and smooth classification differ this drastically (exotic R4\R^4, non-smoothable manifolds detected by gauge theory); dimensions ≥5\ge 5 are governed by surgery theory and algebra. The Whitney trick, which works for n≥5n \ge 5, is exactly what fails in dimension 4.

Misconception

"Same homology, or even same fundamental group, means the same manifold." The Poincaré homology sphere has the homology of S3S^3 but π1\pi_1 of order 120. L(5,1)L(5, 1) and L(5,2)L(5, 2) have the same π1\pi_1 and homology but are not homotopy equivalent; L(7,1)L(7, 1) and L(7,2)L(7, 2) are homotopy equivalent but not homeomorphic.

Misconception

"Every topological 4-manifold can be smoothed, perhaps in several ways." Freedman's E8E_8-manifold has no smooth structure at all (Rokhlin), and the sum E8⊕E8E_8 \oplus E_8 is realised by a topological manifold that is not smoothable (Donaldson). In dimensions ≤3\le 3 every topological manifold has a unique smooth structure (Moise; Radó for surfaces).

ViewpointsH

Many ways of seeing

Geometry— Thurston's eight geometries

For a geometer, 3-manifold topology became geometry. Each of the eight geometries is a homogeneous space: the constant-curvature spaces S3S^3, E3\mathbb{E}^3, H3\mathbb{H}^3; the products S2×RS^2 \times \R and H2×R\mathbb{H}^2 \times \R; and three Lie groups with left-invariant metrics, SL(2,R)~\widetilde{\mathrm{SL}(2,\R)}, the Heisenberg group Nil and the solvable group Sol. Hyperbolic geometry is generic, and by Mostow rigidity it is canonical, so geometric invariants — volume, the length spectrum, the shape of cusps — are topological invariants. Computer programs such as SnapPea (Weeks) and its successor SnapPy compute hyperbolic structures by solving Thurston's gluing equations for ideal tetrahedra. See Riemannian geometry and non-Euclidean geometry.

Topology— Handles, surgery and Kirby calculus

For a topologist, a manifold is built from handles. A closed 3-manifold is S3S^3 after surgery on a framed link (Theorem 2), and the 4-manifold obtained by attaching 2-handles to B4B^4 along that link has intersection form equal to the linking matrix — which is why H1H_1 of the surgery is coker⁡Λ\operatorname{coker}\Lambda. Kirby's theorem (1978) says two framed links give diffeomorphic 3-manifolds exactly when they are related by blow-ups (adding a ±1\pm1-framed unknot) and handle slides; this "Kirby calculus" is the working language of 4-manifold topology (Gompf–Stipsicz). It builds on differential topology, algebraic topology and knot theory.

Algebra— Fundamental groups and lattices

In dimension 3 the fundamental group is almost everything: by geometrisation, closed prime 3-manifolds other than lens spaces are determined up to homeomorphism by π1\pi_1, and hyperbolic 3-manifold groups are word-hyperbolic, residually finite and (by Agol and Wise) virtually special — they embed in right-angled Artin groups after passing to finite index (see geometric group theory). In dimension 4 the algebra is the theory of integral lattices: indefinite unimodular forms are classified by rank, signature and parity (odd: m⟨1⟩⊕n⟨−1⟩m\langle 1\rangle \oplus n\langle -1 \rangle; even: ±(aE8⊕bH)\pm(aE_8 \oplus bH)), while definite ones are wild — there are 24 even unimodular positive definite lattices of rank 24 (Niemeier), including the Leech lattice. Donaldson's theorem says smooth geometry sees only the diagonal ones.

Physics— Gauge theory and quantum invariants

Donaldson's theorem came from physics: he studied the moduli space of anti-self-dual Yang–Mills connections (instantons) on a 4-manifold and showed that for a smooth definite manifold it is a 5-dimensional cobordism between the manifold and a union of copies of ±CP2\pm\C P^2, forcing the form to be diagonal. In 1994 Seiberg and Witten introduced equations from supersymmetric gauge theory whose solution counts give simpler, equally powerful invariants. In dimension 3, Witten (1989) interpreted the Jones polynomial through Chern–Simons quantum field theory, leading to quantum invariants of 3-manifolds; the volume conjecture links these to hyperbolic geometry. The physical derivations are heuristic; the resulting invariants are rigorous mathematics. See gauge theory.

Number theory— Arithmetic hyperbolic 3-manifolds

Some of the most important hyperbolic 3-manifolds come from number theory. For an imaginary quadratic field Q(−d)\Q(\sqrt{-d}) with ring of integers Od\mathcal{O}_d, the Bianchi group PSL(2,Od)\mathrm{PSL}(2, \mathcal{O}_d) is a discrete subgroup of PSL(2,C)\mathrm{PSL}(2, \C) with finite covolume, and Humbert's formula expresses that covolume through the Dedekind zeta function: vol(H3/PSL(2,Od))=∣D∣3/2ζK(2)/(4π2)\mathrm{vol}(\mathbb{H}^3/\mathrm{PSL}(2, \mathcal{O}_d)) = |D|^{3/2}\zeta_K(2)/(4\pi^2), with DD the discriminant. The figure-eight knot complement is a 12-fold cover of H3/PSL(2,O3)\mathbb{H}^3/\mathrm{PSL}(2, \mathcal{O}_3) (Riley); it is the only arithmetic knot complement (Reid, 1991). See algebraic number theory.

Analysis— Ricci flow

Perelman's proof of geometrisation is analysis: evolve a Riemannian metric by Hamilton's Ricci flow ∂tg=−2 Ric(g)\partial_t g = -2\,\mathrm{Ric}(g), a nonlinear heat equation for the metric, which tends to make curvature uniform. Singularities form where the manifold pinches along 2-spheres (necks); Perelman classified them using his entropy functional and non-collapsing estimates, cut along the necks (surgery, in exactly the topologist's sense), and continued the flow. Over long times, what remains decomposes into hyperbolic pieces and graph manifolds — the geometric decomposition. The lesson on geometric analysis works out the round-sphere case.

History & global context

History and global context

  • 1898–1935: foundations. Poul Heegaard (Denmark) introduced Heegaard diagrams in his 1898 thesis. Henri Poincaré (France) found his homology sphere and asked his question in 1904. Heinrich Tietze (Austria) described lens spaces (1908) and Max Dehn (Germany) introduced surgery (1910). Hellmuth Kneser (Germany) proved prime decomposition (1929); Herbert Seifert (Germany) classified Seifert fibred spaces (1933); Kurt Reidemeister (Germany) classified lens spaces with his torsion (1935), and J. H. C. Whitehead (UK) classified them up to homotopy (1941).
  • 1950s–1960s: the tools. Edwin Moise (USA) proved 3-manifolds triangulable (1952); Christos Papakyriakopoulos (Greece, working in Princeton) proved Dehn's lemma and the sphere theorem (1957); Vladimir Rokhlin (USSR) proved his signature theorem (1952); John Milnor (USA) found exotic 7-spheres (1956); Stephen Smale (USA) proved the h-cobordism theorem and the Poincaré conjecture in dimensions ≥5\ge 5 (1961); Andrew Wallace (UK, working in North America) and Raymond Lickorish (UK) proved the surgery theorem.
  • 1970s–1990s: geometry and gauge theory. William Thurston (USA) proved hyperbolisation for Haken manifolds and proposed geometrisation (1982); Robion Kirby (USA) gave his calculus (1978); Michael Freedman (USA) classified simply connected topological 4-manifolds (1982); Simon Donaldson (UK) proved his diagonalisability theorem (1983) and Clifford Taubes (USA) found uncountably many exotic R4\R^4 (1987); Nathan Seiberg and Edward Witten (USA) introduced their equations (1994).
  • 2000s: resolution in dimension 3. Grigori Perelman (Russia) posted his proof of geometrisation (2002–03), building on Richard Hamilton's (USA) programme; he declined the Fields Medal (2006) and the Clay Millennium Prize (2010). Ian Agol (USA), Daniel Wise (Canada), Jeremy Kahn and Vladimir Markovic proved the virtual Haken conjecture (2012–13).
Further reading

Further reading

A suggested path: Weeks for intuition; Rolfsen for surgery and knots; Thurston for geometry; Scott's survey for the eight geometries; Gompf–Stipsicz and Scorpan for 4-manifolds.

  • Jeffrey R. Weeks, The Shape of Space (1985; 3rd edition 2020).
  • Dale Rolfsen, Knots and Links (1976).
  • William P. Thurston, Three-Dimensional Geometry and Topology, Volume 1 (1997).
  • Peter Scott, "The geometries of 3-manifolds", Bulletin of the London Mathematical Society 15 (1983).
  • John Hempel, 3-Manifolds (1976).
  • Matthias Aschenbrenner, Stefan Friedl and Henry Wilton, 3-Manifold Groups (2015).
  • John Morgan and Gang Tian, Ricci Flow and the Poincaré Conjecture (2007).
  • Robert E. Gompf and András I. Stipsicz, 4-Manifolds and Kirby Calculus (1999).
  • Alexandru Scorpan, The Wild World of 4-Manifolds (2005).
  • Michael H. Freedman and Frank Quinn, Topology of 4-Manifolds (1990).
  • Jessica S. Purcell, Hyperbolic Knot Theory (2020).