Triangulation conjecture

StructureClosed topological manifold#✓fully proved

For a natural number \(n\), a closed topological \(n\)-manifold is a nonempty, compact, connected, Hausdorff, second-countable topological space \(M\) together with an atlas of charts, homeomorphisms from open subsets of \(M\) onto open subsets of \(\mathbb{R}^n\), whose domains cover \(M\). Since the charts land in \(\mathbb{R}^n\) itself rather than in a half-space, \(M\) has no boundary.

structure ClosedTopManifold (n : ℕ) where
  /-- The underlying point set. -/
  carrier : Type
  [topology : TopologicalSpace carrier]
  [t2 : T2Space carrier]
  [secondCountable : SecondCountableTopology carrier]
  [charted : ChartedSpace (EuclideanSpace ℝ (Fin n)) carrier]
  [compact : CompactSpace carrier]
  [connected : ConnectedSpace carrier]
  /-- The carrier is nonempty: a closed manifold has points. -/
  [nonempty : Nonempty carrier]

Used by 2

Used byManolescu's disproof of the triangulation conjecture · Triangulable closed manifold

DefinitionTriangulable closed manifold#✓fully proved

A closed topological \(n\)-manifold \(M\) is triangulable if, for some natural number \(N\), there is a simplicial complex \(K\) in \(\mathbb{R}^N\) with finitely many faces such that \(M\) is homeomorphic to the geometric realization of \(K\), the union of its faces with the subspace topology from \(\mathbb{R}^N\).

For a compact manifold this is the usual notion of triangulability. Requiring finitely many faces is essential: otherwise any copy of \(M\) embedded in \(\mathbb{R}^N\) would be the realization of the complex whose faces are its points.

def Triangulable {n : ℕ} (M : ClosedTopManifold n) : Prop :=
  ∃ (N : ℕ) (K : SimplicialComplex ℝ (EuclideanSpace ℝ (Fin N))),
    K.faces.Finite ∧ Nonempty (M.carrier ≃ₜ K.space)

Uses 1 · Used by 1

Statement usesClosed topological manifold

Used byManolescu's disproof of the triangulation conjecture

TheoremManolescu's disproof of the triangulation conjecture#●ready to prove

For every natural number \(n \ge 5\) there is a closed connected topological \(n\)-manifold that is not triangulable.

public theorem_wanted manolescu_triangulation_disproof :
    ∀ n : ℕ, 5 ≤ n → ∃ M : ClosedTopManifold n, ¬ Triangulable M

Sources

• C. Manolescu, Pin(2)-equivariant Seiberg–Witten Floer homology and the triangulation conjecture, J. Amer. Math. Soc. 29 (2016), via the Galewski–Stern and Matumoto reduction. Earlier, the triangulation conjecture was known false in dimension 4 (Casson). Problem manolescu_triangulation_disproof of the lean-eval benchmark.

Uses 2

Statement usesClosed topological manifold · Triangulable closed manifold

2 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.