Core lemmas for gluing overlapping charts

Two results feed the gluing construction:

• Connectivity: if U is a boundary chart (target Iio v), its overlap with any other chart is connected — every component's U-image is an upper end-segment Ioo q v (outer-overlap lemma), and two upper end-segments always intersect.

• End-matching: the transition map on the overlap is strictly monotone in the direction forced by which ends of the two chart images are interior (the endpoint belongs to the chart target). If both interior ends were paired with each other, the overlap would accumulate at two distinct points of M at once, contradicting T2.

theorem OneMfld.tendsto_top_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 v (Set.Iio v)) (nhds q)

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

theorem OneMfld.chartTransition_continuous_injective {M : Type u_1} [TopologicalSpace M] (a b : OpenPartialHomeomorph M NNReal) {I : Set NNReal} (hI : I ⊆ a.target) (hmap : ∀ t ∈ I, ↑a.symm t ∈ b.source) : ContinuousOn (fun (t : NNReal) => ↑b (↑a.symm t)) I ∧ Set.InjOn (fun (t : NNReal) => ↑b (↑a.symm t)) I

A chart transition is continuous and injective wherever the first inverse chart lands in the second chart's source.

theorem OneMfld.chartTransition_image_data {M : Type u_1} [TopologicalSpace M] (a b : OpenPartialHomeomorph M NNReal) {W : Set M} (hW : W ⊆ a.source ∩ b.source) {I J : Set NNReal} (ha : ↑a '' W = I) (hb : ↑b '' W = J) : (∀ t ∈ I, ↑a.symm t ∈ W ∧ ↑a (↑a.symm t) = t) ∧ (∀ x ∈ W, ↑b (↑a.symm (↑a x)) = ↑b x) ∧ I ⊆ a.target ∧ (fun (t : NNReal) => ↑b (↑a.symm t)) '' I = J

On a common source subset, chart transitions preserve coordinates and map the first chart image exactly onto the second.

theorem OneMfld.chartTransition_endpoint_eq {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) {I : Set NNReal} {s t : NNReal} (hI : I ⊆ a.target) (hmap : ∀ x ∈ I, ↑a.symm x ∈ b.source) (hs : s ∈ a.target) (ht : t ∈ b.target) (hne : (nhdsWithin s I).NeBot) (hlim : Filter.Tendsto (fun (x : NNReal) => ↑b (↑a.symm x)) (nhdsWithin s I) (nhds t)) : ↑a.symm s = ↑b.symm t

A transition limit at interior chart endpoints identifies their inverse images.

theorem OneMfld.overlap_connected {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) (hne : (U.source ∩ V.source).Nonempty) : IsConnected (U.source ∩ V.source)

The overlap of a boundary chart U (target Iio v) with any other chart is connected: every component's U-image is an upper end-segment of Iio v, and two upper end-segments intersect, so there is only one component.

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) (hr : r ∈ a.target) (hq : q ∈ b.target) (hrS : r ∉ ↑a '' (a.source ∩ b.source)) (x : M) : x ∈ W → ∀ y ∈ W, ↑a x < ↑a y → ↑b x < ↑b y

Component version of overlap_mono: on a subset W of the overlap whose images are Ioo p r and Ioo q w, with the r-end interior to a.target, the q-end interior to b.target, and r not in the image of the full overlap, the transition is increasing.

theorem OneMfld.overlap_mono {M : Type u_1} [TopologicalSpace M] [T2Space M] (a b : OpenPartialHomeomorph M NNReal) {p r q w : NNReal} (ha : ↑a '' (a.source ∩ b.source) = Set.Ioo p r) (hb : ↑b '' (a.source ∩ b.source) = Set.Ioo q w) (hr : r ∈ a.target) (hq : q ∈ b.target) (x : M) : x ∈ a.source ∩ b.source → ∀ y ∈ a.source ∩ b.source, ↑a x < ↑a y → ↑b x < ↑b y

End-matching, increasing case. Suppose the overlap S = a.source ∩ b.source has image Ioo p r in chart a and Ioo q w in chart b, where the r-end is interior to a.target and the q-end is interior to b.target. Then the transition is increasing: a x < a y → b x < b y on S. (If it were decreasing, the overlap would accumulate at both a.symm r and b.symm q along the same filter, forcing them equal — but then that point would lie in S, putting r in Ioo p r.)

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

End-matching, decreasing case. Same setting, but now the p-end is interior to a.target (and the q-end interior to b.target): the transition is decreasing.