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 naturality and projection formula
Statement
For continuous , and , For , and , Here is commutative unital and cap evaluates the front face, retaining the back face. Both identities hold already on cochains and chains. No AC is needed.
Facts & Assumptions
Cap product boundary identity proves that the front-evaluation/back-retention cap descends to cohomology and homology, including zero output degrees.
Singular cup product on cochains supplies the front/back evaluation formula. Cup product is natural, unital and associative supplies its descent to cohomology together with naturality, the unit, and associativity.
Proof
Given: Cochain representatives of degrees and a singular -simplex . For the first identity is on ; for the second both are on .
If , the left side of the first chain identity is , equal to . This is exactly , since postcomposition commutes with face restriction. If , both sides are zero. Linearity gives the chain identity for every chain.
If , evaluating the left side of the second identity yields . Capping first by leaves the chain ; capping by gives the same scalar and back face by -linearity. If , the inner cap on the right is zero; if , its remaining degree is less than , so the outer cap is zero. In both cases the left side also vanishes. Thus the equality holds on every simplex and extends bilinearly.
For cocycles and cycles, [F1] and [F2] make every operation in steps 1.1–1.2 well-defined on the corresponding quotient classes. Passing the chain identities to classes proves the formulas. The case is initial-vertex multiplication; the case retains the last vertex with no sign, and zero degrees in either factor need no alteration. Empty spaces, zero inputs/ring, point spaces and degenerate simplices use the same formulas. All maps and products are explicit, without AC.
Depends on
Used by
- Fundamental classes and duality for spheres and tori Example
- Cap duality for open subsets of Euclidean space Lemma
- Cap duality on a Euclidean coordinate ball Lemma
- Cap product and the Mayer–Vietoris duality ladder Lemma
- Duality extends to finite unions of coordinate balls Lemma
- Fully relative Poincaré–Lefschetz duality Theorem
Dependency tree · two levels
12 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 cap formula (20); Miller Proposition 34.1 (standard reference, not scraped)