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.
Factor reversal gives the commutativity chain homotopy
Statement
Let be a space and a commutative unital ring. Put and let . On homogeneous tensors put Then and are naturally chain homotopic. In particular and , with , are naturally chain homotopic. No AC is required.
Facts & Assumptions
Alexander--Whitney and shuffle are natural chain-homotopy inverses provides natural maps and specified natural homotopies for and , over .
The singular chain cross product on generators expresses as the signed sum of monotone lattice paths.
Proof
Given: The signed tensor differential . Take the supplied homotopies and .
The coefficients of and in are respectively and . In they are and , respectively. Each corresponding pair agrees modulo two, so . Also . Terms involving or in degree zero are absent, so the calculation includes and .
A shuffle path has horizontal and vertical steps. Its permutation sign is , where counts vertical steps occurring before horizontal steps. Interchanging the two types of steps replaces by , since each horizontal/vertical pair contributes to exactly one of the counts. It therefore changes the sign by . The affine simplex of the swapped path is the original one followed by factor interchange. Matching paths bijectively in the finite shuffle sums gives . This is a signed-shuffle calculation, not merely naturality for maps of the two factors.
Put and . These are natural (with simultaneous maps of ), and step 1.2 gives . Thus The map is a chain map by step 1.1, [F1], and the fact that postcomposition commutes with face boundary. Define . Using the two supplied homotopy equations yields This is an explicitly specified natural homotopy.
Since , precomposing step 2.1 with the chain map gives In degree zero the twists have sign and the maps agree on vertices. If is empty or , all maps have zero complexes as domain and codomain. Degenerate singular simplices and one-point spaces use the same shuffle paths and homotopies; nothing was normalized away. The construction uses finite signed sums and the supplied homotopies, not a selection of new fillers, so it is choice-free.
Depends on
Used by
Dependency tree · two levels
10 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 proof of Theorem 3.11; Miller Lecture 29 (standard reference, not scraped)