Documentation

LeanPool.PolyaEnumerationTheorem.Concrete

Numbers of distinct colorings for some concrete examples #

Trivial group #

source
theorem LeanPool.PolyaEnumerationTheorem.TrivialGroup.numDistinctColoringsOfTrivialGroup (X : Type u) (Y : Type v) [Fintype X] [Fintype Y] [Fintype (Quotient (MulAction.orbitRel (↥⊥) (X → Y)))] :
DistinctColorings.numDistinctColorings X Y ↥⊥ = Fintype.card Y ^ Fintype.card X

When using the trivial group, every coloring is equivalent only to itself. The number of distinct colorings is equal to the number of functions. ⊥ : Subgroup (X ≃ X) denotes the trivial subgroup of X ≃ X.

Necklaces #

We interpret the elements of Fin n as n beads of a necklace, where x is connected to x + 1 and x - 1, computed modulo n. Necklaces can be rotated, but not reflected. We use the additive group Fin n with multiplicative notation, because our definitions require a group with multiplicative notation. Elements of Multiplicative (Fin n) are rotations of the necklace, where i : Fin n rotates the necklace by 2πi/n. We define that there is a single coloring of a necklace with 0 beads. This is defined separately because Multiplicative (Fin 0) is not a group.

source
def LeanPool.PolyaEnumerationTheorem.Necklaces.numDistinctColoringsOfNecklace :
ℕ → ℕ → ℕ

Number of distinct colorings of a necklace with n beads and m colors.

Equations
Instances For

    Bracelets #

    We interpret the elements of ZMod n as n beads of a bracelet, where x is connected to x + 1 and x - 1, computed modulo n. Bracelets can be rotated and reflected. We use the DihedralGroup n, which contains elements r i that rotate the bracelet by 2πi/n and sr i that rotate the bracelet by 2πi/n and then reflect it. We define that there is a single coloring of a bracelet with 0 beads. This is defined separately because ZMod 0 is ℤ by definition.

    source
    @[implicit_reducible]
    instance LeanPool.PolyaEnumerationTheorem.Bracelets.MulActionBracelet (n : ℕ) :
    MulAction (DihedralGroup n) (ZMod n)

    Action of the dihedral group on ZMod n. Elements of ZMod n are interpreted as beads of a bracelet. The dihedral group contains elements r i that rotate the bracelet by 2πi/n, and elements sr i that rotate the bracelet by 2πi/n and then reflect it.

    Equations
    • One or more equations did not get rendered due to their size.
    source
    def LeanPool.PolyaEnumerationTheorem.Bracelets.numDistinctColoringsOfBracelet :
    ℕ → ℕ → ℕ

    Number of distinct colorings of a bracelet with n beads and m colors.

    Equations
    Instances For

      Permutation group #

      We interpret the elements of Fin n as n unordered, indistinguishable objects. We use the group Equiv.Perm (Fin n), which contains all permutations of Fin n. Its elements permute our objects. Since we can permute the objects in any way and still obtain an equivalent configuration, two colorings are equivalent if and only if they assign the same number of objects to each color. Consequently, the number of distinct colorings of n unordered, indistinguishable objects with m colors is equal to the number of ways to separate n objects into m ordered sets (the number of weak compositions of n into m parts), which is equal to (n + m - 1).choose (m - 1) when m > 0. There is exactly one coloring of 0 objects with 0 colors, and no valid colorings of more than 0 objects with 0 colors.

      source
      @[reducible, inline]
      abbrev LeanPool.PolyaEnumerationTheorem.PermutationGroup.numDistinctColoringsOfPerm (n m : ℕ) :
      ℕ

      The number of distinct colorings of n unordered, indistinguishable objects with m colors.

      Equations
      Instances For
        source
        def LeanPool.PolyaEnumerationTheorem.PermutationGroup.numWeakCompositions :
        ℕ → ℕ → ℕ

        The number of weak compositions of n into m parts. This represents the number of ways to separate n objects into m ordered sets.

        Equations
        Instances For