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.
A PL embedded polyhedron becomes a subcomplex after subdivision
Statement
Let be a compact piecewise-linear polyhedron with a fixed finite linear triangulation . If is a piecewise-linear embedding of a compact piecewise-linear polyhedron, then some finite subdivision of contains as the realization of a subcomplex.
Statement references
PL embeddings and subpolyhedra — the image of a piecewise-linear embedding is a subpolyhedron in some finite triangulation.
Subcomplexes, closures, stars, and links in a simplicial complex — a subcomplex is closed under taking faces.
Two finite linear subdivisions have a common simplicial refinement — common refinement for subdivisions of a fixed finite Euclidean complex; the intersection-cell construction below handles the two given linear triangulations directly.
Facts & Assumptions
Given: A compact piecewise-linear polyhedron , a finite linear triangulation of , and a piecewise-linear embedding .
PL embeddings and subpolyhedra: is a subcomplex in some finite linear triangulation of .
Intersections of finite linear complexes form a convex cell complex forms a finite convex intersection-cell complex from two finite linear simplicial complexes in one Euclidean space with the same underlying polyhedron. Finite convex cell complexes admit compatible triangulations gives it a compatible finite linear simplicial triangulation. These are the construction used in the narrower Two finite linear subdivisions have a common simplicial refinement.
Subcomplexes, closures, stars, and links in a simplicial complex: a subcomplex is closed under taking faces.
Proof
By [F1], choose a finite linear triangulation of in which is a subcomplex.
Regard and as finite linear complexes on the same embedded polyhedron . Form all nonempty cells for and , together with their faces. By [F2] these form a finite convex cell complex covering , and a compatible finite simplicial triangulation of that cell complex exists. Each simplex of lies in a cell contained in a simplex of and a simplex of , so is a common linear refinement. In particular it is a subdivision of . Every simplex of the subcomplex representing is a union of these refined simplices; thus the simplices of contained in have realization exactly and form a subcomplex by [F3].
Depends on
Used by
- A compact locally collared polyhedron has a piecewise linear collar Lemma
- Cutting an irreducible manifold along incompressible tori preserves irreducibility Lemma
- Finite piecewise linear level collars give global band products Lemma
- Innermost critical height loops admit strict piecewise linear cap reduction Lemma
- No closed nonorientable piecewise-linear surface embeds in the three-sphere Lemma
- Parametrized piecewise linear balls absorb standard boundary windows Lemma
- Pointed flat piecewise linear caps admit saddle-free replacements Lemma
- Polyhedral two-spheres without height saddles bound parametrized piecewise linear balls Lemma
- Three-disk piecewise linear severing reassembles parametrized balls Lemma
Dependency tree · two levels
8 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
- C. P. Rourke and B. J. Sanderson, Introduction to Piecewise-Linear Topology (standard reference, not scraped)