Basic definitions

InstanceDirect product of groups #

The direct product of two groups $G$ and $H$ is the group $G \times H$ whose elements are ordered pairs $(g, h)$ with $g \in G$ and $h \in H$, multiplied one coordinate at a time. It is a basic way to build new groups from old ones: large groups are assembled from small ones as products, and many groups are understood by recognizing them as products of simpler factors, as in the classification of finite abelian groups.

Definition

Let $G$ and $H$ be groups. On the set $G \times H$ of ordered pairs define

\[(g_1, h_1)\,(g_2, h_2) = (g_1 g_2,\; h_1 h_2),\]

so that the product of two pairs is the pair of products. The identity element is the pair $(e_G, e_H)$ of identities, and the inverse of $(g, h)$ is $(g^{-1}, h^{-1})$. Each group axiom holds in $G \times H$ because it holds in each coordinate separately, so these operations make $G \times H$ a group. The same construction applies to any finite list of groups $G_1 \times \dots \times G_n$.

The direct product comes with two projection homomorphisms $\pi_1 : G \times H \to G$ and $\pi_2 : G \times H \to H$, and two inclusions $g \mapsto (g, e)$ and $h \mapsto (e, h)$. The images of the inclusions are the subgroups $G \times \{e\}$ and $\{e\} \times H$, and the kernel of $\pi_1$ is $\{e\} \times H$.

Examples

The Klein four-group. $\mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/2\mathbb{Z}$ has four elements, and each of its three non-identity elements has order $2$. It is therefore not cyclic, and it is the smallest group that is not cyclic.
Cyclic groups of coprime order. For coprime $m$ and $n$, the ring $\mathbb{Z}/mn\mathbb{Z}$ is isomorphic to $\mathbb{Z}/m\mathbb{Z} \times \mathbb{Z}/n\mathbb{Z}$, which is the Chinese remainder theorem; in particular the additive groups are isomorphic, so $\mathbb{Z}/6\mathbb{Z} \cong \mathbb{Z}/2\mathbb{Z} \times \mathbb{Z}/3\mathbb{Z}$.
Euclidean space. The additive group of $\mathbb{R}^n$ is the direct product of $n$ copies of the additive group $\mathbb{R}$.
Mixed factors. $\mathbb{Z} \times \mathbb{Z}/2\mathbb{Z}$ is an infinite abelian group with exactly one element of order $2$, namely $(0, 1)$.

Properties

Order. The number of elements of $G \times H$ is $|G|\,|H|$ when $G$ and $H$ are finite.
Order of an element. If $g$ and $h$ have finite order, then the order of $(g, h)$ is the least common multiple of the orders of $g$ and $h$ (see order of an element).
Commutativity. Two pairs commute exactly when their coordinates commute, so the product of two abelian groups is abelian. Conversely, if $G \times H$ is abelian then so are $G$ and $H$.
Cyclic products. For finite groups $G$ and $H$, $G \times H$ is cyclic if and only if $G$ and $H$ are both cyclic and their orders are coprime.
Symmetry. $G \times H$ is isomorphic to $H \times G$ by swapping coordinates, and $(G \times H) \times K$ is isomorphic to $G \times (H \times K)$.
Subgroups and quotients. For subgroups $A \le G$ and $B \le H$, the set $A \times B$ is a subgroup of $G \times H$ (see subgroup); if $A$ and $B$ are normal, so is $A \times B$, and the quotient $(G \times H)/(A \times B)$ is isomorphic to $(G/A) \times (H/B)$. Not every subgroup of $G \times H$ has this form: the diagonal $\{(g, g)\}$ in $G \times G$ does not, unless $G$ is trivial.

Universal property

The direct product is the product of $G$ and $H$ in the category of groups. Given homomorphisms $\varphi : K \to G$ and $\psi : K \to H$ from any group $K$, the map $k \mapsto (\varphi(k), \psi(k))$ is a homomorphism $K \to G \times H$, and composing it with $\pi_1$ gives back $\varphi$. Moreover every homomorphism into $G \times H$ is the one built in this way from its two components. In the other direction, when the target group is abelian, homomorphisms $\varphi : G \to P$ and $\psi : H \to P$ combine into the homomorphism $(g, h) \mapsto \varphi(g)\,\psi(h)$ on $G \times H$; in fact, for abelian groups the direct product is also the coproduct, so a finite direct product of abelian groups is often written as a direct sum $G \oplus H$.

Internal direct products

