Auxiliary results on permutations

Cycles of a permutation

The cycles of a permutation f : X → X are defined as the equivalence classes of X quotiented by the equivalence relation of being in the same cycle: x₁ ∼ x₂ ↔ ∃ k : ℤ, fᵏ x₁ = x₂.

To avoid working with cardinalities of quotients, we introduce a lemma that enables us to work with cardinalities of finite sets instead. For a permutation f, we can construct a set of representatives of its cycles, that is, a set that contains exactly one element of X from every cycle of f. The number of cycles of f is equal to the cardinality of any such set of representatives of its cycles.

@[reducible, inline]

abbrev CyclesOfPermutation.numCyclesOfPerm {X : Type u} (f : Equiv.Perm X) [Fintype (Quotient (Equiv.Perm.SameCycle.setoid f))] : ℕ

The number of cycles in the permutation f. Cycles with only a single element are also counted, e.g., c[0, 1] : Equiv.Perm (Fin 3) has two cycles.

Equations

• CyclesOfPermutation.numCyclesOfPerm f = Fintype.card (Quotient (Equiv.Perm.SameCycle.setoid f))

theorem CyclesOfPermutation.numCyclesOfPerm_eq_card {X : Type u} {f : Equiv.Perm X} [Fintype (Quotient (Equiv.Perm.SameCycle.setoid f))] {s : Finset X} (h1 : ∀ x ∈ s, ∀ y ∈ s, f.SameCycle x y → x = y) (h2 : ∀ (x : X), ∃ y ∈ s, f.SameCycle x y) : CyclesOfPermutation.numCyclesOfPerm f = s.card

The number of cycles of a permutation f : X → X is equal to the cardinality of any set of representatives of its cycles. That is, any set that contains exactly one element of X from every cycle of f.

Powers of a permutation

Repeatedly applying a permutation of a finite set on some element will eventually result in that same element. If fⁿ⁺¹ x = x, then for any k ∈ ℤ, we have fᵏ x = fᵐ x for some m ∈ {0, ..., n}.

theorem PowersOfPermutation.exists_perm_pow {X : Type u} [DecidableEq X] [Fintype X] (f : Equiv.Perm X) (x : X) : ∃ (n : ℕ), (f ^ (n + 1)) x = x

Given a permutation on a finite type f : X → X and any x : X there exists n : ℕ such that fⁿ⁺¹ x = x.

theorem PowersOfPermutation.perm_pow_reduce {X : Type u} {n m r : ℕ} {f : Equiv.Perm X} {x : X} (h : (f ^ n) x = x) : (f ^ (m * n + r)) x = (f ^ r) x

Given a permutation f satisfying fⁿ x = x we can reduce fⁿ*ᵐ⁺ʳ x to fʳ x.

theorem PowersOfPermutation.forall_exists_lt_perm_pow_eq_perm_pow {X : Type u} {n : ℕ} {f : Equiv.Perm X} {x : X} (h : (f ^ (n + 1)) x = x) (k : ℤ) : ∃ m < n + 1, (f ^ k) x = (f ^ m) x

Given a permutation f satisfying fⁿ⁺¹ x = x for some n : ℕ, then for any k : ℤ, fᵏ x = fᵐ x for some m ∈ {0, ..., n}.

Contraction or expansion of a domain of a permutation

We can contract a permutation f on Fin (n + 1) by removing n from the domain and remapping f⁻¹ n ↦ f n. We get a permutation on Fin n. We can expand a permutation f on Fin n by adding n to the domain and defining f n = n. We get a permutation on Fin (n + 1).

theorem ContractExpand.lt_of_lt_succ_of_neq {n m : ℕ} (h1 : m < n + 1) (h2 : m ≠ n) : m < n

If n < m + 1 and n ≠ m then n < m.

theorem ContractExpand.perm_perm_val_lt_of_perm_val_eq {n : ℕ} {f : Equiv.Perm (Fin (n + 1))} {i : Fin n} (h : ↑(f ↑↑i) = n) : ↑(f (f ↑↑i)) < n

For any permutation f of Fin (n + 1), if f i = n for some i < n, then f (f i) < n.

def ContractExpand.permContract {n : ℕ} (f : Equiv.Perm (Fin (n + 1))) : Equiv.Perm (Fin n)

A function that takes a permutation f of Fin (n + 1) and returns a permutation of Fin n that behaves exactly the same as f on all inputs except on f⁻¹ n, where it returns f n, and n, which is no longer a valid input.

Equations

• One or more equations did not get rendered due to their size.

def ContractExpand.permExpand {n : ℕ} (f : Equiv.Perm (Fin n)) : Equiv.Perm (Fin (n + 1))

A function that takes a permutation f of Fin n and returns a permutation of Fin (n + 1) that behaves exactly the same as f on all inputs except on n, where it returns n.

Equations

• One or more equations did not get rendered due to their size.