Extraction of Moise charts from the mathlib atlas

Discharges exists_moiseChart_core_mem_nhds: every point of an Eval surface has a boundary-faithful Moise chart (standard unit disk or half-disk model) whose core is a neighborhood. This is the port of the proven chart spine of PL.lean (RadoChartPair.fromChartAt and the euclideanHalfSpace neighborhood lemmas) to the fresh MoiseChart objects; the only new geometry is straightening a small chart ball onto the standard model by the recentering homeomorphism v ↦ ε⁻¹ • (v - p).

The construction: take the preferred chart φ = chartAt (EuclideanHalfSpace 2) x and let p = (φ x).1 in the closed half-plane. Either 0 < p 0 (then a small ball about p lies in the chart image away from the edge, giving a disk chart) or p 0 = 0 (then a small relative half-ball lies in the chart image, giving a half-disk chart). C0 invariance of domain supplies boundary-faithfulness: manifold-boundary points in the chart land on the frontier of the extended target, hence on the model edge line.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.HalfPlaneSet : Set Plane

The closed right half-plane, the ambient model for EuclideanHalfSpace 2.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.HalfPlaneSet = {v : LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane | 0 ≤ v.ofLp 0}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.continuous_coordZero : Continuous fun (v : Plane) => v.ofLp 0

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isOpen_posCoord : IsOpen {v : Plane | 0 < v.ofLp 0}

noncomputable def LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter (p : Plane) (ε : ℝ) (hε : ε ≠ 0) : Plane ≃ₜ Plane

The recentering homeomorphism v ↦ ε⁻¹ • (v - p), straightening the ball ball p ε onto the unit ball.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter p ε hε = (Homeomorph.addRight (-p)).trans (Homeomorph.smulOfNeZero ε⁻¹ ⋯)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_apply {p : Plane} {ε : ℝ} (hε : ε ≠ 0) (v : Plane) : (recenter p ε hε) v = ε⁻¹ • (v + -p)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_symm_apply {p : Plane} {ε : ℝ} (hε : ε ≠ 0) (w : Plane) : (recenter p ε hε).symm w = ε • w + p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_dist {p : Plane} {ε : ℝ} (hε : 0 < ε) (v : Plane) : dist ((recenter p ε ⋯) v) 0 = ε⁻¹ * dist v p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_mem_ball_iff {p : Plane} {ε : ℝ} (hε : 0 < ε) {v : Plane} : (recenter p ε ⋯) v ∈ Metric.ball 0 1 ↔ v ∈ Metric.ball p ε

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_mem_closedBall_iff {p : Plane} {ε : ℝ} (hε : 0 < ε) {v : Plane} : (recenter p ε ⋯) v ∈ Metric.closedBall 0 (1 / 2) ↔ v ∈ Metric.closedBall p (ε / 2)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_coordZero {p : Plane} {ε : ℝ} (hε : ε ≠ 0) (v : Plane) : ((recenter p ε hε) v).ofLp 0 = ε⁻¹ * (v.ofLp 0 - p.ofLp 0)

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.recenter_mem_halfPlane_iff {p : Plane} {ε : ℝ} (hε : 0 < ε) (hp : p.ofLp 0 = 0) {v : Plane} : (recenter p ε ⋯) v ∈ HalfPlaneSet ↔ v ∈ HalfPlaneSet

When the center sits on the edge line, recentering preserves the half-plane condition.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.coordZero_eq_zero_of_mem_frontier {V : Set Plane} (hV : IsOpen V) {z : Plane} (hzmem : z ∈ V ∩ HalfPlaneSet) (hz : z ∈ frontier (V ∩ HalfPlaneSet)) : z.ofLp 0 = 0

A relatively open subset of the closed half-plane meets its own frontier only on the edge line. This is the geometric fact behind boundary-faithfulness of the extracted charts.

Moise charts

inductive LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind : Type

The kind of a Moise chart: interior charts are disks, boundary charts are half-disks.

