Fibres of a colouring

Shared definitions for the cycle sums: the fibre counts of a function Fin n → Fin N and its content multiset.

noncomputable def RS.fibreCard {n N : ℕ} (f : Fin n → Fin N) (j : Fin N) : ℕ

The size of the fibre of a colouring over a colour.

Equations

• RS.fibreCard f j = {i : Fin n | f i = j}.card

def RS.content {n N : ℕ} (f : Fin n → Fin N) : Sym (Fin N) n

The content of a colouring: the multiset of its values.

Equations

• RS.content f = ⟨Multiset.map f Finset.univ.val, ⋯⟩

theorem RS.sum_count_univ {N : ℕ} (m : Multiset (Fin N)) : ∑ j : Fin N, Multiset.count j m = m.card

Counts over all colours total the size of a multiset.

theorem RS.fibreCard_eq_count {n N : ℕ} (f : Fin n → Fin N) (j : Fin N) : fibreCard f j = Multiset.count j ↑(content f)

A fibre's size is the colour's multiplicity in the content.

theorem RS.sum_fibreCard {n N : ℕ} (f : Fin n → Fin N) : ∑ j : Fin N, fibreCard f j = n

The fibres partition the domain.