Formalization Blueprint for “An Introduction to Algebraic Combinatorics” by Darij Grinberg

3.1 Permutations: basic definitions

3.1.1 Basic definitions

Convention 3.1
#

In the Lean formalization, we use \(\operatorname {Fin} n = \{ 0, 1, \ldots , n-1\} \) instead of the textbook’s \([n] = \{ 1, 2, \ldots , n\} \). Both are \(n\)-element sets, so their symmetric groups are isomorphic. Permutations are represented by the type of bijections \(X \to X\) (denoted \(\operatorname {Equiv.Perm}\, X\) in Lean), which is a group under composition. Composition \(\alpha \beta \) is the group multiplication \(\alpha * \beta \), sending \(x\) to \(\alpha (\beta (x))\).

Definition 3.2
#

Let \(X\) be a set.

(a) A permutation of \(X\) means a bijection from \(X\) to \(X\).

(b) It is known that the set of all permutations of \(X\) is a group under composition. This group is called the symmetric group of \(X\), and is denoted by \(S_X\). Its neutral element is the identity map \(\operatorname {id}_X : X \to X\). Its size is \(|X|!\) when \(X\) is finite.

(c) As usual in group theory, we will write \(\alpha \beta \) for the composition \(\alpha \circ \beta \) when \(\alpha , \beta \in S_X\). This is the map that sends each \(x \in X\) to \(\alpha (\beta (x))\).

(d) If \(\alpha \in S_X\) and \(i \in \mathbb {Z}\), then \(\alpha ^i\) shall denote the \(i\)-th power of \(\alpha \) in the group \(S_X\). Note that \(\alpha ^i = \underbrace{\alpha \circ \alpha \circ \cdots \circ \alpha }_{i\text{ times}}\) if \(i \ge 0\). Also, \(\alpha ^0 = \operatorname {id}_X\). Also, \(\alpha ^{-1}\) is the inverse of \(\alpha \) in the group \(S_X\), that is, the inverse of the map \(\alpha \).

Definition 3.3
#

Let \(n \in \mathbb {Z}\). Then, \([n]\) shall mean the set \(\{ 1, 2, \ldots , n\} \). This is an \(n\)-element set if \(n \ge 0\), and is an empty set if \(n \le 0\).

The symmetric group \(S_{[n]}\) (consisting of all permutations of \([n]\)) will be denoted \(S_n\) and called the \(n\)-th symmetric group. Its size is \(n!\) (when \(n \ge 0\)).

Proposition 3.4

Let \(X\) and \(Y\) be two sets, and let \(f : X \to Y\) be a bijection. Then, for each permutation \(\sigma \) of \(X\), the map \(f \circ \sigma \circ f^{-1} : Y \to Y\) is a permutation of \(Y\). Furthermore, the map

\begin{align*} S_f : S_X & \to S_Y, \\ \sigma & \mapsto f \circ \sigma \circ f^{-1} \end{align*}

is a group isomorphism; thus, we obtain \(S_X \cong S_Y\).

Proof

Easy and LTTR.

Definition 3.5
#

Let \(n \in \mathbb {N}\) and \(\sigma \in S_n\). We introduce three notations for \(\sigma \):

(a) A two-line notation of \(\sigma \) means a \(2 \times n\)-array

\[ \begin{pmatrix} p_1 & p_2 & \cdots & p_n \\ \sigma (p_1) & \sigma (p_2) & \cdots & \sigma (p_n) \end{pmatrix}, \]

where the entries \(p_1, p_2, \ldots , p_n\) of the top row are the \(n\) elements of \([n]\) in some order. Commonly, we pick \(p_i = i\).

(b) The one-line notation (short, OLN) of \(\sigma \) means the \(n\)-tuple \((\sigma (1), \sigma (2), \ldots , \sigma (n))\).

(c) The cycle digraph of \(\sigma \) is the directed graph with vertices \(1, 2, \ldots , n\) and arcs \(i \to \sigma (i)\) for all \(i \in [n]\).

Lemma 3.6

