Gluing continuous maps along two closed embeddings

Let i : X₁ → Y and j : X₂ → Y be closed embeddings whose ranges cover Y. Continuous maps a : C(X₁, Z) and b : C(X₂, Z) that agree wherever i x = j p glue to a continuous map on Y, ContinuousMap.glueClosedEmbeddings, restricting to a along i and to b along j. It is the only such map (ContinuousMap.eq_glueClosedEmbeddings), since a continuous map on Y is determined by its restrictions to the two pieces (ContinuousMap.ext_of_range_union_range).

This is the universal property of a space recorded as the union of two closed pieces, as in TauCeti.DehnFilling and TauCeti.SphereSurgery. Mathlib's ContinuousMap.liftCover needs a cover by neighbourhoods of every point, which two closed sets need not be.

Main definitions

• ContinuousMap.glueClosedEmbeddings: the glued map, with the evaluation lemmas ContinuousMap.glueClosedEmbeddings_apply_left and ContinuousMap.glueClosedEmbeddings_apply_right.

Main results

• ContinuousMap.ext_of_range_union_range: continuous maps agreeing along two maps whose ranges cover are equal.
• ContinuousMap.eq_glueClosedEmbeddings: uniqueness of the glued map.

theorem ContinuousMap.ext_of_range_union_range {X₁ : Type u_1} {X₂ : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] {i : X₁ → Y} {j : X₂ → Y} [TopologicalSpace Z] {f g : C(Y, Z)} (hij : Set.range i ∪ Set.range j = Set.univ) (hi : ∀ (x : X₁), f (i x) = g (i x)) (hj : ∀ (p : X₂), f (j p) = g (j p)) : f = g

Continuous maps agreeing along two maps whose ranges cover are equal.

noncomputable def ContinuousMap.glueClosedEmbeddings {X₁ : Type u_1} {X₂ : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] {i : X₁ → Y} {j : X₂ → Y} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z] (a : C(X₁, Z)) (b : C(X₂, Z)) (hi : Topology.IsClosedEmbedding i) (hj : Topology.IsClosedEmbedding j) (hij : Set.range i ∪ Set.range j = Set.univ) (hab : ∀ (x : X₁) (p : X₂), i x = j p → a x = b p) : C(Y, Z)

Gluing along two closed embeddings. Continuous maps a and b on the sources of closed embeddings i and j whose ranges cover Y, agreeing wherever i x = j p, glue to a continuous map on Y (ContinuousMap.eq_glueClosedEmbeddings).

@[simp]

theorem ContinuousMap.glueClosedEmbeddings_apply_left {X₁ : Type u_1} {X₂ : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] {i : X₁ → Y} {j : X₂ → Y} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z] (a : C(X₁, Z)) (b : C(X₂, Z)) (hi : Topology.IsClosedEmbedding i) (hj : Topology.IsClosedEmbedding j) (hij : Set.range i ∪ Set.range j = Set.univ) (hab : ∀ (x : X₁) (p : X₂), i x = j p → a x = b p) (x : X₁) : (a.glueClosedEmbeddings b hi hj hij hab) (i x) = a x

The glued map restricts to a along i.

@[simp]

theorem ContinuousMap.glueClosedEmbeddings_apply_right {X₁ : Type u_1} {X₂ : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] {i : X₁ → Y} {j : X₂ → Y} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z] (a : C(X₁, Z)) (b : C(X₂, Z)) (hi : Topology.IsClosedEmbedding i) (hj : Topology.IsClosedEmbedding j) (hij : Set.range i ∪ Set.range j = Set.univ) (hab : ∀ (x : X₁) (p : X₂), i x = j p → a x = b p) (p : X₂) : (a.glueClosedEmbeddings b hi hj hij hab) (j p) = b p

The glued map restricts to b along j.

theorem ContinuousMap.eq_glueClosedEmbeddings {X₁ : Type u_1} {X₂ : Type u_2} {Y : Type u_3} {Z : Type u_4} [TopologicalSpace Y] {i : X₁ → Y} {j : X₂ → Y} [TopologicalSpace X₁] [TopologicalSpace X₂] [TopologicalSpace Z] {a : C(X₁, Z)} {b : C(X₂, Z)} {hi : Topology.IsClosedEmbedding i} {hj : Topology.IsClosedEmbedding j} {hij : Set.range i ∪ Set.range j = Set.univ} {hab : ∀ (x : X₁) (p : X₂), i x = j p → a x = b p} {f : C(Y, Z)} (hfi : ∀ (x : X₁), f (i x) = a x) (hfj : ∀ (p : X₂), f (j p) = b p) : f = a.glueClosedEmbeddings b hi hj hij hab

Uniqueness of the glued map: a continuous map on Y restricting to a along i and to b along j is ContinuousMap.glueClosedEmbeddings.