Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-generatedprecheck passaudited 2026-08-11
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 G be a finite abelian p-group and let a∈G have maximal element order. Then there is a subgroup H≤G such that G=⟨a⟩⊕H.

Facts & Assumptions

Given: The objects and hypotheses in the statement.

[L1]

Let G be a nontrivial finite abelian p-group. If G has exactly one subgroup of order p, then G is cyclic. (A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic).

[L2]

Let G be a finite abelian group and let p be a prime dividing ∣G∣. Then G contains an element, and hence a subgroup, of order p. (Cauchy's theorem for finite abelian groups).

[L3]

Let P be a property of naturals such that for every n∈N, if P(m) holds for all m<n then P(n). Then P(n) holds for all n∈N. (At n=0 the hypothesis is vacuous, so P(0) is forced.) (Strong (complete) induction).

[L4]

Let G be a group and let N⊴G be a normal subgroup (def-normal-subgroup). The quotient group, or factor group, G/N has the left cosets G/N:={gN:g∈G} as its elements (def-coset, def-index), with product (gN)(hN):=ghN. 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 G/N and coset product (gN)(hN)=ghN).

[L5]

Correspondence theorem: subgroups of G/N correspond to subgroups of G containing N, with normality preserved. For N⊴G, the maps H↦H/N and K↦π−1(K) are inverse inclusion-preserving bijections between subgroups H with N≤H≤G and subgroups K≤G/N; they preserve normality. (Correspondence theorem: subgroups of G/N correspond to subgroups of G containing N, with normality preserved).

[L6]

Let N⊴G. If [G:N] is finite, then the quotient group G/N is finite and ∣G/N∣=[G:N]. In particular, if G is finite, then ∣G/N∣=∣G∣∣N∣. (If [G:N] is finite then ∣G/N∣=[G:N]; for finite G this equals ∣G∣/∣N∣).

[L7]

Let G be a group and g∈G, with integer powers as in def-group-power. Then ⟨g⟩  =  { gn  :  n∈Z }, the cyclic subgroup generated by g (def-generated-subgroup) being exactly the set of integer powers of g. Consequently every cyclic group is abelian, and so is every cyclic subgroup of any group. (⟨g⟩={ gn:n∈Z }, and every cyclic group is abelian).

[L8]

Let G be a group and let N0,…,Nr−1 be normal subgroups, where r∈N. They form an internal direct product when they generate G and, for each i<r, Ni∩⟨Nj:j<r, j≠i⟩={e}. The empty family is an internal direct product of the trivial group. For two subgroups of an abelian group this says G=HK and H∩K={e}; in additive notation one writes G=H⊕K. 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).

[L9]

Let G be a group, g∈G, 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 ι:N→Z of lem-nat-embeds-int. Finite order. Suppose ord⁡(g)=n with n∈N, n≥1. Then: 1. for every k∈Z, gk=e if and only if k=qn for some q∈Z, that is, if and only if n∣k (thm-division-algorithm-in-z); 2. the powers g0,g1,…,gn−1 are pairwise distinct: if i,j∈N with i<n, j<n and gi=gj, then i=j; 3. ⟨g⟩={ gs:s∈N, s<n } and ⟨g⟩≈n; so ⟨g⟩ is finite with ∣⟨g⟩∣=n=ord⁡(g). Infinite order. If ord⁡(g)=∞ then for j,k∈Z, gj=gk implies j=k; so the integer powers of g are pairwise distinct and ⟨g⟩ is not finite. (If ord⁡(g)=n then gk=e iff k is an integer multiple of n, the powers g0,…,gn−1 are distinct, and ⟨g⟩ has exactly n elements; if g has infinite order then gj=gk only for j=k).

Proof

technique · induction
1.1

For induction on ∣G∣, the trivial and cyclic cases hold with the evident complement.

basegivenL1L2L3L4L5L6L7L8L9
2.1

Fix the induction hypothesis for smaller finite abelian p-groups, assume G is noncyclic, and put A=⟨a⟩.

ihstep 1.1
3.1

Write ∣A∣=pm. If ar has order p, then apr=e, so the order characterisation gives pm−1∣r; hence A has the unique order-p subgroup ⟨apm−1⟩. The preceding lemma and Cauchy's theorem therefore give an order-p subgroup B of G different from it, and A∩B={0}.

step 2.1
4.1

In G/B the image of a has the same order as a because A∩B={0}. It is still of maximal order: if y+B had order larger than pm, then (y+B)pm≠B, so ypm≠0 and y would have order larger than that of a.

step 3.1
5.1

Induction in G/B gives G/B=(A+B)/B⊕H′/B for some subgroup H′≥B. Pulling back yields G=A+H′, while A∩H′⊆A∩B={0}.

step 4.1
6.1

Thus H=H′ is the required complement. The order-p and one-factor boundaries are included in the cyclic case, completing the induction.

step 5.1discharge-induction∎

Depends on

Used by

Dependency tree · two levels

46 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