Orbit–stabilizer for pair colourings

Pair contents, the orbit–stabilizer identity for pair-colouring classes (transported along finProdFinEquiv), and the fibre-margin partition.

def RS.pairContent {n k : ℕ} (p : Fin n → Fin k × Fin k) : Multiset (Fin k × Fin k)

The content multiset of a pair colouring.

Equations

• RS.pairContent p = Multiset.map p Finset.univ.val

theorem RS.pairFibre_eq_count {n k : ℕ} (p : Fin n → Fin k × Fin k) (c : Fin k × Fin k) : pairFibre p c = Multiset.count c (pairContent p)

A pair-colouring's fibre size is the pair's multiplicity in its content.

theorem RS.content_comp_equiv {n k : ℕ} (p : Fin n → Fin k × Fin k) : ↑(content (⇑finProdFinEquiv ∘ p)) = Multiset.map (⇑finProdFinEquiv) (pairContent p)

Content of the transported colouring.

theorem RS.pair_orbit_stab {n k : ℕ} (p₀ : Fin n → Fin k × Fin k) : Fintype.card { p : Fin n → Fin k × Fin k // pairContent p = pairContent p₀ } * ∏ c : Fin k × Fin k, (Multiset.count c (pairContent p₀)).factorial = n.factorial

Orbit–stabilizer for pair classes: the class size times the content factorial product is n!.

theorem RS.fibreCard_fst_eq_sum {n k : ℕ} (p : Fin n → Fin k × Fin k) (a : Fin k) : fibreCard (fun (i : Fin n) => (p i).1) a = ∑ b : Fin k, pairFibre p (a, b)

The fibre-margin partition: a first-coordinate fibre size is the row sum of the pair fibres.

theorem RS.fibreCard_snd_eq_sum {n k : ℕ} (p : Fin n → Fin k × Fin k) (b : Fin k) : fibreCard (fun (i : Fin n) => (p i).2) b = ∑ a : Fin k, pairFibre p (a, b)

The second-coordinate analogue.