Closing the graph of a transition map

Three point-set lemmas behind the Hausdorffness of the space glued from local complexifications [BW59, Proposition 1]. For a continuous map φ on an open subset Ω ⊆ Y into Y' write graphOn φ S ⊆ Y × Y' for its graph over S ⊆ Ω.

1. exists_isOpen_graphOn_closure_disjoint: given G ⊆ graphOn φ Ω and a closed E ⊆ Y × Y' with closure G disjoint from E, there is an open S with fst '' G ⊆ S ⊆ Ω such that closure (graphOn φ S) is still disjoint from E. (For the gluing: G is the graph of the transition over the real overlap, E the pairs of real points outside the two domains.)
2. closure_graphOn_inter_subset, isClosed_closure_diff_graphOn: over an open S, the closure of the graph meets S × Y' only in the graph, so the boundary closure Γ ∖ Γ is a closed set, the set the pieces must avoid; closure_graphOn_inter_prod_subset is the version for a homeomorphism between open subsets whose graph closes away from the pairs outside both domains.
3. isClosed_image_prodMap_of_eq: for closed embeddings f : A → Y, g : B → Y' and continuous a : A → X, b : B → X into a Hausdorff X, the set {(f u, g v) | a u = b v} is closed in Y × Y' (the "real diagonal" of two complexifications is closed because X is Hausdorff).

Conventions. Y, Y' are metrizable (analytic spaces are regular and second countable), and the metric of Mathlib's metrizableSpaceMetric on the product is used only inside the proof of (1): S := {y ∈ Ω | infDist (y, φ y) G < infDist (y, φ y) E}; the cases G = ∅ (take S = ∅) and E = ∅ (take S = Ω) are separate. For Ω = ∅ every graph is empty; for E = ∅ there is no shrinking; for S = Ω, (2) says that the graph of a continuous map on an open set into a Hausdorff space is closed in Ω × Y'. Not in the sources.

