Reduction to Fin

If we have a bijection X → Fin n, then the number of distinct colorings of X with colors in Y under the group action of G on X is equal to the number of distinct colorings of Fin n with colors in Y under the induced group action of G on Fin n. This allows us to use Fin n instead of more complex types when working with numbers of distinct colorings.

@[instance_reducible]

instance LeanPool.PolyaEnumerationTheorem.ReductionToFin.MulActionFin (X : Type u) (G : Type w) [enum : FinEnum X] [Monoid G] [MulAction G X] : MulAction G (Fin (FinEnum.card X))

Given a bijection enum.equiv : X → Fin enum.card and a group action of G on X, construct a group action of G on Fin enum.card with g • i ↦ enum.equiv (g • (enum.equiv⁻¹ i)).

Equations

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

def LeanPool.PolyaEnumerationTheorem.ReductionToFin.fwdColoring (X : Type u) (Y : Type v) [enum : FinEnum X] (f : X → Y) : Fin (FinEnum.card X) → Y

Forward map: a coloring of X to a coloring of Fin enum.card.

Equations

• LeanPool.PolyaEnumerationTheorem.ReductionToFin.fwdColoring X Y f i = f (FinEnum.equiv.symm i)

def LeanPool.PolyaEnumerationTheorem.ReductionToFin.invColoring (X : Type u) (Y : Type v) [enum : FinEnum X] (f : Fin (FinEnum.card X) → Y) : X → Y

Inverse map: a coloring of Fin enum.card to a coloring of X.

Equations

• LeanPool.PolyaEnumerationTheorem.ReductionToFin.invColoring X Y f x = f (FinEnum.equiv x)

def LeanPool.PolyaEnumerationTheorem.ReductionToFin.equivOfQuotientOfQuotientFin (X : Type u) (Y : Type v) (G : Type w) [enum : FinEnum X] [Group G] [MulAction G X] : Quotient (MulAction.orbitRel G (X → Y)) ≃ Quotient (MulAction.orbitRel G (Fin (FinEnum.card X) → Y))

A bijection between the distinct colorings of X with colors in Y under the group action of G on X and the distinct colorings of Fin enum.card with colors in Y under the induced group action of G on Fin enum.card.

Equations

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

@[instance_reducible]

instance LeanPool.PolyaEnumerationTheorem.ReductionToFin.instFintypeQuotientForallFinCardOrbitRelOfForallLeanPool (X : Type u) (Y : Type v) (G : Type w) [enum : FinEnum X] [Group G] [MulAction G X] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] : Fintype (Quotient (MulAction.orbitRel G (Fin (FinEnum.card X) → Y)))

An instance of Fintype for the distinct colorings of Fin enum.card with colors in Y under the induced group action of G on Fin enum.card. Required by numDistinctColorings_eq_numDistinctColorings_of_Fin.

Equations

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

theorem LeanPool.PolyaEnumerationTheorem.ReductionToFin.numDistinctColorings_eq_numDistinctColorings_of_Fin (X : Type u) (Y : Type v) (G : Type w) [enum : FinEnum X] [Group G] [MulAction G X] [Fintype (Quotient (MulAction.orbitRel G (X → Y)))] : DistinctColorings.numDistinctColorings X Y G = DistinctColorings.numDistinctColorings (Fin (FinEnum.card X)) Y G

The number of distinct colorings of X with colors in Y under the group action of G on X is equal to the number of distinct colorings of Fin enum.card with colors in Y under the induced group action of G on Fin enum.card.