Group to Nilpotent group

ClassGroup#

A group is a set equipped with an associative binary operation that has an identity element and in which every element has an inverse. Groups are the algebraic language of symmetry: the symmetries of any object, composed one after another, form a group. They are also the common skeleton of many other structures, since the integers under addition, the nonzero real numbers under multiplication and the invertible matrices of a given size are all groups, and rings, fields and vector spaces are built from groups by adding further operations.

Definition

A group is a set \(G\) with a binary operation \((a, b) \mapsto ab\), an element \(e \in G\) and a map \(a \mapsto a^{-1}\) from \(G\) to itself, such that for all \(a, b, c\) in \(G\):

\[(ab)c = a(bc), \qquad ea = a = ae, \qquad a^{-1}a = e.\]

The first axiom is associativity, the second says that \(e\) is an identity element, and the third says that \(a^{-1}\) is a left inverse of \(a\). The axioms can be weakened further: associativity, a left identity and left inverses already determine a group structure, and so do the corresponding right-handed axioms (the right-handed version). A group in which \(ab = ba\) for all \(a\) and \(b\) is called commutative or abelian; abelian groups are often written additively, with \(a + b\), \(0\) and \(-a\) in place of \(ab\), \(e\) and \(a^{-1}\).

The number of elements of a finite group is its order. A map between groups that preserves the operation is a group morphism, and a subset that contains the identity and is closed under the operation and inverses is a subgroup.

Examples
  • The integers form an abelian group under addition, with identity \(0\) and inverse \(n \mapsto -n\). The natural numbers do not, since \(1\) has no additive inverse among them.
  • The nonzero elements of a field, such as the nonzero real numbers, form an abelian group under multiplication.
  • For a positive integer \(n\), the integers modulo \(n\) form an abelian group under addition, the cyclic group of order \(n\).
  • The bijections of a set \(X\) onto itself form a group under composition, the symmetric group of \(X\). When \(X\) has at least three elements this group is not abelian. The even permutations of a finite set form the alternating group.
  • More generally, in any set with an associative operation and an identity, the invertible elements form a group. Applied to square matrices this gives the general linear group.
  • The rotations and reflections of a regular polygon with \(n\) sides form a non-abelian group of order \(2n\) when \(n \ge 3\).
Basic properties

The axioms ask only for a left inverse, but it is automatically a right inverse: \(aa^{-1} = e\) for every \(a\). The identity element is unique, and inverses are unique: if \(ab = e\), then \(a^{-1} = b\). Two consequences of uniqueness are that \((a^{-1})^{-1} = a\) and that \((ab)^{-1} = b^{-1}a^{-1}\), with the order of the factors reversed.

Every element can be cancelled from either side of an equation: \(ab = ac\) implies \(b = c\), and \(ba = ca\) implies \(b = c\). Equations of the form \(ax = b\) have exactly one solution, namely \(x = a^{-1}b\), since \(x = a^{-1}b\) if and only if \(ax = b\); so left multiplication by a fixed element is a bijection of \(G\) onto itself. For a finite group this says that every row of the multiplication table lists each element exactly once.

Powers \(a^n\) are defined for every integer \(n\): \(a^0 = e\), \(a^n\) is the product of \(n\) copies of \(a\) for \(n > 0\), and \(a^{-n} = (a^{-1})^n\). They satisfy \(a^{m+n} = a^m a^n\). The least positive \(n\) with \(a^n = e\), if there is one, is the order of the element \(a\).

Much of group theory studies a group through its subgroups and quotients. The normal subgroups are those that can be factored out to form a quotient group, and the first isomorphism theorem relates quotients to morphisms. Lagrange's theorem and the three Sylow theorems (first, second and third) connect the order of a finite group with the orders of its subgroups. A group can act on a set by permutations, giving a group action, and Cayley's theorem says every group is isomorphic to a group of permutations of some set, namely a subgroup of the symmetric group on its own elements. Nontrivial groups whose only normal subgroups are the trivial subgroup and the whole group are simple; groups can also be described by generators and relations as presented groups, starting from free groups.

Dropping the requirement of inverses gives a monoid, a set with an associative operation and an identity element; adding topology or smooth structure compatible with the operation gives topological groups and Lie groups.

In Mathlib

Mathlib builds a group in layers. A monoid is an associative operation with a two-sided identity, and it already carries powers with natural-number exponents. Adding an inverse, a division operation, with \(a / b\) equal to \(ab^{-1}\), and powers with integer exponents gives an intermediate structure, and a group is that structure together with the axiom that the inverse is a left inverse; the right inverse property is proved as a lemma. The division and the powers default to their usual definitions; carrying them as part of the structure lets specific groups use better-behaved definitions. Mathlib also declares an additive version alongside it, linked to the multiplicative one so that most lemmas about groups are translated automatically into additive form; the additive version does not assume commutativity, and abelian groups written with \(+\) form a separate additive commutative structure. Several basic facts, such as the uniqueness of inverses, the inverse of a product and cancellation, are stated in Mathlib for weaker structures than groups (division monoids, which are monoids with an involutive inverse that reverses products and satisfies \(a^{-1} = b\) whenever \(ab = e\), or structures with cancellation), so they apply to groups as a special case.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibGroup
Uses 1 · Used by 44
Statement usesSet
Used byDirichlet unit theorem · Abelian category · Lucas-Lehmer primality test · Abel-Ruffini theorem (one direction) · Field · Abelianization · Burnside lemma · Cyclic group · Free group · Group action · Group morphism · Index of a subgroup · Nilpotent group · Normal subgroup · Quotient group · Schreier's lemma · Simple group · Subgroup · Subgroup generated by a subset · Cayley's theorem · Classification of abelian simple groups · First Sylow theorem · Lagrange's theorem · Permutation group of a type · Second Sylow theorem · Structure of finitely generated abelian groups · Third Sylow theorem · Character · Representation · Ring · Topological group · Conjugacy classes · Direct product of groups · Orbit · Order of an element · Quotient space (Basic definitions) · Stabilizer of a point · General linear group (Classical automorphism groups) · Orthogonal group · Unitary group · Decomposition into cycles with disjoint support · Decomposition into transpositions · Signature · Maschke theorem

StructureGroup morphism#

A group morphism, or group homomorphism, is a map between two groups that respects the group operation. Morphisms are how groups are compared: they describe when one group is a copy of another, when one is a quotient of another, and how a group can be represented by permutations or matrices. Much of group theory, from normal subgroups to the first, second and third isomorphism theorems, is organized around them.

Definition

Let \(G\) and \(H\) be groups. A map \(f \colon G \to H\) is a group morphism if

\[f(xy) = f(x)\,f(y) \quad \text{for all } x, y \in G.\]

For monoids \(M\) and \(N\), the same definition with the extra requirement \(f(1_M) = 1_N\) defines a morphism of monoids; in a monoid the identity condition does not follow from multiplicativity. For groups it is automatic: from \(f(e)f(e) = f(e)\) one cancels \(f(e)\) in \(H\) and gets \(f(e) = e\), so a product-preserving map into a group already preserves the identity. An isomorphism is a morphism that has an inverse morphism. The inverse map of a bijective morphism is automatically a morphism, since \(f(f^{-1}(u)f^{-1}(v)) = uv\), so every bijective morphism is an isomorphism.

Examples
  • The identity map of \(G\) is a morphism, and so is the trivial map sending every element to the identity of \(H\).
  • The inclusion of a subgroup \(K \le G\) into \(G\) is an injective morphism.
  • For a normal subgroup \(N\) of \(G\), the map sending \(g\) to its coset \(gN\) is a surjective morphism onto the quotient group \(G/N\).
  • The exponential function is a morphism from the real numbers under addition to the positive reals under multiplication, since \(e^{x+y} = e^x e^y\); it is an isomorphism with inverse the natural logarithm.
  • The signature of a permutation of a finite set, which is \(1\) for even and \(-1\) for odd permutations, is a morphism to the group \(\{1, -1\}\). Its kernel is the alternating group.
  • Since \(\det(AB) = \det(A)\det(B)\), the determinant is a morphism from the invertible \(n \times n\) matrices over a field \(K\) to the nonzero elements of \(K\). Mathlib records the determinant as a monoid morphism on all square matrices over a commutative ring.
Properties

A morphism preserves all of the group structure, not only products. It sends the identity to the identity, it sends inverses to inverses, \(f(x^{-1}) = f(x)^{-1}\), and consequently it commutes with integer powers:

\[f(x^n) = f(x)^n \quad \text{for all } n \in \mathbb{Z}.\]

The composite of two morphisms is a morphism, and the identity map is a morphism, so groups and their morphisms form a category.

Two subgroups are attached to every morphism \(f \colon G \to H\).

More generally, the image of a subgroup of \(G\) is a subgroup of \(H\), the preimage of a subgroup of \(H\) is a subgroup of \(G\), and the preimage of a normal subgroup is normal. The first isomorphism theorem ties the two subgroups together: \(G / \ker f\) is isomorphic to the image of \(f\). Every normal subgroup \(N\) of \(G\) is the kernel of the quotient map \(G \to G/N\), so normal subgroups are exactly the kernels of morphisms.

A group action of \(G\) on a set \(X\) amounts to a morphism from \(G\) to the group of permutations of \(X\), and a linear representation is a morphism from \(G\) to the invertible linear maps of a vector space. Morphisms of other algebraic structures follow the same pattern: a ring morphism preserves addition, multiplication and the unit, and a linear map preserves addition and scalar multiplication. The abelianization and free groups are characterized by universal properties: morphisms from the abelianization of \(G\) to an abelian group \(A\) correspond to morphisms \(G \to A\), and morphisms from the free group on a set \(S\) to a group \(H\) correspond to arbitrary maps \(S \to H\).

In Mathlib

Mathlib has no separate notion of group morphism: it uses the morphisms of monoids, which preserve the product and the identity, for groups as well. The definition asks only for a multiplication and an identity element on each side, so the same structure covers monoids, groups and many intermediate cases, and a group morphism must come with a proof that it preserves the identity, which the constructor mentioned above supplies from multiplicativity. The kernel, as a subgroup, is defined whenever the source is a group; the target needs only a multiplication with an identity element. Morphisms are bundled: a morphism is a function packaged with the proofs of its properties, and general results are usually stated for any type of maps that behaves like morphisms, so they apply equally to isomorphisms and to ring morphisms. The additive version, for groups written with \(+\), is a parallel structure, and most of its definitions and theorems are generated automatically from the multiplicative ones.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibMonoidHom
Uses 1 · Used by 16
Statement usesGroup
Used byWilson’s Lemma · Derangements Formula · Translation numbers define a group action up to semiconjugacy · Abelianization · First isomorphism theorem · Free group · Group action · Quotient group · Second isomorphism theorem · Third isomorphism theorem · Alternating group · Cayley's theorem · Structure of finitely generated abelian groups · Representation · Ring morphism · Signature

ClassGroup action#

A group action of a group \(G\) on a set \(X\) lets each element of \(G\) move the points of \(X\), in a way that respects the group law: acting by a product is the same as acting by the factors one after the other. Groups usually arise as groups of symmetries of something, and an action records exactly that relationship. Actions let one study a group through the sets it permutes, and a set through its symmetries, and they underlie the main counting arguments of finite group theory: the orbit–stabilizer theorem, the class formula, Burnside's lemma and the Sylow theorems.