def AnalyticSpace.Glue.graphOn {Y : Type u} {Y' : Type v} {Ω : Set Y} (φ : ↑Ω → Y') (S : Set Y) : Set (Y × Y')

The graph of φ : Ω → Y' over the subset S of the base.

Equations

• AnalyticSpace.Glue.graphOn φ S = {p : Y × Y' | ∃ (y : ↑Ω), ↑y ∈ S ∧ p = (↑y, φ y)}

theorem AnalyticSpace.Glue.graphOn_mono {Y : Type u} {Y' : Type v} {Ω : Set Y} (φ : ↑Ω → Y') {S T : Set Y} (h : S ⊆ T) : graphOn φ S ⊆ graphOn φ T

theorem AnalyticSpace.Glue.fst_mem_of_mem_graphOn {Y : Type u} {Y' : Type v} {Ω : Set Y} {φ : ↑Ω → Y'} {S : Set Y} {p : Y × Y'} (hp : p ∈ graphOn φ S) : p.1 ∈ S

theorem AnalyticSpace.Glue.graphOn_eq_preimage_swap {Y : Type u} {Y' : Type v} {Ω : Set Y} {φ : ↑Ω → Y'} {Ω' : Set Y'} {ψ : ↑Ω' → Y} (hφΩ : ∀ (y : ↑Ω), φ y ∈ Ω') (hψφ : ∀ (y : ↑Ω), ψ ⟨φ y, ⋯⟩ = ↑y) (hψΩ : ∀ (y' : ↑Ω'), ψ y' ∈ Ω) (hφψ : ∀ (y' : ↑Ω'), φ ⟨ψ y', ⋯⟩ = ↑y') : graphOn φ Ω = Prod.swap ⁻¹' graphOn ψ Ω'

The graph of φ over Ω is the transpose of the graph of its inverse ψ over Ω'.

(1) Shrinking the domain so that the closure of the graph avoids a closed set

theorem AnalyticSpace.Glue.exists_isOpen_graphOn_closure_disjoint {Y : Type u} {Y' : Type v} [TopologicalSpace Y] [TopologicalSpace Y'] [TopologicalSpace.MetrizableSpace Y] [TopologicalSpace.MetrizableSpace Y'] {Ω : Set Y} (hΩ : IsOpen Ω) {φ : ↑Ω → Y'} (hφ : Continuous φ) {G E : Set (Y × Y')} (hG : G ⊆ graphOn φ Ω) (hE : IsClosed E) (hGE : Disjoint (closure G) E) : ∃ (S : Set Y), IsOpen S ∧ S ⊆ Ω ∧ Prod.fst '' G ⊆ S ∧ Disjoint (closure (graphOn φ S)) E

Shrinking the domain of a continuous partial map so that the closure of its graph avoids a closed set E, keeping a given subgraph G whose closure already avoids E.

(2) The boundary of the graph over an open set is closed

theorem AnalyticSpace.Glue.closure_graphOn_inter_subset {Y : Type u} {Y' : Type v} [TopologicalSpace Y] [TopologicalSpace Y'] [T2Space Y'] {Ω : Set Y} {φ : ↑Ω → Y'} (hφ : Continuous φ) {S : Set Y} (hS : IsOpen S) (hSΩ : S ⊆ Ω) : closure (graphOn φ S) ∩ S ×ˢ Set.univ ⊆ graphOn φ S

Over an open S, the closure of the graph meets S × Y' only in the graph.

theorem AnalyticSpace.Glue.isClosed_closure_diff_graphOn {Y : Type u} {Y' : Type v} [TopologicalSpace Y] [TopologicalSpace Y'] [T2Space Y'] {Ω : Set Y} {φ : ↑Ω → Y'} (hφ : Continuous φ) {S : Set Y} (hS : IsOpen S) (hSΩ : S ⊆ Ω) : IsClosed (closure (graphOn φ S) \ graphOn φ S)

The boundary closure Γ ∖ Γ of the graph over an open set is closed.

(1′) With an inverse: the closure of the graph meets R × R' only in the graph

theorem AnalyticSpace.Glue.closure_graphOn_inter_prod_subset {Y : Type u} {Y' : Type v} [TopologicalSpace Y] [TopologicalSpace Y'] [T2Space Y] [T2Space Y'] {Ω : Set Y} (hΩ : IsOpen Ω) {φ : ↑Ω → Y'} (hφ : Continuous φ) {Ω' : Set Y'} (hΩ' : IsOpen Ω') {ψ : ↑Ω' → Y} (hψ : Continuous ψ) (hφΩ : ∀ (y : ↑Ω), φ y ∈ Ω') (hψφ : ∀ (y : ↑Ω), ψ ⟨φ y, ⋯⟩ = ↑y) (hψΩ : ∀ (y' : ↑Ω'), ψ y' ∈ Ω) (hφψ : ∀ (y' : ↑Ω'), φ ⟨ψ y', ⋯⟩ = ↑y') {R : Set Y} {R' : Set Y'} (hE : Disjoint (closure (graphOn φ Ω)) ((R \ Ω) ×ˢ (R' \ Ω'))) : closure (graphOn φ Ω) ∩ R ×ˢ R' ⊆ graphOn φ Ω

If φ : Ω → Y' is a homeomorphism onto the open Ω' with inverse ψ, and the closure of its graph avoids the pairs of R × R' outside both domains, then the closure of the graph meets R × R' only in the graph: a limit (a, b) with a ∈ Ω lies on the graph by continuity of φ, one with b ∈ Ω' by continuity of ψ, and the remaining pairs are excluded.

(3) The real diagonal is closed

theorem AnalyticSpace.Glue.isClosed_image_prodMap_of_eq {Y : Type u} {Y' : Type v} [TopologicalSpace Y] [TopologicalSpace Y'] {X : Type u_1} {A : Type u_2} {B : Type u_3} [TopologicalSpace X] [T2Space X] [TopologicalSpace A] [TopologicalSpace B] {f : A → Y} {g : B → Y'} (hf : Topology.IsClosedEmbedding f) (hg : Topology.IsClosedEmbedding g) {a : A → X} {b : B → X} (ha : Continuous a) (hb : Continuous b) : IsClosed {p : Y × Y' | ∃ (u : A) (v : B), a u = b v ∧ p = (f u, g v)}

For closed embeddings f, g and continuous maps a, b into a Hausdorff space, the set of pairs (f u, g v) with a u = b v is closed.