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.
Corestriction after transfer multiplies by the index
Statement
Let have finite index and M be a left G-module. For every , the composite is multiplication by . Here corestriction means the covariant inclusion map in homology; the derived identification retains DC and supplied resolutions.
Facts & Assumptions
Given: The finite-index inclusion, coefficient module, and a finite transversal T.
The transfer formula is well-defined on normalized diagonal coinvariants, is a chain map, and induces a transversal-independent homology map (Bar transfer is a chain map independent of the transversal).
For right-coset representatives , write with ; transfer is the finite sum obtained by applying to the vertices of and using coefficient (Finite-index transfer on normalized bar chains).
Proof
Put . For each define the alternating vertex prism Expanding the vertex-deletion differential cancels every face away from the switch in pairs; the two endpoint faces that survive give where uses and is the -summand of corestriction after the transfer in [F2]. If with and , then permutes , , and both vertex strings and the coefficient change by the same diagonal translation. Hence descends to -coinvariants. Equal adjacent input vertices make every prism summand degenerate, so it also descends to normalized chains. Thus
Each translated summand is in diagonal G-coinvariants. The sum is therefore times that chain in every degree, including zero. Homotopic chain maps give the same map on homology because their difference on a cycle is a boundary. Thus .
Depends on
Used by
Dependency tree · two levels
4 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
- Loh, Group Cohomology, Definitions 1.7.12–13 and Theorem 1.7.15 pp.63–64; Theorem 3.2.18 pp.129–132 (standard reference, not scraped)
- Weibel, An Introduction to Homological Algebra, Chapter 6, Sections 6.4–6.8 (standard reference, not scraped)