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 be a continuous map of pairs, with subspace topologies on . Suppose both and are weak homotopy equivalences. For every , the induced map is a pointed bijection for and a group isomorphism for every . The spaces need not be CW complexes. No choice principle is required.
Facts & Assumptions
Weak homotopy equivalence specifies all-basepoint weak equivalence. Relative homotopy classes and groups uses , distinguished face and union of the other faces; a relative cube sends into the subspace and to the basepoint.
Relative homotopy operations are well defined in their valid degrees proves functoriality for based pair maps and that postcomposition preserves products in degrees .
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.
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 , write , and fix . Put and .
All source pairs below are finite CW pairs. Give each interval its two vertices and open edge, and each cube its product faces: a -face has closure a closed -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 , , and the cylinder face pairs used below meet [F3, F4]. This verification concerns only finite cubes, not products of arbitrary CW spaces.
To prove surjectivity let represent a relative class, so and . Apply [F3] to , the source pair , target map and prescribed constant lift on , with constant comparison there. Obtain with and a homotopy in fixed on . Apply [F4] to extend , viewed in , to a homotopy starting at . It remains fixed on and sends into at every time, because those are its prescribed boundary values. Its endpoint satisfies .
To prove injectivity, take relative cubes and a relative homotopy from to . Write , , and On prescribe a map by , for , and for . These prescriptions agree at the intersections since both relative cubes are constant on ; finite closed pasting gives continuity. The restriction takes values in , and .
Apply [F3] to and with target , prescribed lift on and constant comparison . Obtain extending and a homotopy rel . The cube is relative: and . Concatenation with gives a relative homotopy fixed on . Hence every target relative class is in the image, in degree one as well as higher degrees.
Use [F3] for on the finite pair , target , prescribed lift , and constant comparison on . It yields extending and a homotopy fixed on . Let On define a homotopy by on and by the stationary maps on the two end cubes. They agree on because is fixed there. Thus is continuous, starts at , fixes both end cubes, and fixes at .
Apply [F4] for to extend to a homotopy in starting at . Write for its endpoint. The maps on the two end cubes and on glue to a continuous , since extends the endpoint data . The endpoint boundary equation is . Apply [F3] to on with this prescribed lift and constant comparison. Obtain with . Therefore , , , and . Thus is the required relative homotopy, proving injectivity by equality of arbitrary classes, not merely by testing the distinguished class.
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 , so its bijectivity makes it a group isomorphism in that range. The point was arbitrary, and no point or path was selected for a family of basepoints.
For , and ; adds just one vertex, and 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 . They require no group structure on relative . Relative degree zero is not asserted. If is empty there is no , 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.
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
- May, A Concise Course, Chapter10 §3 pp75–76, HELP and its cylinder proof of injectivity; relative cubical version proved here (standard reference, not scraped)