Stabilizer counts for pair colourings

The stabilizer count for colourings by pairs, transported along finProdFinEquiv from the Fin-codomain machinery.

noncomputable def RS.pairFibre {n k : ℕ} (p : Fin n → Fin k × Fin k) (c : Fin k × Fin k) : ℕ

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

Equations

• RS.pairFibre p c = {i : Fin n | p i = c}.card

theorem RS.card_fixing_pairs {n k : ℕ} (p : Fin n → Fin k × Fin k) : {π : Equiv.Perm (Fin n) | p ∘ ⇑π = p}.card = ∏ c : Fin k × Fin k, (pairFibre p c).factorial

The pair stabilizer count: permutations fixing a pair colouring number the product of its fibre factorials.