Topological classification of surfaces

topological_classification_of_surfaces

Submitter: Junyan Xu.

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

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

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

theorem declaration uses `sorry`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 (LeanEval.Topology.ClassificationOfSurfaces.OrientableRel p n))) ∨
      (1 ≤ p ∧ Nonempty (S ≃ₜ Quot (LeanEval.Topology.ClassificationOfSurfaces.NonOrientableRel p n))) := byS:Type u_1inst✝⁵:TopologicalSpace Sinst✝⁴:T2Space Sinst✝³:ConnectedSpace Sinst✝²:CompactSpace Sinst✝¹:ChartedSpace (EuclideanHalfSpace 2) Sinst✝:IsManifold (modelWithCornersEuclideanHalfSpace 2) 0 S⊢ Nonempty (S ≃ₜ ↑(Metric.sphere 0 1)) ∨
  ∃ p n,
    (1 ≤ p ∨ 1 ≤ n) ∧ Nonempty (S ≃ₜ Quot (OrientableRel p n)) ∨ 1 ≤ p ∧ Nonempty (S ≃ₜ Quot (NonOrientableRel p n))
  sorryAll goals completed! 🐙

Solved by

Not yet solved.