The block-cycle normal form

Every permutation is conjugate to a block sum of rotations whose block lengths are its full cycle type (fixed points included): the normal form against which the skein trace of a permutation factors into cycle loops.

noncomputable def RS.blockCycles (l : List ℕ) : Equiv.Perm (Fin l.sum)

The block sum of rotations prescribed by a list of block lengths.

Equations

• RS.blockCycles [] = 1
• RS.blockCycles (c :: rest) = finSumFinEquiv.permCongr (Equiv.sumCongr (finRotate c) (RS.blockCycles rest))

noncomputable def RS.fullCycleType {n : ℕ} (π : Equiv.Perm (Fin n)) : Multiset ℕ

The full cycle type: the cycle type completed by the fixed points as one-cycles.

Equations

• RS.fullCycleType π = π.cycleType + Multiset.replicate (n - π.cycleType.sum) 1

theorem RS.fullCycleType_sum {n : ℕ} (π : Equiv.Perm (Fin n)) : (fullCycleType π).sum = n

The full cycle type sums to the degree.

The cycle type of a block sum

theorem RS.cycleType_blockCycles (l : List ℕ) (hl : ∀ c ∈ l, 1 ≤ c) : (blockCycles l).cycleType = ↑(List.filter (fun (c : ℕ) => decide (2 ≤ c)) l)

The block cycles realize a prescribed full cycle type.

theorem RS.exists_conj_blockCycles {n : ℕ} (π : Equiv.Perm (Fin n)) : ∃ (l : List ℕ) (h : l.sum = n) (σ : Equiv.Perm (Fin n)), (∀ c ∈ l, 1 ≤ c) ∧ ↑l = fullCycleType π ∧ σ * (finCongr h).permCongr (blockCycles l) * σ⁻¹ = π

The normal form: every permutation is conjugate to the block sum of rotations along its full cycle type.