Classification of surfaces

4 fully proved1 ready to prove

The closed unit disc

AbbreviationClosed unit disc in the complex plane#✓fully proved

The closed unit disc in the complex plane.

abbrev ClosedUnitDisc : Type := Metric.closedBall (0 : ℂ) 1

Used by 4

Used byBoundary point of the unit disc at a real parameter · Classification of compact surfaces · Gluing relation for the non-orientable normal form · Gluing relation for the orientable normal form

DefinitionBoundary point of the unit disc at a real parameter#✓fully proved

For a real number \(r\), this is the point \(e^{2\pi i r}\) of the closed unit disc in \(\mathbb{C}\), which lies on its boundary circle.

noncomputable def ClosedUnitDisc.bdyPtOfReal (r : ℝ) : ClosedUnitDisc :=
  ⟨r.fourierChar, r.fourierChar.2.le⟩

Uses 1 · Used by 2

Statement usesClosed unit disc in the complex plane

Used byGluing relation for the non-orientable normal form · Gluing relation for the orientable normal form

Classification of surfaces

InductiveGluing relation for the orientable normal form#✓fully proved

For natural numbers \(p\) and \(n\), put \(N = 4p + 3n\) and write \(e(t) = e^{2\pi i t}\) for the boundary point of the closed unit disc at the real parameter \(t\). This is the relation on the closed unit disc under which, for every \(x \in [0, 1]\) and every natural number \(k < p\), the point \(e((4k + x)/N)\) is related to \(e((4k + 3 - x)/N)\) and the point \(e((4k + 1 + x)/N)\) is related to \(e((4k + 4 - x)/N)\), and for every \(x \in [0, 1]\) and every natural number \(k < n\), the point \(e(-(3k + x)/N)\) is related to \(e(-(3k + 3 - x)/N)\); no other pairs are related.

Gluing the disc along it identifies the boundary in the pattern \(a_1 b_1 a_1^{-1} b_1^{-1} \cdots a_p b_p a_p^{-1} b_p^{-1} c_1 h_1 c_1^{-1} \cdots c_n h_n c_n^{-1}\), where the arcs \(h_j\) are left free.

inductive OrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → Prop
  | a (x : Icc (0 : ℝ) 1) (i : Fin p) : OrientableRel p n
      (.bdyPtOfReal <| (4 * i + x) / (4 * p + 3 * n))
      (.bdyPtOfReal <| (4 * i + 3 - x) / (4 * p + 3 * n))
  | b (x : Icc (0 : ℝ) 1) (i : Fin p) : OrientableRel p n
      (.bdyPtOfReal <| (4 * i + 1 + x) / (4 * p + 3 * n))
      (.bdyPtOfReal <| (4 * i + 4 - x) / (4 * p + 3 * n))
  | c (x : Icc (0 : ℝ) 1) (i : Fin n) : OrientableRel p n
      (.bdyPtOfReal <| - (3 * i + x) / (4 * p + 3 * n))
      (.bdyPtOfReal <| - (3 * i + 3 - x) / (4 * p + 3 * n))

Uses 2 · Used by 1

Statement usesClosed unit disc in the complex plane · Boundary point of the unit disc at a real parameter

Used byClassification of compact surfaces

InductiveGluing relation for the non-orientable normal form#✓fully proved

For natural numbers \(p\) and \(n\), put \(N = 2p + 3n\) and write \(e(t) = e^{2\pi i t}\) for the boundary point of the closed unit disc at the real parameter \(t\). This is the relation on the closed unit disc under which, for every \(x \in [0, 1]\) and every natural number \(k < p\), the point \(e((2k + x)/N)\) is related to \(e((2k + 1 + x)/N)\), and for every \(x \in [0, 1]\) and every natural number \(k < n\), the point \(e(-(3k + x)/N)\) is related to \(e(-(3k + 3 - x)/N)\); no other pairs are related.

Gluing the disc along it identifies the boundary in the pattern \(a_1 a_1 \cdots a_p a_p c_1 h_1 c_1^{-1} \cdots c_n h_n c_n^{-1}\), where the arcs \(h_j\) are left free.

inductive NonOrientableRel (p n : ℕ) : ClosedUnitDisc → ClosedUnitDisc → Prop
  | a (x : Icc (0 : ℝ) 1) (i : Fin p) : NonOrientableRel p n
      (.bdyPtOfReal <| (2 * i + x) / (2 * p + 3 * n))
      (.bdyPtOfReal <| (2 * i + 1 + x) / (2 * p + 3 * n))
  | c (x : Icc (0 : ℝ) 1) (i : Fin n) : NonOrientableRel p n
      (.bdyPtOfReal <| -(3 * i + x) / (2 * p + 3 * n))
      (.bdyPtOfReal <| -(3 * i + 3 - x) / (2 * p + 3 * n))

Uses 2 · Used by 1

Statement usesClosed unit disc in the complex plane · Boundary point of the unit disc at a real parameter

Used byClassification of compact surfaces

TheoremClassification of compact surfaces#●ready to prove

Let \(S\) be a nonempty, compact, connected Hausdorff space that is a topological manifold of dimension \(2\) with boundary, with charts in the closed half-plane \(\{x \in \mathbb{R}^2 : x_1 \ge 0\}\). Then \(S\) is homeomorphic to the unit sphere in \(\mathbb{R}^3\), or there are natural numbers \(p\) and \(n\) for which one of the following holds: \(p \ge 1\) or \(n \ge 1\), and \(S\) is homeomorphic to the quotient of the closed unit disc by the orientable gluing relation with parameters \(p\) and \(n\); or \(p \ge 1\), and \(S\) is homeomorphic to the quotient of the closed unit disc by the non-orientable gluing relation with parameters \(p\) and \(n\). Each quotient is taken by the equivalence relation that the gluing relation generates, with the quotient topology.

public theorem_wanted classification_of_surfaces (S : Type*) [TopologicalSpace S]
    [T2Space S] [ConnectedSpace S] [CompactSpace S] [Nonempty 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)))

Sources

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

Uses 3

Statement usesClosed unit disc in the complex plane · Gluing relation for the non-orientable normal form · Gluing relation for the orientable normal form

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.