Boundary invariance for C0 surface charts

This file discharges the ChartBoundaryInvariant interface for topological surface charts. The plane has invariance of domain by Moise.instBrouwerFixedPointPlane and the general invariance-of-domain theorem. Steven Sivek's chart-independence argument then shows that a manifold-boundary point is sent to the frontier of the model range by every chart containing it. The frontier of the chart's extended target follows because its interior is contained in the interior of the model range.

instance LeanEval.Topology.ClassificationOfSurfaces.chartBoundaryInvariant_of_invarianceOfDomain (S : Type u_1) [TopologicalSpace S] [ChartedSpace (EuclideanHalfSpace 2) S] : ChartBoundaryInvariant S

C0 invariance of the boundary stratum for surface charts, derived from planar invariance of domain.

def LeanEval.Topology.ClassificationOfSurfaces.reflectAcrossHalfPlaneBoundary (p : Moise.Plane) : Moise.Plane

Reflection in the boundary line of the Euclidean half-plane.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.reflectAcrossHalfPlaneBoundary p = WithLp.toLp 2 fun (i : Fin 2) => if i = 0 then -p.ofLp i else p.ofLp i

def LeanEval.Topology.ClassificationOfSurfaces.foldPlaneToHalfSpace (p : Moise.Plane) : EuclideanHalfSpace 2

Fold the plane onto the Euclidean half-plane by taking the absolute value of its normal coordinate.

Equations

• LeanEval.Topology.ClassificationOfSurfaces.foldPlaneToHalfSpace p = ⟨WithLp.toLp 2 fun (i : Fin 2) => if i = 0 then |p.ofLp i| else p.ofLp i, ⋯⟩

theorem LeanEval.Topology.ClassificationOfSurfaces.continuous_reflectAcrossHalfPlaneBoundary : Continuous reflectAcrossHalfPlaneBoundary

Reflection across the boundary line is continuous.

theorem LeanEval.Topology.ClassificationOfSurfaces.continuous_foldPlaneToHalfSpace : Continuous foldPlaneToHalfSpace

Folding the plane onto the Euclidean half-plane is continuous.

theorem LeanEval.Topology.ClassificationOfSurfaces.injective_reflectAcrossHalfPlaneBoundary : Function.Injective reflectAcrossHalfPlaneBoundary

Reflection across the boundary line is injective.

@[simp]

theorem LeanEval.Topology.ClassificationOfSurfaces.reflectAcrossHalfPlaneBoundary_involutive (p : Moise.Plane) : reflectAcrossHalfPlaneBoundary (reflectAcrossHalfPlaneBoundary p) = p

Reflection across the boundary line is an involution.

theorem LeanEval.Topology.ClassificationOfSurfaces.foldPlaneToHalfSpace_val_of_nonneg (p : Moise.Plane) (hp : 0 ≤ p.ofLp 0) : ↑(foldPlaneToHalfSpace p) = p

Folding fixes points on the nonnegative side of the boundary line.

theorem LeanEval.Topology.ClassificationOfSurfaces.foldPlaneToHalfSpace_val_of_neg (p : Moise.Plane) (hp : p.ofLp 0 < 0) : ↑(foldPlaneToHalfSpace p) = reflectAcrossHalfPlaneBoundary p

Folding a point on the negative side agrees with reflection.

theorem LeanEval.Topology.ClassificationOfSurfaces.norm_reflectAcrossHalfPlaneBoundary (p : Moise.Plane) : ‖reflectAcrossHalfPlaneBoundary p‖ = ‖p‖

Reflection across the boundary line preserves the Euclidean norm.

theorem LeanEval.Topology.ClassificationOfSurfaces.norm_foldPlaneToHalfSpace (p : Moise.Plane) : ‖↑(foldPlaneToHalfSpace p)‖ = ‖p‖

Folding onto the half-plane preserves the Euclidean norm.

theorem LeanEval.Topology.ClassificationOfSurfaces.isOpen_range_halfSpace_of_isOpen_of_isEmbedding_of_boundary {U : Set (EuclideanHalfSpace 2)} (hU : IsOpen U) (f : ↑U → EuclideanHalfSpace 2) (hf : Topology.IsEmbedding f) (hboundary : ∀ (x : ↑U), (↑(f x)).ofLp 0 = 0 ↔ (↑↑x).ofLp 0 = 0) : IsOpen (Set.range f)

Relative invariance of domain for the Euclidean half-plane.

An embedding of an open subset of the half-plane has open image provided it carries the boundary line exactly to the boundary line. The boundary hypothesis is necessary: without it, an embedding may bend a boundary arc into the interior. The proof doubles the source and map across the boundary line, applies planar invariance of domain, and then restricts the resulting open image back to the half-plane.

theorem LeanEval.Topology.ClassificationOfSurfaces.mem_interior_range_halfSpace_of_isEmbedding_of_boundary {X : Type u_1} [TopologicalSpace X] {f g : X → EuclideanHalfSpace 2} (hf : Topology.IsEmbedding f) (hg : Topology.IsEmbedding g) (hboundary : ∀ (x : X), (↑(g x)).ofLp 0 = 0 ↔ (↑(f x)).ofLp 0 = 0) {x : X} (hx : f x ∈ interior (Set.range f)) : g x ∈ interior (Set.range g)

A boundary-preserving re-embedding of a fixed source carries every old interior sheet to an interior sheet of its new half-plane image.

Unlike pointwise physical coverage, this statement compares corresponding source points. It is the local relative-invariance-of-domain input used when two polyhedral pieces are identified along a boundary-preserving seam.