Pólya's enumeration theorem

We interpret functions X → Y as colorings of X with colors in Y. The element x : X is colored with color (f x) : Y in the coloring f : X → Y.

We interpret g : G as a transformation that permutes the elements of X into an equivalent configuration. If we color the elements of X with f : X → Y and then permute X with g : G, we obtain an equivalent configuration which now has the coloring x ↦ (f (g⁻¹ • x)). Note that g⁻¹ appears in the definition of the new coloring because the color of the element x in the new permuted configuration must match the color of its preimage g⁻¹ • x in the original configuration. Thus, for any g : G, we consider the colorings f and x ↦ (f (g⁻¹ • x)) to be equivalent.

Given a group action of G on X, we define an instance of group action of G on X → Y, which transforms colorings into equivalent colorings. This group action induces an equivalence relation defined by f₁ ∼ f₂ ↔ ∃ g, f₁ = g • f₂. Two colorings are equivalent when one can be transformed into the other by some element of G. The quotient of X → Y by this relation contains the orbits (equivalence classes) of equivalent colorings. The number of distinct colorings is the cardinality of this set.

We define a notion of cycles for elements in the group G acting on X. Every g : G induces a permutation of X through its action. The cycles of g : G are defined as the equivalence classes of X quotiented by the equivalence relation of being in the same cycle: x₁ ∼ x₂ ↔ ∃ k : ℤ, (permutation of g)ᵏ x₁ = x₂.

We prove Pólya's enumeration theorem and its commonly used variant, in which the sum ranges over the possible numbers of cycles instead of the elements of the group G.

For additional information, refer to https://en.wikipedia.org/wiki/P%C3%B3lya_enumeration_theorem.

@[implicit_reducible]

instance LeanPool.PolyaEnumerationTheorem.DistinctColorings.MulActionColorings (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] : MulAction G (X → Y)

Group action of G on X → Y with g • f ↦ (x ↦ f (g⁻¹ • x)).

Equations

• LeanPool.PolyaEnumerationTheorem.DistinctColorings.MulActionColorings X Y G = { smul := fun (g : G) (f : X → Y) (x : X) => f (g⁻¹ • x), mul_smul := ⋯, one_smul := ⋯ }

@[implicit_reducible]

instance LeanPool.PolyaEnumerationTheorem.DistinctColorings.instDecidableRelForallEquivOfDecidableEqOfFintypeLeanPool (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype X] [DecidableEq Y] [Fintype G] : DecidableRel HasEquiv.Equiv

The relation defined by f₁ ∼ f₂ ↔ ∃ g, f₁ = g • f₂ is decidable. This instance enables inference of Fintype (Quotient (MulAction.orbitRel G (X → Y))) and guarantees that the number of distinct colorings can be computed when X, Y and G are finite and X and Y have decidable equalities.

Equations

• LeanPool.PolyaEnumerationTheorem.DistinctColorings.instDecidableRelForallEquivOfDecidableEqOfFintypeLeanPool X Y G f₁ f₂ = if h : ∃ (g : G), g • f₂ = f₁ then isTrue h else isFalse h

@[reducible, inline]

abbrev LeanPool.PolyaEnumerationTheorem.DistinctColorings.numDistinctColorings (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] : ℕ

Number of distinct colorings is the cardinality of the quotient of X → Y by the equivalence relation f₁ ∼ f₂ ↔ ∃ g, f₁ = g • f₂.

Equations

• LeanPool.PolyaEnumerationTheorem.DistinctColorings.numDistinctColorings X Y G = Fintype.card (Quotient (MulAction.orbitRel G (X → Y)))

@[reducible, inline]

abbrev LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.CyclesOfGroup (X : Type u) {G : Type v} [Group G] [MulAction G X] (g : G) : Type u

The cycles of g : G are defined as the quotient of X by the equivalence relation of being in the same cycle of g: x₁ ∼ x₂ ↔ ∃ k : ℤ, (permutation of g)ᵏ x₁ = x₂. Cycles are unordered, and cycles of length 1 are also considered proper cycles. This definition of cycles differs from the standard definition of cycles in Mathlib, because cycles of length 1 are recognized as proper cycles.

