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.
Singular cochain complex with coefficients
Definition
Let be any topological space and an abelian group. Its singular cochains with coefficients in are where the chains are those of The singular chain complex and singular homology. Addition and negatives of homomorphisms are pointwise. The coboundary is for , and is zero for . Composition with the homomorphism is additive, so this is a homomorphism. The sign convention is positive: there is no extra degree sign on this composite. On a singular -simplex it says where denotes the affine face map, distinct from the superscripted coboundary. In particular on an oriented path is its endpoint value minus its initial value.
By Singular simplices and singular chain groups with coefficients, the integer chains are finite sums on the specified simplex set . Thus a cochain is equivalently an arbitrary function : the extension sends to . The sum is finite and the formal coefficients are unique. The cochain need not have finite support.
For a commutative unital ring and an -module , there is a canonical identification Indeed the given chain convention is . A homomorphism on integer chains defines an -linear map by ; the defining additive and integer-balanced tensor relations are preserved. Conversely evaluate an -linear map on . These operations are inverse since , and they intertwine the two coboundaries because the coefficient boundary is . The construction also covers the zero ring with its unital zero module.
The resulting graded group and coboundary are called the singular cochain complex. The square-zero identity follows by precomposition with in the chain complex and is spelled out in the next lemma. If is empty there are no singular simplices, so every cochain group is zero; if the same is true. The extension and tensor formulas are uniquely specified and require no AC.