Two vertices \(i\) and \(j\) are in the same connected component of the cycle digraph of \(\sigma \) if and only if there exists \(k \in \mathbb {Z}\) with \(\sigma ^k(i) = j\).

theorem AlgebraicCombinatorics.cycleDigraph_connected_iff {n : } (σ : Sn n) (i j : Fin n) :
(cycleDigraph σ).Reachable i j ∃ (k : ), (σ ^ k) i = j
Proof

By induction on reachability paths: each step corresponds to applying \(\sigma \) or \(\sigma ^{-1}\), so the integer exponent \(k\) accumulates additively. Conversely, for any integer \(k\), the sequence \(i, \sigma (i), \sigma ^2(i), \ldots \) (or the reverse via \(\sigma ^{-1}\)) gives a path in the cycle digraph.

3.1.2 Transpositions, cycles and involutions

Transpositions

Definition 3.7
#

Let \(i\) and \(j\) be two distinct elements of a set \(X\).

Then, the transposition \(t_{i,j}\) is the permutation of \(X\) that sends \(i\) to \(j\), sends \(j\) to \(i\), and leaves all other elements of \(X\) unchanged.

Lemma 3.8

For any two distinct elements \(i, j\) of a set \(X\), we have \(t_{i,j} = t_{j,i}\).

Proof

Immediate from the definitions: both \(t_{i,j}\) and \(t_{j,i}\) swap \(i\) and \(j\) and fix all other elements.

Lemma 3.9

Every transposition is an involution: \(t_{i,j}^2 = \operatorname {id}\).

Proof

Case-split on each element \(x\): if \(x = i\), then \(t_{i,j}(t_{i,j}(i)) = t_{i,j}(j) = i\); similarly for \(x = j\); otherwise \(t_{i,j}\) fixes \(x\).

Lemma 3.10

A transposition is its own inverse: \(t_{i,j}^{-1} = t_{i,j}\).

Proof

Immediate from \(t_{i,j}^2 = \operatorname {id}\).

Lemma 3.11

The number of transpositions in \(S_X\) (for a finite set \(X\)) is \(\binom {|X|}{2}\).

theorem AlgebraicCombinatorics.num_transpositions (X : Type u_1) [DecidableEq X] [Fintype X] :
∃ (S : Finset (Equiv.Perm X)), (∀ σS, σ.IsSwap) (∀ (σ : Equiv.Perm X), σ.IsSwapσ S) S.card = (Fintype.card X).choose 2
Proof

Each \(2\)-element subset \(\{ i,j\} \subseteq X\) gives rise to exactly one transposition \(t_{i,j}\). The bijection between swaps and non-diagonal elements of \(\mathrm{Sym}^2(X)\) establishes the count.

Definition 3.12
#

Let \(n \in \mathbb {N}\) and \(i \in [n-1]\). Then, the simple transposition \(s_i\) is defined by

\[ s_i := t_{i, i+1} \in S_n. \]
Lemma 3.13

Every simple transposition \(s_i\) is a swap (i.e., a \(2\)-cycle).

Proof

Witness the pair \((i, i+1)\) with \(i \ne i+1\).

Lemma 3.14

Every simple transposition \(s_i\) is a cycle (specifically, a \(2\)-cycle).

Proof

A swap is always a cycle: any permutation that exchanges exactly two distinct elements is a \(2\)-cycle.

Lemma 3.15

The support of \(s_i\) is exactly \(\{ i, i+1\} \), and has cardinality \(2\).

Proof

The support of a swap of two distinct elements is exactly \(\{ i, i+1\} \), since \(i \ne i+1\).

Lemma 3.16

For \(n \ge 2\) and \(i \in [n-1]\), we have \(s_i \ne \operatorname {id}\).

Proof

The support of \(s_i\) has cardinality \(2\), but the identity has empty support.

Proposition 3.17

Let \(n \in \mathbb {N}\).

(a) We have \(s_i^2 = \operatorname {id}\) for all \(i \in [n-1]\). In other words, we have \(s_i = s_i^{-1}\) for all \(i \in [n-1]\).