Definition

A (left) action of \(G\) on \(X\) is a map \(G \times X \to X\), written \((g, x) \mapsto g \cdot x\), such that for all \(g, h \in G\) and \(x \in X\)

\[e \cdot x = x, \qquad (gh) \cdot x = g \cdot (h \cdot x),\]

where \(e\) is the identity element. These two axioms are the definition of an action. A set with an action of \(G\) is called a \(G\)-set.

Equivalently, an action is a homomorphism from \(G\) to the group of permutations of \(X\). Each \(g\) gives a bijection \(x \mapsto g \cdot x\), whose inverse is the action of \(g^{-1}\), so each element acts as a permutation of \(X\), and the two axioms say precisely that the assignment of \(g\) to its permutation is a group homomorphism. Conversely, a homomorphism from \(G\) into the monoid of all maps \(X \to X\) under composition (its image then consists of permutations) defines an action. Composing an action with a homomorphism \(H \to G\) gives an action of \(H\); in particular every subgroup of \(G\) acts on every \(G\)-set by restriction.

Right actions, written \(x \cdot g\) with \(x \cdot (gh) = (x \cdot g) \cdot h\), are defined symmetrically; setting \(g \cdot x = x \cdot g^{-1}\) turns a right action into a left one.

Examples
  • The permutation group of a set \(X\) acts on \(X\) by evaluation, \(\sigma \cdot x = \sigma(x)\).
  • Every group acts on itself by left multiplication, \(g \cdot h = gh\). Since \(gh = h\) forces \(g = e\), the corresponding homomorphism into the permutations of \(G\) is injective, which is Cayley's theorem.
  • A group acts on itself by conjugation, \(g \cdot h = ghg^{-1}\). Its orbits are the conjugacy classes, and the stabilizer of \(h\) is its centralizer.
  • For a subgroup \(H\) of \(G\), left multiplication \(g \cdot xH = gxH\) is an action of \(G\) on the set of left cosets of \(H\).
  • The general linear group of invertible \(n \times n\) real matrices acts on \(\mathbb{R}^n\) by matrix multiplication, and the symmetry group of a cube acts on its vertices, edges and faces.
Orbits, stabilizers and kinds of action

The orbit of a point \(x\) is the set \(G \cdot x = \{ g \cdot x : g \in G \}\). Lying in the same orbit is an equivalence relation, so the orbits partition \(X\); the set of orbits is written \(X/G\).

The stabilizer of \(x\) is the subgroup \(G_x = \{ g \in G : g \cdot x = x \}\). Points in one orbit have conjugate stabilizers: \(G_{g \cdot x} = g\,G_x\,g^{-1}\). The points fixed by every element of \(G\) are those whose orbit is a single point.

An action is transitive if it has exactly one orbit, that is, \(X\) is nonempty and any point can be carried to any other. It is faithful if distinct elements of \(G\) act differently, which for a group means that only the identity fixes every point; a faithful action then makes the homomorphism to the permutations of \(X\) injective, and conversely. For nonempty \(X\), the action of the permutation group of \(X\) on \(X\) is both transitive and faithful.

Orbit–stabilizer theorem

For each point \(x\), the map \(gG_x \mapsto g \cdot x\) is a bijection from the left cosets of \(G_x\) onto the orbit of \(x\). It is well defined and injective because \(g \cdot x = h \cdot x\) holds exactly when \(g^{-1}h \in G_x\), and it is surjective by the definition of the orbit. Hence the size of the orbit is the index of the stabilizer (see index of a subgroup), and for a finite group the size of the orbit times the order of the stabilizer is the order of the group:

\[|G \cdot x|\,|G_x| = |G|.\]

In particular the size of every orbit divides \(|G|\).

Consequences

Summing the orbit–stabilizer theorem over the orbits gives the class formula, which for the conjugation action shows for instance that a nontrivial finite \(p\)-group has a nontrivial center. Counting pairs \((g, x)\) with \(g \cdot x = x\) in two ways gives Burnside's lemma: the number of orbits is the average number of points fixed by an element. The Sylow theorems come from actions of a group on its subsets and subgroups; the second Sylow theorem says that conjugation acts transitively on the Sylow \(p\)-subgroups.

Generalizations

The axioms make sense for any monoid in place of \(G\), giving monoid actions; many statements, such as the orbit–stabilizer theorem, need inverses. An action of a group on a vector space by linear maps is a representation, and a ring acting on an abelian group compatibly with both operations gives a module. A vector space acting freely and transitively on a nonempty set makes that set an affine space; for a general additive group, such a set is called a torsor.

In Mathlib

Mathlib defines actions for an arbitrary monoid, not only a group, as a structure attached to the pair of a monoid and a type, with the action written as a scalar multiplication. Its actions are left actions; a right action is expressed as a left action of the opposite monoid. A separately declared additive version, for additive monoids, uses its own symbol, and most results about multiplicative actions are translated to it automatically. Transitivity is stated as "pretransitivity", which does not require the set to be nonempty, so any action on the empty set is pretransitive. The statement that the orbit has the size of the index of the stabilizer uses Mathlib's convention that an infinite set has size 0 and a subgroup of infinite index has index 0, so it holds for infinite orbits too. Because a group already acts on itself by left multiplication, the conjugation action is placed on a separate copy of the group, so the two actions do not clash.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibMulAction
Uses 4 · Used by 10
Statement usesGroup · Set · Permutation group of a type · Group morphism
Used byBurnside lemma · Class formula · Cayley's theorem · First Sylow theorem · Second Sylow theorem · Third Sylow theorem · Module · Orbit · Quotient space (Basic definitions) · Stabilizer of a point

DefinitionClass formula#

The class formula describes how a set on which a group acts breaks up into pieces. The set is the disjoint union of its orbits, and each orbit is a copy of the set of cosets of the stabilizer of any of its points. For a finite group acting on a finite set this turns into a counting rule: the size of the set is a sum of indices of subgroups, and each term divides the order of the group. Applied to the action of a group on itself by conjugation, it gives the class equation, the standard tool for proving that nontrivial groups of prime power order have a nontrivial centre.

Statement

Let \(G\) be a group acting on a set \(X\) (see group action). The orbits \(G \cdot x = \{ g \cdot x : g \in G \}\) partition \(X\); write \(X/G\) for the set of orbits and choose one point \(x_\omega\) in each orbit \(\omega\). Let \(G_x = \{ g \in G : g \cdot x = x \}\) be the stabilizer of \(x\). Then there is a bijection

\[X \;\cong\; \coprod_{\omega \in X/G} G / G_{x_\omega},\]

between \(X\) and the disjoint union, over all orbits, of the sets of left cosets of the chosen stabilizers. If \(G\) and \(X\) are finite, counting both sides gives the class formula

\[|X| \;=\; \sum_{\omega \in X/G} \frac{|G|}{|G_{x_\omega}|} \;=\; \sum_{\omega \in X/G} [G : G_{x_\omega}].\]

The choice of representatives does not matter: points of the same orbit have conjugate stabilizers, which have the same index.

Proof

Sending each point to its orbit shows that \(X\) is the disjoint union of its orbits. It remains to identify a single orbit \(G \cdot x\) with \(G/G_x\). The map \(gG_x \mapsto g \cdot x\) is well defined and injective, because \(g \cdot x = h \cdot x\) holds exactly when \(g^{-1}h \in G_x\), that is, when \(gG_x = hG_x\); it is surjective by the definition of the orbit. This is the orbit–stabilizer theorem, and in the finite case it reads \(|G \cdot x| \, |G_x| = |G|\). Assembling these bijections orbit by orbit gives the statement, and Lagrange's theorem turns the number of cosets into \(|G|/|G_x|\).

Examples
  • Colourings of a square. The cyclic group of order \(4\), acting on the \(16\) ways to colour the corners of a square black or white by rotating the square, has six orbits. The two one-colour colourings are fixed by every rotation, so each forms an orbit of size \(1\). The colouring with two opposite black corners is fixed by the half-turn, so its stabilizer has index \(2\). The colourings with one black corner, three black corners, or two adjacent black corners have trivial stabilizers and orbits of size \(4\). The formula checks out as \(16 = 1 + 1 + 2 + 4 + 4 + 4\).
  • Transitive actions. If there is a single orbit, the formula says that \(X\) is a copy of \(G/G_x\) for any \(x\), so the index of a stabilizer is the size of the set.
  • Conjugation. A group acts on itself by \(g \cdot h = ghg^{-1}\). The orbits are the conjugacy classes and the stabilizer of \(h\) is its centralizer \(C_G(h)\), so in a finite group the class of \(h\) has \(|G|/|C_G(h)|\) elements.
Consequences
In Mathlib

Mathlib states the class formula first as a bijection rather than an equation, and for an arbitrary group acting on an arbitrary type, finite or not. The representative of each orbit is the one supplied by the axiom of choice; a companion version accepts any function that picks a point in each orbit. The counting form assumes that the group and the set are finite and writes each term as a quotient of natural numbers, \(|G|\) divided by the order of the stabilizer, which is exact because the stabilizer's order divides \(|G|\). The class equation is stated for finite groups, with the sum running over the conjugacy classes that have more than one element; each term is the number of elements of the class rather than the index of its centralizer, and the size of the centre is counted the same way. A \(p\)-group in Mathlib is a group in which every element has order a power of \(p\), so the fixed-point congruence needs only the set, not the group, to be finite.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibMulAction.selfEquivSigmaOrbitsQuotientStabilizer
Uses 5
Statement usesGroup action · Orbit · Stabilizer of a point · Index of a subgroup
Proof usesLagrange's theorem

TheoremBurnside lemma#

Burnside's lemma, also called the Cauchy–Frobenius lemma or the orbit-counting lemma, says that when a finite group acts on a finite set, the number of orbits equals the average number of points fixed by an element of the group. It is the basic tool for counting objects up to symmetry: colourings of a necklace up to rotation, of a cube up to rigid motion, or graphs up to relabelling of their vertices. It is also the first step towards the Pólya enumeration theorem.

Statement

Let \(G\) be a finite group with a group action on a finite set \(X\). For \(g \in G\) write

\[X^g = \{\, x \in X : g \cdot x = x \,\}\]

for the set of points fixed by \(g\). Two points lie in the same orbit when one is carried to the other by some element of \(G\); this relation of lying in a common orbit is an equivalence relation, and \(X/G\) denotes its set of classes, the orbits. Then the fixed-point counts sum to the number of orbits times the order of \(G\):

\[\sum_{g \in G} |X^g| = |X/G| \cdot |G|, \qquad\text{equivalently}\qquad |X/G| = \frac{1}{|G|} \sum_{g \in G} |X^g|.\]
Examples
  • Necklaces. Colour the four beads of a square necklace black or white, and regard two colourings as the same when a rotation takes one to the other. The rotation group has order \(4\). The identity fixes all \(16\) colourings, the quarter turns in either direction fix only the \(2\) one-coloured necklaces, and the half turn fixes the \(4\) colourings in which opposite beads agree. So there are \((16 + 2 + 4 + 2)/4 = 6\) necklaces.
  • Transitive actions. If the action has a single orbit, the average number of fixed points is \(1\). When \(|X| \ge 2\) the identity fixes more than one point, so some element of \(G\) fixes no point at all: every transitive permutation group of degree at least \(2\) contains a fixed-point-free element.
  • Conjugation. Let \(G\) act on itself by conjugation. The orbits are the conjugacy classes, and the points fixed by \(g\) are the elements commuting with \(g\). Summing over \(g\) counts commuting ordered pairs, so the number of commuting pairs equals the number of conjugacy classes times \(|G|\). Equivalently, two elements chosen independently and uniformly from \(G\) commute with probability \(k(G)/|G|\), where \(k(G)\) is the number of conjugacy classes.