• disk : ChartKind
• halfDisk : ChartKind

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.instDecidableEqChartKind : DecidableEq ChartKind

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.instDecidableEqChartKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance LeanEval.Topology.ClassificationOfSurfaces.Moise.instReprChartKind : Repr ChartKind

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.instReprChartKind = { reprPrec := LeanEval.Topology.ClassificationOfSurfaces.Moise.instReprChartKind.repr }

def LeanEval.Topology.ClassificationOfSurfaces.Moise.instReprChartKind.repr : ChartKind → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelRegion : ChartKind → Set Plane

The model region of a chart kind: the open unit disk, or its closed-right half.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.disk.modelRegion = Metric.ball 0 1
• LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.halfDisk.modelRegion = {x : LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane | x ∈ Metric.ball 0 1 ∧ 0 ≤ x.ofLp 0}

def LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelCore : ChartKind → Set Plane

The model core of a chart kind: the closed disk of radius one half, or its right half. Cores are compact and their union over a chart cover is what the Radó induction absorbs.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.disk.modelCore = Metric.closedBall 0 (1 / 2)
• LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.halfDisk.modelCore = {x : LeanEval.Topology.ClassificationOfSurfaces.Moise.Plane | x ∈ Metric.closedBall 0 (1 / 2) ∧ 0 ≤ x.ofLp 0}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.isCompact_modelCore (k : ChartKind) : IsCompact k.modelCore

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.ChartKind.modelCore_subset_modelRegion (k : ChartKind) : k.modelCore ⊆ k.modelRegion

def LeanEval.Topology.ClassificationOfSurfaces.Moise.halfDiskModelToHalfSpace : ↑ChartKind.halfDisk.modelRegion → EuclideanHalfSpace 2

Forget the unit-ball condition on a half-disk model point while retaining its half-space coordinate.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.Moise.halfDiskModelToHalfSpace p = ⟨↑p, ⋯⟩

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.halfDiskModelToHalfSpace_val (p : ↑ChartKind.halfDisk.modelRegion) : ↑(halfDiskModelToHalfSpace p) = ↑p

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.isOpenEmbedding_halfDiskModelToHalfSpace : Topology.IsOpenEmbedding halfDiskModelToHalfSpace

The half-disk model is an open subset of the Euclidean half-space.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.mem_interior_range_of_fixed_boundary_preserving_in_halfDiskChart {S : Type u_1} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] {X : Type u_2} [TopologicalSpace X] (D : Set S) (hD : IsOpen D) (chart : ↑D ≃ₜ ↑ChartKind.halfDisk.modelRegion) (hchartBoundary : ∀ (y : S) (hy : y ∈ D), y ∈ ModelWithCorners.boundary S ↔ (↑(chart ⟨y, hy⟩)).ofLp 0 = 0) {f g : X → S} (hf : Topology.IsEmbedding f) (hg : Topology.IsEmbedding g) (hboundary : ∀ (y : X), g y ∈ ModelWithCorners.boundary S ↔ f y ∈ ModelWithCorners.boundary S) {x : X} (hxInterior : f x ∈ interior (Set.range f)) (hxDomain : f x ∈ D) (hxFixed : g x = f x) : f x ∈ interior (Set.range g)

Boundary-relative invariance of domain in a half-disk chart.

Suppose two embeddings of the same source preserve the ambient manifold-boundary stratum. If the corresponding source point is fixed and its old physical image is an interior point of the old range, then that physical point remains in the interior of the new range. The proof restricts to the old physical interior, writes both embeddings in the half-disk chart, applies the half-plane doubling theorem, and transports the resulting open coordinate image back to the surface.

structure LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart (S : Type u_1) [TopologicalSpace S] : Type u_1

A chart of the Moise cover: an open domain homeomorphic to the model disk or half-disk, with the compact core marked out by the chart.

• kind : ChartKind

  Whether this is an interior (disk) or boundary (half-disk) chart.

• domain : Set S

  The chart domain.

• isOpen_domain : IsOpen self.domain

  Chart domains are open.

