Group theory

Group theory is the study of groups: sets with an associative multiplication, an identity element and inverses. Groups record the symmetries of an object, whether the rotations of a polyhedron, the permutations of the roots of a polynomial or the automorphisms of a vector space, and they turn up in nearly every part of mathematics. The subject asks how groups are built from smaller ones, how they act on other objects, and what the order of a finite group forces about its structure.

Groups and homomorphisms

Groups are compared by group morphisms, maps that preserve multiplication; a bijective morphism is an isomorphism. The first examples are the cyclic groups, generated by a single element, and the symmetric groups \(\operatorname{Sym}(X)\) of all bijections of a set \(X\) (in Mathlib, the permutation group of a type). Symmetric groups are universal: Cayley's theorem says that every group is isomorphic to a group of permutations, namely the image of any faithful action in the permutations of the set acted on, for instance the action of the group on itself by multiplication.

Subgroups, cosets and quotients

A subgroup is a subset closed under the group operations, and every subset lies in a smallest one, the subgroup it generates. The left cosets \(gH\) of a subgroup \(H\) partition \(G\), and their number is the index \([G : H]\). Since all cosets have the same size, Lagrange's theorem follows: in a finite group, the order of a subgroup divides the order of the group.

The cosets of \(H\) form a group under the multiplication \((aH)(bH) = abH\) exactly when \(H\) is a normal subgroup, one that contains every conjugate \(gng^{-1}\) of each of its elements \(n\); the result is the quotient group \(G/H\). The kernel of a morphism is always normal, and the first isomorphism theorem identifies the quotient by the kernel with the image. The second isomorphism theorem gives \(H/(H \cap N) \cong HN/N\) for a subgroup \(H\) and a normal subgroup \(N\), and the third gives \((G/N)/(M/N) \cong G/M\) for normal subgroups \(N \le M\). The largest abelian quotient of \(G\) is its abelianization, the quotient by the commutator subgroup; morphisms from \(G\) to an abelian group correspond exactly to morphisms from the abelianization.

Actions and counting

A group action lets each element of \(G\) move the points of a set \(X\) compatibly with multiplication. The points reachable from \(x\) form its orbit, the elements fixing \(x\) form its stabilizer \(G_x\), and for a finite group the size of the orbit times the order of the stabilizer is the order of the group. Splitting \(X\) into orbits gives the class formula, which writes \(X\) as a disjoint union of the coset spaces \(G/G_x\) over one representative \(x\) of each orbit. Averaging fixed points over the group gives the Burnside lemma: for a finite group with finitely many orbits,

\[\sum_{g \in G} |X^g| = |X/G| \cdot |G|,\]

where \(X^g\) is the set of points fixed by \(g\) (Mathlib's statement). Applied to a group acting on itself by conjugation, the orbits are the conjugacy classes and the orbit decomposition becomes the class equation, a basic tool for finite groups; for instance it shows that a nontrivial finite \(p\)-group has nontrivial center.

Finite groups and Sylow theory

The converse of Lagrange's theorem fails in general, but primes rescue part of it. By Cauchy's theorem, if a prime \(p\) divides the order of a finite group, then the group has an element of order \(p\). The first Sylow theorem goes further: for every power \(p^n\) dividing the order of a finite group, there is a subgroup of order \(p^n\); the largest such subgroups are the Sylow \(p\)-subgroups. By the second Sylow theorem all Sylow \(p\)-subgroups are conjugate, and by the third their number is congruent to \(1\) modulo \(p\). Groups whose order is a power of a prime have a rich structure of their own: every finite \(p\)-group is nilpotent, in the sense of nilpotent groups, whose upper central series reaches the whole group after finitely many steps.

Simple groups and structure theorems

A nontrivial group is a simple group if its only normal subgroups are itself and the trivial subgroup; simple groups cannot be broken into a normal subgroup and a quotient, so they play the role of prime factors. Among abelian groups the question is settled by the classification of abelian simple groups: an abelian group is simple exactly when its order is prime. The most familiar infinite family of nonabelian simple groups comes from the alternating group \(A_n\) of even permutations, since alternating groups on 5 letters or more are simple (Mathlib's statement). The Feit–Thompson theorem, that every finite group of odd order is solvable, and the classification of finite simple groups are two landmarks of finite group theory that Mathlib does not yet contain.

For abelian groups a full description exists in the finitely generated case: by the structure theorem, every finitely generated abelian group is isomorphic to the product of \(\mathbb{Z}^n\) and a finite direct sum of cyclic groups of prime power order.

Free groups and presentations

The free group on a set \(S\) consists of reduced words in the elements of \(S\) and their inverses, and each map from \(S\) to a group \(H\) extends to exactly one morphism from the free group to \(H\). Every group is therefore a quotient of a free group, and a presented group is the quotient of a free group by the normal subgroup generated by a set of relations, so that groups can be specified by generators and relations. Generators pass to subgroups through Schreier's lemma: if \(S\) generates \(G\) and \(R\) is a set of representatives of the right cosets of a subgroup \(H\) with \(1 \in R\), then \(H\) is generated by the elements \(rs\,\overline{rs}^{\,-1}\) with \(r \in R\) and \(s \in S\), where \(\overline{g}\) is the representative of the coset \(Hg\). In particular a subgroup of finite index in a finitely generated group is finitely generated.

In Mathlib

Mathlib treats a group as a type equipped with a group structure supplied as a typeclass instance, which in its terminology is the unbundled approach, while subgroups, morphisms and isomorphisms are bundled structures that package their data with their properties. A group morphism is a morphism of the underlying monoids, that is, a map preserving multiplication. Most results are proved for multiplicative groups and translated automatically to additive ones. The structure theorem goes the other way: it is deduced from the structure theorem for finitely generated modules over a principal ideal domain, applied to abelian groups viewed as modules over \(\mathbb{Z}\), so its main form is additive and a multiplicative version is derived from it. Lagrange's theorem and the Sylow theorems measure orders with a cardinality that is \(0\) for an infinite group, so Lagrange's theorem holds for every group; other counting results, such as the orbit-stabilizer theorem, Burnside's lemma and Cauchy's theorem, assume the group is finite and use a cardinality defined only for finite types. Some theorems are more general than in textbooks: Cayley's theorem is stated for any faithful action, and the second and third Sylow theorems need only that there be finitely many Sylow subgroups, not that the group be finite. The first Sylow theorem is stated for every prime power dividing the order, not only the largest one.

Written for Trough, under CC BY-SA 4.0.

Group to Nilpotent group

Permutation group of a type to Third Sylow theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.