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.
CW approximation of an arbitrary space
Statement
For every topological space there are a CW complex and a continuous map that induces a bijection on path components and isomorphisms for every and every .
More generally, given a CW complex with supplied structure and a continuous map , there are a CW complex containing as a subcomplex and a map extending with those same weak-equivalence properties. In particular, for a pair a prescribed CW approximation extends to a map of pairs whose map on the whole spaces is a CW approximation of and whose restriction is exactly .
No choice principle is assumed. Cells are indexed by all actual maps and extension data, not by a selected set of homotopy-class representatives. Only the finite-source clause of cellular approximation is used. No separation or compact-generation assumption is placed on .
Facts & Assumptions
Cellular approximation for maps of CW pairs makes a map from a finite CW pair cellular rel its specified subcomplex, without choice.
Cellular attachments with finite boundary support form a CW complex proves that the supplied cellular attachments with finite boundary support form a CW complex, preserving earlier closed subcomplexes, and gives the continuous map-out test.
Compact CW images have finite cell support without choice gives finite cell support for each compact-source image in a CW complex. Heine-Borel in : with the Euclidean metric a subset of is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line and For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide give compact spheres, disks and their cylinders. In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones and A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact give the compact-to-Hausdorff closed-map test used for the cone quotient.
Cubical and spherical models of higher homotopy agree identifies based sphere classes and boundary-constant cube classes, including their group laws.
Higher homotopy basepoint transport and moving homotopies gives path-induced isomorphisms and their inverses on all , . Its radial-shell formula commutes pointwise with continuous postcomposition.
Transfinite recursion, applied to the well-order , gives recursion for a definable class function producing sets. It uses ZF Replacement and no AC, so the sets of cells need not lie in one fixed set supplied in advance.
Proof
Given: An arbitrary topological space , a supplied CW complex , and a continuous map . The absolute case will take .
Form , with the new vertices discrete, and put , . This is continuous because the disjoint pieces are open. All vertices of every later stage will be exactly those of and these new vertices. No path component or point in a component is selected. Give each sphere used below its finite CW structure with its designated basepoint a vertex. The based quotient model in [F4] gives this structure by one zero-cell and one top cell; is two vertices. A disk boundary and disk can use the corresponding finite CW pair structure.
Suppose is CW and is specified, for . Let be the set of all pairs where is cellular and is continuous, with For , cellular means that the two boundary points go to vertices. Attach one labeled -disk for every member of , using as its attaching map, and define on this disk to equal its stored map . It agrees with on the boundary, so the attachment quotient makes continuous. These are sets: each map is a subset of the relevant domain-codomain Cartesian product; continuity, cellularity and the boundary equation cut out subsets of their power sets. Labels distinguish different extension data even when their boundary maps coincide.
Every attaching image in step 2.1 meets finitely many cells by [F3], and it lies in because is cellular. Thus [F2] proves that is CW with the preceding stage a closed subcomplex. This proves the induction assertion needed to make the next stage legitimate. The construction of its quotient topology, labeled cells and stored map is specified by the preceding data, rather than chosen from possible extensions. Apply [F6] to the finite histories of these constructions (and use a fixed default value on invalid histories) to produce all stages. Taking their union with the weak attachment topology gives a CW complex by [F2], and their compatible maps give a continuous extending . Every stage is a closed subcomplex of . The number of cells can grow with ; Replacement in [F6] is precisely what collects this set-sized sequence.
Each point of can be joined to a vertex. In a positive-dimensional open cell, use its interior characteristic preimage and a line segment to a boundary point of the disk; the image is a path ending in a lower-dimensional cell. Repeat in that cell until dimension zero is reached. This terminates after finitely many decreases, so requires only finitely many existential choices for one specified point. Zero-cells are already vertices. For any vertices whose images can be joined by a path , their endpoint map is a cellular and , so its attached edge joins in . Every component of is met by some (indeed every point is met). If two points of have images in the same component, join each to a vertex as above, compose their image paths with a connecting path in , and use the corresponding edge to join the vertices. The original two points are then in the same component of . Conversely, sends any connecting path to a connecting path. This proves the bijection on path components without selecting a vertex for every component simultaneously.
Fix any vertex and . A based class in has, by [F4] and the cube-disk radial homeomorphism, a representative constant at on its boundary. The constant map is cellular, so this pair occurs in . The characteristic disk of its attached cell has boundary constantly ; it therefore descends to a based sphere map into , whose composite with is the given representative. Descent is continuous by the quotient definition, and the chosen identification is the same for the original and lifted representatives. Thus is onto at every vertex in every positive degree.
To prove injectivity, let have nullhomotopic composite with . Apply the finite-source clause of [F1] to obtain a based homotopy from to a cellular . Its image lies in , which is contained in : all cells added after stage have higher dimension, while every old cell of was present initially. Since embeds with its subspace topology, is a continuous cellular map into . The homotopy composed with followed by the specified nullhomotopy gives a based nullhomotopy of . It defines a disk map extending : collapse the terminal sphere of to obtain its cone, identified with the disk by . The quotient is compact by pulling covers back to the compact sphere cylinder. Its closed subsets are compact and their images in the Hausdorff disk are closed by [F3], so this continuous bijection is a homeomorphism; the nullhomotopy therefore descends continuously to the disk. Consequently . Its attached disk extends in . If is the marked boundary point of that disk, composing its characteristic map with for contracts to while fixing the marked point. Hence , and therefore , is based-nullhomotopic. Postcomposition with commutes with cubical concatenation, so [F4] makes a homomorphism. Its kernel is trivial, which proves injectivity.
Now fix any and one path from a vertex to , whose existence was proved in step 4.1. By [F5], transport gives isomorphisms from the groups based at to those based at , and from the groups based at to those based at . The square with the maps induced by commutes: the radial-shell transport formula is a representative map on a cube using the original representative on its core and the path on its shell, so composing with replaces the path by and the core by its composite. The bottom vertex-based map is an isomorphism by steps 4.2 and 4.3; conjugating it by these two transport isomorphisms proves the same for . This chooses one path only after one basepoint has been fixed; it is not a simultaneous choice of paths for all points.
Taking gives the asserted and . For a pair with prescribed approximation , apply exactly the same construction to its composite with the inclusion . The resulting agrees literally with that composite on the unchanged subcomplex , so it is a map of pairs with the required restriction, and steps 4.1–5.1 give its whole-space weak equivalence. This argument only uses that the prescribed source is CW; it does not require or to be Hausdorff. No mapping-cylinder theorem with a narrower category of spaces is used.
If , the existence of forces , and there are no vertices or extension data, so ; the component assertion and all basepoint assertions have their stated vacuous meanings. Empty extension sets at any stage simply attach no cells. For , step 4.2 attaches loops from all actual path loops and step 4.3 attaches disks for their actual nullhomotopies; trivial kernel implies injectivity for this possibly nonabelian group as well. Degree zero was proved by actual connecting paths rather than by a group argument. Finite-source cellular approximation and canonical indexing of all data preserve the choice-free claim. The zero and endpoint conditions on every attached disk are its stored boundary equation, not additional extension assumptions.
Depends on
- Cellular approximation for maps of CW pairs
- Cellular attachments with finite boundary support form a CW complex
- Compact CW images have finite cell support without choice
- Cubical and spherical models of higher homotopy agree
- Higher homotopy basepoint transport and moving homotopies
- Transfinite recursion
- Heine-Borel in $\mathbb{R}^n$: with the Euclidean metric a subset of $\mathbb{R}^n$ is compact if and only if it is closed and bounded, and the proof by bisection uses no choice principle; the same holds on the real line
- For a metric space with its metric topology, compactness in the topological sense is compactness in the metric sense, and the two notions of compact subset coincide
- In a Hausdorff space a point and a disjoint compact set, and two disjoint compact sets, have disjoint open neighbourhoods; hence every compact subset is closed, and in a compact Hausdorff space the compact subsets are exactly the closed ones
- A closed subspace of a compact space is compact, and a finite union of compact subspaces is compact
Used by
Dependency tree · two levels
62 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
- Hatcher Proposition 4.13; May Chapter 10 §5 (standard reference, not scraped)