The Cycle Decomposition #
This file formalizes the cycle decomposition (or disjoint cycle decomposition) of a permutation, as presented in Section "The cycle decomposition" of the source text.
Main definitions #
numCyclesTotal: The total number of cycles including 1-cycles (fixed points).numCycles: The number of non-trivial cycles (length ≥ 2).cycles: The set of cycles of a permutation.cycleLengthsPartition: The partition of n given by cycle lengths.dcdListToPerm: Convert a list of lists (representing cycles) to a permutation.
Main results #
sameCycle_iff_exists_pow: Two elements belong to the same cycle iff one is a power of the permutation applied to the other (Proposition \ref{prop.perm.cycs.same}).exists_dcd: Every permutation can be written as a product of disjoint cycles (Theorem \ref{thm.perm.dcd.main} (a)).dcd_unique_cycleType: Any two DCDs of the same permutation have the same cycle type (Theorem \ref{thm.perm.dcd.main} (b)).canonicalDcd_exists_unique: For totally ordered sets, there is a unique canonical DCD (Theorem \ref{thm.perm.dcd.main} (c)).cycleType_eq_iff_isConj: Two permutations have the same cycle type iff they are conjugate.sign_eq_neg_one_pow_card_sub_numCycles: The sign of a permutation equals(-1)^(n - k)wherekis the number of cycles (Proposition \ref{prop.perm.cycs.sign}).
References #
- Theorem \ref{thm.perm.dcd.main} in the source
- Definition \ref{def.perm.cycs.cycs}
- Proposition \ref{prop.perm.cycs.same}
- Proposition \ref{prop.perm.cycs.sign}
Implementation notes #
This file mostly provides wrappers and restatements of Mathlib's existing API for
cycle decomposition (Equiv.Perm.cycleFactorsFinset, Equiv.Perm.cycleType, etc.)
in the language of the source text.
The cycle of a permutation containing a given element #
Mathlib provides Equiv.Perm.cycleOf f x, the cycle of f containing x.
We provide additional characterizations and properties.
Two elements belong to the same cycle of a permutation iff one can be reached from the other by repeated application of the permutation. This is the equivalence from Proposition \ref{prop.perm.cycs.same}.
The forward direction uses that for finite types, zpow can be replaced by pow.
Symmetric version: i and j belong to the same cycle iff j = σ^p(i) for some p.
Disjoint Cycle Decomposition (DCD) #
Mathlib's Equiv.Perm.cycleFactorsFinset provides the set of cycles in the DCD.
The key theorem cycleFactorsFinset_noncommProd states that the product of these
cycles equals the original permutation.
Theorem \ref{thm.perm.dcd.main} (a): Existence of DCD.
The number of cycles of a permutation (including 1-cycles / fixed points). This counts all cycles in the DCD as defined in the source text.
Note: Mathlib's cycleFactorsFinset only includes cycles of length ≥ 2.
To get the total count including 1-cycles, we add the number of fixed points.
Equations
Instances For
The total number of cycles (including 1-cycles) for the identity is the cardinality of α. This is a natural base case for reasoning about cycle decompositions.
The number of cycles (of length ≥ 2) in the DCD.
Instances For
The identity permutation has no non-trivial cycles. This is a natural base case for reasoning about cycle decompositions.
Existence of DCD: Every permutation is a product of disjoint cycles. This is Theorem \ref{thm.perm.dcd.main} (a).
Two permutations have the same cycle type iff they are conjugate.
Note: This is NOT Theorem \ref{thm.perm.dcd.main} (b), which states that any two DCDs of the same permutation can be obtained from each other by swapping cycles and rotating. That result is essentially trivial: any DCD of σ yields the same multiset of cycle lengths (the cycle type), and different DCDs are just reorderings/rotations of the same cycles.
This theorem is a deeper result about when two different permutations have the same cycle structure.
Any two DCDs of the same permutation have the same cycle type (as a multiset of lengths). This captures the essence of Theorem \ref{thm.perm.dcd.main} (b): the cycles of a DCD are uniquely determined up to swapping and rotation, hence they have the same lengths.
In Mathlib's formalization, there is a canonical DCD (cycleFactorsFinset), so this is trivial:
any DCD must produce the same set of cycles as cycleFactorsFinset, just possibly listed
in a different order or with different rotations.
Cycles of a permutation (Definition \ref{def.perm.cycs.cycs}) #
This section formalizes Definition \ref{def.perm.cycs.cycs} from the source text:
Definition (def.perm.cycs.cycs): Let X be a finite set. Let σ be a permutation of X.
(a) The cycles of σ are defined to be the cycles in the DCD of σ (as defined in Theorem \ref{thm.perm.dcd.main} (a)). This includes 1-cycles, if there are any in the DCD of σ.
We shall equate a cycle of σ with any of its cyclic rotations; thus, for example, (3, 1, 4) and (1, 4, 3) shall be regarded as being the same cycle (but (3, 1, 4) and (3, 4, 1) shall not).
(b) The cycle lengths partition of σ shall denote the partition of |X| obtained by writing down the lengths of the cycles of σ in weakly decreasing order.
Implementation note: Mathlib's cycleFactorsFinset only includes cycles of length ≥ 2
(non-trivial cycles). Fixed points (1-cycles) are not included. This differs from the
textbook which includes 1-cycles. However, for most purposes this is equivalent since
1-cycles act as the identity. The numCyclesTotal definition above accounts for this
by adding the number of fixed points.
Regarding cyclic rotations: In Mathlib, cycles are represented as permutations (elements
of Perm α), not as lists. Two cycles that are cyclic rotations of each other represent
the same permutation, so they are automatically equated. For example, the cycles
cyc [3, 1, 4] and cyc [1, 4, 3] are equal as permutations by List.formPerm_rotate.
The cycles of a permutation σ are the elements of σ.cycleFactorsFinset.
Each cycle is a permutation that is a cycle in the graph-theoretic sense.
Note: This only includes cycles of length ≥ 2 (non-trivial cycles).
Fixed points (1-cycles) are not included, following Mathlib's convention.
See numCyclesTotal for the total count including 1-cycles.
(Definition \ref{def.perm.cycs.cycs} (a))
Instances For
The identity permutation has no cycles (of length ≥ 2). This is a natural base case for reasoning about cycle decompositions.
The cycles of σ equal the cycle factors finset from Mathlib.
A permutation c is a cycle of σ iff c is a cycle and c agrees with σ on c's support.
Every element of cycles σ is a cycle.
The cycles of σ are pairwise disjoint (their supports are disjoint).
The cycles of σ pairwise commute (since they are disjoint).
The product of cycles equals σ.
Each cycle in cycles σ has length at least 2.
The cardinality of cycles σ equals the number of non-trivial cycles.
The cycle of σ containing x (when x is not a fixed point) is in cycles σ.
The cycle lengths partition of σ is the partition of |X| obtained by listing the lengths of cycles in weakly decreasing order. (Definition \ref{def.perm.cycs.cycs} (b))
Instances For
The cycle lengths partition of the identity permutation consists of all 1s. This is a natural base case for reasoning about cycle decompositions.
The cycle type as a multiset of cycle lengths.
Instances For
The identity permutation has empty cycle lengths. This is a natural base case for reasoning about cycle decompositions.
The cycle lengths equal the cycle type from Mathlib.
The sum of cycle lengths equals the size of the support.
The number of cycle lengths equals the number of cycles.
Every element of the cycle lengths multiset is at least 2.
The cycle lengths partition has parts equal to the cycle type plus 1-cycles.
The cycle lengths partition sums to |X|.
Cyclic rotations of cycles #
The textbook states that cycles are equated with their cyclic rotations.
In Mathlib, this is automatic since cycles are represented as permutations,
and cyclically rotated lists give the same permutation via List.formPerm_rotate.
Cyclic rotation of a list gives the same cycle permutation. This formalizes the textbook statement that (3, 1, 4) and (1, 4, 3) are the same cycle.
Two lists that are cyclic rotations of each other give the same cycle.
Two elements are in the same cycle iff they are in the same equivalence class under the SameCycle relation.
Note: This requires i ∈ σ.support (i.e., i is not a fixed point) because
cycleFactorsFinset only contains non-trivial cycles (length ≥ 2), so fixed points
are not contained in any cycle's support. For fixed points i = j, we have
σ.SameCycle i i but no cycle containing i.
This is an auxiliary characterization connecting cycle membership (in terms of
cycleFactorsFinset) to the SameCycle relation. The main characterization of
Proposition \ref{prop.perm.cycs.same} is sameCycle_iff_exists_pow above.
Sign and cycle count (Proposition \ref{prop.perm.cycs.sign}) #
The sign of a permutation is determined by its number of cycles.
The sign of a permutation equals (-1)^(n - k) where k is the number of cycles
(including 1-cycles). This is Proposition \ref{prop.perm.cycs.sign}.
We prove this using Mathlib's sign_of_cycleType which gives:
sign f = (-1)^(cycleType.sum + cycleType.card)
The key insight is that for a permutation with k total cycles (including 1-cycles), we have n - k = Σ(m_i - 1) where m_i are the cycle lengths.
The sign of a permutation can also be expressed as (-1)^(Σ(m_i - 1)) where
m_i are the cycle lengths (of length ≥ 2).
The sign of a k-cycle is (-1)^(k-1).
Note: Mathlib's IsCycle.sign gives sign σ = -(-1)^(support.card) which equals
(-1)^(support.card - 1) since -(-1)^n = (-1)^(n-1) for n ≥ 1.
Canonical DCD (Theorem \ref{thm.perm.dcd.main} (c)) #
For a totally ordered finite set, there is a unique DCD where:
- Each cycle starts with its smallest element
- Cycles appear in decreasing order of first elements
This canonical form is useful for comparing permutations.
Helper definitions and lemmas for canonical DCD construction #
We build the canonical DCD by:
- Converting each cycle in
cycleFactorsFinsetto its canonical list (starting from minimum) - Adding singleton lists for fixed points
- Sorting by decreasing first element
Get the minimum element of a cycle's support.
Equations
Instances For
The minimum element is in the support.
The minimum element is moved by c.
Get the canonical list representation of a cycle starting from its minimum element.
Equations
Instances For
The canonical list is nonempty.
The first element of the canonical list is the minimum.
The first element is minimal in the canonical list.
formPerm of the canonical list equals the cycle.
The canonical list is nodup.
Elements of the canonical list are exactly the support.
Canonical lists of disjoint cycles are List.Disjoint.
The cyclesList (list of canonical lists for each cycle) is pairwise List.Disjoint.
The flatten of cyclesList is nodup.
The flatten of cyclesList covers exactly σ.support.
The product of formPerms of cyclesList equals σ.
The fixed points list is pairwise disjoint.
Singletons (fixed points) are disjoint from cyclesList.
Convert a list of lists representing cycles to a permutation by taking the product
of the cycle permutations. Each list [a₁, a₂, ..., aₖ] represents the k-cycle
cyc_{a₁, a₂, ..., aₖ} that sends a₁ → a₂ → ... → aₖ → a₁.
Equations
- AlgebraicCombinatorics.CycleDecomposition.dcdListToPerm cycleReps = (List.map List.formPerm cycleReps).prod