Extending maps of an open piece by the identity

Let j : Y → X be an open embedding. A continuous family of self-maps of Y which fixes the points of j ⁻¹' V, for an open neighbourhood V of the complement of the range of j, extends by the identity to a continuous family of self-maps of X which fixes every point of V.

Let χ : Z → Y be an open embedding, for instance a chart onto an open subset of Y, and let Λ be a homeomorphism of Z that moves only points lying over a closed subset C of Y contained in the image of χ. Transporting Λ along χ and extending by the identity off C gives a homeomorphism of Y. This is how a homeomorphism written down in coordinates is made global: the closedness of C is what makes the identity extension continuous at the frontier of the image of χ.

Main results

• Topology.IsOpenEmbedding.exists_continuousMap_extend_id: a continuous family of self-maps of Y extended along j by the identity.
• Topology.IsOpenEmbedding.exists_homeomorph_extend: the homeomorphism of Y extending Λ along χ by the identity.

theorem Topology.IsOpenEmbedding.exists_continuousMap_extend_id {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {j : Y → X} (hj : IsOpenEmbedding j) {Z : Type u_3} [TopologicalSpace Z] {V : Set X} (hV : IsOpen V) (hjV : (Set.range j)ᶜ ⊆ V) (G : C(Z × Y, Y)) (hG : ∀ (z : Z) (y : Y), j y ∈ V → G (z, y) = y) : ∃ (Φ : C(Z × X, X)), (∀ (z : Z) (y : Y), Φ (z, j y) = j (G (z, y))) ∧ ∀ (z : Z), ∀ x ∈ V, Φ (z, x) = x

A family of self-maps of an open piece extends by the identity. Let j : Y → X be an open embedding and G : Z × Y → Y a continuous family of self-maps of Y. If V is an open set containing the points outside the range of j and every G z fixes the points of j ⁻¹' V, then the family transported along j extends to a continuous family of self-maps of X that fixes every point of V.

theorem Topology.IsOpenEmbedding.exists_homeomorph_extend {Y : Type u_1} {Z : Type u_2} [TopologicalSpace Y] [TopologicalSpace Z] {χ : Z → Y} {C : Set Y} (hχ : IsOpenEmbedding χ) (Λ : Z ≃ₜ Z) (hC : IsClosed C) (hCχ : C ⊆ Set.range χ) (hΛ : ∀ (z : Z), χ z ∉ C → Λ z = z) : ∃ (H : Y ≃ₜ Y), (∀ (z : Z), H (χ z) = χ (Λ z)) ∧ ∀ y ∉ C, H y = y

A homeomorphism Λ of Z, moving only points whose images under the open embedding χ lie in a closed set C ⊆ range χ, extends along χ by the identity to a homeomorphism of Y: one that agrees with Λ read through χ and fixes every point off C.