A group $G$ is isomorphic to $N \times K$ for subgroups $N$ and $K$ of $G$ when $N$ and $K$ are both normal, $N \cap K = \{e\}$, and every element of $G$ is a product $nk$ with $n \in N$ and $k \in K$. Under these conditions elements of $N$ commute with elements of $K$, and $(n, k) \mapsto nk$ is an isomorphism. In this case $G$ is called the internal direct product of $N$ and $K$.

Generalizations

The product of an arbitrary family of groups, indexed by any set, is again a group under coordinatewise multiplication.
The semidirect product $N \rtimes_\varphi K$ twists the multiplication of $N \times K$ by an action $\varphi$ of $K$ on $N$ by automorphisms; for the trivial action it is isomorphic to the direct product.
The same coordinatewise construction gives the product of rings and the product of vector spaces.

In Mathlib

Mathlib does not introduce a separate type for the direct product. It uses the ordinary type of ordered pairs and declares a group structure on it, once and for all, whenever both factors are groups, so the group structure on $G \times H$ is available without further input. Most of the surrounding facts, such as the projections, inclusions, the universal property and the swap and reassociation isomorphisms, are stated for monoids or even more general structures, and specialize to groups. Sizes and orders are natural numbers: the number of elements of an infinite set, and the order of an element of infinite order, are both taken to be $0$; with this convention the formulas for the order of $G \times H$ and of an element $(g, h)$, and the criterion for $G \times H$ to be cyclic, hold for all groups, not only finite ones. Products of arbitrary families are a separate construction, functions from the index set, with their own group structure.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibProd.instGroup

Uses 1 · Used by 2

Statement usesGroup

Used byAbel-Ruffini theorem (one direction) · Structure of finitely generated abelian groups

DefinitionOrder of an element #

The order of an element $g$ of a group is the smallest positive integer $n$ such that $g^n = e$, where $e$ is the identity; if no positive power of $g$ equals $e$, the element has infinite order. The order records how long the sequence of powers $g, g^2, g^3, \dots$ runs before it returns to the identity, and it equals the number of elements of the subgroup generated by $g$. It is a basic numerical invariant of a single element, and through Lagrange's theorem it links the structure of individual elements to the size of the group.

Definition

Let $G$ be a group with identity $e$ and let $g \in G$. If some positive power of $g$ equals $e$, then the order of $g$, written $\operatorname{ord}(g)$, is the least positive integer $n$ with $g^n = e$; otherwise $g$ has infinite order. Thus, for $n \ge 1$, $g$ has order $n$ exactly when $g^n = e$ and $g^m \neq e$ for every $m$ with $0 < m < n$. The definition uses only the multiplication and the identity, so it makes sense in any monoid. In additive notation, used for abelian groups such as the integers modulo $n$, the condition $g^n = e$ becomes $ng = 0$.

Equivalently, the order of $g$ is the number of elements of the cyclic subgroup $\langle g \rangle = \{g^k : k \in \mathbb{Z}\}$, an infinite order corresponding to an infinite subgroup. When $g$ has order $n$, the powers $e, g, \dots, g^{n-1}$ are distinct and make up all of $\langle g \rangle$; when $g$ has infinite order, its powers are pairwise distinct.

Examples

The identity is the only element of order $1$: $\operatorname{ord}(g) = 1$ if and only if $g = e$.
In the additive group $\mathbb{Z}/n\mathbb{Z}$ with $n \ge 1$, the class of $1$ has order $n$, and more generally the class of a natural number $a$ has order $n/\gcd(n, a)$. In the integers themselves every nonzero element has infinite order.
In any nontrivial ring, $-1$ has multiplicative order $2$, unless the ring has characteristic $2$, where $-1 = 1$ has order $1$. In a linearly ordered ring such as $\mathbb{R}$, every $x$ with $|x| \neq 1$ has infinite multiplicative order, so $1$ and $-1$ are the only real numbers of finite order.
For $n \ge 1$, a complex number is a primitive $n$-th root of unity exactly when its multiplicative order is $n$; for instance $\exp(2\pi i k/n)$ has order $n$ whenever $\gcd(k, n) = 1$ (see primitive complex roots of unity).
Among the permutations of a finite set, a cycle has order equal to the number of points it moves, and the order of any permutation is the least common multiple of the lengths of the cycles in its decomposition into disjoint cycles (see decomposition into cycles). For example, the permutation $(1\,2)(3\,4\,5)$ of $\{1, \dots, 5\}$ has order $6$.

Properties

Let $g$ be an element of a group $G$ with finite order $n$.

