The same-cycle quotient of a permutation

The orbit space of a permutation of Fin n under the same-cycle relation, its fintype structure, orbit sizes, and the identification of functions fixed by the permutation with functions on the orbit space. This is the indexing object for the cycle-sum identity: a permutation's completed cycle-type product expands as a sum over colourings of its orbits.

def RS.sameCycleSetoid {n : ℕ} (π : Equiv.Perm (Fin n)) : Setoid (Fin n)

The same-cycle setoid of a permutation.

Equations

• RS.sameCycleSetoid π = { r := fun (a b : Fin n) => π.SameCycle a b, iseqv := ⋯ }

def RS.OrbitSpace {n : ℕ} (π : Equiv.Perm (Fin n)) : Type

The orbit space of a permutation.

Equations

• RS.OrbitSpace π = Quotient (RS.sameCycleSetoid π)

def RS.orbitOf {n : ℕ} (π : Equiv.Perm (Fin n)) (i : Fin n) : OrbitSpace π

The class of a point.

Equations

• RS.orbitOf π i = ⟦i⟧

theorem RS.orbitOf_eq_iff {n : ℕ} (π : Equiv.Perm (Fin n)) {i j : Fin n} : orbitOf π i = orbitOf π j ↔ π.SameCycle i j

Two points have the same class exactly when they are on the same cycle.

theorem RS.orbitOf_surjective {n : ℕ} (π : Equiv.Perm (Fin n)) : Function.Surjective (orbitOf π)

Every orbit is the class of a point.

@[instance_reducible]

noncomputable instance RS.instFintypeOrbitSpace {n : ℕ} (π : Equiv.Perm (Fin n)) : Fintype (OrbitSpace π)

The orbit space is finite, being a quotient of a finite type.

Equations

• RS.instFintypeOrbitSpace π = Quotient.fintype (RS.sameCycleSetoid π)

noncomputable def RS.orbFibre {n : ℕ} (π : Equiv.Perm (Fin n)) (O : OrbitSpace π) : Finset (Fin n)

The fibre of an orbit: the points lying in it.

Equations

• RS.orbFibre π O = {i : Fin n | RS.orbitOf π i = O}

noncomputable def RS.orbCard {n : ℕ} (π : Equiv.Perm (Fin n)) (O : OrbitSpace π) : ℕ

The size of an orbit.

Equations

• RS.orbCard π O = (RS.orbFibre π O).card

theorem RS.mem_orbFibre {n : ℕ} (π : Equiv.Perm (Fin n)) {O : OrbitSpace π} {i : Fin n} : i ∈ orbFibre π O ↔ orbitOf π i = O

Membership in an orbit's fibre.

theorem RS.orbFibre_nonempty {n : ℕ} (π : Equiv.Perm (Fin n)) (O : OrbitSpace π) : (orbFibre π O).Nonempty

Every fibre is nonempty.

theorem RS.orbCard_pos {n : ℕ} (π : Equiv.Perm (Fin n)) (O : OrbitSpace π) : 0 < orbCard π O

Hence every orbit has positive size.

theorem RS.fixed_comp_zpow {n : ℕ} (π : Equiv.Perm (Fin n)) {C : Type u_1} {f : Fin n → C} (hf : f ∘ ⇑π = f) (k : ℤ) : f ∘ ⇑(π ^ k) = f

A function fixed by π is constant along powers.

noncomputable def RS.fixedFunEquiv {n : ℕ} (π : Equiv.Perm (Fin n)) (C : Type u_1) : { f : Fin n → C // f ∘ ⇑π = f } ≃ (OrbitSpace π → C)

Functions fixed by the permutation are exactly the functions on the orbit space.

Equations

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

@[simp]

theorem RS.fixedFunEquiv_apply_orbitOf {n : ℕ} (π : Equiv.Perm (Fin n)) {C : Type u_1} (f : { f : Fin n → C // f ∘ ⇑π = f }) (i : Fin n) : (fixedFunEquiv π C) f (orbitOf π i) = ↑f i

The identification reads a fixed function's value at any point of the orbit.