Proof

Count the set of pairs \((g, x) \in G \times X\) with \(g \cdot x = x\) in two ways. Grouping the pairs by \(g\) gives \(\sum_{g} |X^g|\). Grouping them by \(x\) gives \(\sum_{x} |G_x|\), where the stabilizer \(G_x = \{\, g : g \cdot x = x \,\}\) is a subgroup of \(G\). By the orbit-stabilizer theorem, the size of the orbit of \(x\) times the order of \(G_x\) is \(|G|\), so \(|G_x| = |G| / |G \cdot x|\). The points of a single orbit \(O\) therefore contribute \(|O| \cdot |G|/|O| = |G|\) to the second sum, and the total is \(|X/G| \cdot |G|\).

The same argument can be phrased without arithmetic. Points in one orbit have isomorphic stabilizers, and assembling these identifications with the orbit-stabilizer correspondence yields a bijection between the set of fixed pairs and the product of \(X/G\) with \(G\). Burnside's lemma is the comparison of the sizes of the two sides.

In Mathlib

Mathlib states the lemma for a group acting on a type, assuming the group, each set of fixed points and the set of orbits are finite rather than assuming the whole type is finite; with a finite group and finitely many orbits this comes to the same thing, since each orbit is no larger than the group. The orbits are the classes of the orbit relation. To stay within the natural numbers the identity is stated multiplied out, as a sum equal to a product, with no division. It is derived from a bijection, built using choice and recorded separately as a definition, so the counting statement is a direct consequence of comparing cardinalities. An additive version for additive groups is generated automatically. The commuting-pairs consequence is stated for every group, with the convention that an infinite set has cardinality \(0\), so it is trivially true for infinite groups.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibMulAction.sum_card_fixedBy_eq_card_orbits_mul_card_group
Uses 4
Statement usesGroup · Group action · Orbit
Proof usesStabilizer of a point

StructureSubgroup#

A subgroup of a group \(G\) is a subset of \(G\) that is itself a group under the same operation. Subgroups are the basic way of locating smaller groups inside a larger one: much of the structure theory of groups, from Lagrange's theorem to the Sylow theorems, is a study of which subgroups a group has and how they sit inside it.

Definition

Let \(G\) be a group with identity element \(e\). A subset \(H \subseteq G\) is a subgroup if

  • \(e \in H\);
  • \(xy \in H\) whenever \(x, y \in H\);
  • \(x^{-1} \in H\) whenever \(x \in H\).

One writes \(H \le G\). The three conditions say exactly that the operation of \(G\) restricts to \(H\) and that the restricted operation satisfies the group axioms, so a subgroup is a group in its own right, and the inclusion of \(H\) into \(G\) is a group homomorphism. Associativity needs no check, since it is inherited from \(G\).

The conditions can be condensed into a single test: a nonempty subset \(H\) such that \(xy^{-1} \in H\) for all \(x, y \in H\) is a subgroup. Indeed, taking \(y = x\) gives \(e \in H\), then taking \(x = e\) gives closure under inverses, and closure under products follows by applying the test to \(x\) and \(y^{-1}\).

Examples
  • Every group \(G\) has the trivial subgroup \(\{e\}\) and the whole group \(G\) as subgroups. A subgroup other than \(G\) is called proper.
  • In the additive group of integers, the multiples of a fixed integer \(n\) form a subgroup \(n\mathbb{Z}\), and an integer \(b\) lies in it exactly when \(n\) divides \(b\). Every subgroup of \(\mathbb{Z}\) has this form.
  • For an element \(g \in G\), the powers \(g^k\) with \(k \in \mathbb{Z}\) form the cyclic subgroup generated by \(g\), which is the smallest subgroup containing \(g\); its size is the order of \(g\) when that order is finite.
  • The center of \(G\), the set of elements that commute with every element of \(G\), is a subgroup.
  • For a homomorphism \(f \colon G \to K\) of groups, the kernel, the set of \(g\) with \(f(g) = e\), is a subgroup of \(G\), and the image is a subgroup of \(K\).
  • The alternating group \(A_n\) of even permutations is a subgroup of the symmetric group on \(n\) letters.
Properties

The cosets \(gH\) of a subgroup \(H\) partition \(G\), and their number is the index of \(H\) in \(G\). A subgroup that is invariant under conjugation, so that \(gHg^{-1} = H\) for every \(g\), is a normal subgroup; normal subgroups are exactly the kernels of homomorphisms, and the cosets of a normal subgroup form the quotient group. A nontrivial group whose only normal subgroups are the trivial subgroup and the whole group is a simple group. Cayley's theorem shows that every group \(G\) is isomorphic to a subgroup of the group of permutations of its underlying set. The same idea of a subset closed under the operations of a structure gives the subring, the subfield and the vector subspace.

In Mathlib

Mathlib treats a subgroup as a bundled object: a subset of the group packaged together with proofs of the three closure properties, built by extending the notion of a submonoid with closure under inverses. Two subgroups are equal as soon as they have the same elements. A subgroup is not a separate type, but it can be used as one, and it then carries the group structure inherited from the ambient group. Subgroups are ordered by inclusion and form a complete lattice, with the trivial subgroup as least element and the whole group as greatest. The kernel is defined more generally for a homomorphism from a group into any type with a multiplication and an identity element, in particular any monoid. The additive version, for groups written with \(+\), is generated automatically from the multiplicative one; the statements about \(\mathbb{Z}\) above are phrased in terms of it. A separate class covers any kind of object that behaves like a subgroup, so that, for example, a subring can be treated directly as an additive subgroup of its ring, and some general results, like the one on unions, are stated at that level.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibSubgroup
Uses 2 · Used by 24
Statement usesGroup · Set
Used byFirst isomorphism theorem · Index of a subgroup · Normal subgroup · Quotient group · Schreier's lemma · Second isomorphism theorem · Subgroup generated by a subset · Alternating group · Cayley's theorem · First Sylow theorem · Lagrange's theorem · Second Sylow theorem · Third Sylow theorem · Subring · Nielsen–Schreier theorem · Dirichlet's unit theorem · Complex roots of unity · Orbit · Quotient space (Basic definitions) · Stabilizer of a point · Orthogonal group · Special orthogonal group · Special unitary group · Unitary group

DefinitionIndex of a subgroup#

The index of a subgroup \(H\) of a group \(G\) is the number of cosets of \(H\) in \(G\), written \([G : H]\). It measures how large \(G\) is relative to \(H\), and it stays meaningful for infinite groups, where orders cannot be compared directly: the integers and the even integers are both infinite, yet the even integers have index \(2\) in the integers, since they and the odd integers are the only two cosets. The index is the quantity behind Lagrange's theorem, and small indices force strong structure, such as normality in index \(2\).

Definition

Let \(H\) be a subgroup of \(G\). The left cosets \(gH\), for \(g \in G\), partition \(G\). The index of \(H\) in \(G\) is the number of left cosets, which may be finite or infinite. Inversion \(g \mapsto g^{-1}\) carries the left coset \(gH\) to the right coset \(Hg^{-1}\), so left and right cosets are equal in number and either may be used. A subgroup is said to have finite index when \([G : H]\) is finite.

For any subgroup, the index is the cardinality of the coset space \(G/H\). When \(H\) is a normal subgroup, \(G/H\) is the quotient group and the index is its order.

Examples
Properties
Generalizations

The relative index \([K : H \cap K]\) compares two subgroups \(H\) and \(K\) when neither contains the other. When \(H \le K\) it is the index of \(H\) in the group \(K\), the quantity that appears in the tower law.

In Mathlib

Mathlib defines the index of a subgroup as a natural number, the cardinality of the set of left cosets, with the convention that an infinite set has cardinality \(0\); so the index is \(0\) exactly when there are infinitely many cosets. Under this convention Lagrange's formula, the tower law and the divisibility statements hold for all groups without finiteness hypotheses: when some quantity is infinite, both sides of each equation are \(0\), and any number divides \(0\). Finite index is recorded by a separate property of the subgroup, which results such as the normal core bound assume. The relative index of \(H\) in \(K\) is defined for any two subgroups as the index of \(H \cap K\) in \(K\). The general results about the index of a subgroup come with additive versions for additive groups, stated for additive subgroups.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibSubgroup.index
Uses 2 · Used by 9
Statement usesGroup · Subgroup
Used byGalois correspondence · Class formula · Second isomorphism theorem · First Sylow theorem · Lagrange's theorem · Second Sylow theorem · Third Sylow theorem · Focal subgroup theorem · Schur–Zassenhaus theorem

ClassNormal subgroup#

A normal subgroup of a group is a subgroup that is carried into itself by every conjugation. Normal subgroups are exactly the subgroups by which one can divide: the cosets of a normal subgroup form a quotient group, and they are exactly the kernels of group homomorphisms. Much of the structure theory of groups, from the isomorphism theorems to the study of simple groups, is phrased in terms of them.

Definition

A subgroup \(N\) of a group \(G\) is normal if \(g n g^{-1} \in N\) for every \(n \in N\) and every \(g \in G\); one writes \(N \trianglelefteq G\). Applying the condition to \(g^{-1}\) as well shows that \(g N g^{-1} = N\) for every \(g\), so each conjugation maps \(N\) onto itself. Several reformulations are used interchangeably.

  • Cosets. For \(g \in G\), the left coset is \(gN = \{gn : n \in N\}\) and the right coset is \(Ng = \{ng : n \in N\}\). \(N\) is normal exactly when every left coset \(gN\) equals the right coset \(Ng\).
  • Products. If \(N\) is normal, then \(ab \in N\) implies \(ba \in N\), since \(ba\) is a conjugate of \(ab\). Conversely, a subgroup with this property is normal: for \(a = g^{-1}\) and \(b = gn\) one has \(ab = n \in N\) and \(ba = g n g^{-1}\).
  • Normalizer. The normalizer of \(N\), the set of \(g\) with \(g N g^{-1} = N\), is a subgroup of \(G\) containing \(N\); \(N\) is normal exactly when its normalizer is all of \(G\).
Examples
Kernels and quotients

If \(f \colon G \to K\) is a homomorphism and \(f(n) = e\), then \(f(g n g^{-1}) = f(g) f(n) f(g)^{-1} = f(g) f(g)^{-1} = e\); thus the kernel of a homomorphism is normal. Conversely, for a normal subgroup \(N\) the product of cosets \((aN)(bN) = abN\) is well defined, which makes the set of cosets into a group \(G/N\), and the kernel of the projection \(G \to G/N\) is \(N\). So the normal subgroups of \(G\) are precisely the kernels of homomorphisms out of \(G\). The first isomorphism theorem then identifies the image of a homomorphism with the quotient by its kernel, and the second and third isomorphism theorems describe quotients of subgroups and of quotients.

Properties

