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.
Constant coefficients miss monodromy
Statement
The rank-one integral local system on with monodromy has and , whereas the constant integral system has . Thus replacing a nontrivial local system by its abstract stalk as a constant coefficient group does not compute its homology.
Facts & Assumptions
Given: The two integral local systems on , with monodromy and .
Cellular chains compute local homology computes local homology from the lifted cellular incidence matrix.
Proof
Give one vertex and one oriented edge. If denotes the positive loop, a lift of the edge has boundary . Under the published right-chain convention this is , while the corresponding left fiber action of is the specified monodromy . Thus [F1] gives the two-term complex . For , its differential is , with zero kernel and cokernel . For , its differential is zero, so both degree-one and degree-zero groups are .
The two systems have isomorphic stalk at every point but different loop transport and different homology. Hence stalk data without monodromy cannot replace a local system. The sign of the differential could be after reversing the chosen cell, with the same kernel and cokernel. No other degrees occur and no AC is used.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
5 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, Algebraic Topology, §3.H, Exercise 1, p.336 (standard reference, not scraped)