Equations

• LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.CyclesOfGroup X g = Quotient (Equiv.Perm.SameCycle.setoid (MulAction.toPerm g))

@[implicit_reducible]

instance LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.instDecidableRelEquivOfFintypeOfDecidableEqLeanPool (X : Type u) {f : Equiv.Perm X} [Fintype X] [DecidableEq X] : DecidableRel HasEquiv.Equiv

Instance of DecidableRel for relation of being in the same cycle. Enables deciding for arbitrary elements of X and arbitrary permutation of X if the elements are in the same cycle of the permutation. This instance enables inference of Fintype and DecidableEq for CyclesOfGroup when X is finite and has decidable equality.

Equations

• LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.instDecidableRelEquivOfFintypeOfDecidableEqLeanPool X = f.instDecidableRelSameCycle

@[reducible, inline]

abbrev LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.numCyclesOfGroup (X : Type u) {G : Type v} [Group G] [MulAction G X] (g : G) [Fintype (CyclesOfGroup X g)] : ℕ

The number of cycles in the permutation of g. Cycles with only a single element are also counted (e.g. c[0, 1] : Equiv.Perm (Fin 3) has two cycles).

Equations

• LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.numCyclesOfGroup X g = Fintype.card (LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.CyclesOfGroup X g)

@[reducible, inline]

abbrev LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.numGroupOfNumCycles (X : Type u) (G : Type v) [Group G] [MulAction G X] [Fintype G] [(g : G) → Fintype (CyclesOfGroup X g)] (i : ℕ) : ℕ

The number of elements in the group G that have exactly i cycles.

Equations

• LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.numGroupOfNumCycles X G i = {g : G | LeanPool.PolyaEnumerationTheorem.CyclesOfGroupElements.numCyclesOfGroup X g = i}.card

The proof of Pólya's enumeration theorem uses the set of fixed points of g, denoted by MulAction.fixedBy (X → Y) g. This set consists of all colorings f : X → Y that are invariant under the action of g, i.e., those satisfying g • f = f.

theorem LeanPool.PolyaEnumerationTheorem.Theorem.f_mem_fixedBy_iff_forall_eq_to_eq {X : Type u} {Y : Type v} {G : Type w} [Group G] [MulAction G X] (g : G) (f : X → Y) : f ∈ MulAction.fixedBy (X → Y) g ↔ ∀ (a b : X), ⟦a⟧ = ⟦b⟧ → f a = f b

For any g : G we have: a coloring f is in fixed points of g if and only if f maps all elements in the same cycle of g to the same color. Only left to right implication of this lemma is used in the proof of Pólya's enumeration theorem.

def LeanPool.PolyaEnumerationTheorem.Theorem.cycleColoringOfFixedByColoring {X : Type u} {Y : Type v} {G : Type w} [Group G] [MulAction G X] (g : G) (f : ↑(MulAction.fixedBy (X → Y) g)) : CyclesOfGroupElements.CyclesOfGroup X g → Y

A function that maps a coloring from fixed points of g to a coloring of cycles. Colorings that are fixed by g map all elements of a cycle of g to the same color by lemma f_mem_fixedBy_iff_forall_eq_to_eq. We can transform each such coloring to a coloring of cycles of g by coloring each cycle with the color of its elements.

Equations

• LeanPool.PolyaEnumerationTheorem.Theorem.cycleColoringOfFixedByColoring g f = Quotient.lift ↑f ⋯

def LeanPool.PolyaEnumerationTheorem.Theorem.fixedByColoringOfCycleColoring {X : Type u} {Y : Type v} {G : Type w} [Group G] [MulAction G X] (g : G) (f : CyclesOfGroupElements.CyclesOfGroup X g → Y) : ↑(MulAction.fixedBy (X → Y) g)

A function that maps a coloring of cycles to a coloring in fixed points of g. We color each element with the color of its cycle. The resulting function is in fixed points of g because g⁻¹ • x and x are in the same cycle of g.

Equations

