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 operations are well defined in their valid degrees
Statement
Relative is a group for and abelian for . Restriction to defines a pointed map , a homomorphism for ; for n=1 it records the component of the initial endpoint. Maps and homotopies of based pairs act functorially. No group structure on relative is asserted.
Facts & Assumptions
Relative representatives keep all faces except the last-coordinate-zero face constant. Relative homotopy classes and groups
Closed pasting works in each coordinate whose opposite faces are fixed. Cubical concatenation is well defined on higher homotopy classes
Endpoint-fixed coordinate homotopies give group laws, and two coordinates give interchange. Higher homotopy classes form groups and are abelian above degree one
Proof
Given: The spaces, maps, and hypotheses in the statement above.
For n≥2, concatenate and reverse in coordinate 1. Its two faces are part of J; hence F2 makes the product and pasted representative homotopies continuous. The reparametrizations and reversal contractions in F3 act only on coordinate 1. Every J-face remains at x0, and the last-coordinate-zero face continues to map into A. Thus those same explicit homotopies prove associativity, unit and inverses in the relative set.
If n≥3, coordinates 1 and 2 are both available without changing the distinguished coordinate. The four-quarter identity and the two-unit calculation of F3 therefore apply to relative classes, proving commutativity. If n=2 only one coordinate is available, and if n=1 none is; the argument makes no stronger claim in those degrees.
Restriction to F sends a relative homotopy to a boundary-fixed homotopy in A, since . For n≥2 it commutes pointwise with coordinate-1 concatenation, so . For n=1 a relative homotopy moves the initial endpoint along a path in A, so its component is well-defined. Constant representatives map to the distinguished element in every degree.
For a map of based pairs , composing a representative or its homotopy with φ preserves all triple conditions. Composition and identity act pointwise, and composition commutes with products and with restriction to F. A based pair homotopy gives the representative homotopy ; it sends F into B and J to y0. This proves all functoriality and homotopy assertions.
Depends on
Used by
Dependency tree · two levels
9 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)