Classification

Supporting results for the classification of compact one-dimensional manifolds.

noncomputable def OneMfld.subsumeCharts {M : Type u_1} [TopologicalSpace M] (ht : FinitelyIntervalChartedSpace M) {a : OpenPartialHomeomorph M NNReal} (ha : a ∈ ChartedSpace.atlas) {b : OpenPartialHomeomorph M NNReal} (hb : b ∈ ChartedSpace.atlas) (hs : a.source ⊆ b.source) (hab : a ≠ b) : ↑{ht' : FinitelyIntervalChartedSpace M | Nat.card ↑ChartedSpace.atlas = Nat.card ↑ChartedSpace.atlas - 1}

Remove a chart whose source is contained in another chart, reducing the atlas size.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def OneMfld.replaceCharts {M : Type u_1} [TopologicalSpace M] (ht : FinitelyIntervalChartedSpace M) {a : OpenPartialHomeomorph M NNReal} (ha : a ∈ ChartedSpace.atlas) {b : OpenPartialHomeomorph M NNReal} (hb : b ∈ ChartedSpace.atlas) (ho : Overlap a.source b.source) (f : IChart M) (hf : f.source = a.source ∪ b.source) : ↑{ht' : FinitelyIntervalChartedSpace M | Nat.card ↑ChartedSpace.atlas ≤ Nat.card ↑ChartedSpace.atlas - 1}

Replace two overlapping charts by a chart on their union, reducing the atlas size.

Equations

• One or more equations did not get rendered due to their size.

theorem OneMfld.nonempty_atlas {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] (ht : FinitelyIntervalChartedSpace M) : ChartedSpace.atlas.Nonempty

theorem OneMfld.more_than_one_chart {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [CompactSpace M] (ht : FinitelyIntervalChartedSpace M) : Nat.card ↑ChartedSpace.atlas > 1

theorem OneMfld.find_overlap {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [CompactSpace M] (ht : FinitelyIntervalChartedSpace M) {a : OpenPartialHomeomorph M NNReal} (ha : a ∈ ChartedSpace.atlas) {x : M} (hx : x ∈ a.source) (contains : ∀ c ∈ ChartedSpace.atlas \ {a}, ¬a.source ⊆ c.source) : ∃ b ∈ ChartedSpace.atlas \ {a}, Overlap a.source b.source

@[irreducible]

noncomputable def OneMfld.classification' {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [T2Space M] [CompactSpace M] (ht : FinitelyIntervalChartedSpace M) : (M ≃ₜ Circle) ⊕ (M ≃ₜ ↑UnitInterval)

Classify a compact connected Hausdorff one-manifold using induction on a finite interval atlas.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def OneMfld.classification {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [T2Space M] [CompactSpace M] (ht : ChartedSpace NNReal M) : (M ≃ₜ Circle) ⊕ (M ≃ₜ ↑UnitInterval)

A compact connected Hausdorff manifold charted on the half-line is a circle or an interval.

Equations

• OneMfld.classification ht = OneMfld.classification' (OneMfld.finitelyIntervalCharted (OneMfld.intervalCharted (OneMfld.nicelyCharted ht)))