A group with exactly two normal subgroups, the trivial one and itself, is called simple. Every finite group is assembled from simple groups by repeated extensions; these composition factors are unique by the Jordan–Hölder theorem, and the finite simple groups themselves are listed by the classification of finite simple groups. Chains of subgroups, each normal in the next, underlie the definitions of solvable and nilpotent groups. The analogous notion for rings is a two-sided ideal, the kernel of a ring homomorphism.

In Mathlib

Mathlib defines normality as a property of a bundled subgroup, given by the conjugation condition above, and makes it a class so that normality of kernels, centers, intersections and other standard constructions is found automatically. The quotient of a group by any subgroup exists as the set of left cosets, but it receives its group structure only when the subgroup is normal. The statement that kernels are normal allows the target of the homomorphism to be any set with a multiplication and an identity element, not only a group. The additive version, for subgroups of additive groups, is stated separately and paired with the multiplicative class, so the additive form of each lemma about normal subgroups is generated automatically from the multiplicative one.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibSubgroup.Normal
Uses 2 · Used by 15
Statement usesGroup · Subgroup
Used byAbel-Ruffini theorem (one direction) · Galois correspondence · Abelianization · First isomorphism theorem · Nilpotent group · Presented group · Quotient group · Second isomorphism theorem · Simple group · Third isomorphism theorem · Alternating groups on 5 letters or more are simple · Classification of abelian simple groups · First Sylow theorem · Third Sylow theorem · Schur–Zassenhaus theorem

ClassSimple group#

A simple group is a nontrivial group with no normal subgroups other than the trivial subgroup and the group itself. Normal subgroups are exactly the kernels of homomorphisms, so a simple group has no quotient other than itself and the trivial group: every homomorphism out of it is either injective or sends everything to the identity. Simple groups play the role for finite groups that prime numbers play for integers. Every finite group is assembled from simple pieces, and the classification of finite simple groups determines all the finite ones.

Definition

A group \(G\) is simple if it has more than one element and its only normal subgroups are \(\{e\}\) and \(G\), where \(e\) is the identity element (the definition in Mathlib). Equivalently, \(G\) has exactly two normal subgroups. The requirement that \(G\) be nontrivial excludes the one-element group, just as \(1\) is not counted as a prime.

Simplicity is a property of the abstract group: a group isomorphic to a simple group is simple.

Examples
  • Groups of prime order. By Lagrange's theorem a group of prime order \(p\) has no subgroups at all besides \(\{e\}\) and itself, so every group of prime order is simple. These groups are cyclic, isomorphic to \(\mathbb{Z}/p\mathbb{Z}\).
  • Alternating groups. The alternating group \(A_n\) of even permutations of \(n\) letters is simple when \(n \ge 5\); see the article on that theorem. The group \(A_5\), of order \(60\), is the smallest simple group that is not abelian.
  • Projective special linear groups. For a field \(F\), the projective special linear group \(\mathrm{PSL}_n(F)\) is simple for every \(n \ge 2\), except for \(\mathrm{PSL}_2(\mathbb{F}_2)\) and \(\mathrm{PSL}_2(\mathbb{F}_3)\). For \(n = 2\) the condition is that \(F\) have a nonzero element whose square is not \(1\), which every field other than \(\mathbb{F}_2\) and \(\mathbb{F}_3\) has, and under that condition \(\mathrm{PSL}_2(F)\) is simple. Over finite fields these groups are among the finite groups of Lie type and give infinitely many finite simple groups; over infinite fields they give infinite simple groups.

Many familiar groups are not simple. The symmetric group \(S_n\) for \(n \ge 3\) contains \(A_n\) as a normal subgroup of index \(2\), the group \(A_4\) contains a normal subgroup of order \(4\), and the integers under addition contain the normal subgroup of even integers.

Properties
Composition series

A composition series of a group \(G\) is a chain of subgroups $\(\{e\} = G_0 \le G_1 \le \cdots \le G_k = G\)$ in which each \(G_{i-1}\) is normal in \(G_i\) and each quotient \(G_i / G_{i-1}\) is simple. Every finite group has one, obtained by repeatedly choosing maximal normal subgroups. The Jordan–Hölder theorem says that the list of quotients, called the composition factors, does not depend on the series up to order and isomorphism. In this sense the finite simple groups are the building blocks of all finite groups, although groups with the same composition factors need not be isomorphic: the cyclic group of order \(4\) and the Klein four-group both have two factors of order \(2\).

A finite group is solvable precisely when all of its composition factors are cyclic of prime order. The Feit–Thompson theorem, that every finite group of odd order is solvable, is equivalent to the statement that every nonabelian finite simple group has even order.

In Mathlib

Mathlib defines simplicity as a property that a group may or may not have, rather than as a new kind of structure. Nontriviality is part of the definition, so the one-element group is not simple, and the defining property is available for any simple group as the statement that each of its normal subgroups is trivial or the whole group. An additive version covers groups written additively, such as \(\mathbb{Z}/p\mathbb{Z}\). Statements about orders use a cardinality that is \(0\) for an infinite group; since \(0\) is not prime, the characterization of abelian simple groups by prime order also shows that no infinite abelian group is simple. The simplicity of alternating groups is stated for the alternating group on any finite set with at least five elements. Mathlib proves the simplicity of \(\mathrm{PSL}_2(F)\) through Iwasawa's criterion, in a form slightly more general than the usual one: a nontrivial group equal to its own commutator subgroup is simple if it acts faithfully on a set, every normal subgroup acting nontrivially acts transitively, and each point carries a commutative subgroup, moved by conjugation along with the point, with these subgroups together generating the group. Its result on projective special linear groups covers only \(n = 2\).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibIsSimpleGroup
Uses 2 · Used by 2
Statement usesGroup · Normal subgroup
Used byAlternating groups on 5 letters or more are simple · Classification of abelian simple groups

DefinitionSubgroup generated by a subset#

The subgroup generated by a subset \(S\) of a group \(G\) is the smallest subgroup of \(G\) that contains \(S\). It is written \(\langle S \rangle\), and its elements are exactly the finite products of elements of \(S\) and their inverses. Groups are often described by a few generators: a rotation and a reflection generate a dihedral group, for example, and many questions about the whole group, such as whether two homomorphisms out of it agree, reduce to questions about the generators.

Definition

Let \(G\) be a group and \(S \subseteq G\) any subset. The intersection of a family of subgroups is again a subgroup, so the intersection of all subgroups of \(G\) that contain \(S\) is a subgroup. It is the subgroup generated by \(S\):

\[\langle S \rangle = \bigcap \{\, H \le G : S \subseteq H \,\}.\]

By construction \(S\) is contained in \(\langle S \rangle\), and \(\langle S \rangle\) is the least subgroup with this property: for a subgroup \(K\), \(\langle S \rangle \le K\) holds exactly when \(S \subseteq K\). If \(\langle S \rangle = G\), one says that \(S\) generates \(G\), or that \(S\) is a set of generators of \(G\).

The intersection describes \(\langle S \rangle\) from above. From below, \(\langle S \rangle\) consists of the identity and all products

\[s_1^{\varepsilon_1} s_2^{\varepsilon_2} \cdots s_n^{\varepsilon_n}, \qquad s_i \in S,\ \varepsilon_i \in \{1, -1\}.\]

These products contain \(S\) and form a subgroup, since a product of two of them is another, and so is the inverse of one; every subgroup containing \(S\) contains all of them. Equivalently, writing \(S^{-1} = \{s^{-1} : s \in S\}\), \(\langle S \rangle\) coincides with the submonoid generated by \(S \cup S^{-1}\), the smallest subset containing \(S \cup S^{-1}\) and the identity and closed under products. In any monoid, the submonoid generated by a set consists of the finite products of elements of that set, the identity being the empty product; so the elements of \(\langle S \rangle\) are the finite products of elements of \(S \cup S^{-1}\). Minimality gives an induction principle: to show that a property holds on all of \(\langle S \rangle\), it suffices to check it on the elements of \(S\) and the identity, and to show it is preserved by products and inverses.

Examples
Properties

The subgroup generated by \(S\) need not be normal. The smallest normal subgroup containing \(S\), the normal closure, is the subgroup generated by all conjugates of elements of \(S\); normal closures also define a presented group, the quotient of a free group by the normal closure of its set of relators. The products of generators and their inverses are modelled abstractly by the free group on \(S\): for every group \(G\) and map \(S \to G\) whose image generates \(G\), the induced homomorphism from the free group on \(S\) to \(G\) is surjective. Schreier's lemma produces generators for a subgroup from generators of the whole group and a choice of coset representatives. The same pattern, the least substructure containing a given set, defines the span of a set of vectors in a vector space; see generating sets.

In Mathlib

Mathlib defines the subgroup generated by a set as the infimum of all subgroups containing it in the complete lattice of subgroups, which is the intersection above; the description by products is a theorem rather than the definition. The subgroup is a bundled structure carrying its set of elements and the proofs of the subgroup axioms. The facts that the closure contains the set, is least among subgroups containing it, and returns every subgroup unchanged (\(\langle H \rangle = H\)) are packaged as a Galois insertion between subsets and subgroups, from which monotonicity and the formulas for unions follow. An additive version is generated automatically for additive groups, so the same results hold for subgroups of \(\mathbb{Z}\) or of any group written additively. Finite generation is defined through generation as a semigroup by a finite set, which for a group agrees with the textbook notion.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibSubgroup.closure
Uses 2 · Used by 9
Statement usesGroup · Subgroup
Used byAbelianization · Cyclic group · Presented group · Schreier's lemma · Alternating groups on 5 letters or more are simple · Classification of abelian simple groups · Structure of finitely generated abelian groups · Focal subgroup theorem · Decomposition of an orthogonal transformation as a product of reflections

InstanceQuotient group#

A quotient group is the group obtained from a group \(G\) by collapsing a normal subgroup \(N\) to the identity: its elements are the cosets of \(N\), multiplied by multiplying representatives. The construction is the standard way to discard information in a controlled manner, as when the integers are reduced modulo \(n\). Every surjective homomorphism of groups is, up to isomorphism, the projection onto a quotient group, which makes quotients one of the main tools for studying a group through its images.

Definition

Let \(G\) be a group and \(N\) a normal subgroup of \(G\), written \(N \trianglelefteq G\). The left cosets \(gN\) partition \(G\), and two elements \(a, b\) lie in the same coset exactly when \(a^{-1}b \in N\). The set of cosets is written \(G/N\). Its multiplication is

\[(aN)(bN) = (ab)N,\]

and with this operation \(G/N\) is a group: the coset of a product is the product of the cosets, the identity is the coset \(N\) itself, and the inverse of \(aN\) is \(a^{-1}N\).

The one point to check is that the product does not depend on the chosen representatives. If \(a' = an\) and \(b' = bm\) with \(n, m \in N\), then \(a'b' = ab\,(b^{-1}nb)\,m\), and \(b^{-1}nb\) lies in \(N\) because \(N\) is normal, so \(a'b'N = abN\). Normality cannot be dropped: if the cosets of a subgroup \(H\) carry a group structure for which \(g \mapsto gH\) is a homomorphism, then \(H\) is the kernel of that homomorphism, and kernels are always normal.

