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.
The socle is characteristic and decomposes as a direct product of minimal normal subgroups
Statement
Let be a finite group. Then is a characteristic subgroup of . Moreover, for some integer there are pairwise distinct minimal normal subgroups such that
Here the case means the empty direct product, namely the trivial group.
Facts & Assumptions
Given: A finite group .
Distinct minimal normal subgroups of centralize one another (Distinct minimal normal subgroups centralize one another).
Every nontrivial finite characteristically simple group is a direct product of isomorphic simple groups (Finite characteristically simple groups are direct products of isomorphic simple groups).
Every minimal normal subgroup of a finite group is characteristically simple (Minimal normal subgroups of finite groups are characteristically simple).
Automorphisms of permute its minimal normal subgroups.
Proof
By [A1], the subgroup generated by all minimal normal subgroups of is stable under every automorphism of . By definition this subgroup is , so is characteristic in .
Let be a maximal family of pairwise distinct minimal normal subgroups of chosen so that none is contained in the product of the preceding ones; when , this family is empty. For , [L1] shows that centralizes , and minimality gives because the intersection is a normal subgroup of contained in but was chosen outside the preceding product. Hence is an internal direct product, with the case giving the trivial group.
The product is generated by minimal normal subgroups, so it lies in . Conversely, if is any minimal normal subgroup of not contained in , then adjoining would contradict maximality of the chosen family; therefore every minimal normal subgroup of lies in the displayed product. Thus . By [L3], each nontrivial factor is characteristically simple, and [L2] then makes it a direct product of isomorphic simple groups.
Depends on
- Characteristic subgroups
- Internal direct products of finitely many normal subgroups
- Minimal normal subgroups and the socle of a finite group
- Distinct minimal normal subgroups centralize one another
- Minimal normal subgroups of finite groups are characteristically simple
- Finite characteristically simple groups are direct products of isomorphic simple groups
Used by
- FALSE: the socle is always a single simple group False statement
Dependency tree · two levels
14 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
- James E. Humphreys, A Course in Group Theory, Corollary 16.12 and the socle discussion following it (standard reference, not scraped)
- Leonard H. Soicher, Primitive permutation groups (standard reference, not scraped)