(a) Let \(\mathcal{D}\) be the cycle digraph of \(\sigma \). This cycle digraph \(\mathcal{D}\) has the following two properties:

• Outbound uniqueness: For each node \(i\), there is exactly one arc outgoing from \(i\). (Indeed, this is the arc from \(i\) to \(\sigma \left( i\right) \).)

• Inbound uniqueness: For each node \(i\), there is exactly one arc incoming into \(i\). (Indeed, this is the arc from \(\sigma ^{-1}\left( i\right) \) to \(i\), since \(\sigma \) is a permutation and therefore invertible.)

Using these two properties, we will now show that the cycle digraph \(\mathcal{D}\) consists of several node-disjoint cycles.

Indeed, if two cycles \(C\) and \(D\) of \(\mathcal{D}\) have a node in common, then they are identical (because the outbound uniqueness property prevents these cycles from ever separating after meeting at the common node). In other words, any two cycles \(C\) and \(D\) of \(\mathcal{D}\) are either identical or node-disjoint.

Now, let \(i\) be any node of \(\mathcal{D}\). Then, if we start at \(i\) and follow the outgoing arcs, then we obtain an infinite walk

along our digraph \(\mathcal{D}\). Since \(X\) is finite, the Pigeonhole Principle guarantees that this walk will eventually revisit a node it has already been to; i.e., there exist two integers \(u,v\in \mathbb {N}\) with \(u{\lt}v\) and \(\sigma ^{u}\left( i\right) =\sigma ^{v}\left( i\right) \). Let us pick two such integers \(u,v\) with the smallest possible \(v\). Thus,

(since otherwise, \(v\) would not be smallest possible). Now, \(\sigma \) is a permutation and thus has an inverse \(\sigma ^{-1}\). Applying the map \(\sigma ^{-1}\) to both sides of the equality \(\sigma ^{u}\left( i\right) =\sigma ^{v}\left( i\right) \), we obtain \(\sigma ^{u-1}\left( i\right) =\sigma ^{v-1}\left( i\right) \). However, if we had \(u\geq 1\), then (12) would entail \(\sigma ^{u-1}\left( i\right) \neq \sigma ^{v-1}\left( i\right) \), which would contradict \(\sigma ^{u-1}\left( i\right) =\sigma ^{v-1}\left( i\right) \). Thus, we cannot have \(u\geq 1\). Hence, \(u{\lt}1\), so that \(u=0\). Therefore, \(\sigma ^{u}\left( i\right) =\sigma ^{0}\left( i\right) \), so that \(\sigma ^{0}\left( i\right) =\sigma ^{u}\left( i\right) =\sigma ^{v}\left( i\right) \). This shows that our walk is circular: it comes back to its starting node \(\sigma ^{0}\left( i\right) =i\) after \(v\) steps. We have thus found a cycle in our digraph \(\mathcal{D}\):

This shows that the node \(i\) lies on a cycle \(C_{i}\) of \(\mathcal{D}\).

We thus have shown that each node \(i\) of \(\mathcal{D}\) lies on a cycle \(C_{i}\). Any arc of our digraph \(\mathcal{D}\) must belong to one of these chosen cycles.

Combining these facts, we conclude that \(\mathcal{D}\) consists of several node-disjoint cycles. Let us label these cycles as

(making sure to label each cycle only once). Then, each element of \(X\) appears exactly once in the composite list

and we have

(since \(\sigma \) moves any node \(i\in X\) one step forward along its chosen cycle). This proves Theorem 3.123 (a).

(b) See [ Goodma15 , Theorem 1.5.3 ] or [ Bourba74 , Chapter I, § 5.7, Proposition 7 ] . Let

be a DCD of \(\sigma \). Then, for each \(i\in X\), the cycle of this DCD that contains \(i\) is uniquely determined by \(\sigma \) and \(i\) up to cyclic rotation (indeed, it is a rotated version of the list \(\left( i,\sigma \left( i\right) ,\sigma ^{2}\left( i\right) ,\ldots ,\sigma ^{r-1}\left( i\right) \right) \), where \(r\) is the smallest positive integer satisfying \(\sigma ^{r}\left( i\right) =i\)). Therefore, all cycles of this DCD are uniquely determined by \(\sigma \) up to cyclic rotation and up to the relative order in which these cycles appear in the DCD. This is the claim of Theorem 3.123 (b).