The map \(\pi \colon G \to G/N\), \(g \mapsto gN\), is a homomorphism, the canonical projection; equivalently, \(gN\) is the identity of \(G/N\) if and only if \(g \in N\). So the normal subgroups of \(G\) are precisely the kernels of homomorphisms out of \(G\).

Examples
Properties

The same construction applies to other algebraic structures: a ring modulo an ideal gives a quotient ring, and a module modulo a submodule gives a quotient module. When \(N\) is not normal the cosets still form a set on which \(G\) acts by left multiplication, but the rule \((aN)(bN) = (ab)N\) is no longer well defined, so they do not form a quotient group. A presented group is a quotient of a free group by the normal subgroup generated by the relations.

In Mathlib

Mathlib defines the set of left cosets \(G/H\) for every subgroup \(H\), normal or not, as the quotient of \(G\) by the relation "\(a^{-1}b \in H\)". The group structure is attached to this type as an instance whenever Mathlib knows that \(H\) is normal, so the same notation serves both for the coset space of an arbitrary subgroup and for the quotient group. For commutative groups a separate instance supplies the abelian group structure with no normality hypothesis. The construction passes through congruence relations: a normal subgroup determines the congruence "\(a\) and \(b\) lie in the same coset", and the group structure is the one carried by the quotient by that congruence. The universal property allows the target to be any monoid, not only a group. Additive versions, such as \(\mathbb{Z}/n\mathbb{Z}\), are generated automatically from the multiplicative ones, and the additive circle is defined for any period in any additive commutative group. Orders are counted with a cardinality that gives \(0\) for an infinite set, so the counting identity above holds for all groups.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibQuotientGroup.Quotient.group
Uses 4 · Used by 12
Statement usesGroup · Subgroup · Normal subgroup · Group morphism
Used byFiniteness of the class number · Galois correspondence · Abelianization · First isomorphism theorem · Nilpotent group · Presented group · Second isomorphism theorem · Third isomorphism theorem · First Sylow theorem · Structure of finitely generated abelian groups · Quotient ring · Dirichlet's unit theorem

DefinitionFirst isomorphism theorem#

The first isomorphism theorem says that a group homomorphism \(\varphi \colon G \to H\) identifies the quotient of \(G\) by the kernel of \(\varphi\) with the image of \(\varphi\). Every homomorphism therefore factors as a surjection onto a quotient followed by an isomorphism and an inclusion, and the question of which groups are homomorphic images of \(G\) becomes the question of which normal subgroups \(G\) has. The theorem is also known as the fundamental theorem on homomorphisms, and it is the first of three isomorphism theorems, together with the second and the third.

Statement

Let \(\varphi \colon G \to H\) be a homomorphism of groups, with kernel \(K = \{ g \in G : \varphi(g) = e \}\) and image \(\varphi(G)\), a subgroup of \(H\). The kernel is a normal subgroup of \(G\), so the quotient group \(G/K\) is defined, and the map

\[G/K \to \varphi(G), \qquad gK \mapsto \varphi(g)\]

is a well-defined isomorphism of groups. When \(\varphi\) is surjective this reads \(G/\ker\varphi \cong H\).

Proof

Write \(\psi(gK) = \varphi(g)\). Two cosets \(gK\) and \(hK\) are equal exactly when \(g^{-1}h \in K\), that is, when \(\varphi(g)^{-1}\varphi(h) = e\), that is, when \(\varphi(g) = \varphi(h)\). Read from left to right this says \(\psi\) is well defined; read from right to left it says \(\psi\) is injective. Since multiplication of cosets is \((gK)(hK) = ghK\) and \(\varphi\) preserves products, \(\psi\) is a homomorphism, and it maps onto \(\varphi(G)\) by construction. Well-definedness and the homomorphism property are a special case of a more general fact: a homomorphism that is trivial on a normal subgroup \(N\) descends to a homomorphism on \(G/N\).

Examples
Consequences
Generalizations

The same argument works wherever a structure has a notion of quotient by a "kernel". For rings, the quotient of a ring by the kernel of a ring homomorphism is isomorphic to its image (see the first isomorphism theorem for rings). For modules, the quotient by the kernel of a linear map is linearly isomorphic to its range, which for vector spaces yields the rank–nullity theorem. At the bottom of the hierarchy, any function from a set \(X\) induces an equivalence relation on \(X\), and the set of its classes is in bijection with the image. In universal algebra and category theory the theorem takes the form of a factorization of a morphism through its image.

In Mathlib

Mathlib gives the theorem as a construction rather than an existence statement: it builds a specific isomorphism of groups from the quotient by the kernel to the image, where the image is regarded as a group in its own right, a subgroup of the codomain. The isomorphism is assembled from a bijective homomorphism, so its inverse is not given by an explicit formula and the definition is marked noncomputable. A computable variant of the surjective case, an isomorphism onto the whole codomain, exists for a homomorphism equipped with a right inverse. The version for additive groups is generated automatically from the multiplicative one. In the counting statements, Mathlib assigns size \(0\) to an infinite set and index \(0\) to a subgroup of infinite index, so the statements hold for all groups without finiteness hypotheses. For an infinite group the statements still say something: the index of the kernel is infinite exactly when the image is, and the product formula says that the kernel or the image is infinite. Only the divisibility statement becomes vacuous, since every number divides \(0\).

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibQuotientGroup.quotientKerEquivRange
Uses 4 · Used by 4
Statement usesGroup morphism · Normal subgroup · Quotient group · Subgroup
Used bySecond isomorphism theorem · Third isomorphism theorem · Structure of finitely generated abelian groups · General linear group (Classical automorphism groups)

DefinitionSecond isomorphism theorem#

The second isomorphism theorem describes what happens when a subgroup \(H\) of a group \(G\) meets a normal subgroup \(N\): the product \(HN\) is a subgroup, and the quotient \(HN/N\) is isomorphic to \(H/(H \cap N)\). It lets one compute a quotient of a large subgroup by passing to a quotient of a smaller one, and it is a basic tool in the study of composition series. Because \(H \cap N\) lies in both \(H\) and \(N\), which both lie in \(HN\), the four subgroups form a diamond in the lattice of subgroups, and the result is also called the diamond isomorphism theorem.

Statement

Let \(G\) be a group, \(H\) a subgroup of \(G\) and \(N\) a normal subgroup of \(G\). Then:

  1. The set \(HN = \{hn : h \in H,\ n \in N\}\) is a subgroup of \(G\); in fact it is the subgroup generated by \(H\) and \(N\).
  2. \(N\) is normal in \(HN\), and \(H \cap N\) is normal in \(H\).
  3. The map \(h(H \cap N) \mapsto hN\) is a well-defined isomorphism of groups $\(H/(H \cap N) \cong HN/N.\)$

In terms of indices, the index of \(N\) in \(HN\) equals the index of \(H \cap N\) in \(H\): $\([HN : N] = [H : H \cap N].\)$

Examples
  • Integers. In the additive group \(\mathbb{Z}\), take \(H = a\mathbb{Z}\) and \(N = b\mathbb{Z}\) for positive integers \(a\) and \(b\). Every subgroup of \(\mathbb{Z}\) is normal, \(H \cap N = \operatorname{lcm}(a,b)\mathbb{Z}\) and \(H + N = \gcd(a,b)\mathbb{Z}\). The additive form of the theorem gives \(a\mathbb{Z}/\operatorname{lcm}(a,b)\mathbb{Z} \cong \gcd(a,b)\mathbb{Z}/b\mathbb{Z}\). Comparing orders, \(\operatorname{lcm}(a,b)/a = b/\gcd(a,b)\), which is the identity \(\gcd(a,b)\operatorname{lcm}(a,b) = ab\).
  • Symmetric group. In \(S_4\) let \(N\) be the Klein four-group of double transpositions together with the identity, which is normal, and let \(H \cong S_3\) be the stabilizer of the point \(4\). No double transposition fixes a point, so \(H \cap N\) is trivial. Then the products \(hn\) are pairwise distinct, since \(hn = h'n'\) gives \(h'^{-1}h = n'n^{-1} \in H \cap N\), so \(|HN| = 6 \cdot 4 = 24\) forces \(HN = S_4\). The theorem yields \(S_4/N \cong S_3\).
  • Trivial cases. If \(H \le N\) both sides are trivial groups. If \(H \cap N\) is trivial, \(H\) embeds isomorphically in \(G/N\) as the image \(HN/N\).
Consequences
  • Product formula. For a finite group, write \([HN : N] = |HN|/|N|\) and \([H : H \cap N] = |H|/|H \cap N|\), using Lagrange's theorem in its counting form. The index identity then becomes $\(|HN|\,|H \cap N| = |H|\,|N|.\)$
  • Divisibility of indices. When \([G : N]\) is finite, \(HN/N\) is a subgroup of the finite group \(G/N\), so by Lagrange's theorem the index of \(H \cap N\) in \(H\) divides the index of \(N\) in \(G\). Mathlib records that the index of \(N \cap H\) in \(H\) divides the index of \(N\) in \(G\) for every normal \(N\), with its convention that an infinite index is \(0\), which every integer divides.
  • Composition series. If \(N_1\) and \(N_2\) are distinct maximal normal subgroups of \(G\), then \(N_1 N_2 = G\) and the theorem gives \(G/N_1 \cong N_2/(N_1 \cap N_2)\). This step drives the usual inductive proof of the Jordan–Hölder theorem.
Proof

Since \(N\) is normal, \(hN = Nh\) for every \(h \in G\), so \(HN = NH\); hence \(HN\) is closed under products and inverses and is a subgroup, and \(N\), being normal in \(G\), is normal in \(HN\). Define \(\varphi \colon H \to HN/N\) by \(\varphi(h) = hN\); it is the inclusion of \(H\) in \(HN\) followed by the quotient map \(HN \to HN/N\), so it is a homomorphism. It is surjective: an element of \(HN/N\) has the form \(hnN\) with \(h \in H\) and \(n \in N\), and \(hnN = hN = \varphi(h)\). Its kernel consists of the \(h \in H\) with \(hN = N\), that is, \(h \in N\); so the kernel is \(H \cap N\), which is therefore normal in \(H\). The first isomorphism theorem, in the form a surjective homomorphism induces an isomorphism from the quotient by its kernel onto its target, now gives \(H/(H \cap N) \cong HN/N\). Taking cardinalities of the two quotients gives the index identity.

Generalizations

The argument uses only that each element of \(H\) conjugates \(N\) into itself, so normality of \(N\) in all of \(G\) is more than needed. It suffices that \(H\) lies in the normalizer of \(N\), and Mathlib states the theorem under exactly that hypothesis; the normal case follows because every subgroup lies in the normalizer of a normal subgroup.

Analogous statements hold for rings and ideals, for modules, and more generally for groups with operators. For submodules \(P\) and \(Q\) of a module over a ring, \(P/(P \cap Q)\) is isomorphic to \((P + Q)/Q\) as modules; here every submodule is a valid kernel, so no normality condition appears. The other isomorphism theorems are the first and the third isomorphism theorem.

In Mathlib

