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 Fundamental Theorem of Finite Abelian Groups
1 · Prerequisites
- Binary Operations, Monoids, Groups and Subgroups
- Congruences, the Integers Modulo n and the Chinese Remainder Theorem
- Construction of the Natural Numbers
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Cosets, Index and Lagrange's Theorem
- Countability and Uncountability
- Cyclic Groups and Direct Products
- Divisibility, Greatest Common Divisors and Bézout's Identity
- Finite Counting, Factorials and Binomial Coefficients
- Foundations of the Real Numbers for Analysis
- Group Homomorphisms and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Primes, Euclid's Lemma and the Fundamental Theorem of Arithmetic
- Relations, Functions, and Quotients
- Roots, Rational Powers, and Classical Inequalities
- The ZFC Axioms and the Basic Set Constructions
2 · Summary
Finite abelian groups inherit the cyclic-group classification, Lagrange's theorem, quotient groups, and external direct products from the declared cyclic-groups development. These results supply element orders, subgroup orders, cyclic prime-power factors, and product cardinalities. Internal direct products and -primary components then provide the language for separating a finite abelian group into coprime parts.
Cauchy's theorem identifies order- elements, primary components give the canonical prime-power decomposition, and a maximal-order cyclic subgroup splits from each finite abelian -group. Induction yields the elementary-divisor form. Successive -multiple quotients prove uniqueness, and Chinese-remainder regrouping yields invariant factors. The classification then gives subgroup-order existence, exponent and cyclicity criteria, indecomposable factors, partition counts, and the squarefree-order criterion.
3 · Logical flowchart
4 · Definitions, theorems and proofs
Internal direct products of finitely many normal subgroups
Definition
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 Normal subgroup: invariance under conjugation and The subgroup generated by a subset, the cyclic subgroup , and cyclic groups, and the comparison product is The external direct product with componentwise multiplication.
Internal direct products are external direct products, equivalently every element has a unique factorisation
Statement
Let . The following are equivalent: the form an internal direct product of ; every has a unique expression with ; and the multiplication map is an isomorphism. These statements include the empty family and the one-factor case.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
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).
For groups and , the componentwise operation of def-external-direct-product-of-groups makes a group. Its identity is , and Moreover the coordinate maps and are group homomorphisms. ( is a group with identity , coordinatewise inverses, and homomorphic coordinate projections).
Let and be monoids (def-semigroup-and-monoid). A monoid homomorphism from to is a function such that - (H1) for all ; - (H2) . Let and be groups (def-group). A group homomorphism from to is a function satisfying (H1) alone: Condition (H2) is not imposed for groups because it follows: a group homomorphism automatically satisfies and (lem-group-homomorphism-basic-properties). For monoids it does not follow and must be assumed, which is why the two definitions differ. A homomorphism from a structure to itself is an endomorphism. The identity map of is a monoid homomorphism, and a composite of monoid homomorphisms is one, since and ; the same computation, without the second clause, shows a composite of group homomorphisms is a group homomorphism. (Monoid homomorphism and group homomorphism).
A group homomorphism is injective if and only if its kernel is trivial. For a group homomorphism , is injective exactly when . (A group homomorphism is injective if and only if its kernel is trivial).
If and , then is a subgroup and . Here . (If and , then is a subgroup and ).
Proof
The internal intersection condition gives for . Unique factorisation gives the same conclusion, since an element of has expressions supported in either coordinate. In either case normality puts inside , so distinct factors commute and the multiplication map is a homomorphism.
Conversely, suppose that is an isomorphism. Coordinate subgroups in the external product commute, so their images commute, and surjectivity says that the factors generate . If , the commuting factors express as an ordered product of elements from the other . The tuple supported at and this tuple supported away from have the same image, so injectivity gives . Hence the factors form an internal direct product.
Under the internal-product condition, the image of is the subgroup generated by the factors, hence is all of . If , then each is the inverse of a product of the other factors and so lies in ; therefore every . Thus is an isomorphism.
Under unique factorisation, every element has exactly one preimage under the homomorphism . Thus is bijective and hence is an isomorphism.
For the empty family, each condition says that is trivial. For one factor, each says that , and the multiplication map is then the identity after identifying the one-fold product with .
The p-primary component of an abelian group
Definition
Let be an abelian group and a prime. Its -primary component is Thus the identity is included by . In additive notation, . Powers and element orders use Powers : natural exponents in a monoid and integer exponents in a group, with and The order of a finite group and the order of an element, with when no positive power of is the identity. No finiteness or maximality is part of the definition.
Cauchy's theorem for finite abelian groups
Statement
Let be a finite abelian group and let be a prime dividing . Then contains an element, and hence a subgroup, of order .
Facts & Assumptions
Given: The objects and hypotheses in the statement.
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 finite group and . Then Consequently, under the canonical embedding , divides . (Lagrange's theorem: for every subgroup of a finite group ).
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 ).
If is abelian and , then is abelian. (Every quotient group of an abelian group is abelian).
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 ).
Let be a finite group such that the positive integer is prime. Then every has order , satisfies , and hence generates . In particular, is cyclic. (A finite group of prime order is cyclic and every nonidentity element generates it).
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 ).
If is cyclic, then exactly one of the following applies: - if has infinite order, ; - if has finite order , necessarily , then . (Every cyclic group is isomorphic to or to for its finite order ).
Proof
For strong induction on , the trivial group has no relevant prime divisor, and if then is cyclic of order .
Fix the induction hypothesis for every finite abelian group of order smaller than . Choose . If , cyclic-group classification supplies of order . Otherwise put , a nontrivial proper subgroup.
If , the induction hypothesis in gives an element of order . If , then and the induction hypothesis in the smaller finite abelian quotient gives a coset of order .
In the latter case . Let be the order of ; then and . Since the coset of has order , the order of is , so has order .
Every branch supplies an element of order , completing the strong induction.
A p-primary component has the full p-power order and is the unique subgroup of that order
Statement
Let be finite abelian and write with . Then is a subgroup of order . It is the unique subgroup of having that order. In particular, if , then .
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Let be an abelian group and a prime. Its -primary component is Thus the identity is included by . In additive notation, . Powers and element orders use def-group-power and def-order-in-a-group. No finiteness or maximality is part of the definition. (The p-primary component of an abelian group).
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 finite group and . Then Consequently, under the canonical embedding , divides . (Lagrange's theorem: for every subgroup of a finite group ).
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 ).
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).
Second isomorphism theorem for groups: . If and , then (Second isomorphism theorem for groups: ).
If is abelian and , then is abelian. (Every quotient group of an abelian group is abelian).
Let be a group (def-group) with identity , let , and let powers be as in def-group-power. For all : 1. ; 2. ; 3. ; 4. : any two powers of one element commute; 5. if then . Claim 5 is false in general without its hypothesis: in a group in which and do not commute the equation can fail already at , and a witness is recorded on the companion page. Claims 1 and 3 hold in any monoid (def-semigroup-and-monoid) for exponents in , and so does claim 5 for exponents in under the same commuting hypothesis; only the extension to negative exponents needs inverses. (Exponent laws in a group: and for all , and when and commute).
Proof
If and , commutativity and the power laws give and , so is a subgroup. If a prime divides , Cauchy's theorem in gives an element of order ; the definition of forces . Hence for some .
If , then divides . Cauchy's theorem in this abelian quotient gives a nonidentity coset of order .
Then , so for some and therefore , contradicting the choice of a nonidentity coset. Hence .
If has order , Lagrange applied inside makes every have -power order, so ; equal finite orders give . The case gives the trivial subgroup.
A finite abelian group is the internal direct product of its primary components
Statement
If is finite abelian and is its prime factorisation, then the subgroups form an internal direct product of . Thus For the trivial group, this is the empty product.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Let be finite abelian and write with . Then is a subgroup of order . It is the unique subgroup of having that order. In particular, if , then . (A p-primary component has the full p-power order and is the unique subgroup of that order).
Let . The following are equivalent: the form an internal direct product of ; every has a unique expression with ; and the multiplication map is an isomorphism. These statements include the empty family and the one-factor case. (Internal direct products are external direct products, equivalently every element has a unique factorisation).
Powers are the natural powers of def-group-power and finite products those of def-monoid-finite-product, both taken in the commutative monoid of lem-units-of-z. Call an injective list of primes when every is prime (def-prime) and forces (def-injection-surjection-bijection). Let with and let be an injective list of primes such that every prime divisor of equals for some . Then, with as in def-p-adic-valuation: 1. ; 2. for every prime that is not among ; 3. the exponents are determined by : if and , then for every . Clause 3 needs only injectivity of the list, not the covering hypothesis. (For and any injective list of primes containing every prime divisor of , one has ; the exponents are determined by , and for every prime outside the list).
Let , not both , and put Then contains a positive element, and its least positive element is (def-common-divisor-and-gcd). In particular there are integers with so the equation is solvable in . (Bézout's identity: for integers not both zero, is the least positive element of ; in particular has an integer solution).
If and are finite groups, then their external direct product is finite and has order . (For finite groups and , ).
Let be a finite group and . Then Consequently, under the canonical embedding , divides . (Lagrange's theorem: for every subgroup of a finite group ).
Proof
Each has order , and the product of these orders is . Distinct primary components have trivial intersection because an element in both has order dividing powers of two distinct primes.
Multiplication from the external product of the primary components to is injective: a tuple in its kernel would place each component in the intersection with the product of the others, whose order is both a power of and coprime to .
The external product has order . Its injective multiplication map therefore has image of order and is surjective.
The internal-direct-product recognition theorem gives the displayed isomorphism. When is trivial the prime list is empty and both sides are the trivial group.
A nontrivial finite abelian p-group with a unique subgroup of order p is cyclic
Statement
Let be a nontrivial finite abelian -group. If has exactly one subgroup of order , then is cyclic.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
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 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 ).
If is abelian and , then is abelian. (Every quotient group of an abelian group is abelian).
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 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
Assume for contradiction that is not cyclic. Choose of maximal order and put , which is then proper.
Cauchy's theorem in gives of order . Thus in additive notation for some integer , while .
Maximality gives , so . Since has order , the integer is divisible by , say .
Then is nonzero, lies outside , and satisfies . Its order- subgroup differs from the unique order- subgroup inside , contradicting the hypothesis. Therefore is cyclic.
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.
Every finite abelian p-group is a direct product of cyclic p-groups
Statement
Every finite abelian -group is isomorphic to a finite direct product of cyclic groups of prime-power order. The trivial -group is the empty product.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Let be a finite abelian -group and let have maximal element order. Then there is a subgroup such that (A maximal-order cyclic subgroup splits off a finite abelian p-group).
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 . The following are equivalent: the form an internal direct product of ; every has a unique expression with ; and the multiplication map is an isomorphism. These statements include the empty family and the one-factor case. (Internal direct products are external direct products, equivalently every element has a unique factorisation).
If is cyclic, then exactly one of the following applies: - if has infinite order, ; - if has finite order , necessarily , then . (Every cyclic group is isomorphic to or to for its finite order ).
Proof
For induction on , the trivial group gives the empty product.
Fix the induction hypothesis for smaller finite abelian -groups. If is nontrivial, choose of maximal order and split .
The cyclic factor has prime-power order. If is nontrivial then , so the induction hypothesis decomposes into cyclic -groups.
Concatenating that decomposition with and applying internal-product recognition gives the asserted external direct product, completing the induction.
Elementary-divisor data for a finite abelian group
Definition
An elementary-divisor decomposition of a finite abelian group is an isomorphism where every is a prime power. The unordered multiset of the , counted with multiplicity, is the elementary-divisor data. The cyclic factors and product use Every cyclic group is isomorphic to or to for its finite order and The external direct product with componentwise multiplication. The data records factor isomorphism types, not distinguished internal subgroups; the trivial group has empty data.
The successive quotients p^iG/p^{i+1}G recover the cyclic summand multiplicities of a finite abelian p-group
Statement
Suppose with , and in additive notation write . Define by . Then Consequently, for every , the number of summands of order is , so the elementary divisors are intrinsic. The restriction to is the whole content of the hypothesis : no summand has order , and is not defined.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
An elementary-divisor decomposition of a finite abelian group is an isomorphism where every is a prime power. The unordered multiset of the , counted with multiplicity, is the elementary-divisor data. The cyclic factors and product use thm-classification-of-cyclic-groups and def-external-direct-product-of-groups. The data records factor isomorphism types, not distinguished internal subgroups; the trivial group has empty data. (Elementary-divisor data for a finite abelian group).
Every finite abelian -group is isomorphic to a finite direct product of cyclic groups of prime-power order. The trivial -group is the empty product. (Every finite abelian p-group is a direct product of cyclic p-groups).
Natural exponents, in a monoid. Let be a monoid (def-semigroup-and-monoid) and . By the recursion theorem (thm-recursion), applied with the set , the element and the function from to , there is exactly one function , written , with In particular for every , including , and . Since contains (def-natural-numbers), the exponent is a genuine value of the definition and not a separate convention. Integer exponents, in a group. Let be a group (def-group) and . Write for the embedding of lem-nat-embeds-int, which is injective, preserves addition, multiplication and order, and has as image exactly the nonnegative integers. For define - , the natural power, when and ; - when and . Why this is well defined. The order on is total and antisymmetric (thm-int-ordered-ring, def-int-order), so exactly one of and holds and the two clauses never both apply. In the first clause is nonnegative, so for some , and is unique because is injective. In the second clause gives by compatibility of the order with addition (thm-int-ordered-ring, def-int-operations), so is a positive integer and again for a unique . The inverse is a single determined element by lem-inverse-unique and def-invertible-element. Finally the two readings of , as a natural power and as an integer power, agree by construction, so no ambiguity is introduced. Abbreviation. In an exponent we write for the integer when a natural number is used where an integer is expected; this is unambiguous because is injective and preserves the arithmetic and the order, and because the two readings of agree as just noted. Additive notation. When the group is written additively the same object is written or rather than , with and ; the definitions are identical, only the symbols differ. (Powers : natural exponents in a monoid and integer exponents in a group, with ).
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 ).
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 ).
If and are finite groups, then their external direct product is finite and has order . (For finite groups and , ).
For every , view as its canonical nonnegative integer and put . Then the left cosets of in are exactly the congruence classes modulo , and coset addition is the published addition of congruence classes. Thus as the same group on the same underlying set. This includes and . (For every , the congruence-class group is the quotient group ).
Proof
On a cyclic factor , the quotient is trivial when and has order when .
Taking direct products componentwise therefore gives with equal to the number of exponents at least .
The number of exponents equal to is the number at least minus the number at least , namely .
Each subgroup and quotient is defined intrinsically, and the sequence terminates at zero, so these differences uniquely recover all summands.
Fundamental theorem of finite abelian groups: elementary-divisor form
Statement
Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
If is finite abelian and is its prime factorisation, then the subgroups form an internal direct product of . Thus For the trivial group, this is the empty product. (A finite abelian group is the internal direct product of its primary components).
Every finite abelian -group is isomorphic to a finite direct product of cyclic groups of prime-power order. The trivial -group is the empty product. (Every finite abelian p-group is a direct product of cyclic p-groups).
An elementary-divisor decomposition of a finite abelian group is an isomorphism where every is a prime power. The unordered multiset of the , counted with multiplicity, is the elementary-divisor data. The cyclic factors and product use thm-classification-of-cyclic-groups and def-external-direct-product-of-groups. The data records factor isomorphism types, not distinguished internal subgroups; the trivial group has empty data. (Elementary-divisor data for a finite abelian group).
Suppose with , and in additive notation write . Define by . Then Consequently, for every , the number of summands of order is , so the elementary divisors are intrinsic. (The successive quotients p^iG/p^{i+1}G recover the cyclic summand multiplicities of a finite abelian p-group).
If is cyclic, then exactly one of the following applies: - if has infinite order, ; - if has finite order , necessarily , then . (Every cyclic group is isomorphic to or to for its finite order ).
Proof
Primary decomposition separates into its intrinsic -primary components, and cyclic decomposition expresses each component as a product of cyclic -groups. This proves existence.
For a fixed prime , the successive quotients recover the multiplicity of every cyclic order .
Doing this independently for each prime proves uniqueness of the multiset of elementary divisors. The assertion concerns factor isomorphism types, not uniqueness of internal complements.
Invariant-factor data for a finite abelian group
Definition
An invariant-factor list for a finite abelian group is a finite list of integers together with an isomorphism . The cyclic factors and product use Every cyclic group is isomorphic to or to for its finite order and The external direct product with componentwise multiplication. Unit factors are omitted. The trivial group has the empty list.
Elementary divisors regroup uniquely into invariant factors
Statement
Every multiset of prime-power elementary divisors regroups in exactly one way into an invariant-factor list.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
An elementary-divisor decomposition of a finite abelian group is an isomorphism where every is a prime power. The unordered multiset of the , counted with multiplicity, is the elementary-divisor data. The cyclic factors and product use thm-classification-of-cyclic-groups and def-external-direct-product-of-groups. The data records factor isomorphism types, not distinguished internal subgroups; the trivial group has empty data. (Elementary-divisor data for a finite abelian group).
An invariant-factor list for a finite abelian group is a finite list of integers together with an isomorphism . The cyclic factors and product use thm-classification-of-cyclic-groups and def-external-direct-product-of-groups. Unit factors are omitted. The trivial group has the empty list. (Invariant-factor data for a finite abelian group).
Let be a finite pairwise-coprime list of positive integers and let . The map is a bijection. It preserves addition, multiplication, , and componentwise. For the empty list, and both sides have one element. (Chinese remainder theorem for a finite pairwise-coprime list: simultaneous residues determine one class modulo the product, and the resulting bijection preserves addition and multiplication).
Let be the canonical embedding. If and have finite orders , then in the external direct product (If and have finite orders and , then in ).
If is cyclic, then exactly one of the following applies: - if has infinite order, ; - if has finite order , necessarily , then . (Every cyclic group is isomorphic to or to for its finite order ).
Powers are the natural powers of def-group-power and finite products those of def-monoid-finite-product, both taken in the commutative monoid of lem-units-of-z. Call an injective list of primes when every is prime (def-prime) and forces (def-injection-surjection-bijection). Let with and let be an injective list of primes such that every prime divisor of equals for some . Then, with as in def-p-adic-valuation: 1. ; 2. for every prime that is not among ; 3. the exponents are determined by : if and , then for every . Clause 3 needs only injectivity of the list, not the covering hypothesis. (For and any injective list of primes containing every prime divisor of , one has ; the exponents are determined by , and for every prime outside the list).
Proof
For each prime , sort its exponents increasingly. Left-pad the shorter prime lists with zeros until all have the same length, then multiply the prime powers columnwise to obtain .
The aligned exponents are nondecreasing, so . The Chinese remainder theorem identifies each column product of coprime cyclic groups with .
Conversely, canonical prime factorisation of each recovers every padded exponent column and hence the original elementary divisors.
The empty multiset gives the empty list, so uniqueness includes the trivial group.
Fundamental theorem of finite abelian groups: invariant-factor form
Statement
For every finite abelian group there is a unique list such that . Moreover . The trivial group corresponds to the empty list and empty product.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors. (Fundamental theorem of finite abelian groups: elementary-divisor form).
Every multiset of prime-power elementary divisors regroups in exactly one way into an invariant-factor list. (Elementary divisors regroup uniquely into invariant factors).
An invariant-factor list for a finite abelian group is a finite list of integers together with an isomorphism . The cyclic factors and product use thm-classification-of-cyclic-groups and def-external-direct-product-of-groups. Unit factors are omitted. The trivial group has the empty list. (Invariant-factor data for a finite abelian group).
If and are finite groups, then their external direct product is finite and has order . (For finite groups and , ).
Proof
The elementary-divisor theorem supplies a unique multiset of prime powers, and the regrouping lemma converts it into a unique invariant-factor list.
The order formula for finite direct products gives ; for the empty list this product is , the order of the trivial group.
Converse of Lagrange for finite abelian groups: every divisor occurs as a subgroup order
Statement
Let be finite abelian and let be a positive divisor of . Then has a subgroup of order .
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Let (def-integers). We say divides , and write , when the product being that of def-int-operations. We write when this fails. In this situation is called a divisor, or a factor, of , and is called a multiple of . This is the relation the library already has, not a second one. The published thm-division-algorithm-in-z introduces it in its own Statement, in these words: "We say divides , written , when for some ." Since multiplication on is commutative (thm-int-comm-ring), and are the same condition, so the definition above is that relation verbatim and the two usages agree everywhere. The theorem defined it for use on its own page and left the systematic theory to a later page; this is that page, and this item records the agreement rather than introducing a rival notion. The remainder test. For the same Statement records that holds exactly when the remainder in , , is . Boundary values. Each is one line from the ring axioms, and each is used below, so all three are recorded here rather than assumed: - for every integer , including , since ; - only for , since forces ; - and for every , since and . (Divisibility in : when for some integer ).
The order of a finite group. Let be a group (def-group) whose underlying set is finite (def-countable), so that for some (def-equinumerous). That natural number is unique: if and then , since is symmetric and transitive, and then by claim 3 of lem-pigeonhole. The order of is that unique natural number, written . A group is infinite when its underlying set is not finite, and is then not defined. The order of an element. Let be any group and , with natural powers as in def-group-power. Put - If , the order of is its least element, which exists by the well-ordering principle (thm-well-ordering-principle): every nonempty subset of has a least element, and that element is unique, being every element of and a member of it. We then say has finite order. - If we say has infinite order and write , where is a symbol reserved for this case and is not a natural number. No arithmetic is performed with it here. By construction whenever it is finite, and exactly when , since . Every element of a finite group has finite order. If is finite then for every , by lem-order-of-element-exists, so is a natural number. (The order of a finite group and the order of an element, with when no positive power of is the identity).
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 with , and put (def-divides-in-z). Then is nonempty and has a least element , and is prime (def-prime). In particular every integer greater than has a prime divisor. (Every integer has a prime divisor; indeed the least divisor of that exceeds is prime).
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 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 ).
If is abelian and , then is abelian. (Every quotient group of an abelian group is abelian).
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 ).
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).
Proof
Use strong induction on . If , take the trivial subgroup; this also settles the trivial group.
For , choose a prime . Cauchy's theorem gives a subgroup of order , and is finite abelian of order .
The integer divides , so induction gives a subgroup of order .
By correspondence its full preimage has . The case returns .
The exponent of a finite group
Definition
For a finite group , its exponent is The set is nonempty by for every element of a finite group , and The well-ordering principle gives its least member; powers use Powers : natural exponents in a monoid and integer exponents in a group, with . Thus the definition is well-defined. For the trivial group .
Invariant factors determine the order and exponent of a finite abelian group
Statement
If with , then and . For the empty list, .
Facts & Assumptions
Given: The objects and hypotheses in the statement.
For every finite abelian group there is a unique list such that . Moreover . The trivial group corresponds to the empty list and empty product. (Fundamental theorem of finite abelian groups: invariant-factor form).
For a finite group , its exponent is The set is nonempty by cor-g-to-the-group-order-is-identity, and thm-well-ordering-principle gives its least member; powers use def-group-power. Thus the definition is well-defined. For the trivial group . (The exponent of a finite group).
If and are finite groups, then their external direct product is finite and has order . (For finite groups and , ).
Let be the canonical embedding. If and have finite orders , then in the external direct product (If and have finite orders and , then in ).
Proof
The finite-product order formula gives , including the empty product.
The order of an element of the product is the least common multiple of its component orders. Because , every element order divides , while an element generating the last factor has order .
The least common annihilating exponent is therefore when the list is nonempty, and is for the trivial group.
A nontrivial finite abelian group is cyclic if and only if it has one invariant factor
Statement
A nontrivial finite abelian group is cyclic if and only if its invariant-factor list has exactly one entry.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
For every finite abelian group there is a unique list such that . Moreover . The trivial group corresponds to the empty list and empty product. (Fundamental theorem of finite abelian groups: invariant-factor form).
If with , then and . For the empty list, . (Invariant factors determine the order and exponent of a finite abelian group).
If is cyclic, then exactly one of the following applies: - if has infinite order, ; - if has finite order , necessarily , then . (Every cyclic group is isomorphic to or to for its finite order ).
Proof
A one-entry invariant-factor decomposition is an isomorphism with one cyclic group, so is cyclic.
Conversely a nontrivial finite cyclic group is isomorphic to , giving the one-entry list; uniqueness of invariant factors rules out any different list.
Indecomposable and decomposable nontrivial finite abelian groups
Definition
A nontrivial finite abelian group is indecomposable if it is not an internal direct product of two nontrivial subgroups in the sense of Internal direct products of finitely many normal subgroups. It is decomposable if such a product exists. The trivial group is assigned neither label.
Every nontrivial finite abelian group is an internal direct product of indecomposable subgroups
Statement
Every nontrivial finite abelian group is an internal direct product of finitely many indecomposable subgroups.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
A nontrivial finite abelian group is indecomposable if it is not an internal direct product of two nontrivial subgroups in the sense of def-internal-direct-product-of-subgroups. It is decomposable if such a product exists. The trivial group is assigned neither label. (Indecomposable and decomposable nontrivial 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 . The following are equivalent: the form an internal direct product of ; every has a unique expression with ; and the multiplication map is an isomorphism. These statements include the empty family and the one-factor case. (Internal direct products are external direct products, equivalently every element has a unique factorisation).
Let be a finite group and . Then Consequently, under the canonical embedding , divides . (Lagrange's theorem: for every subgroup of a finite group ).
Proof
For strong induction on , the order-one case is vacuous because the only group of that order is trivial.
Fix a nontrivial and assume the result for every nontrivial finite abelian group of smaller order. If is indecomposable, the one-factor product is the required decomposition.
If is decomposable, write with and nontrivial. Lagrange gives , so the induction hypothesis decomposes each into indecomposable factors.
Unique factorisation in and in the two inductive products combines to unique factorisation by all the smaller factors; internal-product recognition completes the induction.
The indecomposable finite abelian groups are exactly the nontrivial cyclic groups of prime-power order
Statement
The indecomposable finite abelian groups are exactly the nontrivial cyclic groups of prime-power order.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
A nontrivial finite abelian group is indecomposable if it is not an internal direct product of two nontrivial subgroups in the sense of def-internal-direct-product-of-subgroups. It is decomposable if such a product exists. The trivial group is assigned neither label. (Indecomposable and decomposable nontrivial finite abelian groups).
Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors. (Fundamental theorem of finite abelian groups: elementary-divisor form).
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).
Every subgroup of a cyclic group is cyclic. If , then the least positive integer for which satisfies . (Every subgroup of a cyclic group is cyclic; the least positive exponent in a nontrivial subgroup supplies a generator).
Let be a finite group such that the positive integer is prime. Then every has order , satisfies , and hence generates . In particular, is cyclic. (A finite group of prime order is cyclic and every nonidentity element generates it).
Proof
The elementary-divisor theorem writes any nontrivial finite abelian group as a product of nontrivial cyclic prime-power factors. Indecomposability forces exactly one factor.
Conversely, if with both factors nontrivial, Cauchy's theorem gives an order- subgroup in each factor. Their images are distinct, but a cyclic group has a unique subgroup of each possible order. Hence no such decomposition exists.
Partitions of a positive integer
Definition
For , a partition of is a finite nondecreasing list of positive integers with , using finite natural sums as in Finite sums and finite products of natural numbers, and in and naturals as in The natural numbers (von Neumann). Equality is equality of these lists. The nondecreasing convention removes permutations from the data.
Isomorphism classes of abelian groups of order p^n are counted by partitions of n
Statement
For a prime and , isomorphism classes of abelian groups of order are in bijection with partitions of . For , the unique group is the trivial group and corresponds separately to the empty partition.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors. (Fundamental theorem of finite abelian groups: elementary-divisor form).
For , a partition of is a finite nondecreasing list of positive integers with , using finite natural sums as in def-nat-finite-sum-and-product and naturals as in def-natural-numbers. Equality is equality of these lists. The nondecreasing convention removes permutations from the data. (Partitions of a positive integer).
If and are finite groups, then their external direct product is finite and has order . (For finite groups and , ).
Proof
The elementary-divisor theorem writes such a group uniquely as with the positive exponents arranged nondecreasingly. The product-order formula gives .
Thus the exponents form a partition of , and every partition constructs a group of order . Uniqueness of elementary divisors makes the two constructions inverse.
The number of finite abelian groups of order n is the product of the partition numbers of the prime exponents of n
Statement
Let , and write its canonical prime factorisation as , with the distinct and . Then the number of isomorphism classes of abelian groups of order is where is the number of partitions of . For one has , so the empty product is .
Facts & Assumptions
Given: The objects and hypotheses in the statement.
If is finite abelian and is its prime factorisation, then the subgroups form an internal direct product of . Thus For the trivial group, this is the empty product. (A finite abelian group is the internal direct product of its primary components).
For a prime and , isomorphism classes of abelian groups of order are in bijection with partitions of . For , the unique group is the trivial group and corresponds separately to the empty partition. (Isomorphism classes of abelian groups of order p^n are counted by partitions of n).
Powers are the natural powers of def-group-power and finite products those of def-monoid-finite-product, both taken in the commutative monoid of lem-units-of-z. Call an injective list of primes when every is prime (def-prime) and forces (def-injection-surjection-bijection). Let with and let be an injective list of primes such that every prime divisor of equals for some . Then, with as in def-p-adic-valuation: 1. ; 2. for every prime that is not among ; 3. the exponents are determined by : if and , then for every . Clause 3 needs only injectivity of the list, not the covering hypothesis. (For and any injective list of primes containing every prime divisor of , one has ; the exponents are determined by , and for every prime outside the list).
Let be a monoid (def-semigroup-and-monoid) and let be a family of elements of , written . There is exactly one function satisfying and we write In particular the empty product is , and . Why the recursion is legitimate. The clause consults as well as , so thm-recursion does not apply to it directly. Apply that theorem instead with the set , the element , and the function given by : it yields a unique with and . Writing , induction (thm-induction-principle) gives for every , since and . Hence , so satisfies the two displayed equations. It is the only such function: if satisfies them too, then contains and is closed under , hence is all of by induction. The value depends only on . If satisfy for every , then . Indeed the set of for which this implication holds contains , both products then being ; and if it holds at , and agree at every , then they agree at every and also at itself, because is equivalent to (lem-nat-order-is-membership), so . Induction finishes it. This is what makes the notation unambiguous: it names a value determined by the first terms alone, and a finite list of length , that is a function on the von Neumann natural (def-natural-numbers), determines the product computed from any extension of . (The product of a finite list in a monoid, by recursion, with the empty product () equal to the identity).
Proof
Primary decomposition makes an abelian group of order the product of one abelian -group of order for each .
The choices for distinct primes are independent and the preceding corollary counts the th choice by , so the product rule gives the formula. The empty prime factorisation of gives one choice.
Squarefree positive integers
Definition
A positive integer is squarefree if no square of a prime divides . Equivalently, every exponent in its canonical prime factorisation is or . The integer is squarefree by the empty factorisation.
Every abelian group of order n is cyclic if and only if n is squarefree
Statement
For a positive integer , every abelian group of order is cyclic if and only if is squarefree.
Facts & Assumptions
Given: The objects and hypotheses in the statement.
A positive integer is squarefree if no square of a prime divides . Equivalently, every exponent in its canonical prime factorisation is or . The integer is squarefree by the empty factorisation. (Squarefree positive integers).
Every finite abelian group is isomorphic to a finite direct product of cyclic groups of prime-power order. The multiset of their orders is uniquely determined by the group, up to permutation of the factors. (Fundamental theorem of finite abelian groups: elementary-divisor form).
If is finite abelian and is its prime factorisation, then the subgroups form an internal direct product of . Thus For the trivial group, this is the empty product. (A finite abelian group is the internal direct product of its primary components).
Let be a finite pairwise-coprime list of positive integers and let . The map is a bijection. It preserves addition, multiplication, , and componentwise. For the empty list, and both sides have one element. (Chinese remainder theorem for a finite pairwise-coprime list: simultaneous residues determine one class modulo the product, and the resulting bijection preserves addition and multiplication).
Let be the canonical embedding. If and have finite orders , then in the external direct product (If and have finite orders and , then in ).
Proof
If is squarefree, each primary component of an abelian group of order has prime order and is cyclic. The Chinese remainder theorem combines the cyclic factors of pairwise coprime orders into a cyclic group of order .
If , write with and . The abelian group , omitting trivial factors, has order but exponent strictly below , so it is not cyclic.
For the sole group is trivial and cyclic, agreeing with squarefreeness of .
5 · Examples, counterexamples and false statements
None yet.
Sources
Standard references
Recommended treatments; not extraction sources.