(b) We have \(s_i s_j = s_j s_i\) for any \(i, j \in [n-1]\) with \(|i - j| {\gt} 1\).

(c) We have \(s_i s_{i+1} s_i = s_{i+1} s_i s_{i+1}\) for any \(i \in [n-2]\).

Proof

To prove that two permutations \(\alpha \) and \(\beta \) of \([n]\) are identical, it suffices to show that \(\alpha (k) = \beta (k)\) for each \(k \in [n]\). Using this strategy, we can prove all three parts straightforwardly (distinguishing cases corresponding to the relative positions of \(k\), \(i\), \(i+1\), \(j\) and \(j+1\)). This is done in detail for part (c) in [ Grinbe15 , solution to Exercise 5.1 (a) ] ; the proofs of parts (a) and (b) are easier and LTTR.

Cycles

Definition 3.18
#

Let \(X\) be a set. Let \(i_1, i_2, \ldots , i_k\) be \(k\) distinct elements of \(X\). Then,

\[ \operatorname {cyc}_{i_1, i_2, \ldots , i_k} \]

means the permutation of \(X\) that sends

\begin{align*} & i_1 \text{ to } i_2, \\ & i_2 \text{ to } i_3, \\ & \ldots , \\ & i_{k-1} \text{ to } i_k, \\ & i_k \text{ to } i_1 \end{align*}

and leaves all other elements of \(X\) unchanged. In other words, \(\operatorname {cyc}_{i_1, i_2, \ldots , i_k}\) means the permutation of \(X\) that satisfies

\[ \operatorname {cyc}_{i_1, \ldots , i_k}(p) = \begin{cases} i_{j+1}, & \text{if } p = i_j \text{ for some } j \in \{ 1, 2, \ldots , k\} ;\\ p, & \text{otherwise} \end{cases} \]

for every \(p \in X\), where \(i_{k+1}\) means \(i_1\).

This permutation is called a \(k\)-cycle.

theorem AlgebraicCombinatorics.cyc_apply_getElem {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) (j : ) (hj : j < l.length) :
(cyc l) l[j] = l[(j + 1) % l.length]
theorem AlgebraicCombinatorics.cyc_apply_of_not_mem {X : Type u_1} [DecidableEq X] {l : List X} {x : X} (h : xl) :
(cyc l) x = x
Lemma 3.19

A \(2\)-cycle is exactly a transposition: \(\operatorname {cyc}_{i,j} = t_{i,j}\).

theorem AlgebraicCombinatorics.cyc_pair {X : Type u_1} [DecidableEq X] (i j : X) :
Proof

Immediate from the definitions: both sides send \(i\) to \(j\), send \(j\) to \(i\), and fix all other elements.

Lemma 3.20

If the list \([i_1, \ldots , i_k]\) has no duplicates and \(k \ge 2\), then \(\operatorname {cyc}_{i_1, \ldots , i_k}\) is a cycle (i.e., it has exactly one nontrivial orbit).

theorem AlgebraicCombinatorics.cyc_isCycle {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) (hn : 2 l.length) :
Proof

The cycle permutation of a list with no duplicates and length \(\ge 2\) acts with exactly one nontrivial orbit, hence is a cycle.

Lemma 3.21

Cyclic rotation of the list does not change the cycle: \(\operatorname {cyc}_{i_1, i_2, \ldots , i_k} = \operatorname {cyc}_{i_2, i_3, \ldots , i_k, i_1} = \cdots = \operatorname {cyc}_{i_k, i_1, \ldots , i_{k-1}}\).

theorem AlgebraicCombinatorics.cyc_rotate {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) (n : ) :
cyc (l.rotate n) = cyc l
Proof

A \(k\)-cycle constructed from a list is invariant under cyclic rotation of that list.

Lemma 3.22

For a nodup list \(l = [i_1, \ldots , i_k]\) and \(x \in l\), we have \(\operatorname {cyc}(l)(x)\) equal to the next element after \(x\) in \(l\) (wrapping around at the end).

