How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Finite cellulations of compact C² subsurfaces relative to an embedded graph
Statement
Assume . Let be a compact codimension-zero subsurface of a Hausdorff second-countable boundaryless surface , with boundary. Let be a finite embedded graph: its vertices are distinct points, each edge is a regular embedded arc up to its endpoints, and different edge interiors are disjoint and avoid the vertices. Closed regular edges may first be subdivided by inserting finitely many vertices. Then has a finite triangular cellulation containing in its one-skeleton. Each closed triangle is an embedded topological disk, the prescribed graph and original boundary retain their regular arcs, and the cell maps induce a homeomorphism from a finite abstract simplicial complex onto after finite subdivision. Interior edges have two incident triangles and boundary edges one; vertex links are circles or intervals, respectively.
A cell map is required to be a homeomorphism; the statement does not assert a differentiable straightening of an arbitrary prescribed graph at its vertices. This permits tangencies between prescribed edge germs. The empty or empty is allowed.
Facts & Assumptions
Given: as in the statement, with countable choice.
For a Euclidean map from dimension to dimension , critical values are null when (Morse-Sard for Euclidean maps).
A map with invertible derivative has a local inverse; a scalar equation with nonzero normal derivative has a unique local root (C² inverses and scalar return roots).
A simple polygon has two complementary regions, one bounded and one unbounded, with that polygon as the frontier of each (Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each).
A simple polygonal region has a finite face-to-face triangular subdivision (Every simple polygon admits a triangulation).
An abstract simplicial complex has finite subsets as its simplices, with every face also a simplex (An abstract simplicial complex). A finite disk-cell structure is a CW structure if its cell maps are the stated disk attachments and its topology is the weak topology on the closed cells (CW complex with closure finiteness and weak topology).
A map with invertible derivative has a local inverse (The Euclidean inverse function theorem).
Under the stated countable choice, a nonempty compact connected topological one-manifold without boundary is a circle (A nonempty compact connected one-dimensional manifold without boundary is a circle).
Proof
If is empty use the empty complex. Otherwise choose finitely many relatively compact coordinate disks in with smaller cores covering . Their closures remain inside their respective charts. The boundary has finitely many components: a finite cover of this compact one-manifold by connected interval neighborhoods meets every component, so there are only finitely many. By F7 each component is a circle, covered by finitely many of its regular graph arcs. Work with these finitely many boundary curves and the finitely many edges of . Choose each coordinate-disk radius in a short open interval that leaves its smaller covering core inside it. At each stage restrict the radial function to the compact pieces of every preceding curve and graph edge in the chart annulus. Finitely many parameter intervals inside that chart cover these compact pieces. By F1 for maps of dimension one to one, a radius avoiding the critical values makes the new circle transverse to all those curves. Avoid also the finitely many distances of existing vertices and crossings. Finitely many null sets and finitely many forbidden values cannot fill the radius interval. Thus the disk boundaries, and have finitely many transverse crossings, with no new triple crossing and no crossing at a prescribed vertex. Finiteness follows from compactness and the local isolation supplied by transversality. These choices are finite.
Subdivide at all crossings and insert vertices in isolated closed edges. The union of , and the portions of the disk circles inside is a finite embedded graph . Each of its nonvertex points has an arc chart by F2. Its vertex stars are tame finite stars, even when two prescribed germs are tangent: in a chart at a vertex , a regular one-sided edge with and has strictly increasing distance from for small , since . Hence every sufficiently small concentric circle meets each incident germ exactly once. Their cyclic order cannot change without an intersection. A homeomorphism on each such circle sending these finitely many ordered intersection points to fixed radial directions, extended with the same radius and sending to the center, straightens the star; continuity of it and its inverse at the center follows from preservation of radius. Thus each star has finitely many well-defined sectors, or half-sectors at . Cover each remaining compact edge portion by finitely many arc charts and choose a thin strip about it; compactness and separation from the other finite edge portions make the strips disjoint away from the chosen vertex stars. Their two sides and the vertex sectors are the finite local side data of .
Every connected component of is planar before we count the components: membership in any coordinate disk is constant on , because it avoids that disk's boundary. A point of belongs to a covering disk core, so all of lies in that disk and its closure lies in the corresponding compact chart disk. Its frontier lies in and has a side or vertex sector from step 2.1. An empty frontier would make it a nonempty compact boundaryless open surface contained in a planar disk, which is impossible since its chart image would be both open and compact in the plane. A frontier consisting only of finitely many vertices cannot enclose a bounded open region: a ray from an interior point avoiding their finitely many directions would exit without meeting the frontier. Each edge-side germ or vertex sector lies in just one complementary component. The finite side data therefore bounds the number of components; call them . This proves both planarity and finiteness without an arbitrary surface-Jordan assertion.
(Compact planar cores, including slit sides.) For each choose one point in each of its finitely many incident side sectors. Join those points to one interior point by finitely many paths in ; inside its planar chart these may be finite polygonal paths, obtained by the elementary open-and-closed argument for the set of points reachable by finite segments in small open balls. Trim the vertex stars and edge strips sufficiently thinly to miss those compact paths. On each edge use a product strip, and at each vertex trim its sectors by a small arc. The remaining portion of is a compact planar surface with boundary, with finitely many piecewise regular boundary circuits. It is connected: the selected paths join all side sectors, while any extra component would have to border one of those same trimmed edge or vertex sectors, whose connected inner boundary collar already joins the selected paths. The original face is recovered by attaching the finitely many product half-strips and vertex sectors. Distinct occurrences of a slit edge are retained as distinct sides; they are identified only when these strips are restored. Consequently repeated boundary vertices or slit sides in the closure of are not falsely regarded as a single embedded polygonal boundary.
(Regular planar circuits reduce to polygons.) The finitely many boundary circuits of a planar core are disjoint piecewise regular embedded circles. For a regular compact arc, F2 straightens it in finitely many charts to a coordinate line. Its compact middle portions have disjoint thin product strips. A sufficiently fine inscribed broken line meets each strip fiber once: on every chosen straightening chart the arc has nonzero derivative in one fixed direction, the chords retain this sign by uniform continuity of its tangent, and the finite subdivision is fine enough to remain in that chart. Thus the broken line is a graph over the arc there. For a closed regular circuit, its unit normal is . The normal strip map is with invertible derivative along its zero section, so F6 and compactness make a short strip injective: a hypothetical sequence of collisions in arbitrarily short strips has base points converging to one common curve point, where the local inverse excludes it. A sufficiently fine inscribed polygon projects locally increasingly to the central circle in that collar, including at its corners, by the tangent estimate just used. The projection has degree one because it is uniformly close to the identity parameterization, hence is a one-sheeted circle covering and the polygon is a single graph over the old circle. For a finitely cornered circuit first use the vertex-sector charts of step 2.1 to match the finite endpoint sectors. Graph interpolation in a strip, chosen to be the identity on its outer boundary, gives a homeomorphism carrying the arc to its broken line. At corners the radial sector interpolation agrees with the strip maps. Finite closed pasting gives an ambient homeomorphism of a neighborhood of the circuit, equal to the identity outside it. The neighborhoods of distinct core boundary circuits are disjoint, so all can be polygonalized at once. Their assigned inside/outside sides are now those of F3. This proves precisely the regular-curve adapter used here; it imports neither Jordan–Schönflies for arbitrary curves nor a general surface triangulation theorem.
(Planar subdivisions with holes.) A polygonalized compact core may have several boundary circles. Choose a direction whose projections of all its finitely many vertices are distinct. Between consecutive projections all boundary segments are ordered affine graphs. Moving vertically from outside the bounded domain, membership changes at a boundary segment and nowhere else, by the local side charts and F3. Its intersection with each open slab is therefore a finite union of bands between consecutive affine graphs. Their closures are convex triangles or quadrilaterals. Refine all vertical walls at their finitely many intersections, use the same refinement on both sides, and fan each convex cell from one interior point. This gives a finite triangulation, also in the presence of holes; for a single simple polygon this is exactly F4. Pull it back by the homeomorphisms of step 5.1. Fill each restored product half-strip by a rectangle subdivision, and fill each restored vertex sector by a finite fan. These cell maps are embeddings of closed disks in the original chart sectors. Subdivide the old edges at the union of the two incident side subdivisions, so restored pieces meet face-to-face. Prescribed edges of and the original boundary remain edges of the resulting subdivision. The additional subdivision edges are tame embedded arcs supplied by these homeomorphisms; they are not claimed to be merely because the original chart and prescribed graph are . Only their topological incidence and disk-face maps are needed below. The prescribed graph edges and original boundary arcs themselves have not been changed.
The finitely many embedded closed triangles cover , and their incidences give a circular link at an interior vertex and an interval link at a boundary vertex, because they fill exactly the chart sectors of step 2.1. If multiple edges have the same endpoints or a triangular incidence initially repeats a vertex, first subdivide every edge with a distinct new midpoint, fan each disk face from its distinct new center, and subdivide the resulting triangles once more. Every new small triangle then has vertices specified by its incident old vertex, edge midpoint and face center; distinct such incidence flags share exactly their common flags. Thus their vertex sets define a finite abstract simplicial complex as in F5. The face maps paste to a continuous bijection from its compact realization onto Hausdorff , hence to a homeomorphism: a compact-to-Hausdorff continuous bijection is closed. The same finite closed-cell pasting proves the weak topology and finite disk attachments required by F5. No choice beyond the stated ACω is used; all geometric selections in this proof are finite and F1 is applied only on finitely many Euclidean curve pieces.
Depends on
- The countable-choice principle used in the foliation pair
- Morse-Sard for Euclidean maps
- C² inverses and scalar return roots
- Polygonal Jordan curve theorem: a polygon has exactly two complementary regions and is the frontier of each
- Every simple polygon admits a triangulation
- An abstract simplicial complex
- CW complex with closure finiteness and weak topology
- The Euclidean inverse function theorem
- A nonempty compact connected one-dimensional manifold without boundary is a circle
Used by
Dependency tree · two levels
46 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gallier and Xu, A Guide to the Classification Theorem for Compact Surfaces (standard reference, not scraped)
- Diestel, Graph Theory, Chapter 4 (standard reference, not scraped)