Gluing a vanishing approximation across an open frontier

Moise Chapter 8 replaces a chart-transition map on an open, locally finite subcomplex. The replacement is controlled by a tolerance which tends to zero at the frontier, so it fits continuously with the unchanged map outside the open set. This file isolates that analytic argument from the later complex bookkeeping.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.StronglyPositiveOn {X : Type u_1} [TopologicalSpace X] (U : Set X) (phi : X → ℝ) : Prop

A positive control on U is strongly positive when it has a positive lower bound on every compact subset of U. This is Moise's notation phi >> 0, stated without continuity.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.StronglyPositiveOn U phi = ∀ (C : Set X), IsCompact C → C ⊆ U → ∃ (eps : ℝ), 0 < eps ∧ ∀ x ∈ C, eps ≤ phi x

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierDistance {X : Type u_1} [PseudoMetricSpace X] (U : Set X) (x : X) : ℝ

Distance to the complement, the canonical frontier-vanishing control on an open set.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierDistance U x = Metric.infDist x Uᶜ

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierDistance_pos {X : Type u_1} [PseudoMetricSpace X] {U : Set X} (hU : IsOpen U) (hUc : Uᶜ.Nonempty) {x : X} (hx : x ∈ U) : 0 < frontierDistance U x

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.stronglyPositiveOn_frontierDistance {X : Type u_1} [PseudoMetricSpace X] {U : Set X} (hU : IsOpen U) (hUc : Uᶜ.Nonempty) : StronglyPositiveOn U (frontierDistance U)

Distance to the complement is strongly positive on the open set.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.VanishesAtFrontier {X : Type u_1} [TopologicalSpace X] (U : Set X) (phi : X → ℝ) : Prop

