The two-component structure of a disconnected overlap

When two interior charts overlap disconnectedly, the overlap has exactly two connected components, one at each end of each chart (outer-overlap lemma + two end-segments at the same end must intersect). We also generalize the end-matching theorems of GlueCore from the full overlap to a single component W: the extra hypothesis is that the relevant interior endpoint is not in the image of the full overlap.

theorem OneMfld.tendsto_bot_of_strictAntiOn_image {p v q w : NNReal} (hpv : p < v) {f : NNReal → NNReal} (hm : StrictAntiOn f (Set.Ioo p v)) (himg : f '' Set.Ioo p v = Set.Ioo q w) : Filter.Tendsto f (nhdsWithin p (Set.Ioi p)) (nhds w)

A strictly antitone map of Ioo p v onto Ioo q w tends to w at the bottom end.

theorem OneMfld.overlap_mono_on' {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) {W : Set M} (hW : W ⊆ a.source ∩ b.source) {p r q w : NNReal} (ha : ↑a '' W = Set.Ioo p r) (hb : ↑b '' W = Set.Ioo q w) (hp : p ∈ a.target) (hw : w ∈ b.target) (hpS : p ∉ ↑a '' (a.source ∩ b.source)) (x : M) : x ∈ W → ∀ y ∈ W, ↑a x < ↑a y → ↑b x < ↑b y

Mirror component version: with the p-end interior to a.target, the w-end interior to b.target, and p not in the image of the full overlap, the transition is again increasing.

theorem OneMfld.two_components_structure {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) (hat : a.target = Set.Ioo 0 1) (hb : IsConnected b.source) (hba : (b.source \ a.source).Nonempty) (hne : (a.source ∩ b.source).Nonempty) (hdisc : ¬IsConnected (a.source ∩ b.source)) : ∃ (W₀ : Set M) (W₁ : Set M) (r : NNReal) (p : NNReal), a.source ∩ b.source = W₀ ∪ W₁ ∧ (∀ z ∈ W₀, connectedComponentIn (a.source ∩ b.source) z = W₀) ∧ (∀ z ∈ W₁, connectedComponentIn (a.source ∩ b.source) z = W₁) ∧ Disjoint W₀ W₁ ∧ ↑a '' W₀ = Set.Ioo 0 r ∧ ↑a '' W₁ = Set.Ioo p 1 ∧ 0 < r ∧ r ≤ p ∧ p < 1

Two-component structure. A disconnected overlap of a chart with target Ioo 0 1 and a connected-source chart has exactly two components: one whose image is a lower end-segment Ioo 0 r and one whose image is an upper end-segment Ioo p 1, with r ≤ p.

theorem OneMfld.two_components_other_chart {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) (hbt : b.target = Set.Ioo 0 1) (haconn : IsConnected a.source) (hab : (a.source \ b.source).Nonempty) {W₀ W₁ : Set M} (hW₀ : ∀ z ∈ W₀, connectedComponentIn (a.source ∩ b.source) z = W₀) (hW₁ : ∀ z ∈ W₁, connectedComponentIn (a.source ∩ b.source) z = W₁) (hne₀ : W₀.Nonempty) (hne₁ : W₁.Nonempty) (hd : Disjoint W₀ W₁) : ∃ (s : NNReal) (q : NNReal), 0 < s ∧ s ≤ q ∧ q < 1 ∧ (↑b '' W₀ = Set.Ioo q 1 ∧ ↑b '' W₁ = Set.Ioo 0 s ∨ ↑b '' W₀ = Set.Ioo 0 s ∧ ↑b '' W₁ = Set.Ioo q 1)

The other chart also sees the two components as end-segments, one lower and one upper (in one of the two possible arrangements).