Powers. For every integer $m$, $g^m = e$ if and only if $n$ divides $m$. More generally, for integers $a$ and $b$, $g^a = g^b$ if and only if $a \equiv b \pmod n$, so a power of $g$ depends only on the residue of its exponent modulo $n$.
Orders of powers. For $k \ge 1$, the power $g^k$ has order $n/\gcd(n, k)$. In particular $g^k$ generates the same cyclic subgroup as $g$ exactly when $\gcd(n, k) = 1$.
Inverses and conjugates. The inverse $g^{-1}$ has the same order as $g$, and if $ag = g'a$ for some $a$, that is, if $g' = aga^{-1}$ is a conjugate of $g$, then $g$ and $g'$ have the same order. Order is therefore constant on conjugacy classes.
Homomorphisms. For a homomorphism $\varphi$, the order of $\varphi(g)$ divides the order of $g$, and an injective homomorphism preserves the order.
Lagrange. If $G$ is finite, with $|G|$ elements (the order of $G$), the order of $g$ divides $|G|$, by Lagrange's theorem applied to $\langle g \rangle$; hence $g^{|G|} = e$.
Products. If $g$ and $h$ commute and have coprime orders, then $\operatorname{ord}(gh) = \operatorname{ord}(g)\operatorname{ord}(h)$. Without commutativity the orders of $g$ and $h$ say little about that of $gh$: in the infinite dihedral group, two reflections of order $2$ can have a product of infinite order. In a direct product, the order of $(a, b)$ is $\operatorname{lcm}(\operatorname{ord}(a), \operatorname{ord}(b))$.

Cyclic groups. A finite group is cyclic exactly when it has an element whose order equals the order of the group.
Cauchy's theorem. Lagrange's theorem has a partial converse for element orders: every prime dividing the order of a finite group is the order of some element.
Exponent. The exponent of $G$ is the least positive integer $n$ with $g^n = e$ for every $g \in G$, when one exists. The order of every element divides the exponent, and for a finite group the exponent is the least common multiple of the orders of the elements.

In Mathlib

Mathlib defines the order of an element of any monoid, not only of a group, and returns a natural number, using $0$ for infinite order: the order of $g$ is $0$ exactly when no positive power of $g$ equals the identity. The definition is the minimal period of the identity under left multiplication by $g$, a special case of the minimal period of a periodic point of a map, which is likewise $0$ for a point that is not periodic. With this convention many statements above hold for every element: "$0$ divides $m$" means $m = 0$, congruence modulo $0$ is equality, an infinite subgroup has size $0$ as a natural number, and every number divides $0$, so the divisibility by the order of the group holds trivially for infinite groups. Likewise the exponent is $0$ exactly when no positive $n$ satisfies $g^n = e$ for every $g$, so every order divides it in that case too. The additive order, used for the integers modulo $n$, is a separate notion generated automatically from the multiplicative one, and having finite order is a separate predicate on elements.

Written for Trough, under CC BY-SA 4.0.

Sources

MathliborderOf

Uses 2 · Used by 6

Statement usesGroup · Natural number

Used byLucas-Lehmer primality test · Classification of abelian simple groups · Second Sylow theorem · Structure of finitely generated abelian groups · Cauchy's theorem (group theory) · Primitive complex roots of unity

DefinitionStabilizer of a point #

The stabilizer of a point under a group action is the set of group elements that leave the point where it is. It is always a subgroup of the acting group, and it measures how much symmetry the point retains: the larger the stabilizer, the smaller the orbit. This trade-off, the orbit–stabilizer theorem, turns questions about group actions into questions about subgroups and their indices, and it is the basic counting tool behind the class equation, Burnside's lemma and the Sylow theorems.

Definition

Let a group $G$ act on a set $X$, and write $g \cdot x$ for the action of $g \in G$ on $x \in X$. The stabilizer of $x$ is the subgroup

\[G_x = \{\, g \in G : g \cdot x = x \,\}.\]

Thus an element $g$ lies in $G_x$ exactly when $g \cdot x = x$. Other common notations are $\operatorname{Stab}_G(x)$ and $\operatorname{Stab}(x)$; the stabilizer is also called the isotropy group of $x$.

The set $G_x$ is a subgroup. The identity fixes every point. If $g$ and $h$ fix $x$, then $(gh) \cdot x = g \cdot (h \cdot x) = x$, and applying $g^{-1}$ to both sides of $g \cdot x = x$ gives $g^{-1} \cdot x = x$.

Examples

