The Pólya–Redfield enumeration theorem

A finite group G acting on a finite set α acts on colourings α → C by (g • F) a = F (g⁻¹ • a). With colour weights w c in a commutative ring and colouring weight W F = ∏ₐ w (F a), |G| · Σ_{orbits} W = Σ_g ∏_{cycles of g} p_{length}, p_k = Σ_c (w c)^k: the cycle index evaluated at the power sums (Theorem of the Day's Z(G, Ω; x, x⁽²⁾, …)). Proof: a weighted Burnside lemma, and a colouring fixed by g is constant on each cycle of g, so the fixed colourings factor over the cycles. With w = 1 it counts colourings up to symmetry: |G| · #orbits = Σ_g |C|^{c(g)}.

Main results

• PolyaRedfield.sum_fixed_weight: the weight of the colourings fixed by g is the product over the cycles of g of the power sums
• PolyaRedfield.card_mul_sum_orbit_weight: Pólya–Redfield: |G| · Σ_orbits W = cycle index at the power sums
• PolyaRedfield.card_mul_card_orbits: unweighted: |G| · #orbits = Σ_g |C|^(number of cycles of g)

References

• R. Whitty, Theorem of the Day, «The Pólya–Redfield Enumeration Theorem» (CombinatorialTheory/PRET).
• J. H. Redfield, The theory of group-reduced distributions, Amer. J. Math. 49 (1927); G. Pólya, Acta Math. 68 (1937).

theorem PolyaRedfield.burnside_weighted {G : Type u_1} {X : Type u_2} {R : Type u_3} [Group G] [Fintype G] [MulAction G X] [Fintype X] [Fintype (MulAction.orbitRel.Quotient G X)] [(g : G) → DecidablePred fun (x : X) => g • x = x] [CommRing R] (W : X → R) (hW : ∀ (g : G) (x : X), W (g • x) = W x) : ↑(Fintype.card G) * ∑ O : MulAction.orbitRel.Quotient G X, W (Quotient.out O) = ∑ g : G, ∑ x : X with g • x = x, W x

theorem PolyaRedfield.fixed_iff_sameCycle {α : Type u_1} {C : Type u_2} (σ : Equiv.Perm α) (F : α → C) : (∀ (a : α), F (σ a) = F a) ↔ ∀ (a b : α), σ.SameCycle a b → F a = F b

theorem PolyaRedfield.sum_fixed_perm {α : Type u_1} {C : Type u_2} {R : Type u_3} [Fintype α] [Fintype C] [CommRing R] (σ : Equiv.Perm α) (w : C → R) : ∑ F : α → C with ∀ (a : α), F (σ a) = F a, ∏ a : α, w (F a) = ∏ q : Quotient (Equiv.Perm.SameCycle.setoid σ), ∑ c : C, w c ^ {a : α | ⟦a⟧ = q}.card

theorem PolyaRedfield.prod_classes {α : Type u_1} {M : Type u_2} [Fintype α] [CommMonoid M] (σ : Equiv.Perm α) (h : ℕ → M) : ∏ q : Quotient (Equiv.Perm.SameCycle.setoid σ), h {a : α | ⟦a⟧ = q}.card = h 1 ^ Fintype.card ↑(Function.fixedPoints ⇑σ) * (Multiset.map h σ.cycleType).prod

theorem PolyaRedfield.sum_fixed_weight {G : Type u_1} {α : Type u_2} {C : Type u_3} {R : Type u_4} [Group G] [MulAction G α] [Fintype α] [Fintype C] [CommRing R] (w : C → R) (g : G) : ∑ F : α → C with g • F = F, ∏ a : α, w (F a) = (∑ c : C, w c) ^ Fintype.card ↑(Function.fixedPoints ⇑(MulAction.toPerm g)) * (Multiset.map (fun (k : ℕ) => ∑ c : C, w c ^ k) (MulAction.toPerm g).cycleType).prod

The weight of the colourings fixed by g is the product over the cycles of g of the power sums.

theorem PolyaRedfield.card_mul_sum_orbit_weight {G : Type u_1} {α : Type u_2} {C : Type u_3} {R : Type u_4} [Group G] [Fintype G] [MulAction G α] [Fintype α] [Fintype C] [CommRing R] (w : C → R) : ↑(Fintype.card G) * ∑ O : MulAction.orbitRel.Quotient G (α → C), ∏ a : α, w (Quotient.out O a) = ∑ g : G, (∑ c : C, w c) ^ Fintype.card ↑(Function.fixedPoints ⇑(MulAction.toPerm g)) * (Multiset.map (fun (k : ℕ) => ∑ c : C, w c ^ k) (MulAction.toPerm g).cycleType).prod

Pólya–Redfield (weighted form), as stated in the queue.

theorem PolyaRedfield.card_mul_card_orbits {G : Type u_1} {α : Type u_2} {C : Type u_3} [Group G] [Fintype G] [MulAction G α] [Fintype α] [Fintype C] : Fintype.card G * Fintype.card (MulAction.orbitRel.Quotient G (α → C)) = ∑ g : G, Fintype.card C ^ (Fintype.card ↑(Function.fixedPoints ⇑(MulAction.toPerm g)) + (MulAction.toPerm g).cycleType.card)

Unweighted corollary: |G| · #orbits = ∑_g |C|^(number of cycles of g, fixed points included).