(c) In order to obtain a DCD of \(\sigma \) that satisfies these two requirements, it suffices to

• start with an arbitrary DCD of \(\sigma \),

• then rotate each cycle of this DCD so that it begins with its smallest entry, and

• then repeatedly swap these cycles so they appear in the order of decreasing first entries.

It is clear that the result of this procedure is uniquely determined (a consequence of Theorem 3.123 (b)). Thus, Theorem 3.123 (c) is proven.

This is the cycle factors pairwise disjointness lemma from Mathlib.

The cycles are pairwise disjoint, hence pairwise commuting. Their product equals \(\sigma \) by the cycle factorization theorem from Mathlib.

This is the characterization of cycle factor membership from Mathlib.

This is the conjugacy-iff-same-cycle-type characterization from Mathlib.

Follows from the cycle type summation lemma in Mathlib.

Follows from the fact that each cycle type entry is at least \(2\), which is proved in Mathlib.

This is the defining property of a partition of \(|X|\).

This is the rotation invariance of cycle permutations from Mathlib.

Follows from Lemma 3.133.

The forward direction uses that for finite types, \(\mathbb {Z}\)-powers can be replaced by \(\mathbb {N}\)-powers (reducing \(k\) modulo the order of \(\sigma \)). The backward direction is immediate.

The symmetric version (the third equivalence) follows by applying the first equivalence to \(\sigma ^{-1}\).

For the forward direction, if \(i\) and \(j\) are both in the support of a cycle \(c\), then \(i\) and \(j\) are in the same cycle of \(c\), and since \(c\) is the cycle of \(\sigma \) containing \(i\), this transfers to \(i\) and \(j\) being in the same cycle of \(\sigma \). For the backward direction, the cycle of \(\sigma \) containing \(i\) is among the cycles of \(\sigma \), and both \(i\) and \(j\) belong to its support.

Immediate from the definitions.

This follows from the sign-of-a-cycle lemma in Mathlib, which gives \((-1)^{\sigma } = -(-1)^{k}\) for a \(k\)-cycle \(\sigma \). Since \(-(-1)^k = (-1)^{k-1}\) for \(k \geq 1\), the result follows.

Let

be the \(k\) cycles of \(\sigma \). Thus,

so that, by Proposition 3.110 (e) and (c),

Since each element of \(\left[ n\right] \) appears exactly once in the DCD, we have \(n_{1}+n_{2}+\cdots +n_{k}=n\). Hence,

Thus, \(\left( -1\right) ^{\sigma }=\left( -1\right) ^{n-k}\). This proves Proposition 3.139.

This follows from the sign-from-cycle-type formula in Mathlib by observing that \((m_1 + \cdots + m_j) + j\) and \((m_1 + \cdots + m_j) - j\) have the same parity (they differ by \(2j\)).

The first element is the minimum element of \(c\), and every element in the canonical list belongs to the support of \(c\), so the minimum is \(\leq \) every element.

The canonical list is the orbit of the minimum element under \(c\). The cycle permutation of this list recovers \(c\) because the minimum element is moved by \(c\).

By definition, the minimum element of \(c\) is the minimum of the support, which is an element of the support.

Follows from the no-duplicates property of permutation cycle lists in Mathlib.

The canonical list enumerates the orbit of the minimum element under \(c\), which is exactly the support of \(c\) (since \(c\) is a cycle).

By Lemma 3.147, membership in the canonical list is equivalent to membership in the support. Since \(c\) and \(d\) are disjoint, their supports are disjoint.

Each canonical list determines a cycle permutation that recovers the original cycle (by Lemma 3.144), and the product of all cycles equals \(\sigma \) (by the cycle factorization theorem from Mathlib).

Each individual canonical list is nodup (Lemma 3.146), and different cycles have disjoint canonical lists (Lemma 3.148).

By Lemma 3.147, each canonical list covers exactly the support of its cycle, and the union of all cycle supports equals \(\sigma \)’s support.