• chart : ↑self.domain ≃ₜ ↑self.kind.modelRegion

  The chart homeomorphism onto the model region.

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.core {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : Set S

The core of a chart: the part of the domain corresponding to the model core.

Equations

• c.core = Subtype.val '' ⇑c.chart ⁻¹' {p : ↑c.kind.modelRegion | ↑p ∈ c.kind.modelCore}

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.core_subset_domain {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : c.core ⊆ c.domain

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.isCompact_core {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) : IsCompact c.core

Chart cores are compact closed disks or half-disks transported through the chart.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.mem_core_iff {S : Type u_1} [TopologicalSpace S] (c : MoiseChart S) {s : S} : s ∈ c.core ↔ ∃ (hs : s ∈ c.domain), ↑(c.chart ⟨s, hs⟩) ∈ c.kind.modelCore

Extraction from the mathlib atlas

def LeanEval.Topology.ClassificationOfSurfaces.Moise.MoiseChart.BoundaryFaithful {S : Type u_2} [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (c : MoiseChart S) : Prop

A chart is boundary-faithful when its model kind honestly reflects the manifold boundary: disk charts contain no manifold-boundary points, and in a half-disk chart the manifold-boundary stratum is exactly the model edge line.

The forward half-disk implication is ChartBoundaryInvariant. The reverse implication follows from the same invariance-of-domain layer: chart independence identifies a zero normal coordinate with the frontier of the half-space model.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartImage_eq_inter (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) : Subtype.val '' (chartAt (EuclideanHalfSpace 2) x).target = ↑(modelWithCornersEuclideanHalfSpace 2).symm ⁻¹' (chartAt (EuclideanHalfSpace 2) x).target ∩ HalfPlaneSet

The image of the preferred chart's target in the plane is a relatively open subset of the closed half-plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartImage_mem_nhds_of_coord_pos (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) (hpt : 0 < (↑(↑(chartAt (EuclideanHalfSpace 2) x) x)).ofLp 0) : Subtype.val '' (chartAt (EuclideanHalfSpace 2) x).target ∈ nhds ↑(↑(chartAt (EuclideanHalfSpace 2) x) x)

The chart image is an ambient plane neighborhood of the center's image when the latter is away from the edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.chartImage_mem_nhdsWithin (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) : Subtype.val '' (chartAt (EuclideanHalfSpace 2) x).target ∈ nhdsWithin (↑(↑(chartAt (EuclideanHalfSpace 2) x) x)) HalfPlaneSet

The chart image is a relative half-plane neighborhood of the center's image.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.coordZero_of_boundary (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) {y : S} (hy : y ∈ (chartAt (EuclideanHalfSpace 2) x).source) (hybd : y ∈ ModelWithCorners.boundary S) : (↑(↑(chartAt (EuclideanHalfSpace 2) x) y)).ofLp 0 = 0

Boundary points of the chart source have edge-line chart coordinates: the chart-level consequence of planar invariance of domain.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_moiseChart_of_coord_pos (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) (hpt : 0 < (↑(↑(chartAt (EuclideanHalfSpace 2) x) x)).ofLp 0) : ∃ (c : MoiseChart S), c.BoundaryFaithful ∧ c.core ∈ nhds x

Interior case of the chart extraction: a disk chart at a point whose preferred chart coordinate is away from the edge.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_moiseChart_of_coord_zero (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) (hpt : (↑(↑(chartAt (EuclideanHalfSpace 2) x) x)).ofLp 0 = 0) : ∃ (c : MoiseChart S), c.BoundaryFaithful ∧ c.core ∈ nhds x

Boundary case of the chart extraction: a half-disk chart at a point whose preferred chart coordinate lies on the edge line.

theorem LeanEval.Topology.ClassificationOfSurfaces.Moise.exists_moiseChart_core_mem_nhds (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] (x : S) : ∃ (c : MoiseChart S), c.BoundaryFaithful ∧ c.core ∈ nhds x

Local chart extraction (Moise Ch. 8, Thm. 1, local part; bordered version).

Every point of an Eval surface has a boundary-faithful Moise chart whose core is a neighborhood of the point: interior points get disk charts, edge points get half-disk charts, and invariance of domain supplies boundary-faithfulness.