Classification of one-manifolds

TheoremClassification of connected \(1\)-manifolds without boundary#✓fully proved

Every connected, Hausdorff, second-countable smooth \(1\)-manifold \(M\) without boundary is diffeomorphic either to the circle \(S^1\) or to the real line \(\mathbb{R}\).

theorem connected_boundaryless_one_manifold_classification
    (M : Type*) [TopologicalSpace M] [ChartedSpace (EuclideanSpace ℝ (Fin 1)) M]
    [IsManifold (𝓡 1) ∞ M]
    [T2Space M] [ConnectedSpace M] [SecondCountableTopology M] :
    Nonempty (M ≃ₘ⟮𝓡 1, 𝓡 1⟯ Circle) ∨ Nonempty (M ≃ₘ⟮𝓡 1, 𝓡 1⟯ (EuclideanSpace ℝ (Fin 1)))

Sources

• Classification of connected boundaryless 1-manifolds; Milnor (1965); Hirsch; Lean states dichotomy specialization for 𝓡 1.

Uses 1 · Used by 1

Proof usesExistence of Riemannian metrics

Used byClassification of compact connected \(1\)-manifolds with boundary

TheoremClassification of compact connected \(1\)-manifolds with boundary#✓fully proved

Every compact, connected, Hausdorff, second-countable smooth \(1\)-manifold \(M\) with (possibly empty) boundary is diffeomorphic either to the circle \(S^1\) or to the closed interval \([0, 1]\).

theorem compact_connected_one_manifold_with_boundary_classification
    (M : Type*) [TopologicalSpace M] [ChartedSpace (EuclideanHalfSpace 1) M]
    [IsManifold (𝓡∂ 1) ∞ M]
    [T2Space M] [CompactSpace M] [ConnectedSpace M] [SecondCountableTopology M] :
    Nonempty (M ≃ₘ⟮𝓡∂ 1, 𝓡 1⟯ Circle) ∨ Nonempty (M ≃ₘ⟮𝓡∂ 1, 𝓡∂ 1⟯ (Set.Icc (0 : ℝ) 1))

Sources

• Classification of 1-manifolds with boundary; Hirsch, Differential Topology; J. Lee, Introduction to Smooth Manifolds, 2nd ed., collar theorem; Lean states compact connected 𝓡∂ 1 with closed interval specialization.

Uses 1

Proof usesClassification of connected \(1\)-manifolds without boundary

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.