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.
Induction is left adjoint to restriction for finite-group modules over a commutative ring
Statement
Let be a commutative ring, let be a finite group, let , let be an -linear -module, and let be an -linear -module. Then there is a natural isomorphism
Facts & Assumptions
Given: A commutative ring , a finite group , a subgroup , an -linear -module , and an -linear -module .
The induced module consists of the functions satisfying , with acting by (The induced -linear -module as -covariant functions on ).
For modules, is an abelian group under pointwise addition, with maps induced by composition (The abelian group and maps induced by pre- and postcomposition).
-equivariant maps are exactly the -module maps, and likewise for (For a commutative ring , -linear -actions are exactly the compatible left -module structures).
Proof
For , define by for and for . If , then for every , so ; if , then . Thus .
Choose a left transversal for with . If is -equivariant, define . The sum is finite because is finite.
If is -equivariant, define . For , one has by the action formula in [F1], so . Hence .
The map is -equivariant. Indeed, for and each , write with and . Then , using the covariance from [F1] and the -equivariance of . Reindexing the finite sum by shows .
For , because for and . Hence .
For and , one has . The function inside equals , because at a point it takes the value by covariance. So .
Steps 3.1 and 3.2 show that and are inverse group isomorphisms, giving the stated adjunction. Via [F3], this is equally the usual -module adjunction.
Depends on
Used by
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
- Peter Webb, A Course in Finite Group Representation Theory, Lemma 4.3.7 (standard reference, not scraped)
- Pavel Etingof et al., Introduction to Representation Theory, Theorem 4.33 (standard reference, not scraped)