Symmetric groups. The symmetric group $S_n$ acts on $\{1, \dots, n\}$, for $n \ge 1$. The stabilizer of $n$ consists of the permutations that fix $n$, and restricting them to $\{1, \dots, n-1\}$ identifies it with $S_{n-1}$. Its index in $S_n$ is $n$, the number of points.
Symmetries of a square. The dihedral group of order $8$ acts on the four vertices of a square. The stabilizer of a vertex consists of the identity and the reflection in the diagonal through that vertex, so it has order $2$, and $8 = 4 \cdot 2$.
Rotations of the sphere. The group of rotations of $\mathbb{R}^3$ about the origin acts on the unit sphere. The stabilizer of the north pole is the group of rotations about the vertical axis, and the stabilizer of any other point is the group of rotations about the axis through it.
Cosets. A group $G$ acts on the set $G/H$ of left cosets of a subgroup $H$ by $g \cdot aH = gaH$. The stabilizer of the coset $H$ is $H$ itself, and the stabilizer of a coset $aH$ is the conjugate $aHa^{-1}$.
Conjugation. A group acts on itself by conjugation, $g \cdot h = g h g^{-1}$, and the stabilizer of $h$ under this action is the centralizer of $h$, the subgroup of elements that commute with $h$. The orbits of this action are the conjugacy classes.
Free actions. When $G$ acts on itself by left multiplication, $gh = h$ forces $g$ to be the identity, so every stabilizer is trivial. An action is called free when every stabilizer is trivial.

Properties

Stabilizers along an orbit. Stabilizers of points in the same orbit are conjugate: for every $g$ in $G$, the stabilizer of $g \cdot x$ is $g G_x g^{-1}$. Indeed $h$ fixes $g \cdot x$ exactly when $g^{-1} h g$ fixes $x$. Consequently, if $y = g \cdot x$, then conjugation by $g$ is an isomorphism from $G_x$ onto $G_y$. A stabilizer need not be normal: for the action on $G/H$ the stabilizers are exactly the conjugates of $H$, and they all equal $H$ only when $H$ is normal.

Orbit–stabilizer theorem. Two elements $g$ and $h$ send $x$ to the same point exactly when $g^{-1}h \in G_x$, that is, when they lie in the same left coset of $G_x$. So $g G_x \mapsto g \cdot x$ is a bijection from the set of left cosets of $G_x$ onto the orbit of $x$, and the index of $G_x$ equals the size of the orbit of $x$. For a finite group $G$, the size of the orbit times the order of the stabilizer is the order of $G$:

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

In particular both factors divide $|G|$, in line with Lagrange's theorem. For a transitive action, where the orbit is all of $X$, the index of every stabilizer is the number of points of $X$. Summing over the orbits of a finite set gives the class formula, and counting the pairs $(g, x)$ with $g \cdot x = x$ in two ways, once by points and once by group elements, gives Burnside's lemma.

Free actions. Mathlib expresses freeness as a cancellation law: $g \cdot x = h \cdot x$ implies $g = h$, and each $g$ acts injectively (which is automatic for a group action). A group action satisfies this law exactly when every stabilizer is trivial.

Intersections of stabilizers. For a subset $S$ of $X$, an element lies in the pointwise stabilizer of $S$ exactly when it fixes every point of $S$, so the pointwise stabilizer is the intersection of the stabilizers $G_x$ for $x$ in $S$. Taking $S = X$ gives the kernel of the action, the set of elements that act as the identity; it is a normal subgroup, and the action is faithful exactly when it is trivial. The setwise stabilizer of $S$ is the stabilizer of $S$ as a point of the induced action on subsets: an element $g$ lies in it exactly when, for every $y$ in $X$, $g \cdot y$ lies in $S$ if and only if $y$ does.

Applied to the action of a group on its subgroups by conjugation, the stabilizer of a subgroup is its normalizer. Mathlib states this for Sylow subgroups: the stabilizer of a Sylow $p$-subgroup $P$ under conjugation is the normalizer of $P$. In a finite group the Sylow $p$-subgroups form a single orbit by the second Sylow theorem, so by the orbit–stabilizer theorem their number is the index of the normalizer of any one of them. More generally, for a transitive action the orbit–stabilizer bijection identifies $X$ with the coset space $G/G_x$, compatibly with the action of $G$; in this way the unit sphere corresponds to the rotation group modulo the rotations about one axis.

In Mathlib

Mathlib defines the stabilizer for an action of a group as a bundled subgroup of the acting group, so the closure properties above are part of the definition rather than separate results. Membership unfolds directly to the equation $g \cdot x = x$. For an action of a monoid, where inverses are unavailable, the same set is provided as a submonoid, and the additive version, for actions written with $+$, is generated from the multiplicative one. There is no separate notion of setwise stabilizer: it is the stabilizer of a set under the induced action on sets, while the pointwise stabilizer of a set is a separate subgroup, called its fixing subgroup. Conjugation is set up as an action of a copy of $G$, so the statement about centralizers compares two subgroups of that copy. The form of the orbit–stabilizer theorem with the index holds for every group, using the conventions that a subgroup of infinite index has index $0$ and an infinite set has size $0$; the form with orders assumes the group is finite.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibMulAction.stabilizer

