PL approximation of homeomorphisms #
The crux of the Moise route (Moise, Geometric Topology in Dimensions 2 and 3, Ch. 5-6):
- Ch. 5, Thms. 3-6 (combinatorial Schoenflies and cone extension): a PL homeomorphism between the boundaries of two triangles extends to a PL homeomorphism of the triangles;
- Ch. 6, Thm. 2: an embedding of a finite one-dimensional complex into the plane can be approximated, arbitrarily closely and fixing vertex images, by a PL embedding;
- Ch. 6, Thm. 3: an embedding of a finite combinatorial 2-manifold-with-boundary into the plane can be approximated, arbitrarily closely, by a PL embedding.
Moise's own remark (end of Ch. 8): the restriction to dimension 2 in the entire triangulation
proof is used only through Thm. 6.3. This file is therefore the mathematical core of the
route. Moise states Ch. 6 with strongly positive control functions φ ≫ 0 to handle
non-compact complexes; our complexes are finite, so uniform ε-control is equivalent and the
statements below use it.
The full Jordan curve theorem (Ch. 4) is not used by these theorems: Thm. 6.2 needs only broken-line connectivity (Ch. 1), and Thm. 6.3 needs the polygonal theorems of Ch. 2-3 through the combinatorial Schoenflies theorem.
Every closed triangle has an explicit polygonal presentation of its frontier.
The topological interior of a full-dimensional plane simplex is its barycentric interior.
Every maximal face of a plane complex is a nondegenerate closed triangle.
The frontier of a two-cell of a plane complex is covered facewise by its one-skeleton.
Every point of a pure complex lies in a maximal triangle.
A vertex of a maximal triangle lies on its Euclidean frontier.
The convex hull of at most two vertices of a maximal triangle lies in its frontier.
A used complex vertex outside a maximal face is not geometrically contained in that face.
Refine a polygonal presentation of a complex support so that every used complex vertex is an explicit polygon vertex.
If every vertex of a graph complex supported on a polygon is among the polygon vertices, then each polygon edge lies in a single graph face.
A facewise-affine embedding of a graph complex supported on a polygon transports that polygon to a polygon whose carrier is the exact image.
The image of a polygon under a PL embedding of its carrier is again a polygon.
A connected set mapped off a polygon lies in its exterior as soon as one image point does. This is the component argument used implicitly in Moise's proof of Chapter 6, Theorem 3.
Two polygonal disks have disjoint interiors if each boundary avoids the other interior and the boundaries are genuinely different. If the interiors met, connectedness would force one bounded complementary component into the other; taking closures would then force every point of its boundary into the other closed disk.
The bounded region of a polygon lies in every closed ball containing its boundary.
A polygonal boundary with a continuous filling avoiding p has p on its unbounded side.
If p were inside the polygon, polygonal Schoenflies straightens its closed region to a
triangle. Radial projection from the image of p, followed by the inverse boundary
homeomorphism, would retract the source triangle onto its frontier, contradicting
IsTriangle.no_retraction.
A uniformly small perturbation of a triangle boundary has a uniformly small continuous
extension over the triangle. This is the bounded, finite-dimensional Tietze extension theorem
applied to the displacement b - h.
PL maps compose on a polygon when the first map embeds it onto another polygon.
The proof refines the source polygon at the breakpoints of the first PL presentation and at the preimages of the breakpoints of the second. On the resulting cyclic edge complex both maps are affine edge by edge.
A finite plane complex is a combinatorial 2-manifold-with-boundary in the weak sense needed by the approximation theorem: purely two-dimensional, with every edge in at most two cells. (Moise additionally asks for connected vertex links; embeddability in the plane forces the link conditions, so they are omitted from the hypothesis here — if the proof turns out to need them, strengthen this predicate rather than weakening the theorem.)
Equations
Instances For
An injective map preserves the exact face-to-face intersection of two simplex carriers.
Images of disjoint faces of an embedded finite graph admit disjoint metric thickenings.
A finite embedded two-complex has one positive separation radius which works for every maximal cell and every complex vertex not belonging to that cell.
A polygonal arc extracted from a broken line is the PL image of a straight segment.
Theorem boundary (Moise Ch. 5, Thms. 3-6: combinatorial Schoenflies / cone extension).
A map that is PL and injective on the frontier of a triangle, carrying it onto the frontier of a second triangle, extends to a map of the closed triangles with the same properties. Moise proves this by coning from an interior point: the extension is linear on each segment from the cone point to the boundary.
A PL embedding of a triangular boundary onto a polygon extends over the polygonal disk.
The target polygon is straightened by the finite PL Schoenflies homeomorphism, the triangular boundary problem is solved by coning, and the result is pulled back through the inverse straightening using common subdivision.
The named graph-replacement subdivision restricts to the frontier of each maximal triangle, and its polygonal image bounds a certified PL cell extension.
A certified PL filling of the polygonalized boundary of one maximal face.
- polygon : PolygonalCircle
The
polygondeclaration. The
mapdeclaration.- eqOn_frontier : Set.EqOn self.map g (frontier (K.cellCarrier ↑t))
- continuousOn : ContinuousOn self.map (K.cellCarrier ↑t)
- injOn : Set.InjOn self.map (K.cellCarrier ↑t)
- isPLOnSet : IsPLOnSet (K.cellCarrier ↑t) self.map
- finitePL : Nonempty (FinitePLHomeomorphBetween self.map (K.cellCarrier ↑t) self.polygon.closedRegion)
Instances For
The cell interior maps into the bounded complementary component of its polygonal boundary.
Cell extensions chosen from one boundary map agree wherever their source cells overlap.
Glue a chosen family of cell extensions as a function. Coherence on overlaps is proved
separately by CellExtensionData.family_eqOn_cell_inter.
Equations
- K.cellwiseExtensionMap E x = if hx : ∃ (t : ↥K.cells), x ∈ K.cellCarrier ↑t then (E (Classical.choose hx)).map x else x
Instances For
A finite coherent family of certified cell extensions glues to one PL map on the whole complex. The common witness cuts the source by every barycentric coordinate line occurring in any local certificate.
The side condition needed to glue cell extensions injectively: the embedded global graph does not enter the bounded interior selected for any cell boundary.
Equations
Instances For
Moise's finite side-control condition: the polygonal disk selected for a cell contains no
complex vertex outside that cell. For a graph embedding this finite condition implies
GraphAvoidsInteriors; the propagation along nonincident edges is the combinatorial content of
the last paragraph of Chapter 6, Theorem 3.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Moise's finite vertex-avoidance condition propagates over every graph face.
Under graph-side compatibility, the bounded interiors selected for distinct cells are disjoint.
Cellwise PL extensions form a global embedding once their polygon interiors avoid the global one-skeleton.
Quantitative control for the glued cell extension. If h oscillates by less than η on
each cell and the polygonalized graph is δ-close to h, then every filled cell moves points by
less than δ + 2 * η.
Package the cell extension produced from the named graph replacement.
Any PL embedding of a triangular frontier has a certified polygonal-disk extension.
A close graph approximation preserves the side of every cell boundary. Bounded Tietze
extension turns the boundary displacement into a filling which stays inside the prescribed
vertex-to-cell thickening; PolygonalCircle.mem_exteriorRegion_of_continuous_extension then
detects the unbounded side.
Topological side-stability boundary in Moise Ch. 6, Thm. 3.
The simultaneous graph replacement is performed in pairwise separated vertex disks and edge tubes. Consequently an original complex vertex outside a triangular face remains on the unbounded side of the replacement polygon for that face. Equivalently, it does not belong to the polygonal closed disk selected by any certified extension.
This is the precise content hidden in Moise's sentence
f(σ) ⊂ N(h(σ), εσ). It is a planar side-preservation (or mod-two winding)
statement, not a metric convexity estimate: its proof compares the replacement boundary with
the original embedded boundary in the complement of the outside vertex.
Moise Ch. 6, Thm. 2: PL approximation on one-dimensional complexes.
An embedding of the support of a finite one-dimensional complex into the plane can be
ε-approximated by a PL embedding that agrees with it on every vertex. Moise's proof: choose a
fine subdivision, replace each small arc by a broken line in a small neighborhood (Ch. 6, Thm. 1,
which rests on the broken-line connectivity of open connected sets, Ch. 1), keeping the broken
lines disjoint except at shared endpoints.
Moise Ch. 6, Thm. 3 in the generality used by its proof: PL approximation of an embedded pure finite two-complex in the plane.
An embedding of the support of a pure finite two-complex into the plane can be
ε-approximated by a PL embedding. Moise's proof: approximate on the one-skeleton by
Thm. 6.2, then extend across each 2-cell by the combinatorial Schoenflies theorem
(pl_extension_of_triangle_boundary), with the subdivision chosen fine enough that the extended
images of distinct cells have disjoint interiors.
The face-to-face plane-complex axioms and purity already provide all incidence properties used in the argument; no separate link or edge-degree hypothesis is needed.
Moise Ch. 6, Thm. 3 for a finite combinatorial two-manifold with boundary. This public
surface-shaped interface is a direct specialization of
pl_approximation_pure_two_complex.