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.
The singular chain cross product satisfies the boundary formula
Statement
For singular chains and , When , the first term is omitted; when , the second term is omitted.
Facts & Assumptions
Given: Singular chains and .
The chain cross product is the alternating shuffle sum on singular simplex generators (The singular chain cross product on generators).
The singular boundary is the alternating sum of codimension-one faces (The singular boundary operator).
Proof
By bilinearity from [L1], it is enough to prove the formula for generators and , where and are singular simplices.
If , there is one -shuffle, and the cross product is the evident product of the point simplex with . Restricting it to any face of gives the product of with the corresponding face of , so . The same argument with the factors reversed gives when . These are the stated formulas in the two boundary cases. Hence it remains to assume .
Expand with [L1] and [L2]. A face deletes a vertex of a shuffle path. If the deleted vertex is internal and its two adjacent steps have different directions, the resulting diagonal face is shared by the shuffle obtained by interchanging those two steps. The two shuffles have opposite permutation signs, while the face occurs in the same boundary position, so these internal faces cancel in pairs.
Under the remaining assumption , the uncancelled faces lie on the boundary of . For the face in , deleting the corresponding horizontal coordinate gives the shuffle chain for with boundary sign . For the face in , the horizontal directions precede the boundary sign , giving the total sign . Consequently the universal shuffle chain satisfies Postcomposing with gives
Step 3.1 extends by bilinearity to the stated formula for arbitrary integral chains and .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
4 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
- Haynes Miller, Algebraic Topology I, Lecture 7 (standard reference, not scraped)