Mathlib works inside the lattice of subgroups of \(G\). The product \(HN\) appears as the join of \(H\) and \(N\), the smallest subgroup containing both, and \(H \cap N\) appears as \(N\) pulled back to a subgroup of \(H\); likewise \(N\) is viewed as a subgroup of the join. The theorem is a bundled isomorphism of groups, built by choice from the first isomorphism theorem rather than by an explicit formula for its inverse. The additive version, for additive groups such as \(\mathbb{Z}\), is generated automatically from the multiplicative one; the automatic translation also turns the word Prod in the name into Sum, so the additive name differs from the multiplicative one by more than its namespace. The index identity uses Mathlib's relative index, which is \(0\) when the index is infinite, so it holds for every group, finite or not.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibQuotientGroup.quotientInfEquivProdNormalQuotient
Uses 6
Statement usesSubgroup · Normal subgroup · Quotient group · Index of a subgroup
Proof usesFirst isomorphism theorem · Group morphism

DefinitionThird isomorphism theorem#

The third isomorphism theorem says that taking a quotient of a quotient group gives nothing new: if \(N \le M\) are normal subgroups of a group \(G\), then \(M/N\) is a normal subgroup of \(G/N\), and dividing \(G/N\) by it gives \(G/M\). In symbols, \((G/N)/(M/N) \cong G/M\), so the quotient by \(N\) can be removed from both sides. Together with the correspondence between subgroups of \(G/N\) and subgroups of \(G\) containing \(N\), it shows that every quotient of \(G/N\) is already a quotient of \(G\). This lets an argument by induction on the order of a finite group, or the construction of a composition series, replace a quotient of a quotient group by a single quotient of the original group.

Statement

Let \(G\) be a group and let \(N\) and \(M\) be normal subgroups of \(G\) with \(N \le M\). Write \(M/N\) for the image of \(M\) under the quotient map \(G \to G/N\), that is, the set of cosets \(mN\) with \(m \in M\). Then:

  1. \(M/N\) is a normal subgroup of \(G/N\).
  2. The rule \((gN)(M/N) \mapsto gM\) is a well-defined map and an isomorphism of groups $\((G/N)/(M/N) \cong G/M.\)$
Examples
  • Integers. Let \(m\) and \(n\) be positive integers with \(m \mid n\). In the additive group \(\mathbb{Z}\), every subgroup is normal and \(n\mathbb{Z} \le m\mathbb{Z}\). The additive form of the theorem gives $\((\mathbb{Z}/n\mathbb{Z})/(m\mathbb{Z}/n\mathbb{Z}) \cong \mathbb{Z}/m\mathbb{Z}.\)$ For \(n = 12\) and \(m = 4\): the subgroup of \(\mathbb{Z}/12\mathbb{Z}\) generated by the class of \(4\) has three elements, and the quotient by it is cyclic of order \(4\).
  • Symmetric group. In \(S_4\), the Klein four-group \(V\) (the identity and the three double transpositions) is normal and lies in the alternating group \(A_4\), which is also normal. Here \(S_4/V \cong S_3\) and \(A_4/V\) is its subgroup of order \(3\), so the theorem gives \((S_4/V)/(A_4/V) \cong S_4/A_4\), a group of order \(2\).
  • Extreme cases. For \(M = G\) both sides are trivial. For \(N\) trivial, \(G/N\) is canonically isomorphic to \(G\), with \(M/N\) corresponding to \(M\), and under this identification the statement reduces to \(G/M \cong G/M\).
Proof

