Alphabeta MathDefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-04
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.
An abstract simplicial complex
Definition
An abstract simplicial complex is a pair consisting of a set of vertices and a family of finite subsets of such that:
- ;
- if and , then ;
- every singleton with lies in .
The elements of are the simplices of the complex. If is nonempty, its dimension is , and the empty simplex has dimension .
Used by
- A simplicial map and its geometric realization Definition
- An orientation of a simplex Definition
- Deleted-position labels from a fixed reduced expression, the lexicographic shelling criterion, and Möbius data Definition
- Face poset and order complex Definition
- Finite large spherical complexes, their almost-negative matrices, the metric flag condition, and links Definition
- Local finiteness, finiteness, and finite dimensionality of a simplicial complex Definition
- Spherical subsets, the nerve, the poset of spherical cosets, and the Davis realization Definition
- Subcomplexes, closures, stars, and links in a simplicial complex Definition
- The Brady-Watt ordered root complex X(c), its subcomplexes X(sigma) and X(sigma,rho), and their positive-cone realizations Definition
- The geometric realization of an abstract simplicial complex Definition
- Weak-join classifying model of a discrete group Definition
- A finite triangulated surface has a one-polygon schema Lemma
- A geodesically convex cover has the homotopy type of its nerve Lemma
- An augmented simplicial cone has an explicit chain contraction Lemma
- Face coherence, global hat coordinates and a uniform star radius Lemma
- Finite cellulations of compact C² subsurfaces relative to an embedded graph Lemma
- Finite triangulation of a compact connected surface Lemma
- Gram realisations, radial normalisation, finite spherical complexes and link Gram formulas Lemma
- Intersection of root subcomplexes and purity under convexity Lemma
- Smooth manifolds have CW homotopy type Lemma
- The factorization criterion, linear independence of the faces, and the geometric simplicial structure of X(sigma) Lemma
- Deletion-labeled Bruhat intervals are lexicographically shellable, with the explicit earlier/later chain comparison Theorem
- The finite chamber tiling, the face-stabiliser identification, and the spherical Coxeter complex as a triangulation of the sphere Theorem
- The separating-root lemma, the exact facet halfspaces of the added cones, and the spherical convexity of |X(sigma)| Theorem
Dependency tree · 0 levels
Nothing. This result depends on no other item in the library.
Sources
- Allen Hatcher, Algebraic Topology (standard reference, not scraped)
- Vidit Nanda, Computational Algebraic Topology, Lecture 01: Complexes (standard reference, not scraped)