NiceCharts

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

noncomputable def OneMfld.improvedChart {M : Type u_1} [TopologicalSpace M] (φ : OpenPartialHomeomorph M NNReal) (x : M) (h : x ∈ φ.source) : ↑{ψ : OpenPartialHomeomorph M NNReal | x ∈ ψ.source ∧ Bornology.IsBounded ψ.target}

Restrict a chart around the specified point to a bounded target.

Equations

• OneMfld.improvedChart φ x h = ⟨φ.restrOpen (↑φ.symm '' (φ.target ∩ Set.Iio (↑φ x + 1))) ⋯, ⋯⟩

noncomputable def OneMfld.improvedChart' {M : Type u_1} [TopologicalSpace M] (φ : OpenPartialHomeomorph M NNReal) (x : M) (h : x ∈ φ.source) (bounded : Bornology.IsBounded φ.target) : ↑{ψ : OpenPartialHomeomorph M NNReal | x ∈ ψ.source ∧ Bornology.IsBounded ψ.target ∧ ConnectedSpace ↑ψ.target}

Restrict a bounded chart to the connected component containing the specified point.

Equations

• OneMfld.improvedChart' φ x h bounded = ⟨φ.restrOpen (↑φ.symm '' connectedComponentIn φ.target (↑φ.toPartialEquiv x)) ⋯, ⋯⟩

noncomputable def OneMfld.niceChart {M : Type u_1} [TopologicalSpace M] (φ : OpenPartialHomeomorph M NNReal) (x : M) (h : x ∈ φ.source) : ↑{ψ : OpenPartialHomeomorph M NNReal | x ∈ ψ.source ∧ Bornology.IsBounded ψ.target ∧ ConnectedSpace ↑ψ.target}

Choose a chart around the specified point with a bounded connected target.

Equations

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

theorem OneMfld.nice_chart_source {M : Type u_1} [TopologicalSpace M] {φ : OpenPartialHomeomorph M NNReal} {x : M} {h : x ∈ φ.source} : x ∈ (↑(niceChart φ x h)).source

theorem OneMfld.nice_chart_bounded {M : Type u_1} [TopologicalSpace M] {φ : OpenPartialHomeomorph M NNReal} {x : M} {h : x ∈ φ.source} : Bornology.IsBounded (↑(niceChart φ x h)).target

theorem OneMfld.nice_chart_connected {M : Type u_1} [TopologicalSpace M] {φ : OpenPartialHomeomorph M NNReal} {x : M} {h : x ∈ φ.source} : ConnectedSpace ↑(↑(niceChart φ x h)).target

class OneMfld.NicelyChartedSpace (H : Type u_2) [TopologicalSpace H] [Bornology H] (M : Type u_3) [TopologicalSpace M] extends ChartedSpace H M : Type (max u_2 u_3)

A charted space whose atlas has bounded connected targets.

• atlas : Set (OpenPartialHomeomorph M H)
• chartAt : M → OpenPartialHomeomorph M H
• mem_chart_source (x : M) : x ∈ (ChartedSpace.chartAt x).source
• chart_mem_atlas (x : M) : ChartedSpace.chartAt x ∈ ChartedSpace.atlas
• is_bounded (φ : OpenPartialHomeomorph M H) (h : φ ∈ ChartedSpace.atlas) : Bornology.IsBounded φ.target
• is_connected (φ : OpenPartialHomeomorph M H) (h : φ ∈ ChartedSpace.atlas) : ConnectedSpace ↑φ.target

@[instance_reducible]

noncomputable def OneMfld.nicelyCharted {M : Type u_1} [TopologicalSpace M] (ht : ChartedSpace NNReal M) : NicelyChartedSpace NNReal M

Replace an atlas by one with bounded connected chart targets.

Equations

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