Group Presentation

Statement

A group presentation $\langle X \mid R \rangle$ specifies a group as the quotient of the free group $F(X)$ by the normal closure $N(R)$ of a set of relations $R \subseteq F(X)$. Any group $G$ with generators $X$ satisfying relations $R$ admits a unique surjective homomorphism

The presented group $\langle X \mid R \rangle$ is universal: it maps to any group that satisfies the relations. Equivalently, to define a homomorphism $\langle X \mid R \rangle \to G$, choose images of generators in $G$ that satisfy all relations in $R$.

Visualization

$D_4 = \langle r, s \mid r^4, s^2, (rs)^2 \rangle$ — the dihedral group of order 8.

Generators: $r$ (rotation by $90°$), $s$ (a reflection). Relations:

r⁴ = 1          (4 rotations return to identity)
s² = 1          (reflecting twice returns to identity)
(rs)² = 1       (i.e. rs = sr⁻¹, reflections don't commute with rotations)

Multiplication table for $D_4 = \{1, r, r^2, r^3, s, rs, r^2s, r^3s\}$:

$\cdot$	$1$	$r$	$r^2$	$r^3$	$s$	$rs$
$1$	$1$	$r$	$r^2$	$r^3$	$s$	$rs$
$r$	$r$	$r^2$	$r^3$	$1$	$rs$	$r^2s$
$s$	$s$	$r^3s$	$r^2s$	$rs$	$1$	$r^3$

To verify: $(rs)(rs) = r(sr)s = r(r^{-1}s^{-1})s = s^{-1}s = 1$ using $sr = r^{-1}s$ from the relation $(rs)^2 = 1$.

Proof Sketch

1. Form $F = F(X)$ and let $N = N(R)$ be the normal closure of $R$ in $F$. Define $P = F/N$.
2. The map $\iota : X \to P$ by $\iota(x) = xN$ makes $P$ generated by images of $X$ satisfying all relations in $R$ (since $r \in N$ implies $rN = N = e_P$).
3. Universality: given $G$ and $f : X \to G$ satisfying relations $R$, the free group lift $\tilde{f} : F \to G$ vanishes on $N(R)$ (since $f$ satisfies all relations), hence factors through $P$.
4. Uniqueness follows from $P$ being generated by $\iota(X)$.

Connections

Presentations are the concrete side of the Free GroupFree Group$$\mathrm{Hom}(F(X),\, G) \cong G^X$$The free group on a set X is the universal group with generators X and no relationsRead more →, which supplies the ambient object. The kernel of the quotient map is analyzed by the First Isomorphism TheoremFirst Isomorphism Theorem$$G / \ker(f) \cong \operatorname{im}(f)$$The image of a homomorphism is isomorphic to the domain modulo the kernelRead more →. Presentations arise crucially in the Impossibility of the Quintic FormulaImpossibility of the Quintic Formula$$S_5 \text{ is not solvable} \implies \text{no radical formula for degree } \geq 5$$No general algebraic formula exists for polynomials of degree 5 or higherRead more →: the symmetric group $S_5$ has a presentation, and showing $A_5$ is simpleSimple Groups$$G \text{ simple} \Longleftrightarrow \forall N \unlhd G,\; N = 1 \text{ or } N = G$$A simple group has no proper nontrivial normal subgroups; the atoms of group compositionRead more → via its presentation rules out a solvable composition series. The Correspondence TheoremCorrespondence Theorem$$\{H \leq G : N \leq H\} \;\ \longleftrightarrow\ \; \{\bar{H} \leq G/N\}$$Subgroups of G/N are in bijection with subgroups of G containing N, preserving the latticeRead more → translates subgroups of $G$ into subgroups of $F(X)$ containing $N(R)$.

import Mathlib.GroupTheory.PresentedGroup

/-- The universal property of a presented group: given a function from generators
    to a group G that satisfies all relations, there is a unique group homomorphism
    from the presented group to G.
    Mathlib: `PresentedGroup.toGroup`. -/
theorem presented_group_universal
    {α G : Type*} [Group G]
    (rels : Set (FreeGroup α)) (f : α → G)
    (hf : ∀ r ∈ rels, FreeGroup.lift f r = 1) :
    ∃ φ : PresentedGroup rels →* G, ∀ x : α, φ (PresentedGroup.of x) = f x := by
  exact ⟨PresentedGroup.toGroup hf, fun x => by simp [PresentedGroup.toGroup]⟩