Uses 3 · Used by 6

Statement usesGroup action · Subgroup · Group

Used byBurnside lemma · Class formula · Second Sylow theorem · Third Sylow theorem · Orbit · Quotient space (Basic definitions)

DefinitionOrbit #

The orbit of a point under a group action is the set of all points the group can move it to. When a group acts on a set, the orbits cut the set into disjoint pieces, and the size of each piece is tied to the structure of the group by the orbit–stabilizer theorem. Counting arguments built on orbits underlie much of finite group theory, including the class equation, Burnside's lemma and the Sylow theorems.

Definition

Let a group $G$ act on a set $X$, and write $g \cdot x$ for the action of $g \in G$ on $x \in X$. The orbit of $x$ is the set

\[G \cdot x = \{\, g \cdot x : g \in G \,\}.\]

Thus a point $y$ lies in the orbit of $x$ exactly when $y = g \cdot x$ for some $g$ in $G$. Taking $g$ to be the identity shows that every point lies in its own orbit.

Examples

Rotations of the plane. The group of rotations about the origin acts on $\mathbb{R}^2$. The orbit of a point at distance $r > 0$ from the origin is the circle of radius $r$ about the origin, and the orbit of the origin is the origin alone.
Permutations. A single permutation $\sigma$ of a finite set generates a cyclic group of permutations, whose orbits are the cycles of $\sigma$, each fixed point counting as a cycle of length one. For $\sigma = (1\,2\,3)(4\,5)$ acting on $\{1, \dots, 6\}$, the orbits are $\{1, 2, 3\}$, $\{4, 5\}$ and $\{6\}$.
Conjugation. A group acts on itself by conjugation, $g \cdot h = g h g^{-1}$. The orbit of $h$ under this action is its conjugacy class (see conjugacy classes).
Cosets. A subgroup $H$ of $G$ acts on $G$ by left multiplication. The orbit of $a$ under this action is the right coset $Ha$.
Transitive actions. An action is transitive if any point can be moved to any other by some group element. On a nonempty set this means there is exactly one orbit: for any point $x$, the action is transitive if and only if the orbit of $x$ is all of $X$.

Properties

Orbits partition the set. For a group action, the orbit of $g \cdot x$ equals the orbit of $x$, and two orbits $G \cdot x$ and $G \cdot y$ are equal exactly when $x$ lies in $G \cdot y$. So two orbits are either equal or disjoint, and the relation of lying in a common orbit is an equivalence relation whose classes are the orbits. The orbits together cover $X$, and $X$ is in bijection with the disjoint union of its orbits. The set of orbits is often written $X/G$.

Orbit–stabilizer theorem. Let $G_x = \{\, g \in G : g \cdot x = x \,\}$ be the stabilizer of $x$. Two elements $g$ and $h$ send $x$ to the same point exactly when $g^{-1}h \in G_x$, that is, when they lie in the same left coset of $G_x$. Hence the rule $g G_x \mapsto g \cdot x$ gives a bijection between the orbit of $x$ and the set of left cosets of $G_x$. In particular the index of $G_x$ equals the size of the orbit, and for a finite group

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

(the counting form). So the size of every orbit of a finite group divides the order of the group.

Fixed points. A point is fixed by every element of $G$ exactly when its orbit has at most one element, which, since the orbit contains the point, means the orbit is the point alone.

Counting. Summing the orbit–stabilizer formula over the orbits of a finite group acting on a finite set gives the class formula

\[|X| = \sum_{G \cdot x \,\in\, X/G} \frac{|G|}{|G_x|},\]

one representative $x$ being chosen from each orbit. The same bookkeeping, done over pairs of a group element and a point it fixes, gives Burnside's lemma, which counts orbits as the average number of fixed points.

Actions of $p$-groups. Let $p$ be a prime and let $G$ be a group in which every element has order a power of $p$. Then every finite orbit of $G$ has a power of $p$ as its size. Every orbit of size greater than $1$ therefore contributes a multiple of $p$, so for an action on a finite set $|X|$ is congruent modulo $p$ to the number of fixed points. This congruence drives standard proofs of Cauchy's theorem and of the first, second and third Sylow theorems.

