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.
A normal p-subgroup acts trivially on every simple module in characteristic p
Statement
Let be a normal -subgroup and let be a simple -module, where has characteristic . Then every element of acts trivially on .
Facts & Assumptions
Given: A finite group , a normal -subgroup , and a simple -module .
For every characteristic- field, the group algebra of a finite -group is local (For a finite group and a field of characteristic p, the group algebra is local exactly when the group is a p-group).
A simple module has no proper nonzero submodule (Simple module: a nonzero module with no proper nonzero submodule).
Finite-dimensional modules have finite length (A module has a composition series if and only if it is Noetherian and Artinian, the converse using dependent choice).
Proof
Restrict from to the normal subgroup . By [L2], the restricted module has finite length, so it contains a minimal nonzero -submodule . Then is simple as an -module by [F1].
Since is a finite -group, [L1] makes local. Its augmentation quotient is the trivial simple module , and every simple module over a local finite-dimensional algebra is its unique simple quotient. Hence is the trivial -module. Therefore the fixed-point space contains and is nonzero. Because is normal in , the subspace is -stable: for , , and , one has .
The nonzero -stable submodule must equal by simplicity of . Hence every element of acts trivially on every vector of .
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
16 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 (23 Feb 2016 draft) (standard reference, not scraped)