The control tends to zero when points of U approach its frontier.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.VanishesAtFrontier U phi = ∀ x ∈ frontier U, Filter.Tendsto phi (nhdsWithin x U) (nhds 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.vanishesAtFrontier_frontierDistance {X : Type u_1} [PseudoMetricSpace X] {U : Set X} (hU : IsOpen U) : VanishesAtFrontier U (frontierDistance U)

Distance to the complement tends to zero along the open set at every frontier point.

Compact exhaustion of a proper open set

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierCore {X : Type u_1} [PseudoMetricSpace X] (U : Set X) (n : ℕ) : Set X

The n-th compact core of an open set, cut out by distance to its complement.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierCore U n = {x : X | 1 / (↑n + 1) ≤ LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierDistance U x}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isCompact_frontierCore {X : Type u_1} [PseudoMetricSpace X] [CompactSpace X] (U : Set X) (n : ℕ) : IsCompact (frontierCore U n)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierCore_subset {X : Type u_1} [PseudoMetricSpace X] {U : Set X} : Uᶜ.Nonempty → ∀ (n : ℕ), frontierCore U n ⊆ U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.iUnion_frontierCore {X : Type u_1} [PseudoMetricSpace X] {U : Set X} (hU : IsOpen U) (hUc : Uᶜ.Nonempty) : ⋃ (n : ℕ), frontierCore U n = U

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierCore_subset_interior_succ {X : Type u_1} [PseudoMetricSpace X] (U : Set X) (n : ℕ) : frontierCore U n ⊆ interior (frontierCore U (n + 1))

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierGlue {X : Type u_1} {Y : Type u_2} (U : Set X) (g h : X → Y) : X → Y

Replace h by g on U.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierGlue U g h = U.piecewise g h

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierGlue_of_mem {X : Type u_1} {Y : Type u_2} {U : Set X} {g h : X → Y} {x : X} (hx : x ∈ U) : frontierGlue U g h x = g x

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.frontierGlue_of_notMem {X : Type u_1} {Y : Type u_2} {U : Set X} {g h : X → Y} {x : X} (hx : x ∉ U) : frontierGlue U g h x = h x

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MatchesAtFrontier {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] (U : Set X) (g h : X → Y) : Prop

A replacement agrees asymptotically with the old map at the frontier of its open domain. This is the topology-only form of Moise's condition phi(P) → 0.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.MatchesAtFrontier U g h = ∀ x ∈ frontier U, Filter.Tendsto g (nhdsWithin x U) (nhds (h x))

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_frontierGlue_of_matches {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [TopologicalSpace Y] {U : Set X} (hU : IsOpen U) {g h : X → Y} (hg : ContinuousOn g U) (hh : Continuous h) (hmatch : MatchesAtFrontier U g h) : Continuous (frontierGlue U g h)

A frontier-matching replacement on an open set glues continuously to the unchanged map. Unlike continuous_frontierGlue, this form does not require a metric on the target.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_frontierGlue {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PseudoMetricSpace Y] {U : Set X} (hU : IsOpen U) {g h : X → Y} (hg : ContinuousOn g U) (hh : Continuous h) {phi : X → ℝ} (hphi : VanishesAtFrontier U phi) (hclose : ∀ x ∈ U, dist (g x) (h x) ≤ |phi x|) : Continuous (frontierGlue U g h)

A replacement on an open set glues continuously to the old map when its error tends to zero at the frontier. No local finiteness or PL data enters this lemma.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.matchesAtFrontier_of_vanishing_close {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [PseudoMetricSpace Y] {U : Set X} (hU : IsOpen U) {g h : X → Y} (hg : ContinuousOn g U) (hh : Continuous h) {phi : X → ℝ} (hphi : VanishesAtFrontier U phi) (hclose : ∀ x ∈ U, dist (g x) (h x) ≤ |phi x|) : MatchesAtFrontier U g h

Metric closeness controlled by a frontier-vanishing function supplies the topology-only matching condition. This is the bridge from the quantitative Chapter 6 approximation to the metric-free paste in the ambient surface.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.range_frontierGlue {X : Type u_1} {Y : Type u_2} {U : Set X} {g h : X → Y} : Set.range (frontierGlue U g h) = g '' U ∪ h '' Uᶜ

The range of a frontier glue is exactly the union of the replacement image and the unchanged image. This set-level formula is the one used in Moise Chapter 8 when the modified old complex is united with the finite chart complex.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.injective_frontierGlue {X : Type u_1} {Y : Type u_2} {U : Set X} {g h : X → Y} (hg : Set.InjOn g U) (hh : Function.Injective h) (hcross : Disjoint (g '' U) (h '' Uᶜ)) : Function.Injective (frontierGlue U g h)

A replacement which is injective on the open set and misses the unchanged outside image glues to a globally injective map. No compactness or continuity is needed for this part.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isEmbedding_frontierGlue {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactSpace X] [PseudoMetricSpace Y] [T2Space Y] {U : Set X} (hU : IsOpen U) {g h : X → Y} (hgcont : ContinuousOn g U) (hhcont : Continuous h) {phi : X → ℝ} (hphi : VanishesAtFrontier U phi) (hclose : ∀ x ∈ U, dist (g x) (h x) ≤ |phi x|) (hginj : Set.InjOn g U) (hhinj : Function.Injective h) (hcross : Disjoint (g '' U) (h '' Uᶜ)) : Topology.IsEmbedding (frontierGlue U g h)

On a compact source, the continuous injective frontier glue is a topological embedding. This packages the exact analytic conclusion used for Moise's modified map f'_n.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isEmbedding_frontierGlue_of_matches {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [CompactSpace X] [TopologicalSpace Y] [T2Space Y] {U : Set X} (hU : IsOpen U) {g h : X → Y} (hgcont : ContinuousOn g U) (hhcont : Continuous h) (hmatch : MatchesAtFrontier U g h) (hginj : Set.InjOn g U) (hhinj : Function.Injective h) (hcross : Disjoint (g '' U) (h '' Uᶜ)) : Topology.IsEmbedding (frontierGlue U g h)

Compact-to-Hausdorff embedding form of the topology-only frontier glue.