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.
Integral homology of a finite cyclic group
Example
For , , with trivial integral coefficients, , for , and for . In particular multiplication by kills positive homology.
Facts & Assumptions
Given: m is a positive integer; coefficients are trivial integers; the derived-functor convention carries DC and supplied resolutions.
The order of a finite group annihilates its positive integral homology. (Positive integral homology is annihilated by the group order).
Group homology is the homology obtained by tensoring the supplied projective resolution with the right trivial module (Group homology as a derived functor).
Under DC, any two projective resolutions of the same object are chain-homotopy equivalent over that object (Projective resolutions of the same object are homotopy equivalent over that object).
Verification
Put and . Use one copy of R in each nonnegative degree, augmentation , differential multiplication by in odd degrees and by N in positive even degrees. Since and , this is an augmented chain complex.
For , the coefficient of in is (indices modulo m). Thus its kernel consists exactly of constant coefficient vectors, namely . Also , so the image of multiplication by N is and its kernel is . If , then . Hence , proving exactness in every degree. This also covers m=1: the two maps are zero and identity and the displayed sums are empty.
Each term is free, so step 2.1 makes this complex a projective resolution of the trivial left -module. Let be the supplied resolution used in [F2]. By [F3], and are chain-homotopy equivalent over . The additive functor carries the comparison maps and their homotopies to comparison maps and homotopies, so . Tensoring makes multiplication by zero and multiplication by N multiplication by m. Thus degree zero is , every odd degree has kernel modulo , and every positive even degree has kernel of , which is zero.
Multiplication by m on is zero, and on the zero groups it is zero. This explicitly verifies the conclusion of F1. Degree zero is excluded: in . For m=1 all positive groups vanish.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
11 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
- Weibel, An Introduction to Homological Algebra, Calculation 6.2.1, Theorem 6.2.2 and Example 6.2.3, pp.167–168 (standard reference, not scraped)