• LeanPool.PolyaEnumerationTheorem.Theorem.fixedByColoringOfCycleColoring g f = ⟨fun (x : X) => f ⟦x⟧, ⋯⟩

def LeanPool.PolyaEnumerationTheorem.Theorem.equivOfFixedByColoringOfCycleColoring {X : Type u} {Y : Type v} {G : Type w} [Group G] [MulAction G X] (g : G) : (CyclesOfGroupElements.CyclesOfGroup X g → Y) ≃ ↑(MulAction.fixedBy (X → Y) g)

Functions cycleColoringOfFixedByColoring and fixedByColoringOfCycleColoring are inverses and form a bijection.

Equations

• One or more equations did not get rendered due to their size.

theorem LeanPool.PolyaEnumerationTheorem.Theorem.forall_card_pow_numCyclesOfGroup_eq_card_fixedBy {X : Type u} {Y : Type v} {G : Type w} [Group G] [MulAction G X] [Fintype Y] [(g : G) → Fintype ↑(MulAction.fixedBy (X → Y) g)] [(g : G) → Fintype (CyclesOfGroupElements.CyclesOfGroup X g)] (g : G) : Fintype.card Y ^ CyclesOfGroupElements.numCyclesOfGroup X g = Fintype.card ↑(MulAction.fixedBy (X → Y) g)

For any g : G we have: the number of colors raised to the power of the number of cycles of g is equal to the number of colorings that are fixed by g.

theorem LeanPool.PolyaEnumerationTheorem.Theorem.numDistinctColorings_mul_card_group_eq_sum_card_pow_numCyclesOfGroup (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype Y] [Fintype G] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] [Finite (X → Y)] [(g : G) → Fintype (CyclesOfGroupElements.CyclesOfGroup X g)] : DistinctColorings.numDistinctColorings X Y G * Fintype.card G = ∑ g : G, Fintype.card Y ^ CyclesOfGroupElements.numCyclesOfGroup X g

A version of Pólya's enumeration theorem where the number of distinct colorings of X with colors in Y, under the group action of G on X, is multiplied by the cardinality of the group G.

theorem LeanPool.PolyaEnumerationTheorem.Theorem.numDistinctColorings_eq_sum_card_pow_numCyclesOfGroup_div_card_group (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype Y] [Fintype G] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] [Finite (X → Y)] [(g : G) → Fintype (CyclesOfGroupElements.CyclesOfGroup X g)] : DistinctColorings.numDistinctColorings X Y G = (∑ g : G, Fintype.card Y ^ CyclesOfGroupElements.numCyclesOfGroup X g) / Fintype.card G

Pólya's enumeration theorem: Provides a formula for the number of distinct colorings of X with colors in Y, under the group action of G on X.

theorem LeanPool.PolyaEnumerationTheorem.Theorem.numDistinctColorings_mul_card_group_eq_sum_numGroupOfNumCycles_mul_card_pow (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype Y] [Fintype G] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] [Fintype X] [Finite (X → Y)] [(g : G) → DecidableRel HasEquiv.Equiv] : DistinctColorings.numDistinctColorings X Y G * Fintype.card G = ∑ i : Fin (Fintype.card X + 1), CyclesOfGroupElements.numGroupOfNumCycles X G ↑i * Fintype.card Y ^ ↑i

A version of Pólya's enumeration theorem where the sum ranges over the possible numbers of cycles, and the number of distinct colorings of X with colors in Y, under the group action of G on X, is multiplied by the cardinality of the group G.

theorem LeanPool.PolyaEnumerationTheorem.polya_theorem (X : Type u) (Y : Type v) (G : Type w) [Group G] [MulAction G X] [Fintype Y] [Fintype G] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] [Finite (X → Y)] [(g : G) → Fintype (CyclesOfGroupElements.CyclesOfGroup X g)] : DistinctColorings.numDistinctColorings X Y G = (∑ g : G, Fintype.card Y ^ CyclesOfGroupElements.numCyclesOfGroup X g) / Fintype.card G

Short alias for Pólya's enumeration theorem.