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.

Weak equivalences of pairs induce isomorphisms on relative homotopy

Statement

Let f:(X,A)(Y,B) be a continuous map of pairs, with subspace topologies on A,B. Suppose both f:XY and g=fA:AB are weak homotopy equivalences. For every aA, the induced map f:πn(X,A,a)πn(Y,B,f(a)) is a pointed bijection for n=1 and a group isomorphism for every n2. The spaces need not be CW complexes. No choice principle is required.

Facts & Assumptions

[F1]

Weak homotopy equivalence specifies all-basepoint weak equivalence. Relative homotopy classes and groups uses D=In, distinguished face F=In1×{0} and union J of the other faces; a relative cube sends F into the subspace and J to the basepoint.

[F2]

Relative homotopy operations are well defined in their valid degrees proves functoriality for based pair maps and that postcomposition preserves products in degrees n2.

[F3]

Finite relative homotopy lifting across a weak equivalence lifts a finite-relative CW source across a weak equivalence with a prescribed lift and prescribed comparison homotopy on its subcomplex. The lift extends the prescribed map exactly. For a constant prescribed comparison, the resulting homotopy is fixed on that subcomplex.

[F4]

Relative CW inclusions are cofibrations gives HEP for any CW subcomplex, with arbitrary target and without choice.

Proof

Given: The maps of pairs and their weak-equivalence hypotheses. Fix one aA, write b=f(a), and fix n1. Put D=In and S=In=FJ.

1.1

All source pairs below are finite CW pairs. Give each interval its two vertices and open edge, and each cube its product faces: a d-face has closure a closed d-cube, radially homeomorphic to a disk, with boundary its lower faces. Finite pasting gives the weak topology for this finite closed-face cover, so this is a finite CW structure. Unions of faces are subcomplexes. In particular (S,J), (D,S), and the cylinder face pairs used below meet [F3, F4]. This verification concerns only finite cubes, not products of arbitrary CW spaces.

F1given
2.1

To prove surjectivity let u:DY represent a relative class, so u(S)B and uJ=b. Apply [F3] to g:AB, the source pair (S,J), target map uS and prescribed constant lift a on J, with constant comparison there. Obtain v:SA with vJ=a and a homotopy T:uSgv in B fixed on J. Apply [F4] to extend T, viewed in Y, to a homotopy E:D×IY starting at u. It remains fixed on J and sends S into B at every time, because those are its prescribed boundary values. Its endpoint U satisfies US=fv.

F3F4step 1.1
2.2

To prove injectivity, take relative cubes w0,w1:DX and a relative homotopy H:D×IY from fw0 to fw1. Write Q=D×I, V=S×I, and V0=(S×{0,1})(J×I). On V0 prescribe a map z:V0A by z(x,0)=w0(x), z(x,1)=w1(x) for xS, and z(x,t)=a for xJ. These prescriptions agree at the intersections since both relative cubes are constant on J; finite closed pasting gives continuity. The restriction HV takes values in B, and HV0=gz.

F1step 1.1
3.1

Apply [F3] to f:XY and (D,S) with target U, prescribed lift v on S and constant comparison US=fv. Obtain w:DX extending v and a homotopy Ufw rel S. The cube w is relative: w(F)A and w(J)=a. Concatenation with E gives a relative homotopy ufw fixed on J. Hence every target relative class is in the image, in degree one as well as higher degrees.

F1F3step 2.1
3.2

Use [F3] for g on the finite pair (V,V0), target HV, prescribed lift z, and constant comparison on V0. It yields v:VA extending z and a homotopy T:HVgv fixed on V0. Let R=Q=(D×{0,1})V. On R define a homotopy ER by T on V and by the stationary maps fw0,fw1 on the two end cubes. They agree on S×{0,1} because T is fixed there. Thus ER is continuous, starts at HR, fixes both end cubes, and fixes J×I at b.

F3step 2.2
4.1

Apply [F4] for (Q,R) to extend ER to a homotopy in Y starting at H:QY. Write U:QY for its endpoint. The maps w0,w1 on the two end cubes and v on V glue to a continuous zR:RX, since v extends the endpoint data z. The endpoint boundary equation is UR=fzR. Apply [F3] to f on (Q,R) with this prescribed lift and constant comparison. Obtain W:QX with WR=zR. Therefore W(,0)=w0, W(,1)=w1, W(F×I)A, and W(J×I)=a. Thus W is the required relative homotopy, proving injectivity by equality of arbitrary classes, not merely by testing the distinguished class.

F1F3F4step 1.1step 3.2
5.1

Steps 3.1 and 4.1 give bijectivity in every positive degree. By [F2] the induced map is pointed in every degree and is a homomorphism for n2, so its bijectivity makes it a group isomorphism in that range. The point a was arbitrary, and no point or path was selected for a family of basepoints.

F2step 3.1step 4.1
6.1

For n=1, F={0} and J={1}; (S,J) adds just one vertex, and (V,V0) adds the initial-endpoint interval while the terminal-endpoint interval stays constant. The constructions therefore apply literally to relative paths with their variable initial point in A. They require no group structure on relative π1. Relative degree zero is not asserted. If A is empty there is no a, and the quantified conclusion is vacuous; no source cube at a nonexistent basepoint is requested. Equal pairs, constant cubes and coincident endpoint maps cause no change. All homotopies fix the stated faces at every time, including their corners and endpoints; the finite HELP time reparametrization preserves each stationary prescribed track. All calls to [F3] have finite sources, and [F4] is choice-free. This proves the assertion without AC.

F1F3F4step 1.1step 2.1step 2.2step 3.2step 4.1step 5.1

Depends on

Used by

Dependency tree · two levels

29 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