Colour classes of prescribed composition

Colourings Fin n → Fin N with prescribed fibre sizes α : Fin N → ℕ: the class count (n! divided by the fibre factorials, in product form), the fixed-colouring permutation character colourChar, and the Fubini exchange expressing its weighted permutation sum as a sum of stabilizer weights over the class.

def RS.compContent {N : ℕ} (α : Fin N → ℕ) : Multiset (Fin N)

The content multiset of a composition.

Equations

• RS.compContent α = ∑ j : Fin N, Multiset.replicate (α j) j

theorem RS.compContent_count {N : ℕ} (α : Fin N → ℕ) (j : Fin N) : Multiset.count j (compContent α) = α j

A composition's content multiset carries each colour as often as prescribed.

theorem RS.compContent_card {N : ℕ} (α : Fin N → ℕ) : (compContent α).card = ∑ j : Fin N, α j

Its size is the composition's total.

def RS.compContentSym {n N : ℕ} (α : Fin N → ℕ) (hsum : ∑ j : Fin N, α j = n) : Sym (Fin N) n

The composition content as a symmetric power, given total n.

Equations

• RS.compContentSym α hsum = ⟨RS.compContent α, ⋯⟩

theorem RS.fibreCard_eq_iff {n N : ℕ} (g : Fin n → Fin N) (α : Fin N → ℕ) : (∀ (j : Fin N), fibreCard g j = α j) ↔ ↑(content g) = compContent α

A colouring has fibre sizes α iff its content is compContent α.

theorem RS.card_colourClass {n N : ℕ} (α : Fin N → ℕ) (hsum : ∑ j : Fin N, α j = n) : Fintype.card { g : Fin n → Fin N // ∀ (j : Fin N), fibreCard g j = α j } * ∏ j : Fin N, (α j).factorial = n.factorial

The colour-class count: the number of colourings with fibre sizes α times the product of the fibre factorials is n!.

noncomputable def RS.colourChar {n N : ℕ} (α : Fin N → ℕ) (π : Equiv.Perm (Fin n)) : ℕ

The permutation character of the colour class α: the number of colourings with fibre sizes α fixed by π.

Equations

• RS.colourChar α π = {g : Fin n → Fin N | (∀ (j : Fin N), RS.fibreCard g j = α j) ∧ g ∘ ⇑π = g}.card

theorem RS.sum_colourChar_weight {n N : ℕ} (α : Fin N → ℕ) (W : Equiv.Perm (Fin n) → ℂ) : ∑ π : Equiv.Perm (Fin n), ↑(colourChar α π) * W π = ∑ g : { g : Fin n → Fin N // ∀ (j : Fin N), fibreCard g j = α j }, ∑ π : Equiv.Perm (Fin n) with ↑g ∘ ⇑π = ↑g, W π

Fubini for the colour character: the colourChar-weighted permutation sum is the sum, over the colour class, of the stabilizer weight sums.