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 glue along a common connected CW subcomplex
Statement
Let be a CW complex decomposed into subcomplexes with intersection . Suppose is path-connected and are -connected. Let be CW complexes containing the same CW subcomplex , and let , be weak homotopy equivalences equal to the identity on .
Then the ordinary amalgamated union is a CW complex and the glued map is a weak homotopy equivalence. This assertion uses no choice principle. No global homotopy inverses or global cellular approximations of are assumed.
Facts & Assumptions
Weak homotopy equivalence gives component bijectivity and all-basepoint isomorphisms. Connectivity of a CW pair says that -connectedness means that every ambient component meets the subspace.
Cellular attachments with finite boundary support form a CW complex constructs a CW union by attaching one side's supplied relative cells to the other and gives its final map-out topology.
Compact CW images have finite cell support without choice gives finite CW support for each compact image. 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 cubes, disks and characteristic disk cylinders.
Finite relative homotopy lifting across a weak equivalence lifts maps on a CW pair with finitely many relative cells, using a supplied boundary homotopy; the lift extends the boundary map exactly and constant boundary tracks stay constant. No choice is used.
Cellular approximation for maps of CW pairs applies choice-free to a source with finitely many cells outside its fixed cellular subcomplex.
Cellular mapping cylinders and relative cylinders are CW complexes proves the CW structure and endpoint embeddings for the relative cylinder of a cellular map fixed on . It identifies the cells outside the source endpoint as the target cells outside and one prism cell for every source cell outside ; finiteness follows only when both of those cell sets are finite.
Higher homotopy basepoint transport and moving homotopies gives transport isomorphisms; its radial-shell formula commutes with postcomposition. Higher homotopy group by based cubes supplies based cubes and based nullhomotopies.
Proof
Given: All spaces and maps in the statement. Choose one point ; this is one existential instantiation, not a family of choices.
Build from by adjoining the vertices and then the positive-dimensional cells of using their supplied boundaries. The boundaries have finite support and are cellular, so [F2] proves that the result is CW with both sides as subcomplexes. Its underlying set identifies exactly the common , and its map-out test is continuity on the two endpoint spaces agreeing on , hence is the ordinary amalgamated topology. The maps therefore glue continuously to . The spaces are path-connected: each point is joined to a point of by [F1], and points of are mutually joined. Since induce component bijections, are also path-connected. Thus and are path-connected, and is automatically bijective on components.
Let and let be a based cube. By [F3], its image lies in a finite subcomplex of . Put , , . These are subcomplexes, , and each has finitely many cells outside . Apply [F4] to , the source pair , the inclusion , the identity and the constant homotopy on . It gives equal to the identity on and a homotopy from the inclusion to rel . Do the same on the side. The two maps and homotopies agree on and glue continuously on : the sides are closed subcomplexes, and their cylinder products form a finite closed cover of . This gives and a homotopy fixed on . Composing with proves that . Therefore is surjective.
For injectivity, let have a based nullhomotopy after composing with . By [F3] put the image of in a finite source subcomplex , and set , , . Each is finite relative to . Apply [F5] separately to and , fixing , where both maps are already the cellular identity. Obtain cellular and homotopies , rel . They glue to a cellular map and a homotopy rel . These are two applications of finite-relative cellular approximation; no approximation of either whole or is selected.
There is a finite-relative target subcomplex containing the image of and all of . Indeed has compact cube domain. On each of the finitely many characteristic cells of , the composite of with its characteristic disk cylinder has compact domain by [F3], so its image lies in a finite target subcomplex. A finite union of these finite subcomplexes, together with one for , is a finite subcomplex . The remaining part is just . This also includes the endpoints . Set , . Then and are cellular maps of CW complexes fixed on ; corestriction is continuous because these are subspaces. The reversed homotopy followed by is a based nullhomotopy of wholly in .
Form the relative cylinder of fixed on , using [F6]. It has top inclusion , target inclusion , and retraction with . The cell description splits it into subcomplexes with intersection : use the target cells of and the top and prism cells of for , and the corresponding cells for . Their characteristic boundaries stay on their indicated side because do. Each is the relative cylinder of that side's map. In particular and are CW pairs with finitely many relative cells: by [F6] those relative cells are exactly the target cells of or and the prism cells over or , respectively, and all four sets are finite by steps 2.2–3.1. The possibly infinite common introduces no new relative cells.
Apply [F4] to with source pair . Its target map is and its prescribed lift on is . On that subcomplex , so the reversed homotopy is exactly the required homotopy from to of the prescribed lift. Thus [F4] gives a continuous extending the inclusion of exactly. Apply the identical argument on the side. Both maps equal the identity on , so closed pasting gives a continuous with . No global inverse of a weak equivalence has been invoked.
The cylinder height homotopy in [F6] joins to while fixing the cubical boundary at , since has its whole cylinder track collapsed. Step 3.1 supplies a based nullhomotopy of in , hence of in . Concatenation proves that is based null in . Composing with from step 5.1 gives a based nullhomotopy of in . Therefore the homomorphism at has trivial kernel. Together with step 2.1 it is an isomorphism in every positive degree, including degree one without an abelian assumption.
For arbitrary , path-connectedness in step 1.1 supplies one path from to . The transport square for this path and its image under commutes by the representative formula in [F7]. Since the map at is an isomorphism by step 6.1, the map at is an isomorphism as well. Combining with component bijectivity from step 1.1 proves weak equivalence [F1]. Only a path for the one point currently under consideration is used.
Nonempty is required to supply and the single-component reduction; empty is outside this statement. A side equal to and empty relative cell sets cause no change in the constructions or finite lifting arguments. All degrees are positive in the group calculation, and components were treated separately. Constant cubes and repeated cell-boundary identifications retain their prescribed values because every construction fixes and every lift extends its specified source subcomplex exactly. The nullhomotopy in step 6.1 fixes the basepoint even when is not a vertex. The only witness families taken together in steps 2.1–5.1 are finite, or are given data on the common ; each cellular approximation and lifting has finitely many relative source cells. This proves the claim without AC.
Depends on
- Weak homotopy equivalence
- Connectivity of a CW pair
- Cellular attachments with finite boundary support form a CW complex
- Compact CW images have finite cell support without choice
- 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
- Finite relative homotopy lifting across a weak equivalence
- Cellular approximation for maps of CW pairs
- Cellular mapping cylinders and relative cylinders are CW complexes
- Higher homotopy basepoint transport and moving homotopies
- Higher homotopy group by based cubes
Used by
- Homotopy excision Theorem
Dependency tree · two levels
66 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, Chapter11 §3 p87, weak CW-triad reduction; Chapter10 §3 p75 HELP; finite-data proof supplied locally (standard reference, not scraped)