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 maximal-order cyclic subgroup splits off a finite abelian p-group
Statement
Let be a finite abelian -group and let have maximal element order. Then there is a subgroup such that
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Let be a nontrivial finite abelian -group. If has exactly one subgroup of order , then is cyclic. (A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic).
Let be a finite abelian group and let be a prime dividing . Then contains an element, and hence a subgroup, of order . (Cauchy's theorem for finite abelian groups).
Let be a property of naturals such that for every , if holds for all then . Then holds for all . (At the hypothesis is vacuous, so is forced.) (Strong (complete) induction).
Let be a group and let be a normal subgroup (def-normal-subgroup). The quotient group, or factor group, has the left cosets as its elements (def-coset, def-index), with product Independence of the chosen representatives is proved in thm-coset-multiplication-well-defined-iff-normal, and the group axioms are proved in thm-quotient-group-laws. (The quotient group and coset product ).
Correspondence theorem: subgroups of correspond to subgroups of containing , with normality preserved. For , the maps and are inverse inclusion-preserving bijections between subgroups with and subgroups ; they preserve normality. (Correspondence theorem: subgroups of correspond to subgroups of containing , with normality preserved).
Let . If is finite, then the quotient group is finite and In particular, if is finite, then (If is finite then ; for finite this equals ).
Let be a group and , with integer powers as in def-group-power. Then the cyclic subgroup generated by (def-generated-subgroup) being exactly the set of integer powers of . Consequently every cyclic group is abelian, and so is every cyclic subgroup of any group. (, and every cyclic group is abelian).
Let be a group and let be normal subgroups, where . They form an internal direct product when they generate and, for each , The empty family is an internal direct product of the trivial group. For two subgroups of an abelian group this says and ; in additive notation one writes . Normal subgroups and generated subgroups are those of def-normal-subgroup and def-generated-subgroup, and the comparison product is def-external-direct-product-of-groups. (Internal direct products of finitely many normal subgroups).
Let be a group, , and let orders be as in def-order-in-a-group. Throughout, a natural number written where an integer is expected means its image under the embedding of lem-nat-embeds-int. Finite order. Suppose with , . Then: 1. for every , if and only if for some , that is, if and only if (thm-division-algorithm-in-z); 2. the powers are pairwise distinct: if with , and , then ; 3. and ; so is finite with . Infinite order. If then for , implies ; so the integer powers of are pairwise distinct and is not finite. (If then iff is an integer multiple of , the powers are distinct, and has exactly elements; if has infinite order then only for ).
Proof
For induction on , the trivial and cyclic cases hold with the evident complement.
Fix the induction hypothesis for smaller finite abelian -groups, assume is noncyclic, and put .
Write . If has order , then , so the order characterisation gives ; hence has the unique order- subgroup . The preceding lemma and Cauchy's theorem therefore give an order- subgroup of different from it, and .
In the image of has the same order as because . It is still of maximal order: if had order larger than , then , so and would have order larger than that of .
Induction in gives for some subgroup . Pulling back yields , while .
Thus is the required complement. The order- and one-factor boundaries are included in the cyclic case, completing the induction.
Depends on
- A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic
- Cauchy's theorem for finite abelian groups
- Strong (complete) induction
- The quotient group $G/N$ and coset product $(gN)(hN)=ghN$
- Correspondence theorem: subgroups of $G/N$ correspond to subgroups of $G$ containing $N$, with normality preserved
- If $[G:N]$ is finite then $|G/N|=[G:N]$; for finite $G$ this equals $|G|/|N|$
- $\langle g \rangle = \{\, g^{n} : n \in \mathbb{Z} \,\}$, and every cyclic group is abelian
- Internal direct products of finitely many normal subgroups
- If $\operatorname{ord}(g) = n$ then $g^{k} = e$ iff $k$ is an integer multiple of $n$, the powers $g^{0}, \dots, g^{n-1}$ are distinct, and $\langle g \rangle$ has exactly $n$ elements; if $g$ has infinite order then $g^{j} = g^{k}$ only for $j = k$
Used by
Dependency tree · next 3 levels
Direct dependencies and their dependencies through the next three levels: 99 results over 22 levels. An arrow runs from a result to what uses it, and this result sits at the bottom with a heavier outline. Click the chart to enlarge it.
Sources
- Keith Conrad, Decomposition of Finite Abelian Groups, §§1-4 (standard reference, not scraped)
- Richard Elman, Lectures on Abstract Algebra, Ch. 14 (standard reference, not scraped)