Disjoint cycle notation

A permutation of a finite type is written in disjoint cycle notation as a list of cycles, each cycle a list of points traversed in order, such that no point is listed twice and every cycle has at least two points. Fixed points are omitted, and the identity is the empty list of cycles. The cycle l denotes List.formPerm l, sending each listed point to the next and the last back to the first, and the notation denotes the product of its cycles. The cycles are disjoint, so they commute and the product does not depend on their order.

Equiv.Perm.IsCycleNotation σ p says that p is a disjoint cycle notation for σ. The lengths of the listed cycles are then the cycle type of σ, the listed points are its support, and the full cycle partition of σ is recovered by padding the lengths with one part equal to one for each point not listed. Reversing every cycle gives a notation for the inverse, and every permutation has a notation.

Main definitions

• Equiv.Perm.IsCycleNotation: p is a disjoint cycle notation for σ.

Main results

• Equiv.Perm.IsCycleNotation.cycleType_eq: the cycle type is the multiset of listed lengths.
• Equiv.Perm.IsCycleNotation.parts_partition_eq: the full cycle partition is the listed lengths padded by fixed points.
• Equiv.Perm.IsCycleNotation.inv: reversing every cycle writes the inverse.
• Equiv.Perm.exists_isCycleNotation: every permutation has a disjoint cycle notation.

References

The proof of Equiv.Perm.IsCycleNotation.cycleType_eq follows the cycle-type computation in the construction half of Mathlib's Equiv.Perm.exists_with_cycleType_iff (Mathlib/GroupTheory/Perm/Cycle/PossibleTypes.lean).

structure Equiv.Perm.IsCycleNotation {α : Type u_1} [DecidableEq α] (σ : Perm α) (p : List (List α)) : Prop

p is a disjoint cycle notation for σ: no point is listed twice, every listed cycle has at least two points, and σ is the product of the cycles List.formPerm l for l ∈ p. Fixed points of σ are not listed, and the identity is written as the empty list.

• nodup_flatten : p.flatten.Nodup

  No point is listed twice.

• two_le_length (l : List α) : l ∈ p → 2 ≤ l.length

  Every listed cycle has at least two points.

• prod_map_formPerm : (List.map List.formPerm p).prod = σ

  The permutation is the product of the listed cycles.

@[simp]

theorem Equiv.Perm.isCycleNotation_nil_iff {α : Type u_1} [DecidableEq α] {σ : Perm α} : σ.IsCycleNotation [] ↔ σ = 1

The empty list of cycles writes exactly the identity.

theorem Equiv.Perm.IsCycleNotation.nodup {α : Type u_1} [DecidableEq α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) {l : List α} (hl : l ∈ p) : l.Nodup

Every listed cycle lists distinct points.

theorem Equiv.Perm.IsCycleNotation.pairwise_disjoint {α : Type u_1} [DecidableEq α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) : List.Pairwise Disjoint (List.map List.formPerm p)

The listed cycles are disjoint permutations.

theorem Equiv.Perm.IsCycleNotation.isCycle_formPerm {α : Type u_1} [DecidableEq α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) {l : List α} (hl : l ∈ p) : l.formPerm.IsCycle

Every listed cycle is a cycle.

theorem Equiv.Perm.IsCycleNotation.of_cons {α : Type u_1} [DecidableEq α] {σ : Perm α} {p : List (List α)} {l : List α} (h : σ.IsCycleNotation (l :: p)) : (List.map List.formPerm p).prod.IsCycleNotation p

Dropping the first cycle of a disjoint cycle notation leaves a notation for the product of the remaining cycles.

theorem Equiv.Perm.IsCycleNotation.apply_ne_self_iff {α : Type u_1} [DecidableEq α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) {x : α} : σ x ≠ x ↔ x ∈ p.flatten

A point is moved by σ exactly when it is listed.

theorem Equiv.Perm.IsCycleNotation.inv {α : Type u_1} [DecidableEq α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) : σ⁻¹.IsCycleNotation (List.map List.reverse p)

Inverse in cycle notation: reversing every cycle of a disjoint cycle notation for σ gives one for σ⁻¹.

theorem Equiv.Perm.exists_isCycleNotation {α : Type u_1} [DecidableEq α] [Finite α] (σ : Perm α) : ∃ (p : List (List α)), σ.IsCycleNotation p

Every permutation has a disjoint cycle notation.

theorem Equiv.Perm.IsCycleNotation.support_eq {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) : σ.support = p.flatten.toFinset

The support of a permutation is the set of listed points.

theorem Equiv.Perm.IsCycleNotation.cycleType_eq {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) : σ.cycleType = ↑(List.map List.length p)

The cycle type is read off a disjoint cycle notation: it is the multiset of lengths of the listed cycles.

theorem Equiv.Perm.IsCycleNotation.card_support {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) : σ.support.card = (List.map List.length p).sum

The number of points moved by a permutation is the total length of the listed cycles.

theorem Equiv.Perm.IsCycleNotation.parts_partition_eq {α : Type u_1} [DecidableEq α] [Fintype α] {σ : Perm α} {p : List (List α)} (h : σ.IsCycleNotation p) : σ.partition.parts = ↑(List.map List.length p) + Multiset.replicate (Fintype.card α - (List.map List.length p).sum) 1

The full cycle partition from a disjoint cycle notation: the lengths of the listed cycles, padded by one part equal to one for each point that is not listed.