The orbits of the conjugation action are the conjugacy classes, and for that action the class formula becomes the class equation of a finite group. The orbit of a subgroup $K$ under the conjugation action of $G$ on its subgroups is the set of conjugates of $K$; the second Sylow theorem says that in a finite group the Sylow $p$-subgroups form a single such orbit. Orbits are also the starting point for quotient constructions, where one replaces a space by its set of orbits.

In Mathlib

Mathlib defines the orbit for any rule that lets elements of one type act on another, with no axioms at all: the orbit of $x$ is the image of the map $g \mapsto g \cdot x$. Most results need more. That a point lies in its own orbit holds for actions of monoids, while the partition into orbits, the orbit relation and the orbit–stabilizer theorem need a group. The restriction matters: the natural numbers act on themselves by multiplication, the orbit of $1$ contains $0$, but the orbit of $0$ is $\{0\}$. An orbit is a subset of the acted-on type rather than a separate structure. The orbit–stabilizer theorem is stated as an explicit bijection with the coset space, from which the counting forms follow; the form with the index holds for every group, using the convention that an infinite set has size $0$ and a subgroup of infinite index has index $0$. Mathlib calls a transitive action pretransitive, since it does not require the set to be nonempty. Additive versions, for actions written with $+$, are generated from the multiplicative ones.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibMulAction.orbit

Uses 5 · Used by 8

Statement usesGroup action · Group · Set

Proof usesStabilizer of a point · Subgroup

Used byBurnside lemma · Class formula · First Sylow theorem · Second Sylow theorem · Third Sylow theorem · Nielsen–Schreier theorem · Dirichlet's unit theorem · Quotient space (Basic definitions)

DefinitionQuotient space (Basic definitions)#

The quotient space $G/H$ of a group $G$ by a subgroup $H$ is the set of left cosets $aH$ of $H$ in $G$. It is not a group in general, but $G$ acts on it by left multiplication, and this action is the model for every transitive group action: by the orbit-stabilizer theorem, each orbit of an action of $G$ is a copy of the quotient of $G$ by the stabilizer of any of its points. Counting arguments in finite group theory, from Lagrange's theorem to the class formula, rest on this identification.

Definition

Let $H$ be a subgroup of a group $G$. Call $a, b \in G$ equivalent when $a^{-1}b \in H$; this is an equivalence relation whose classes are the left cosets $aH = \{ah : h \in H\}$. The quotient space $G/H$ is the set of these classes, so that $aH = bH$ exactly when $a^{-1}b \in H$. Its number of elements is the index $[G : H]$.

The group $G$ acts on $G/H$ by $g \cdot (aH) = (ga)H$. This action is transitive, since $(ba^{-1}) \cdot (aH) = bH$, and the stabilizer of the coset $H$ itself is $H$.

The right cosets $Ha$ form a second quotient space, but nothing new arises in counting: $Ha \mapsto a^{-1}H$ is a well-defined bijection from right cosets to left cosets.

Orbit-stabilizer theorem

Let $G$ act on a set $X$ and let $x \in X$, with orbit $G \cdot x$ and stabilizer $G_x = \{g \in G : g \cdot x = x\}$. The theorem states that

\[G/G_x \to G \cdot x, \qquad gG_x \mapsto g \cdot x\]

is well defined and a bijection. Mathlib states the bijection from the orbit to $G/G_x$, and its inverse sends $gG_x$ to $g \cdot x$. The map is compatible with the actions: the image of $g \cdot c$ is $g$ applied to the image of $c$ for every coset $c$. Thus every transitive action of $G$ on a nonempty set is, up to relabelling the points, the action of $G$ on some quotient space $G/K$.

In terms of size, the index of $G_x$ equals the number of points of the orbit of $x$. When $G$ is finite, $|G \cdot x| \cdot |G_x| = |G|$, so the size of every orbit divides the order of $G$.

Proof

