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.
Higher homotopy group by based cubes
Definition
Let , , and . Write for the points with at least one coordinate 0 or 1. The set consists of continuous with , modulo homotopies fixed on that entire boundary. This is a quotient by an equivalence relation by Homotopy relative to a fixed subspace, and path homotopy relative to endpoints, are equivalence relations.
The proposed product traverses first in coordinate 1: Here , absent when . The constant map is denoted and reversal is . The following lemmas establish well-definedness and the group laws. For this is the convention of Based loops and the fundamental group. Separately, is the set of path components pointed by the component of ; no group law on it is asserted.
Depends on
Used by
- A weakly contractible CW complex is contractible Corollary
- Eilenberg--Mac Lane space Definition
- Fibration connecting map Definition
- Relative homotopy classes and groups Definition
- Stable homotopy groups of a sequential prespectrum Definition
- Weak homotopy equivalence Definition
- Based and free homotopy classes of maps between spheres agree Lemma
- Cubical concatenation is well defined on higher homotopy classes Lemma
- Cubical pinch is additive on relative homology Lemma
- High relative cells do not change lower homotopy Lemma
- Standard and reflected two-sphere immersions have homotopic formal data in ℝ³ Lemma
- Stiefel manifolds are connected in positive codimension and simply connected in codimension at least two Lemma
- The basepoint evaluation of the Stiefel section space is a fibration Lemma
- The quaternion double cover generates the third homotopy group of SO(3) Lemma
- The second homotopy group of SO(3) vanishes Lemma
- Weak equivalences glue along a common connected CW subcomplex Lemma
- Cubical and spherical models of higher homotopy agree Proposition
- Higher homotopy basepoint transport and moving homotopies Proposition
- The sphere immersion groups are algebraic-topology computations, not differential-topology constructions Remark
- All standard Aᵢⱼ generate PBₙ Theorem
- The Pontryagin-Thom correspondence in fixed codimension Theorem
- The stable Pontryagin-Thom theorem identifies framed bordism with stable stems Theorem
Dependency tree · two levels
11 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
- Hatcher, Algebraic Topology, Chapter 4 (standard reference, not scraped)