ClassifyOverlaps

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

noncomputable def OneMfld.Homeomorph.toOpenPartialHomeomorphOnOpens {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [Nonempty X] [Nonempty Y] {A : Set X} {B : Set Y} (h : ↑A ≃ₜ ↑B) (hA : IsOpen A) (hB : IsOpen B) : OpenPartialHomeomorph X Y

Turn a homeomorphism of open subtypes A ≃ₜ B into a partial homeomorphism X ⇀ Y.

The Nonempty hypotheses are needed, and are not an artefact of the proof: a PartialEquiv X Y carries a total toFun : X → Y, so OpenPartialHomeomorph Unit Empty is an empty type even though (∅ : Set Unit) ≃ₜ (∅ : Set Empty) with both sets open.

Equations

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

noncomputable def OneMfld.OpenPartialHomeomorph.toHomeomorphOfCompactTarget {X : Type u_2} {Y : Type u_3} [TopologicalSpace X] [TopologicalSpace Y] [PreconnectedSpace X] [T2Space X] [CompactSpace Y] (φ : OpenPartialHomeomorph X Y) (hne : φ.source.Nonempty) (ht : φ.target = Set.univ) : X ≃ₜ Y

An OpenPartialHomeomorph from a preconnected Hausdorff space onto the whole of a compact space, with nonempty source, is a global homeomorphism: its source is compact (hence closed) as well as open, so it is clopen and equals univ.

Equations

• OneMfld.OpenPartialHomeomorph.toHomeomorphOfCompactTarget φ hne ht = φ.toHomeomorphOfSourceEqUnivTargetEqUniv ⋯ ht

theorem OneMfld.overlap_image_ne_target {M : Type u_1} [TopologicalSpace M] (U V : OpenPartialHomeomorph M NNReal) (hUV : (U.source \ V.source).Nonempty) : ↑U '' (U.source ∩ V.source) ≠ U.target

The chart image of the overlap is never the whole target (since U.source is not contained in V.source).

theorem OneMfld.overlap_image_Iio {M : Type u_1} [TopologicalSpace M] [T2Space M] (U V : OpenPartialHomeomorph M NNReal) {v : NNReal} (hUt : U.target = Set.Iio v) (hV : IsConnected V.source) (hUV : (U.source \ V.source).Nonempty) (hVU : (V.source \ U.source).Nonempty) (hc : IsConnected (U.source ∩ V.source)) : ∃ p < v, ↑U '' (U.source ∩ V.source) = Set.Ioo p v

The outer-overlap lemma for a boundary chart, specialized to a connected overlap.

theorem OneMfld.overlap_image_Ioo {M : Type u_1} [TopologicalSpace M] [T2Space M] (U V : OpenPartialHomeomorph M NNReal) {u v : NNReal} (hUt : U.target = Set.Ioo u v) (hV : IsConnected V.source) (hVU : (V.source \ U.source).Nonempty) (hc : IsConnected (U.source ∩ V.source)) : (∃ (p : NNReal), u ≤ p ∧ p < v ∧ ↑U '' (U.source ∩ V.source) = Set.Ioo p v) ∨ ∃ (q : NNReal), u < q ∧ q ≤ v ∧ ↑U '' (U.source ∩ V.source) = Set.Ioo u q

The outer-overlap lemma for an interior chart, specialized to a connected overlap.

theorem OneMfld.hchart_overlap_connected {M : Type u_1} [TopologicalSpace M] [T2Space M] (b : HChart M) (V : OpenPartialHomeomorph M NNReal) (hV : IsConnected V.source) (hbV : (b.source \ V.source).Nonempty) (hVb : (V.source \ b.source).Nonempty) (hne : (b.source ∩ V.source).Nonempty) : IsConnected (b.source ∩ V.source)

The overlap of a boundary chart with a connected chart is connected.

theorem OneMfld.Ioc_union_Ioo_eq_Ioo {μ ν : NNReal} (hμν : μ < ν) : Set.Ioc 0 μ ∪ Set.Ioo μ ν = Set.Ioo 0 ν

theorem OneMfld.lt_div_self_of_lt_one {μ ρ : NNReal} (hμ0 : 0 < μ) (hρ0 : 0 < ρ) (hρ1 : ρ < 1) : μ < μ / ρ

theorem OneMfld.OChart.exists_orient_lower {M : Type u_1} [TopologicalSpace M] [T2Space M] (a : OChart M) (V : OpenPartialHomeomorph M NNReal) (hat : a.target = Set.Ioo 0 1) (hV : IsConnected V.source) (haV : (a.source \ V.source).Nonempty) (hVa : (V.source \ a.source).Nonempty) (hc : IsConnected (a.source ∩ V.source)) : ∃ (a' : OChart M) (r : NNReal), a'.source = a.source ∧ a'.target = Set.Ioo 0 1 ∧ 0 < r ∧ r < 1 ∧ ↑a'.toOpenPartialHomeomorph '' (a.source ∩ V.source) = Set.Ioo 0 r

Re-orient an OChart with target Ioo 0 1 (flipping if necessary) so that its image of the overlap with V.source is the lower end-segment Ioo 0 r with 0 < r < 1. The source is unchanged.

theorem OneMfld.OChart.exists_orient_upper {M : Type u_1} [TopologicalSpace M] [T2Space M] (a : OChart M) (V : OpenPartialHomeomorph M NNReal) (hat : a.target = Set.Ioo 0 1) (hV : IsConnected V.source) (haV : (a.source \ V.source).Nonempty) (hVa : (V.source \ a.source).Nonempty) (hc : IsConnected (a.source ∩ V.source)) : ∃ (a' : OChart M) (q : NNReal), a'.source = a.source ∧ a'.target = Set.Ioo 0 1 ∧ 0 < q ∧ q < 1 ∧ ↑a'.toOpenPartialHomeomorph '' (a.source ∩ V.source) = Set.Ioo q 1

Re-orient an OChart with target Ioo 0 1 (flipping if necessary) so that its image of the overlap with V.source is the upper end-segment Ioo q 1 with 0 < q < 1. The source is unchanged.

theorem OneMfld.exists_glue_h_h {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : HChart M) (h : Overlap a.source b.source) : ∃ (φ : OpenPartialHomeomorph M ↑UnitInterval), φ.source = a.source ∪ b.source ∧ φ.target = Set.univ

Two overlapping H-charts glue to a chart of M onto the unit interval: rescale both to target Iio 1, note the overlap is connected and appears as an upper end-segment in each chart (outer-overlap lemma), and apply the unit-interval gluing.

noncomputable def OneMfld.glueHH {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : HChart M) (h : Overlap a.source b.source) : ↑{φ : OpenPartialHomeomorph M ↑UnitInterval | φ.source = a.source ∪ b.source ∧ φ.target = Set.univ}

Glue two overlapping H-charts into a single chart of M onto the unit interval.

Equations

• OneMfld.glueHH a b h = ⟨⋯.choose, ⋯⟩

noncomputable def OneMfld.handleHH {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [T2Space M] (a b : HChart M) (h : Overlap a.source b.source) : M ≃ₜ ↑UnitInterval

Join overlapping boundary charts into a homeomorphism with the closed unit interval.

Equations

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

theorem OneMfld.exists_glue_o_h {M : Type u_1} [TopologicalSpace M] [T2Space M] (a : OChart M) (b : HChart M) (h : Overlap a.source b.source) (hc : IsConnected (a.source ∩ b.source)) : ∃ (f : HChart M), f.source = a.source ∪ b.source

An O-chart and an H-chart with connected overlap glue to an H-chart on the union: rescale both, orient the O-chart so the overlap sits at its lower end, and apply the ℝ≥0 gluing.

noncomputable def OneMfld.handleOH' {M : Type u_1} [TopologicalSpace M] [T2Space M] (a : OChart M) (b : HChart M) (h : Overlap a.source b.source) (hc : IsConnected (a.source ∩ b.source)) : ↑{f : HChart M | f.source = a.source ∪ b.source}

Glue an O-chart and an H-chart with connected overlap into an H-chart on the union.

Equations

• OneMfld.handleOH' a b h hc = ⟨⋯.choose, ⋯⟩

noncomputable def OneMfld.handleOH {M : Type u_1} [TopologicalSpace M] [T2Space M] (a : OChart M) (b : HChart M) (h : Overlap a.source b.source) : ↑{f : HChart M | f.source = a.source ∪ b.source}

Glue an O-chart and an H-chart: the overlap with an H-chart is automatically connected.

Equations

• OneMfld.handleOH a b h = OneMfld.handleOH' a b h ⋯

theorem OneMfld.exists_glue_o_o {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OChart M) (h : Overlap a.source b.source) (hc : IsConnected (a.source ∩ b.source)) : ∃ (f : OChart M), f.source = a.source ∪ b.source

Two O-charts with connected overlap glue to an O-chart on the union: rescale both, orient the first chart's overlap low and the second's high, and apply the ℝ≥0 gluing.

noncomputable def OneMfld.circleOfDisconnectedOverlap {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [T2Space M] (a b : OChart M) (h : Overlap a.source b.source) (hc : ¬IsConnected (a.source ∩ b.source)) : M ≃ₜ Circle

A disconnected overlap of two O-charts closes M up into a circle: the glued chart of exists_circle_chart maps a.source ∪ b.source onto the whole of AddCircle 1; transfer to Circle and apply the compact-target argument.

Equations

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

noncomputable def OneMfld.handleOO {M : Type u_1} [TopologicalSpace M] [ConnectedSpace M] [T2Space M] (a b : OChart M) (h : Overlap a.source b.source) : (M ≃ₜ Circle) ⊕ ↑{f : OChart M | f.source = a.source ∪ b.source}

Glue two O-charts: with a connected overlap they merge into an O-chart on the union; with a disconnected overlap, M is a circle.

Equations

• OneMfld.handleOO a b h = if hc : IsConnected (a.source ∩ b.source) then Sum.inr ⟨⋯.choose, ⋯⟩ else Sum.inl (OneMfld.circleOfDisconnectedOverlap a b h hc)