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 noncompact algebraic line needs a deleted boundary triangulation
Example
The analytic complex affine line cannot be homeomorphic to the realization of a finite simplicial complex. It is homeomorphic to a finite triangulated compactification with one boundary vertex deleted. Thus "finite triangulation" for noncompact varieties must allow a deleted subcomplex or another equivalent noncompact finite-cell convention.
Facts & Assumptions
Given: The usual analytic topology on , and the fixed complex structure that identifies with (Complex -space and its real coordinate dictionary, The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement).
The realization of a finite simplicial complex is compact (A finite simplicial complex has a compact Hausdorff realization).
A homeomorphism is a continuous bijection with continuous inverse, and composites of continuous maps are continuous (Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological, Continuity of a map of topological spaces at a point and globally).
Verification
The increasing open disks for positive integers cover , and no finite subfamily covers: a finite union of such disks is contained in the largest of them. Hence is not compact, and by [F1] it is not homeomorphic to the realization of any finite simplicial complex.
Let be the boundary complex of the octahedron with vertices and eight triangular faces, one for each choice of signs. Its realization is : every listed triangular face satisfies the equation and every point of the -sphere lies in such a face. The radial normalization maps this realization bijectively onto the unit sphere , with inverse ; both maps are continuous, so by [F2] it is a homeomorphism. Deleting the subcomplex consisting of the single vertex identifies with .
For put and map to . Its squared Euclidean norm is , so the image lies on , and its third coordinate is strictly less than . The map is defined on and is inverse to the previous formula by direct substitution; both are continuous. Composing with the identification and with step 1.2 gives a homeomorphism , a finite triangulation with one boundary vertex deleted; step 1.1 shows that deleting a boundary simplex is necessary for a noncompact space.
Remarks
- The example exhibits the deleted-boundary convention used by the finite triangulation statements of the companion page. It makes no claim about compactifications of higher-dimensional or singular varieties, and it does not assert that an arbitrary algebraic morphism becomes simplicial.
Depends on
- Continuity of a map of topological spaces at a point and globally
- Homeomorphism, open map, closed map, embedding, and what it means for a property to be topological
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- A finite simplicial complex has a compact Hausdorff realization
- Complex $m$-space and its real coordinate dictionary
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
28 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
- Mark Goresky, Lecture Notes on Sheaves and Perverse Sheaves, version of June 26, 2026 (standard reference, not scraped)