Alphabeta Math
LemmaStatement: 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.

Relative homotopy compares with the CW quotient in the connectivity range

Statement

Let (X,A) be an r-connected CW pair with r0, and suppose A is s-connected with s0. For every aA, the ordinary quotient induces πi(X,A,a)πi(X/A,),=A/A, bijectively for 1ir+s and surjectively for i=r+s+1. These bijections are group isomorphisms for i2 and pointed bijections for i=1. No choice principle is required.

Facts & Assumptions

[F1]

Connectivity of a CW pair gives relative connectivity including components. N connected space and n connected map says that s-connectedness for s0 includes nonemptiness and path-connectedness. Relative homotopy classes and groups identifies relative representatives with subspace a point with absolute based cubes.

[F2]

Cellular mapping cylinders and relative cylinders are CW complexes constructs the ordinary mapping cylinder of a cellular map and proves its retraction weak at all basepoints. Cellular attachments with finite boundary support form a CW complex assembles CW unions along subcomplexes from the supplied cells and boundary maps.

[F4]

Long exact sequence of relative homotopy groups gives the pair sequence, with exact pointed tail in degree one.

[F5]

Homotopy excision gives isomorphism below the sum of the two pair connectivities and surjection at that sum, with positive indices and connected common subcomplex.

[F6]

CW quotients and collapse of a contractible subcomplex gives the CW quotient and makes collapse of a contractible subcomplex a weak equivalence. Weak equivalences of pairs induce isomorphisms on relative homotopy gives relative bijections when both ambient and subspace maps are weak equivalences.

Proof

Given: The CW pair and r,s. Fix any aA, which is possible since A is nonempty by [F1].

1.1

Apply [F2] to the constant cellular map A{v}, with empty fixed subcomplex. Its ordinary cylinder, after reversing the interval coordinate, is exactly the cone CA of [F3], with A as its free-end subcomplex and v as apex. It is CW, and its retraction to v induces a component bijection and isomorphisms on all positive groups at every basepoint. In particular CA is path-connected and has trivial positive homotopy groups. Its explicit contraction is [x,u][x,u+t(1u)], from the identity to the apex; quotient-times-interval continuity is included in [F2].

F2F3given
2.1

Build Y=XACA from X by adjoining the apex vertex and then the remaining cells of CAA. Their boundary maps have finite support and are cellular, so [F2] gives a CW complex containing X and CA as subcomplexes with intersection exactly A. Its map-out test is continuity on X and CA with agreement on A, since these tests are precisely their supplied characteristic-disk tests. Thus this is the ordinary amalgamated union, not a different topology on that set.

F2step 1.1
2.2

The pair (CA,A) is (s+1)-connected. Component-surjectivity holds because CA is path-connected and A nonempty. In the pointed tail of [F4], π0(A)π0(CA) is bijective since both spaces are path-connected. Thus every relative degree-one class is in the image of π1(CA), which is zero by step 1.1. For 2js+1, the adjacent absolute cone groups are zero, and [F4] identifies πj(CA,A,a) with πj1(A,a); the latter is zero by s-connectedness. This range is empty for s=0. These calculations hold at the specified arbitrary point a and also at every other point of A.

F1F4step 1.1
3.1

Apply [F5] to the union in step 2.1, whose common subcomplex A is nonempty path-connected. Its two pair connectivities are r for (X,A) and s+1 for (CA,A). We obtain e:πi(X,A,a)πi(Y,CA,a) bijective for 1i<r+s+1 and surjective for i=r+s+1. All the hypotheses, including the endpoint when r=s=0, are covered by steps 1.1–2.2.

F1F5step 2.1step 2.2
3.2

Collapse CA inside Y. It is a nonempty contractible subcomplex by steps 1.1–2.1, so [F6] makes p:YY/CA a weak equivalence. The restriction CA{} is also weak by step 1.1. Hence the pair comparison of [F6] induces a bijection p:πi(Y,CA,a)πi(Y/CA,,) in every positive degree. The relative target classes are precisely absolute based cubes by [F1]; no nontrivial boundary values remain. For i2 the comparison preserves the group operations, while at i=1 this is an identification of the underlying pointed sets.

F1F6step 1.1step 2.1
4.1

There is a canonical homeomorphism Y/CAX/A. Set-theoretically it retains exactly the points of XA and the one collapsed point. A function out of Y/CA is continuous exactly when its composite on Y is continuous and constant on CA. By the union map-out test in step 2.1, this says exactly that its restriction on X is continuous and constant on A, which is the quotient map-out criterion for X/A. Testing characteristic maps into the two-point open-set classifier, as in [F6], proves equality of the two topologies. Under this identification, pX is the original quotient map q:XX/A. Consequently pe=q on the cubical relative representatives. Combining steps 3.1 and 3.2 gives bijectivity for the integral indices 1ir+s and surjectivity at r+s+1, as claimed.

F1F6step 2.1step 3.1step 3.2
5.1

For r=s=0 only the positive degree-one surjection is asserted, and step 3.1 gives it; no relative degree-zero group has been introduced. If A=X, both the relative source sets and the positive groups of the one-point quotient are trivial, consistent with every claimed range. A singleton A and no relative cells are also allowed. Every cone endpoint and quotient value is fixed by its defining relation; the argument uses the arbitrary original basepoint a, which need not be a vertex. The cone contraction is explicit, its collapse uses choice-free HEP, and the excision theorem and relative weak comparison are choice-free. Therefore this entire comparison requires no AC, including for infinite CW complexes.

F1F2F5F6step 1.1step 2.2step 3.1step 4.1

Depends on

Used by

Dependency tree · two levels

45 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