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.
Cap product with cohomology written first
Definition
Let be a space and a commutative unital ring. For , , and a singular -simplex , define Extend -bilinearly in and the finite chains of Singular simplices and singular chain groups with coefficients. An -linear cochain is a function on simplex generators; each value multiplies one specified back-face generator. Thus the formula is well-defined on finite formal chains and is -balanced in its two inputs. It gives with negative chain groups zero. This is the cap product with cohomology first: evaluate on the front face and retain the back face.
The face convention is the same as Singular cup product on cochains. In terms of its Alexander–Whitney diagonal , cap is the bidegree- part of , followed by evaluation of the first factor by . There is no additional sign in this evaluation. Subsequent boundary and projection identities use this order.
For , this multiplies a simplex by the value of at its first vertex; in particular the constant value-one cochain acts as the identity on chains. For , it returns times the last vertex, a degree-zero chain, whose boundary is zero. For it is zero by definition. On a degenerate simplex the same face formula applies; unnormalized chains retain these generators. Empty , zero inputs and the zero ring give zero maps. The construction also applies to the higher singular simplices of a point and requires no AC.
Depends on
Used by
- Poincaré duality gives a nonsingular cup pairing Corollary
- Cap product on the oriented circle Example
- Fundamental classes and duality for spheres and tori Example
- Finite generation from cap with a finite fundamental cycle Lemma
- Manifold degree is functorial and detected in top cohomology Proposition
- Cap product boundary identity Theorem
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 §3.3, Cap Product; Miller Lecture 34 (standard reference, not scraped)