Topological classification of surfaces

topological_classification_of_surfaces — a formalization challenge from the lean-eval benchmark.

Notes

A compact connected surface with boundary is homeomorphic to one of the representative surfaces that we formalize.

Formal statement

theorem classification_of_surfaces (S : Type*) [TopologicalSpace S]
    [T2Space S] [ConnectedSpace S] [CompactSpace S]
    [ChartedSpace (EuclideanHalfSpace 2) S]
    [IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S] :
    Nonempty (S ≃ₜ Metric.sphere (0 : EuclideanSpace ℝ (Fin 3)) 1) ∨
    ∃ p n, ((1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n))) ∨
      (1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))) := by
  sorry

Informal solution sketch

Show surfaces are triangulable and therefore homeomorphic to cell complexes, and show each cell complex is equivalent to one in normal form.

Source

Jean Gallier & Dianna Xu, A Guide to the Classification Theorem for Compact Surfaces, https://www.cis.upenn.edu/~jean/surfclassif-root.pdf

How to submit

Challenge.lean and Solution.lean are part of the trusted benchmark and must not be modified. Write your proof in Submission.lean (plus any local modules under Submission/). Mathlib may be used freely; anything not in Mathlib has to be inlined into the submission.

Comparator configuration

• Solution module: Solution
• Theorems checked: classification_of_surfaces
• Permitted axioms: propext, Quot.sound, Classical.choice

Submitted by Junyan Xu.