Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-13
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 X there are a CW complex ΓX and a continuous map γ:ΓXX that induces a bijection on path components and isomorphisms πn(ΓX,z)πn(X,γ(z)) for every zΓX and every n1.

More generally, given a CW complex P with supplied structure and a continuous map q:PX, there are a CW complex Z containing P as a subcomplex and a map Q:ZX extending q with those same weak-equivalence properties. In particular, for a pair (X,A) a prescribed CW approximation qA:PA extends to a map of pairs (Z,P)(X,A) whose map on the whole spaces is a CW approximation of X and whose restriction is exactly qA.

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 X.

Facts & Assumptions

[F1]

Cellular approximation for maps of CW pairs makes a map from a finite CW pair cellular rel its specified subcomplex, without choice.

[F2]

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.

[F4]

Cubical and spherical models of higher homotopy agree identifies based sphere classes and boundary-constant cube classes, including their group laws.

[F5]

Higher homotopy basepoint transport and moving homotopies gives path-induced isomorphisms and their inverses on all πn, n1. Its radial-shell formula commutes pointwise with continuous postcomposition.

[F6]

Transfinite recursion, applied to the well-order N, 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 X, a supplied CW complex P, and a continuous map q:PX. The absolute case will take P=.

1.1

Form Z0=P{vx:xX}, with the new vertices discrete, and put Q0P=q, Q0(vx)=x. This is continuous because the disjoint pieces are open. All vertices of every later stage will be exactly those of P 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; S0 is two vertices. A disk boundary and disk can use the corresponding finite CW pair structure.

F2F4given
2.1

Suppose Zk1 is CW and Qk1:Zk1X is specified, for k1. Let Ek be the set of all pairs (a,b) where a:Sk1Zk1 is cellular and b:DkX is continuous, with bSk1=Qk1a. For k=1, cellular means that the two boundary points go to vertices. Attach one labeled k-disk for every member of Ek, using a as its attaching map, and define Qk on this disk to equal its stored map b. It agrees with Qk1 on the boundary, so the attachment quotient makes Qk 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.

F2step 1.1
3.1

Every attaching image in step 2.1 meets finitely many cells by [F3], and it lies in Zk1k1 because a is cellular. Thus [F2] proves that Zk 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 Z by [F2], and their compatible maps give a continuous Q:ZX extending q. Every stage is a closed subcomplex of Z. The number of cells can grow with k; Replacement in [F6] is precisely what collects this set-sized sequence.

F2F3F6step 2.1
4.1

Each point of Z 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 u,v whose images can be joined by a path b:IX, their endpoint map is a cellular a:S0Z0 and (a,b)E1, so its attached edge joins u,v in Z. Every component of X is met by some vx (indeed every point is met). If two points of Z have images in the same component, join each to a vertex as above, compose their image paths with a connecting path in X, and use the corresponding edge to join the vertices. The original two points are then in the same component of Z. Conversely, Q sends any connecting path to a connecting path. This proves the bijection on path components without selecting a vertex for every component simultaneously.

step 1.1step 2.1step 3.1
4.2

Fix any vertex vZ and n1. A based class in πn(X,Q(v)) has, by [F4] and the cube-disk radial homeomorphism, a representative b:DnX constant at Q(v) on its boundary. The constant map a:Sn1{v}Zn1 is cellular, so this pair occurs in En. The characteristic disk of its attached cell has boundary constantly v; it therefore descends to a based sphere map into Zn, whose composite with Q is the given representative. Descent is continuous by the quotient definition, and the chosen identification Dn/DnSn is the same for the original and lifted representatives. Thus Q is onto at every vertex in every positive degree.

F4step 1.1step 2.1step 3.1
4.3

To prove injectivity, let u:(Sn,)(Z,v) have nullhomotopic composite with Q. Apply the finite-source clause of [F1] to obtain a based homotopy from u to a cellular a:SnZ. Its image lies in Zn, which is contained in Zn: all cells added after stage n have higher dimension, while every old cell of P was present initially. Since Zn embeds with its subspace topology, a is a continuous cellular map into Zn. The homotopy composed with Q followed by the specified nullhomotopy gives a based nullhomotopy of Qa. It defines a disk map b:Dn+1X extending Qa: collapse the terminal sphere of Sn×I to obtain its cone, identified with the disk by (z,t)(1t)z. 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 (a,b)En+1. Its attached disk extends a in Z. If s0 is the marked boundary point of that disk, composing its characteristic map with (z,t)(1t)z+ts0 for zSn contracts a to v while fixing the marked point. Hence a, and therefore u, is based-nullhomotopic. Postcomposition with Q commutes with cubical concatenation, so [F4] makes Q a homomorphism. Its kernel is trivial, which proves injectivity.

F1F3F4step 2.1step 3.1
5.1

Now fix any zZ and one path c from a vertex v to z, whose existence was proved in step 4.1. By [F5], transport gives isomorphisms from the groups based at z to those based at v, and from the groups based at Q(z) to those based at Q(v). The square with the maps induced by Q 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 Q replaces the path by Qc 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 Q:πn(Z,z)πn(X,Q(z)). This chooses one path only after one basepoint has been fixed; it is not a simultaneous choice of paths for all points.

F5step 4.1step 4.2step 4.3
6.1

Taking P= gives the asserted ΓX and γ. For a pair (X,A) with prescribed approximation qA:PA, apply exactly the same construction to its composite with the inclusion AX. The resulting Q agrees literally with that composite on the unchanged subcomplex P, 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 P is CW; it does not require A or X to be Hausdorff. No mapping-cylinder theorem with a narrower category of spaces is used.

step 1.1step 3.1step 4.1step 5.1
7.1

If X=, the existence of q forces P=, and there are no vertices or extension data, so Z=; the component assertion and all basepoint assertions have their stated vacuous meanings. Empty extension sets at any stage simply attach no cells. For n=1, 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.

F1F4F6step 2.1step 4.1step 4.2step 4.3step 6.1

Depends on

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