theorem AlgebraicCombinatorics.cyc_apply_eq_next {X : Type u_1} [DecidableEq X] {l : List X} (hl : l.Nodup) {x : X} (hx : x l) :
(cyc l) x = l.next x hx
Proof

This is a standard property of cycle permutations constructed from lists.

Lemma 3.23

For a nodup list of length \(\ge 2\), the support of \(\operatorname {cyc}_{i_1, \ldots , i_k}\) equals \(\{ i_1, \ldots , i_k\} \).

Proof

The support of a cycle is exactly the set of elements in the list.

Lemma 3.24

For nodup lists \(l, l'\) of length \(\ge 2\), \(\operatorname {cyc}(l) = \operatorname {cyc}(l')\) if and only if \(l\) and \(l'\) are cyclic rotations of each other.

theorem AlgebraicCombinatorics.cyc_eq_cyc_iff_isRotated {X : Type u_1} [DecidableEq X] {l l' : List X} (hl : l.Nodup) (hl' : l'.Nodup) (hlen : 2 l.length) (_hlen' : 2 l'.length) :
cyc l = cyc l' l ~r l'
Proof

Two cycle permutations constructed from nodup lists of length \(\ge 2\) are equal if and only if the lists are cyclic rotations of each other.

Lemma 3.25

If \(\sigma \) is a cycle with \(|\mathrm{support}(\sigma )| = 2\), then \(\sigma \) is a transposition: there exist distinct \(i, j\) with \(\sigma = t_{i,j}\).

theorem AlgebraicCombinatorics.cycle_eq_transposition {X : Type u_1} [DecidableEq X] [Fintype X] {σ : Equiv.Perm X} ( : σ.IsCycle) (hcard : σ.support.card = 2) :
∃ (i : X) (j : X), i j σ = Equiv.swap i j
Proof

Since \(\sigma \) is a cycle with support of size \(2\), its order is \(2\), so \(\sigma ^2 = 1\). Then \(\sigma (\sigma (x)) = x\) for all \(x\). A cycle of order \(2\) must be a swap of two elements, giving the result.

Exercise 3.26

Let \(n \in \mathbb {N}\) and let \(k \in [n]\). Let \(X\) be an \(n\)-element set. How many \(k\)-cycles exist in \(S_X\)?

Proof

First, we note that there is exactly one \(1\)-cycle in \(S_X\) (for \(n {\gt} 0\)), since a \(1\)-cycle is just the identity map. This should be viewed as a degenerate case; thus, we WLOG assume that \(k {\gt} 1\).

For any \(k\) distinct elements \(i_1, i_2, \ldots , i_k\) of \(X\), we have \(\operatorname {cyc}_{i_1, i_2, \ldots , i_k} = \operatorname {cyc}_{i_2, i_3, \ldots , i_k, i_1} = \cdots = \operatorname {cyc}_{i_k, i_1, i_2, \ldots , i_{k-1}}\). That is, \(\operatorname {cyc}_{i_1, i_2, \ldots , i_k}\) does not change if we cyclically rotate the list \((i_1, i_2, \ldots , i_k)\).

Any \(k\)-cycle \(\operatorname {cyc}_{i_1, i_2, \ldots , i_k}\) uniquely determines the elements \(i_1, i_2, \ldots , i_k\) up to cyclic rotation (since \(k {\gt} 1\)). Therefore, if \(\sigma \in S_X\) is a \(k\)-cycle, then there are precisely \(k\) lists \((i_1, i_2, \ldots , i_k)\) for which \(\sigma = \operatorname {cyc}_{i_1, i_2, \ldots , i_k}\).

Hence, the map

\begin{align*} f : \{ k\text{-tuples of distinct elements of } X\} & \to \{ k\text{-cycles in } S_X\} , \\ (i_1, i_2, \ldots , i_k) & \mapsto \operatorname {cyc}_{i_1, i_2, \ldots , i_k} \end{align*}

is a \(k\)-to-\(1\) map. Therefore,

\begin{align*} (\text{\# of } k\text{-cycles in } S_X) & = \frac{1}{k} \cdot n(n-1)(n-2) \cdots (n-k+1) \\ & = \binom {n}{k} \cdot (k-1)!. \end{align*}

Involutions

Definition 3.27
#

Let \(X\) be a set. An involution of \(X\) means a map \(f : X \to X\) that satisfies \(f \circ f = \operatorname {id}\). Clearly, an involution is always a permutation, and equals its own inverse.

Lemma 3.28

Any transposition \(t_{i,j}\) is an involution.

Proof

This is exactly \(t_{i,j}^2 = \operatorname {id}\).

Lemma 3.29

The cycle digraph of an involution of a finite set consists of \(1\)-cycles and \(2\)-cycles only. That is, every cycle factor of an involution has support of size at most \(2\).

Proof

Let \(c\) be a cycle factor of the involution \(\sigma \). Since \(c\) agrees with \(\sigma \) on its support and \(\sigma ^2 = 1\), we get \(c^2 = 1\) (by checking on both the support and its complement). For a cycle, \(\operatorname {orderOf}(c) = |{\operatorname {supp}(c)}|\), so \(|{\operatorname {supp}(c)}| \mid 2\), giving \(|{\operatorname {supp}(c)}| \le 2\).

3.1.3 Further properties of involutions

Lemma 3.30

The order of an involution divides \(2\).

Proof

From \(\sigma ^2 = 1\), we get \(\operatorname {orderOf}(\sigma ) \mid 2\).

Lemma 3.31

A nontrivial involution (i.e., \(\sigma \ne \operatorname {id}\)) has order exactly \(2\).

Proof

Since \(\operatorname {orderOf}(\sigma ) \mid 2\) and \(2\) is prime, \(\operatorname {orderOf}(\sigma ) \in \{ 1, 2\} \). The case \(\operatorname {orderOf}(\sigma ) = 1\) gives \(\sigma = 1\), contradicting \(\sigma \ne 1\).

Lemma 3.32

A \(k\)-cycle with \(k {\gt} 2\) is never an involution.

Proof

If \(\sigma \) is a \(k\)-cycle, then \(\operatorname {orderOf}(\sigma ) = k\). If \(\sigma \) were an involution, then \(k \mid 2\), so \(k \leq 2\), contradicting \(k {\gt} 2\).

Lemma 3.33

A product of pairwise disjoint transpositions is an involution.

theorem AlgebraicCombinatorics.isInvolution_of_disjoint_transpositions {X : Type u_1} [DecidableEq X] {pairs : List (X × X)} (hdisjoint : List.Pairwise (fun (p q : X × X) => p.1 q.1 p.1 q.2 p.2 q.1 p.2 q.2) pairs) (hdistinct : ppairs, p.1 p.2) :
IsInvolution (List.map (fun (p : X × X) => transposition p.1 p.2) pairs).prod
Proof

Let \(\sigma = t_1 t_2 \cdots t_m\) where the \(t_i\) are pairwise disjoint transpositions. Since disjoint permutations commute, \(\sigma ^2 = t_1^2 t_2^2 \cdots t_m^2 = 1\).

Lemma 3.34

Every involution of a finite set is a product of pairwise disjoint transpositions.

theorem AlgebraicCombinatorics.involution_is_product_of_disjoint_transpositions {X : Type u_1} [DecidableEq X] [Fintype X] {σ : Equiv.Perm X} (h : IsInvolution σ) :
∃ (pairs : List (X × X)), List.Pairwise (fun (p q : X × X) => p.1 q.1 p.1 q.2 p.2 q.1 p.2 q.2) pairs (∀ ppairs, p.1 p.2) σ = (List.map (fun (p : X × X) => transposition p.1 p.2) pairs).prod
Proof

By Lemma 3.29, every cycle factor of \(\sigma \) has support of size at most \(2\). The cycle factorization of \(\sigma \) only contains cycles of length \(\geq 2\), so each cycle factor is a transposition. The cycle factors are pairwise disjoint, and their product equals \(\sigma \).