The Schoenflies theorem for polygons #
Statements following Moise, Geometric Topology in Dimensions 2 and 3:
- Ch. 2, Thm. 2: the closed region bounded by a polygon is a finite polyhedron — this is the triangulation theorem for polygonal disks, proved by cutting along the lines through the edges;
- Ch. 3, Thm. 5: any two polygons are equivalent under an ambient homeomorphism of the plane;
- Ch. 3, Thm. 7: the ambient homeomorphism can be chosen supported in any open set containing the closed region (the relative version used for gluing).
Only the polygonal case is stated. The full Schoenflies theorem (Moise Ch. 9) comes after the triangulation theorem in Moise and is not on this route's critical path.
A triangle mesh with exactly one maximal triangle has triangular support.
A finite sequence of supported free-triangle removals ending in one triangle. The frontier
equality in remove is the exact geometric content of Moise's Figure 3.3 needed by the
Schoenflies induction.
- single {U : Set Plane} (M : TriangleMesh) (hcard : M.triangles.card = 1) : AmbientShellingIn U M
- remove {U : Set Plane} (M : TriangleMesh) (t : Finset M.Vertex) (ht : t ∈ M.triangles) (g : Plane ≃ₜ Plane) (hfix : Set.EqOn (⇑g) id Uᶜ) (hfrontier : ⇑g '' frontier M.toPlaneComplex.support = frontier (M.eraseTriangle t).toPlaneComplex.support) (tail : AmbientShellingIn U (M.eraseTriangle t)) : AmbientShellingIn U M
Instances For
A shelling carrying the finite-PL certificate and support image equality required to compose each elementary move on the whole current disk.
- single {U : Set Plane} (M : TriangleMesh) (hcard : M.triangles.card = 1) : PLAmbientShellingIn U M
- remove {U : Set Plane} (M : TriangleMesh) (t : Finset M.Vertex) (ht : t ∈ M.triangles) (g : Plane ≃ₜ Plane) (hpl : FinitePLHomeomorphOn g M.toPlaneComplex.support) (hfix : Set.EqOn (⇑g) id Uᶜ) (hsupport : ⇑g '' M.toPlaneComplex.support = (M.eraseTriangle t).toPlaneComplex.support) (hfrontier : ⇑g '' frontier M.toPlaneComplex.support = frontier (M.eraseTriangle t).toPlaneComplex.support) (tail : PLAmbientShellingIn U (M.eraseTriangle t)) : PLAmbientShellingIn U M
Instances For
A supported ambient shelling composes to a single relative Schoenflies homeomorphism.
A PL-aware shelling composes to a finite PL ambient straightening of its original disk.
An affine equivalence of the Euclidean plane is an ambient homeomorphism.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Moise Chapter 3, Theorem 2 for plane triangles: two nondegenerate closed triangles are carried to one another by an affine ambient homeomorphism.
The edge complex of a polygon #
The nonempty abstract faces of the cyclic edges of a polygon.
Equations
Instances For
A polygon, regarded as its finite one-dimensional geometric complex.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The support of the polygon edge complex is exactly the polygon carrier.
Removing finitely many points from a polygon carrier leaves a dense subset of that carrier. This lets incidence arguments move away from the finite mesh vertex set.
For a mesh whose support is a polygonal disk, the support frontier is exactly the finite union of its incidence-one edge carriers. Polygonality rules out isolated frontier vertices.
Restrict a finite PL certificate on a polygonal disk to its polygonal frontier.
After the three Figure 3.3 base breakpoints have been made polygon vertices, each polygon edge is contained in one base half or avoids the open base altogether.
Once the three Figure 3.3 breakpoints are vertices, the normalized thin-kite move carries the polygon to another polygon. Away from the standard triangle only pointwise fixation is needed; inside it, the old polygon has exactly the horizontal base trace.
A sufficiently thin normalized kite fixes a refined polygon outside the standard triangle. This is the finite boundary-avoidance step used in the inverse, two-edge Figure 3.3 move.
In a triangulated polygonal disk with more than one maximal triangle, every maximal triangle has an edge-neighbor. A triangle attached only at vertices would make its open interior a clopen piece of the connected polygon interior.
If a polygonal-disk mesh has another triangle, some point of the polygon frontier lies outside any prescribed maximal triangle.
The proved starting point of Moise Chapter 3, Theorem 3: a nontrivial triangulated polygonal disk has a weakly free triangle, and that triangle has an edge-neighbor.
Moise Chapter 3, Theorem 3, preliminary step: a nontrivial triangulated polygonal disk has two distinct triangles containing incidence-one edges.
In a two-triangle polygonal disk, each maximal triangle has exactly its two outer edges on the boundary.
Both maximal triangles of a two-triangle polygonal disk are Figure 3.3 free triangles.
The two non-boundary edges in the hard free-triangle configuration are genuine chords: away from their endpoints they lie in the polygon interior.
A bad weakly free triangle supplies the two proper polygonal crosscuts used in Moise's cutting induction.
A bad weakly free triangle supplies two proper polygonal crosscuts.
The hard free-triangle branch produces a theta crosscut realized by an actual mesh edge.
In the two-frontier-edge Figure 3.3 case, the opposite edge is a proper chord of the polygonal disk.
Equations
- M.twoEdgeFreeBaseChord J hsupport T k hfree = { P := M.freeTriangleOrder T k 0, Q := M.freeTriangleOrder T k 1, ne := ⋯, P_mem := ⋯, Q_mem := ⋯, interior_subset := ⋯ }
Instances For
The proper chord in a two-edge ear is realized by the corresponding mesh edge.
In the one-edge Figure 3.3 case, the base is exactly an incidence-one mesh edge.
A non-boundary edge of T is carried by the support remaining after T is deleted.
In the one-edge case, the surviving support attaches to the deleted triangle exactly along the two apex edges.
Exact frontier update in the one-edge Figure 3.3 case.
The old frontier splits into the unchanged part outside the ear and its one-edge trace.
In the two-edge case the old frontier is its unchanged outside part together with the two apex edges.
A Figure 3.3 push which fixes the old frontier away from the ear realizes the exact one-edge deletion frontier.
The supported thin-kite construction realizes the exact one-edge frontier update while remaining the identity off any prescribed neighborhood of the ear.
If a two-edge Figure 3.3 triangle lies on the first side of its base crosscut, that whole side is exactly the closed triangle.
Symmetric form: if the ear lies on the second side, that side is the closed triangle.
In the preceding situation, the first side contains no maximal triangle besides the ear.
Once the first crosscut side is the ear, the second side is exactly the mesh obtained by deleting that ear.
Symmetric form: if the ear lies on the second side, the first side is the erased mesh.
Away from the triangle incident to the new chord, cutting a polygonal disk does not change the frontier trace on a mesh triangle. This is the transport lemma used in Moise's strengthened free-triangle induction.
The symmetric frontier-trace transport theorem for the other cut subdisk.
A geometrically free triangle not incident to the cut edge remains geometrically free after the first cut subdisk is glued back into the original polygonal disk.
The symmetric geometric-freeness transport theorem for the second cut subdisk.
Each cut subdisk has a maximal triangle incident to the new chord edge.
The symmetric chord-incidence existence theorem.
On either side of a crosscut there is at most one maximal triangle containing the chord.
Symmetric uniqueness on the second cut subdisk.
If one cut subdisk consists of a single triangle, the two edges other than the chord are boundary edges of the original disk.
Symmetric one-triangle-side conclusion.
Removing a two-frontier-edge Figure 3.3 ear leaves another polygonal disk. The proof uses the proper base chord and the exact two-side decomposition from Chapter 2.
Moise Chapter 3, Theorem 3 in the strengthened form used by the induction: every nontrivial triangulated polygonal disk has at least two geometrically free maximal triangles.
A compact set with nonempty interior and polygonal frontier is the closed region bounded by that polygon. This recognition lemma lets Figure 3.3 identify the new disk from its frontier.
A homeomorphism carrying the frontier of one polygonal mesh disk to another carries the whole closed disk to the other closed disk.
The one-edge Figure 3.3 move removes an ear through polygonal disks, relative to any open neighborhood of that ear.
The inverse two-edge Figure 3.3 move removes an ear through polygonal disks, relative to any open neighborhood of the ear.
Theorem boundary (Moise Ch. 2, Thm. 2: polygonal disks are finite polyhedra).
The closed region bounded by a polygon is the support of a finite, purely two-dimensional plane complex. Moise's proof cuts the region by the finitely many lines through the polygon's edges and triangulates each convex piece.
The closed region bounded by a polygon admits a geometric triangulation.
This is real glue (not a boundary): it consumes closedRegion_is_polyhedron (Moise Ch. 2,
Thm. 2) and the realization bridge PlaneComplex.toGeometricTriangulation.
Theorem boundary (Moise Ch. 3, Thm. 7: the relative Schoenflies theorem for polygons).
The straightening homeomorphism can be chosen to fix everything outside a prescribed open set
containing the closed region: h sends the polygon to the frontier of a triangle and is the
identity off U. This is the version used to reconcile chart triangulations without disturbing
the part of the complex already built.
Moise Ch. 3, Thm. 5: any two polygons in the plane are equivalent under an ambient homeomorphism. This follows from relative straightening and the affine equivalence of the two resulting triangles.