Since \(N \le M\), the rule \(gN \mapsto gM\) is well defined: if \(gN = g'N\) then \(g^{-1}g' \in N \subseteq M\), so \(gM = g'M\). It is a homomorphism \(\varphi \colon G/N \to G/M\), and it is surjective. Its kernel consists of the cosets \(gN\) with \(gM = M\), that is, with \(g \in M\); so the kernel is exactly \(M/N\), which is therefore normal in \(G/N\). The first isomorphism theorem, in the form a surjective homomorphism induces an isomorphism from the quotient by its kernel onto its target, turns \(\varphi\) into the isomorphism \((G/N)/(M/N) \cong G/M\).

Consequences
Generalizations

Analogues hold for any algebraic structure whose quotients are formed by congruences; for modules and rings, congruences correspond to submodules and ideals. Mathlib proves several instances.

The other isomorphism theorems are the first and the second isomorphism theorem.

In Mathlib

Mathlib states the theorem with \(M/N\) taken as the image of \(M\) under the quotient homomorphism \(G \to G/N\), which keeps it a subgroup of \(G/N\); that this image is normal is recorded once and found automatically wherever it is needed. Both \(N\) and \(M\) must be normal in \(G\), and the inclusion \(N \le M\) is passed as a hypothesis. The result is a bundled isomorphism of groups. Unlike the second isomorphism theorem, it is not obtained from the first isomorphism theorem by a choice of preimages: Mathlib writes down both directions, \((gN)(M/N) \mapsto gM\) and its inverse \(gM \mapsto (gN)(M/N)\), and checks that they are mutually inverse. The additive version, for additive groups such as \(\mathbb{Z}\), is generated automatically from the multiplicative one. The index identity counts an infinite index as \(0\), so it holds for every group, finite or not.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibQuotientGroup.quotientQuotientEquivQuotient
Uses 4
Statement usesNormal subgroup · Quotient group · Group morphism
Proof usesFirst isomorphism theorem

DefinitionAbelianization#

The abelianization of a group \(G\) is the largest abelian quotient of \(G\): the quotient obtained by imposing the relations \(gh = hg\) for all elements \(g, h\) and no others. It is written \(G^{\mathrm{ab}}\). Every homomorphism from \(G\) to an abelian group passes through it, so it carries exactly the information about \(G\) that is detected by homomorphisms to abelian groups. It appears throughout algebra and topology, from the sign of a permutation to the first homology group of a space.

Definition

For elements \(g, h\) of \(G\) the commutator is \([g, h] = g h g^{-1} h^{-1}\); it equals the identity exactly when \(g\) and \(h\) commute. The commutator subgroup \([G, G]\) is the subgroup generated by all commutators (the commutator subgroup is the closure of the set of commutators). It is a normal subgroup, indeed a characteristic one, since every automorphism of \(G\) sends commutators to commutators. The abelianization is the quotient group

\[G^{\mathrm{ab}} = G / [G, G],\]

which is the abelianization of \(G\), together with the quotient map \(G \to G^{\mathrm{ab}}\), a surjective homomorphism whose kernel is the commutator subgroup.

The quotient is abelian because the image of \(ghg^{-1}h^{-1}\) is the identity, so the images of \(g\) and \(h\) commute. More is true: for a normal subgroup \(N\) of \(G\), the quotient \(G/N\) is abelian if and only if \(N\) contains \([G, G]\). So \([G, G]\) is the smallest normal subgroup with abelian quotient, and \(G^{\mathrm{ab}}\) is the largest abelian quotient of \(G\).

Universal property

Let \(A\) be an abelian group and \(f \colon G \to A\) a homomorphism. Since \(A\) is abelian, \(f\) sends every commutator to the identity, so the commutator subgroup lies in the kernel of \(f\). Hence \(f\) factors through the quotient map: there is a homomorphism \(\bar f \colon G^{\mathrm{ab}} \to A\) with \(\bar f(g[G, G]) = f(g)\), and it is the only homomorphism with this property. In other words, homomorphisms \(G \to A\) correspond bijectively to homomorphisms \(G^{\mathrm{ab}} \to A\), the correspondence being composition with the quotient map. This property characterizes \(G^{\mathrm{ab}}\) up to unique isomorphism, and it is the usual way to compute with it.

Examples
Properties

In topology, the first homology group of a path-connected space is the abelianization of its fundamental group; this is the first case of the Hurewicz theorem. In number theory, a topological variant matters: the quotient of the absolute Galois group of a field by the closure of its commutator subgroup is the Galois group of the maximal abelian extension of the field inside a fixed separable closure, the object described by class field theory. Abelianization is also the first step of the nilpotent and solvable hierarchies, which measure how far a group is from being abelian.

In Mathlib

Mathlib defines the abelianization of a group as its quotient by the commutator subgroup, where the commutator subgroup is defined as the commutator of the whole group with itself and then shown to equal the subgroup generated by the commutator elements, with the convention \([g, h] = g h g^{-1} h^{-1}\) (some texts use \(g^{-1} h^{-1} g h\), which generates the same subgroup). The universal property is packaged as a bijection between homomorphisms out of \(G\) and homomorphisms out of \(G^{\mathrm{ab}}\), for any target group whose multiplication is commutative. Mathlib's statement that the commutator subgroup of \(S_n\) is \(A_n\) assumes at least five letters, though it proves the inclusion of the commutator subgroup in \(A_n\) for every \(n\). The free abelian group on a type is defined in Mathlib as the abelianization of the free group, written additively.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibGroup.Abelianization
Uses 5
Statement usesGroup · Normal subgroup · Quotient group · Subgroup generated by a subset · Group morphism

DefinitionFree group#

The free group on a set \(S\) is the group whose elements are the words in the letters of \(S\) and their formal inverses, with no relations imposed beyond those that every group must satisfy. It is the most general group generated by a copy of \(S\): every map from \(S\) into a group extends to a homomorphism in exactly one way. Because of this, every group is a quotient of a free group, and describing a group by generators and relations amounts to describing such a quotient.

Definition

Fix a set \(S\) and introduce, for each \(s \in S\), a new symbol \(s^{-1}\). A word is a finite sequence of letters, each of the form \(s\) or \(s^{-1}\). An elementary reduction deletes two adjacent letters of the form \(s\,s^{-1}\) or \(s^{-1}s\), and two words are called equivalent when one can be turned into the other by a finite chain of reductions and their reverses. The free group \(F(S)\) is the set of equivalence classes, with multiplication given by concatenating words. The empty word is the identity, and the inverse of a word is obtained by reversing it and inverting each letter. Each \(s \in S\) gives the element of \(F(S)\) represented by the one-letter word \(s\), and distinct elements of \(S\) give distinct elements of \(F(S)\).

A word is reduced if no elementary reduction applies to it. Reduction is confluent: if a word reduces to two words, both of these reduce to a common word. It follows that every equivalence class contains exactly one reduced word, so an element of \(F(S)\) can be named by its reduced word: the word obtained by reducing as far as possible is reduced, and distinct elements have distinct reduced words. For instance, with \(S = \{a, b\}\), the word \(a\,b\,b^{-1}a^{-1}b\) reduces to \(b\).

Universal property

Let \(G\) be any group and \(f \colon S \to G\) any map. Then there is a unique homomorphism \(\varphi \colon F(S) \to G\) that sends each generator \(s\) to \(f(s)\); it sends a word \(s_1^{\varepsilon_1} \cdots s_n^{\varepsilon_n}\), with each \(\varepsilon_i = \pm 1\), to the product \(f(s_1)^{\varepsilon_1} \cdots f(s_n)^{\varepsilon_n}\). In other words, restricting to the generators is a bijection between homomorphisms \(F(S) \to G\) and maps \(S \to G\). In particular, two homomorphisms out of \(F(S)\) that agree on the generators are equal. This property determines \(F(S)\) up to isomorphism. A group \(G\) is called free when it is isomorphic to \(F(S)\) for some set \(S\); the image of \(S\) in \(G\) under such an isomorphism is then called a basis of \(G\).

Examples
Properties
In Mathlib

Mathlib defines the free group on an arbitrary type, which may be infinite. A word is a list of pairs, each consisting of a generator and a flag that records whether the letter is the generator or its inverse, and the free group is the quotient of the type of such lists by the equivalence relation generated by a single elementary reduction. Computing the reduced word of an element assumes that equality of generators is decidable, which is always available classically. The property of being free is recorded separately: a group is free when it admits a free basis, meaning an isomorphism with the free group on some type, and the Nielsen–Schreier theorem is stated for this property. Torsion-freeness is obtained as a consequence of the stronger fact that free groups have unique roots, meaning that taking \(n\)-th powers is injective for every positive integer \(n\), which Mathlib proves for every free group through an unnamed instance. An additive copy of the whole theory, the free additive group, is generated automatically; despite its name it is not commutative once there are two generators.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibFreeGroup
Uses 2 · Used by 2
Statement usesGroup · Group morphism
Used byPresented group · Nielsen–Schreier theorem

DefinitionPresented group#

A presented group is a group described by a set of generators together with a set of relations that those generators must satisfy, and by nothing else. Writing \(\langle S \mid R \rangle\) for the group with generators \(S\) and relations \(R\) gives a compact, finite description of many infinite groups, and it is the standard way groups arise in combinatorial group theory and topology, for instance as fundamental groups of spaces built from cells. Every group has a presentation, so the notion is fully general; the price is that a presentation can hide basic facts about its group, such as whether two words name the same element.

Definition

Let \(S\) be a set and let \(F(S)\) be the free group on \(S\), whose elements are reduced words in the letters of \(S\) and their inverses. A set \(R \subseteq F(S)\) of words is called a set of relators. Let \(N\) be the smallest normal subgroup of \(F(S)\) containing \(R\), its normal closure, which is the subgroup generated by all conjugates \(w r w^{-1}\) with \(r \in R\) and \(w \in F(S)\). The presented group is the quotient

\[\langle S \mid R \rangle = F(S)/N,\]

which is the group with generators \(S\) and relators \(R\).

A relation written as an equation \(u = v\) between two words stands for the relator \(u v^{-1}\); the two descriptions give the same group. Each generator \(s \in S\) has an image in the quotient, and these images generate the whole group. Every relator becomes the identity, and more precisely a word represents the identity exactly when it lies in the normal closure \(N\): the relators and their consequences are the only identities imposed.

A group \(G\) has the presentation \(\langle S \mid R \rangle\) when \(G\) is isomorphic to it. A presentation is finite when \(S\) and \(R\) are both finite, and a group admitting a finite presentation is called finitely presented.

Examples
  • Free groups. With no relators, \(\langle S \mid \varnothing \rangle\) is the free group \(F(S)\) itself.
  • Cyclic groups. For \(n \ge 1\), the group \(\langle a \mid a^n \rangle\) is cyclic of order \(n\), and \(\langle a \mid \varnothing \rangle\) is the infinite cyclic group \(\mathbb{Z}\) (see cyclic group).
  • Free abelian group of rank two. The single relator \(a b a^{-1} b^{-1}\) forces the two generators to commute, so \(\langle a, b \mid a b a^{-1} b^{-1} \rangle \cong \mathbb{Z} \times \mathbb{Z}\).
  • Dihedral groups. The symmetry group of a regular \(n\)-gon has the presentation \(\langle r, s \mid r^n, s^2, (s r)^2 \rangle\), with \(r\) a rotation and \(s\) a reflection; it has order \(2n\).
  • Coxeter groups. Given a symmetric matrix \((m_{ij})\) of positive integers with \(m_{ii} = 1\) and \(m_{ij} \ge 2\) for \(i \ne j\), the group \(\langle s_i \mid (s_i s_j)^{m_{ij}} \rangle\) is the Coxeter group of the matrix; Mathlib also allows the entry \(0\), meaning that no relation is imposed on \(s_i s_j\). Finite reflection groups and the symmetric groups arise this way.
Properties

Universal property. Let \(G\) be a group and \(f \colon S \to G\) a function such that every relator evaluates to the identity when each letter \(s\) is replaced by \(f(s)\). Then \(f\) extends to a group homomorphism \(\langle S \mid R \rangle \to G\) that sends each generator \(s\) to \(f(s)\), and this extension is the only homomorphism that does so. In words, a homomorphism out of a presented group is the same as an assignment of elements to the generators that respects the relations. This is the main tool for working with presentations: to define a group morphism one only needs to check that each relator is sent to the identity (finitely many checks when the presentation is finite). To prove that a group \(G\) has a given presentation, one typically uses this property to build a homomorphism onto \(G\) and then shows that it is injective, or builds an inverse by other means.

Every group is presented. If \(G\) is any group, take \(S\) to be a generating set, map \(F(S)\) onto \(G\), and take \(R\) to be the kernel of this map. By the first isomorphism theorem \(G \cong \langle S \mid R \rangle\). More generally, if a family of elements generates \(G\) and a set of words normally generates the kernel of the induced map from the free group onto \(G\), then \(G\) is isomorphic to the group presented by those generators and words. In particular every finitely presented group is isomorphic to a presented group with finitely many generators and relators.

Constructions. Renaming the generators along a bijection, and the relators with them, gives an isomorphic presented group. The free product of \(\langle S_1 \mid R_1 \rangle\) and \(\langle S_2 \mid R_2 \rangle\) is presented by the disjoint union of the generators and the union of the relators. Adding relators to a presentation gives a quotient of the original group.

Algorithmic questions. A presentation determines its group, but extracting information from it can be impossible in general. There are finitely presented groups in which no algorithm decides whether a given word represents the identity, and no algorithm decides, given finite presentations, whether two of them define isomorphic groups or whether one defines the trivial group. Some invariants are computable: the abelianization can be read off a finite presentation by linear algebra over \(\mathbb{Z}\) (Smith normal form), but it forgets most of the group.

In Mathlib

Mathlib builds the presented group from a type of generators, which may be infinite, and an arbitrary set of elements of the free group on that type, read as relators rather than as equations. The group is defined directly as the quotient of the free group by the normal closure of the relators, so it is a concrete group rather than a property of some other group; the statement that a given group has a presentation is recorded separately, as a structure carrying the generating family, the relators and a proof that the relators normally generate the kernel. Finite presentability is a property of a group, phrased through a surjection from a free group on finitely many generators whose kernel is the normal closure of a finite set. The construction itself has a counterpart for additive groups, the presented additive group.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibPresentedGroup
Uses 4
Statement usesFree group · Normal subgroup · Quotient group · Subgroup generated by a subset

TheoremSchreier's lemma#

Schreier's lemma gives an explicit set of generators for a subgroup of a group, built from a set of generators of the whole group and one chosen representative from each coset of the subgroup. Its best-known consequence is that a subgroup of finite index in a finitely generated group is itself finitely generated. The generators it produces, often called Schreier generators, are used in the study of subgroups of free groups and in algorithms of computational group theory such as the Schreier–Sims algorithm.

Statement

Let \(G\) be a group, \(H\) a subgroup of \(G\), and \(S\) a subset that generates \(G\), meaning that the subgroup generated by \(S\) is all of \(G\). A right transversal of \(H\) is a subset \(R \subseteq G\) that meets every right coset \(Hg\) in exactly one element; equivalently, every element of \(G\) can be written in exactly one way as \(hr\) with \(h \in H\) and \(r \in R\) (in this case \(H\) and \(R\) are complements). Such a transversal always exists and can be chosen to contain the identity. For \(g \in G\) write \(\overline{g}\) for the element of \(R\) lying in the coset \(Hg\).

Schreier's lemma says that if \(1 \in R\), then

\[H = \left\langle\, rs\,\overline{rs}^{\,-1} \;:\; r \in R,\ s \in S \,\right\rangle,\]

that is, the elements \(rs\,\overline{rs}^{\,-1}\) generate \(H\). Each such element lies in \(H\), because \(g\) and \(\overline{g}\) lie in the same right coset of \(H\).

Examples
  • Integers. Take \(G = \mathbb{Z}\) under addition, \(S = \{1\}\), \(H = n\mathbb{Z}\) for some \(n \ge 1\), and \(R = \{0, 1, \dots, n-1\}\). Written additively, the generators are \(r + 1 - \overline{r+1}\). For \(r < n-1\) this is \(0\), and for \(r = n-1\) it is \(n\), so the lemma recovers the fact that \(n\mathbb{Z}\) is generated by \(n\).
  • A subgroup of a free group. Let \(G\) be the free group on \(a\) and \(b\), with \(S = \{a, b\}\), and let \(H\) consist of the words in which the exponents of \(a\) add up to an even number. Then \(H\) has index \(2\) and \(R = \{1, a\}\) is a right transversal. The four generators are \(1\), \(b\), \(a^2\) and \(aba^{-1}\), so \(H\) is generated by \(b\), \(a^2\) and \(aba^{-1}\).

The generating set often contains the identity and repeated or redundant elements, so it is usually far from the smallest possible generating set.

Consequences
  • Counting generators. If \(S\) is finite and \(H\) has finite index \(n\), the lemma uses at most \(n\,|S|\) generators. Hence \(H\) can be generated by at most \([G : H]\,|S|\) elements (formal statement).
  • Finite generation. A subgroup of finite index in a finitely generated group is finitely generated. The finite index hypothesis matters: the free group on two generators has subgroups that are not finitely generated, such as the normal subgroup generated by \(b\).
  • Rank. If \(G\) is finitely generated and \(d(G)\) is the least number of generators of \(G\), then \(d(H) \le [G : H]\,d(G)\) for every subgroup \(H\) of finite index (formal statement).
  • Finitely many commutators. If a group has only finitely many commutators \(xyx^{-1}y^{-1}\), then its commutator subgroup is finite, and its order is bounded by a function of the number of commutators. The proof passes to a finitely generated subgroup with the same commutators and applies the rank bound above to the intersection of its center with its commutator subgroup. The result is closely related to Schur's theorem, which says that a group whose center has finite index has a finite commutator subgroup.
Proof

Let \(U\) be the set of elements \(rs\,\overline{rs}^{\,-1}\) and \(K\) the subgroup it generates. Every element of \(U\) lies in \(H\), so \(K \le H\).

The main step is that every element of \(G\) is a product \(kr\) with \(k \in K\) and \(r \in R\). The set \(KR\) contains \(1 = 1 \cdot 1\). It is closed under multiplication on the right by each \(s \in S\), since

\[krs = k\,\bigl(rs\,\overline{rs}^{\,-1}\bigr)\,\overline{rs}.\]

It is also closed under multiplication on the right by \(s^{-1}\): put \(r' = \overline{rs^{-1}}\). Then \(r's\) lies in the coset \(Hr\), so \(\overline{r's} = r\) and \(r'sr^{-1} \in U\), and

\[krs^{-1} = k\,\bigl(r'sr^{-1}\bigr)^{-1}\,r'.\]

Since every element of \(G\) is a product of elements of \(S\) and their inverses, \(KR = G\).

Finally let \(h \in H\) and write \(h = kr\). Then \(r = k^{-1}h\) lies in \(H\), the coset \(H \cdot 1\). That coset meets \(R\) only in \(1\), so \(r = 1\) and \(h = k \in K\). Hence \(K = H\).

The Nielsen–Schreier theorem states that every subgroup of a free group is free. When \(G\) is free on \(S\) and the transversal is chosen more carefully, as a so-called Schreier transversal, the nontrivial Schreier generators form a free basis of \(H\). This leads to the Schreier index formula: a subgroup of index \(n\) in a free group of rank \(k\) is free of rank \(n(k-1) + 1\), as in the free group example above, where \(n = k = 2\) gives rank \(3\). In finite group theory the Schreier generators of a point stabilizer in a permutation group underlie the Schreier–Sims algorithm.

In Mathlib

Mathlib states the lemma for an arbitrary group, with no finiteness assumptions on the generating set, the subgroup or its index. The transversal is expressed through Mathlib's general notion of complementary subsets, where every element factors uniquely as an element of the subgroup times an element of the transversal, and the chosen representative of each element is a function supplied by that complement. The main statement describes the subgroup generated inside the ambient group; a companion statement says the same set generates the subgroup regarded as a group in its own right, and a third version works with finite sets. Each of these has an additive counterpart for additive groups. The counting consequences assume the subgroup has finite index, which matters because Mathlib assigns index \(0\) to a subgroup of infinite index. The rank of a group is defined only for finitely generated groups, as the least size of a finite generating set.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibSubgroup.closure_mul_image_eq
Uses 3
Statement usesGroup · Subgroup · Subgroup generated by a subset

ClassCyclic group#

A cyclic group is a group in which every element is a power of one fixed element. Cyclic groups are among the most elementary groups: up to isomorphism there is exactly one finite cyclic group with \(n\) elements for each \(n \ge 1\), namely the integers modulo \(n\), and one infinite one, the integers under addition. They are the building blocks of the finitely generated abelian groups, and they turn up throughout number theory, most famously as the multiplicative group of residues modulo a prime.

Definition

A group \(G\) is cyclic if it contains an element \(g\) such that every element of \(G\) has the form \(g^k\) for some integer \(k\). Such an element is called a generator. In other words, \(G\) is cyclic exactly when it equals the subgroup generated by a single element (see subgroup generated by a subset). Written additively, the condition says that every element is an integer multiple \(kg\) of the generator.

For every element \(g\) of any group, the set of powers \(\{g^k : k \in \mathbb{Z}\}\) is a subgroup, and that subgroup is cyclic. Its order is the order of \(g\). Consequently a finite group \(G\) is cyclic if and only if it has an element whose order is \(|G|\).

Examples
  • The integers \(\mathbb{Z}\) under addition are cyclic, generated by \(1\) (or by \(-1\)). Every infinite cyclic group is isomorphic to \(\mathbb{Z}\).
  • The integers modulo \(n\), written \(\mathbb{Z}/n\mathbb{Z}\), form a cyclic group under addition, generated by the class of \(1\). A residue class \(a\) generates it exactly when \(\gcd(a, n) = 1\).
  • The complex \(n\)th roots of unity form a cyclic group of order \(n\) under multiplication, generated by \(e^{2\pi i/n}\).
  • Every group of prime order is cyclic, by Lagrange's theorem: any element other than the identity generates a subgroup whose order divides the prime and exceeds \(1\).
  • The group \(\mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/2\mathbb{Z}\), the Klein four-group, is not cyclic: it has order \(4\), but every element other than the identity has order \(2\).
Classification

A cyclic group is determined up to isomorphism by its order. If \(g\) generates \(G\), the map \(k \mapsto g^k\) is a surjective group morphism from \(\mathbb{Z}\) onto \(G\). Its kernel is a subgroup of \(\mathbb{Z}\), hence of the form \(n\mathbb{Z}\) for a unique \(n \ge 0\), and the first isomorphism theorem gives

\[G \cong \mathbb{Z}/n\mathbb{Z}.\]

Here \(n\) is the order of \(G\) when \(G\) is finite, and \(n = 0\), giving \(\mathbb{Z}\) itself, when \(G\) is infinite; this is the isomorphism Mathlib constructs. In particular two cyclic groups of the same order are isomorphic.

Properties
Cyclic groups in number theory

The units of a finite field form a cyclic group; more generally, every finite subgroup of the group of units of an integral domain is cyclic. For a prime \(p\) this says that the nonzero residues modulo \(p\) form a cyclic group under multiplication; a generator is called a primitive root modulo \(p\). For composite moduli the situation is more delicate: the group of units modulo \(n\) for a positive integer \(n\) is cyclic exactly when \(n\) is \(1\), \(2\), \(4\), \(p^m\) or \(2p^m\) for an odd prime \(p\) and \(m \ge 1\); Mathlib's list also includes \(n = 0\), whose units are \(\pm 1\) in \(\mathbb{Z}\). The units modulo \(8\), for instance, form a Klein four-group.

In Mathlib

Mathlib treats being cyclic as a property of a type rather than as extra structure: the definition asks only for the existence of a generator, and it is stated for any type with integer powers, so it applies to groups and to more general objects alike. The additive version is a separate class, written out alongside this one and paired with it by Mathlib's translation between multiplicative and additive notation, and a group is cyclic precisely when its additive counterpart is. Sizes are measured with a cardinality that gives \(0\) for an infinite set; with this convention the integers modulo \(0\) are the integers, so the classification above reads uniformly as "a cyclic group of order \(n\) is the integers modulo \(n\)" for every \(n\), finite groups and \(\mathbb{Z}\) included. The criterion for products is likewise stated for arbitrary groups under the same convention.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibIsCyclic
Uses 3 · Used by 5
Statement usesGroup · Subgroup generated by a subset · Integer
Used byDirichlet’s Theorem · Dirichlet unit theorem · Classification of abelian simple groups · Structure of finitely generated abelian groups · Primitive element theorem

ClassNilpotent group#

A nilpotent group is a group that can be built from abelian pieces by repeatedly taking central extensions (extensions in which the kernel lies in the center), in finitely many steps. Every abelian group is nilpotent, and so is every finite \(p\)-group. Nilpotency sits between commutativity and solvability: nilpotent groups keep much of the arithmetic control that abelian groups enjoy, which makes them a basic class in finite group theory, in the theory of discrete groups and in Lie theory.

Definition

Write \(Z(G)\) for the center of \(G\) and \([x, y] = xyx^{-1}y^{-1}\) for the commutator of two elements. The upper central series of \(G\) is the increasing chain of normal subgroups

\[1 = Z_0 \le Z_1 \le Z_2 \le \cdots\]

in which \(Z_{i+1}\) consists of the elements \(x\) with \([x, y] \in Z_i\) for every \(y \in G\); equivalently, \(Z_{i+1}/Z_i\) is the center of the quotient group \(G/Z_i\). Thus \(Z_1 = Z(G)\). The group \(G\) is nilpotent if \(Z_c = G\) for some \(c\), and the least such \(c\) is the nilpotency class of \(G\). The trivial group has class \(0\), and a nilpotent group has class at most \(1\) exactly when it is abelian, so a nontrivial group has class \(1\) exactly when it is abelian.

There are two equivalent descriptions. The lower central series is defined by \(\gamma_1 = G\) and \(\gamma_{i+1} = [\gamma_i, G]\), the subgroup generated by all commutators \([x, y]\) with \(x \in \gamma_i\) and \(y \in G\). A group is nilpotent if and only if its lower central series reaches the trivial subgroup, and \(\gamma_{c+1} = 1\) holds for the same least \(c\) as \(Z_c = G\). More flexibly, \(G\) is nilpotent if and only if it has a finite central series, a finite sequence of subgroups \(1 = H_0, H_1, \dots, H_n = G\) with \([H_{i+1}, G] \le H_i\) for each \(i\). Such a sequence need not increase, but if \(G\) is nilpotent then the upper central series, which is increasing, is one. The upper series climbs as fast as any such chain and the lower series descends as fast as any such chain, which is why all three descriptions give the same class.

Examples
  • Abelian groups are nilpotent, of class at most \(1\).
  • Every finite \(p\)-group is nilpotent, where a finite \(p\)-group is a group whose order is a power of a prime \(p\); equivalently, a finite group in which every element has order a power of \(p\). The proof uses the fact that a nontrivial finite \(p\)-group has nontrivial center and inducts on the order. The dihedral group of order \(8\) and the quaternion group of order \(8\) are nonabelian examples of class \(2\).
  • The Heisenberg group of upper triangular \(3 \times 3\) integer matrices with ones on the diagonal is an infinite nilpotent group of class \(2\): its center and its commutator subgroup both consist of the matrices whose off-diagonal entries are zero except possibly the top right one.
  • The symmetric group \(S_3\) is not nilpotent. Its center is trivial, so its upper central series never leaves \(1\). It is nevertheless solvable (defined below), so nilpotency is a strictly stronger condition.
Properties
Finite nilpotent groups

For finite groups, nilpotency has several characterizations through the Sylow \(p\)-subgroups: for each prime \(p\), the subgroups whose order is the largest power of \(p\) dividing \(|G|\), whose existence is the first Sylow theorem. For a finite group \(G\) the following are equivalent: \(G\) is nilpotent; every proper subgroup is strictly smaller than its normalizer; every maximal subgroup (a proper subgroup contained in no larger proper subgroup) is normal; every Sylow subgroup is normal; and \(G\) is isomorphic to the direct product of its Sylow subgroups (the characterization). So a finite nilpotent group is nothing more than a direct product of \(p\)-groups for distinct primes \(p\), and its study reduces to the study of \(p\)-groups.

One consequence is a full converse to Lagrange's theorem for this class: if \(G\) is finite and nilpotent and \(n\) divides \(|G|\), then \(G\) has a normal subgroup of order \(n\). The alternating group \(A_4\), which has order \(12\) but no subgroup of order \(6\), shows that solvable groups do not share this property.

Nilpotency for Lie algebras is defined the same way, with the Lie bracket in place of the group commutator; a connected Lie group is nilpotent exactly when its Lie algebra is. A group is called virtually nilpotent if it has a nilpotent subgroup of finite index. By Gromov's theorem, a finitely generated group of polynomial growth is virtually nilpotent; polynomial growth means that the number of elements expressible as words of length at most \(n\) in a fixed finite generating set is bounded by a polynomial in \(n\). Conversely, every finitely generated virtually nilpotent group has polynomial growth, so polynomial growth characterizes virtual nilpotency among finitely generated groups.

In Mathlib

Mathlib defines nilpotency through the upper central series, a sequence of subgroups indexed by all natural numbers, and asks that some term equal the whole group; the lower central series and arbitrary central series appear as equivalent conditions proved afterwards. Mathlib defines the lower central series of any subgroup \(H\) of \(G\), computed inside \(G\); the lower central series of \(G\) itself is the case \(H = G\). It is indexed from \(0\), so its term number \(i\) is the textbook \(\gamma_{i+1}\). Ascending and descending central series are infinite sequences required only to satisfy the commutator condition: they need not be increasing (or decreasing), need not consist of normal subgroups, and need not reach the top or the bottom. A \(p\)-group is defined by the orders of its elements, each a power of \(p\), so finiteness is a separate hypothesis. The nilpotency class is defined for every group, taking the value \(0\) when the group is not nilpotent. Nilpotency is a property of a group type, so a subgroup is nilpotent when it is nilpotent as a group in its own right. Most of the definitions and general results also have additive versions, stated for additive groups; the results specific to finite groups do not.

Written for Trough, under CC BY-SA 4.0.

Sources
MathlibGroup.IsNilpotent
Uses 3
Statement usesGroup · Normal subgroup · Quotient group

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.