If $g G_x = h G_x$, then $g^{-1}h$ fixes $x$, so $h \cdot x = g \cdot (g^{-1}h) \cdot x = g \cdot x$; the map is well defined. Reading the same computation backwards, $g \cdot x = h \cdot x$ forces $g^{-1}h \in G_x$, so the map is injective. Every point of the orbit has the form $g \cdot x$, so the map is surjective. Compatibility with the action is the identity $(g'g) \cdot x = g' \cdot (g \cdot x)$.

Examples

Integers modulo $n$. For $n \ge 1$, the quotient of the additive group $\mathbb{Z}$ by $n\mathbb{Z}$ consists of the $n$ cosets $r + n\mathbb{Z}$ with $0 \le r < n$. Here $n\mathbb{Z}$ is normal, so the quotient space is also a group.
Permutations. The permutation group $S_3$ acts transitively on $\{1, 2, 3\}$, and the stabilizer of $3$ is the subgroup $\{e, (1\,2)\}$ of order $2$. Its three cosets correspond to the three points, and $6 = 3 \cdot 2$.
The sphere. The rotation group $SO(3)$ acts transitively on the unit sphere in $\mathbb{R}^3$, and the stabilizer of the north pole is the group of rotations about the vertical axis, a copy of $SO(2)$. The sphere is therefore in bijection with $SO(3)/SO(2)$.
Conjugation. Let $G$ act on itself by $g \cdot a = gag^{-1}$. The orbit of $a$ is its conjugacy class and the stabilizer is the centralizer of $a$, so in a finite group the size of a conjugacy class is the index of a centralizer and divides $|G|$.

Consequences

Lagrange's theorem. Since the cosets of $H$ all have $|H|$ elements and partition $G$, $|G| = |G/H| \cdot |H|$.
Class formula. Splitting a finite set $X$ into orbits and applying the theorem to each orbit writes $|X|$ as a sum of indices $[G : G_x]$, one for each orbit; in Mathlib this is a bijection between $X$ and the disjoint union of the quotients $G/G_x$, one $x$ chosen in each orbit.
Burnside's lemma. For a finite group acting on a finite set, the average number of points fixed by an element of the group is the number of orbits; its proof counts pairs $(g, x)$ with $g \cdot x = x$ by the orbit-stabilizer theorem.

When $H$ is a normal subgroup, the multiplication $(aH)(bH) = (ab)H$ is well defined and makes $G/H$ the quotient group. The quotient of a vector space by a subspace is the analogous construction in linear algebra, where the additive group is abelian, so every subspace is a normal subgroup and the quotient is again a vector space. Quotient spaces of topological or Lie groups by closed subgroups are the homogeneous spaces of geometry, such as the sphere above.

In Mathlib

Mathlib defines the quotient of a group by a subgroup for every subgroup, as the quotient by the left-coset relation; the same notation denotes the quotient group when the subgroup is normal, and the group structure is then an extra instance on the same set. The action of $G$ on $G/H$ is a special case of a more general construction that lets any monoid acting compatibly on $G$ act on the quotient. The orbit-stabilizer theorem is stated as an explicit bijection, written in the direction from the orbit to the quotient, with no finiteness assumption. The numerical version through the index uses natural-number cardinality, which is $0$ for an infinite set, so it holds for every group: an infinite orbit and a stabilizer of infinite index both count as $0$. The same convention makes the formula $|G| = |G/H| \cdot |H|$ hold for every group and subgroup, with both sides $0$ when $G$ is infinite. The product formula for orbits and stabilizers assumes that the group is finite.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibMulAction.orbitEquivQuotientStabilizer

Uses 5

Statement usesGroup · Subgroup · Group action · Orbit · Stabilizer of a point

Class formula

DefinitionConjugacy classes #

The conjugacy classes of a group are the pieces into which the group splits when elements that differ only by a change of viewpoint, $a$ and $gag^{-1}$, are counted as the same. They are the orbits of the group acting on itself by conjugation. They carry much of the structure of a finite group: the class equation built from their sizes shows that nontrivial finite groups of prime-power order have a nontrivial center, a normal subgroup is a union of them, and their number equals the number of irreducible complex characters.

Definition

Let $G$ be a group with identity $e$. Two elements $a, b \in G$ are conjugate when $b = gag^{-1}$ for some $g \in G$. Conjugacy is an equivalence relation: $a = eae^{-1}$, if $b = gag^{-1}$ then $a = g^{-1}bg$, and if moreover $c = hbh^{-1}$ then $c = (hg)a(hg)^{-1}$. Its equivalence classes are the conjugacy classes of $G$. The class of $a$ is

\[\operatorname{Cl}(a) = \{\, gag^{-1} : g \in G \,\},\]

and the set of all classes is the quotient of $G$ by conjugacy, so that two elements have the same class exactly when they are conjugate. Equivalently, $G$ acts on itself by $g \cdot x = gxg^{-1}$, and the class of $a$ is the orbit of $a$ under this action (see orbit).

Examples

Abelian groups. In a commutative group, $gag^{-1} = a$ for all $g$, so conjugacy is equality: every class has one element and the classes correspond one to one with the elements.
The identity. In any group, the identity is conjugate only to itself, so $\{e\}$ is always a class.
Symmetric groups. In the symmetric group on a finite set, two permutations are conjugate exactly when they have the same cycle type, that is, the same multiset of cycle lengths in their decomposition into disjoint cycles. For $S_n$, conjugacy amounts to equality of the partitions of $n$ the permutations determine, and every partition occurs, so $S_n$ has as many classes as $n$ has partitions. In $S_3$ the classes are the identity, the three transpositions and the two $3$-cycles, of sizes $1 + 3 + 2 = 6$.
Dihedral groups. For odd $n$ the dihedral group of order $2n$ has $(n+3)/2$ conjugacy classes: the identity, the $(n-1)/2$ pairs of mutually inverse nontrivial rotations, and one class containing all $n$ reflections.
Matrix groups. In the general linear group over a field, conjugacy is similarity of invertible matrices. Over an algebraically closed field, two invertible matrices are conjugate exactly when they have the same Jordan normal form up to the order of the blocks.

Properties

Size of a class. The centralizer $C_G(a) = \{ g \in G : ga = ag \}$ is the stabilizer of $a$ under conjugation, and the size of the class of $a$ equals the index of $C_G(a)$ (see index of a subgroup). For a finite group, Lagrange's theorem then shows that the size of every class divides $|G|$.
Central elements. The center $Z(G)$ consists of the elements that commute with every element of $G$. An element is central exactly when its class has a single element: sending each element to its class is a bijection from $Z(G)$ onto the one-element classes.
The class equation. For a finite group the classes partition $G$, so their sizes add up to $|G|$. Separating the one-element classes gives the class equation

$$|G| = |Z(G)| + \sum_{i=1}^{r} |\operatorname{Cl}(a_i)|,$$

where $a_1, \dots, a_r$ represent the classes with more than one element. It is the class formula for the conjugation action. If $|G| = p^n$ with $p$ prime and $n \ge 1$, each $|\operatorname{Cl}(a_i)|$ is a power of $p$ greater than $1$ and $p$ divides $|G|$, so $p$ divides $|Z(G)|$: every nontrivial finite group of prime-power order has a nontrivial center. - Invariants of a class. If $y = axa^{-1}$, then $x$ and $y$ have the same order (see order of an element), and a homomorphism sends conjugate elements to conjugate elements (see group morphism). - Normal subgroups. A normal subgroup contains the whole class of each of its elements, so it is a union of conjugacy classes; conversely, a subgroup that is a union of classes is normal. Since a normal subgroup contains the class $\{e\}$ and its order divides $|G|$, class sizes limit the possible normal subgroups. The alternating group $A_5$ has classes of sizes $1, 12, 12, 15, 20$, and no sum of these that includes $1$ divides $60$ except $1$ and $60$, so $A_5$ is simple. - Commuting pairs. For a finite group with $k$ conjugacy classes, the number of ordered pairs of commuting elements is $k\,|G|$, so two elements chosen uniformly at random commute with probability $k/|G|$.

A class function is a function on $G$ that is constant on each conjugacy class. The characters of the irreducible complex representations of a finite group form an orthonormal basis of the space of class functions, so their number equals the number of conjugacy classes. Conjugation also acts on subgroups, sending $H$ to $gHg^{-1}$; the second Sylow theorem says that the Sylow $p$-subgroups of a finite group form a single class under this action.

In Mathlib

Mathlib defines conjugacy classes for any monoid, not only for groups: $a$ and $b$ are conjugate when $cac^{-1} = b$ for some invertible element $c$. In a group every element is invertible, so this is the usual notion. The conjugacy classes form a quotient type, with a map sending each element to its class and, for each class, the set of its elements. Sizes are measured with natural-number cardinality, which is $0$ for an infinite set, and the index of a subgroup is likewise $0$ when it is infinite; with these conventions the equality between the size of a class and the index of the centralizer, and the count of commuting pairs, hold for every group, while the class equation and the partition of $G$ into classes are stated for finite groups. An additive version covers additive groups.

Written for Trough, under CC BY-SA 4.0.

Sources

MathlibConjClasses

Uses 1 · Used by 1

Statement usesGroup

Used byAlternating groups on 5 letters or more are simple

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.

Basic definitions

InstanceDirect product of groups#

Definition

Examples

Properties

Universal property

Internal direct products

Generalizations

In Mathlib

Sources

DefinitionOrder of an element#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

DefinitionStabilizer of a point#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

DefinitionOrbit#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

DefinitionQuotient space (Basic definitions)#

Definition

Orbit-stabilizer theorem

Proof

Examples

Consequences

Related concepts

In Mathlib

Sources

DefinitionConjugacy classes#

Definition

Examples

Properties

Related concepts

In Mathlib

Sources

InstanceDirect product of groups #

DefinitionOrder of an element #

DefinitionStabilizer of a point #

DefinitionOrbit #

DefinitionConjugacy classes #