The permutation module on a colour class

The symmetric group Equiv.Perm (Fin n) acts on the colour class {g : Fin n → Fin N // ∀ j, fibreCard g j = α j} by precomposition with the inverse. The resulting ofMulAction representation has character equal to colourChar α.

def RS.colourClass (n : ℕ) {N : ℕ} (α : Fin N → ℕ) : Type

The colour class: colourings with prescribed fibre sizes.

Equations

• RS.colourClass n α = { g : Fin n → Fin N // ∀ (j : Fin N), RS.fibreCard g j = α j }

@[instance_reducible]

noncomputable instance RS.colourClass.fintype (n : ℕ) {N : ℕ} (α : Fin N → ℕ) : Fintype (colourClass n α)

A colour class is finite.

Equations

• RS.colourClass.fintype n α = Subtype.fintype fun (g : Fin n → Fin N) => ∀ (j : Fin N), RS.fibreCard g j = α j

@[instance_reducible]

noncomputable instance RS.colourClass.decidableEq (n : ℕ) {N : ℕ} (α : Fin N → ℕ) : DecidableEq (colourClass n α)

And its members can be compared.

Equations

• RS.colourClass.decidableEq n α = Classical.decEq (RS.colourClass n α)

@[instance_reducible]

instance RS.colourClass.mulAction {n N : ℕ} (α : Fin N → ℕ) : MulAction (Equiv.Perm (Fin n)) (colourClass n α)

The symmetric group acts on the colour class by precomposition with the inverse permutation.

Equations

• RS.colourClass.mulAction α = { smul := fun (π : Equiv.Perm (Fin n)) (g : RS.colourClass n α) => ⟨↑g ∘ ⇑π⁻¹, ⋯⟩, mul_smul := ⋯, one_smul := ⋯ }

noncomputable def RS.colourRep {n N : ℕ} (α : Fin N → ℕ) : Representation ℂ (Equiv.Perm (Fin n)) (MonoidAlgebra ℂ (colourClass n α))

The permutation representation on the colour class.

Equations

• RS.colourRep α = Representation.ofMulAction ℂ (Equiv.Perm (Fin n)) (RS.colourClass n α)

theorem RS.colourRep_character {n N : ℕ} (α : Fin N → ℕ) (π : Equiv.Perm (Fin n)) : (colourRep α).character π = ↑(colourChar α π)

The character of the colour-class permutation representation equals the combinatorial colour character.

theorem RS.card_orbitSpace (n : ℕ) (π : Equiv.Perm (Fin n)) : Fintype.card (OrbitSpace π) = π.cycleType.card + (n - π.cycleType.sum)

The number of orbits equals cycleType.card + (n - cycleType.sum).