Numbers of distinct colorings for some concrete examples

Trivial group

theorem TrivialGroup.numDistinctColoringsOfTrivialGroup (X : Type u) (Y : Type v) [Fintype X] [Fintype Y] [DecidableEq X] [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.

def Necklaces.numDistinctColoringsOfNecklace : ℕ → ℕ → ℕ

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

Equations

• Necklaces.numDistinctColoringsOfNecklace 0 x = 1
• Necklaces.numDistinctColoringsOfNecklace n.succ x = DistinctColorings.numDistinctColorings (Fin (n + 1)) (Fin x) (Multiplicative (Fin (n + 1)))

@[reducible, inline]

abbrev Necklaces.computeNumDistinctColoringsOfNecklace : ℕ → ℕ → ℕ

Computes the number of distinct colorings of a necklace with n beads and m colors.

Equations

• Necklaces.computeNumDistinctColoringsOfNecklace 0 x = 1
• Necklaces.computeNumDistinctColoringsOfNecklace n.succ x = ComputationNumberOfDistinctColorings.computeNumDistinctColorings (Fin (n + 1)) (Fin x) (Multiplicative (Fin (n + 1)))

theorem Necklaces.computeNumDistinctColoringsOfNecklace_eq_numDistinctColoringsOfNecklace (n m : ℕ) : Necklaces.computeNumDistinctColoringsOfNecklace n m = Necklaces.numDistinctColoringsOfNecklace n m

computeNumDistinctColoringsOfNecklace computes the number of distinct colorings of a necklace with n beads and m colors.

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.

instance 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

• Bracelets.MulActionBracelet n = MulAction.mk ⋯ ⋯

instance Bracelets.instFinEnumZModHAddNatOfNat_polyaEnumerationTheorem (n : ℕ) : FinEnum (ZMod (n + 1))

Finite enumeration of ZMod (n + 1). ZMod 0 is ℤ by definition and cannot be finitely enumerated.

Equations

• Bracelets.instFinEnumZModHAddNatOfNat_polyaEnumerationTheorem n = FinEnum.mk (n + 1) 1

def Bracelets.numDistinctColoringsOfBracelet : ℕ → ℕ → ℕ

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

Equations

• Bracelets.numDistinctColoringsOfBracelet 0 x = 1
• Bracelets.numDistinctColoringsOfBracelet n.succ x = DistinctColorings.numDistinctColorings (ZMod (n + 1)) (Fin x) (DihedralGroup (n + 1))

@[reducible, inline]

abbrev Bracelets.computeNumDistinctColoringsOfBracelet : ℕ → ℕ → ℕ

Computes the number of distinct colorings of a bracelet with n beads and m colors.

Equations

• Bracelets.computeNumDistinctColoringsOfBracelet 0 x = 1
• Bracelets.computeNumDistinctColoringsOfBracelet n.succ x = ComputationNumberOfDistinctColorings.computeNumDistinctColorings (ZMod (n + 1)) (Fin x) (DihedralGroup (n + 1))

theorem Bracelets.computeNumDistinctColoringsOfBracelet_eq_numDistinctColoringsOfBracelet (n m : ℕ) : Bracelets.computeNumDistinctColoringsOfBracelet n m = Bracelets.numDistinctColoringsOfBracelet n m

computeNumDistinctColoringsOfBracelet computes the number of distinct colorings of a bracelet with n beads and m colors.

Cube

We interpret the elements of Fin 6 as 6 faces of the cube, where:

• 0 is the face at the front,
• 1 is the face at the right,
• 2 is the face at the back,
• 3 is the face at the left,
• 4 is the face at the top,
• 5 is the face at the bottom.

There are 24 rotational symmetries of the cube.

def Cube.r : Equiv.Perm (Fin 6)

The rotation of the cube by π/2 around the axis through the centers of the top and bottom faces. The front face moves to the position of the right face.

Equations

• Cube.r = (↑[0, 1, 2, 3]).formPerm Cube.r.proof_2

def Cube.s : Equiv.Perm (Fin 6)

The rotation of the cube by π/2 around the axis through the centers of the front and back faces. The right face moves to the position of the top face.

Equations

• Cube.s = (↑[1, 4, 3, 5]).formPerm Cube.s.proof_2

def Cube.rotationalSymmetriesOfCube : Finset (Equiv.Perm (Fin 6))

The finite set of rotational symmetries of the cube. First, we rotate the cube using s at most three times to set the position of 1. Then, we move 0 to the position of any other face by rotating the cube appropriately. To move 0 to one of the faces in {0, 1, 2, 3}, we use r the appropriate number of times. To move 0 to 4 or 5, we first use r once to move 0 to 1, then use s once or three times. Since we can move 0 to any position and 1 to any position adjacent to the new position of 0 (by using s the appropriate number of times in the beginning), we have 6 * 4 = 24 different rotational symmetries. Since we can infer the new positions of all faces based only on the new positions of 0 and 1, we have obtained all rotational symmetries of the cube.

Equations

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

theorem Cube.s_pow_four : Cube.s ^ 4 = 1

The order of s is 4.

theorem Cube.r_inv : Cube.r⁻¹ = Cube.r ^ 3

The inverse of r is r³.

theorem Cube.s_inv : Cube.s⁻¹ = Cube.s ^ 3

The inverse of s is s³.

theorem Cube.pow_add_val_eq_of_pow_eq_one {n : ℕ} {G : Type u} [Monoid G] {g : G} (hg : g ^ n = 1) (i j : Fin n) : g ^ ↑(i + j) = g ^ (↑i + ↑j)

If g has order n, then we can reduce its powers modulo n. When its power corresponds to a sum of elements from Fin n, it can be rewritten as the sum of their values.

theorem Cube.r_mul_mem_rotationalSymmetriesOfCube (x : Equiv.Perm (Fin 6)) (hx : x ∈ Cube.rotationalSymmetriesOfCube) : Cube.r * x ∈ Cube.rotationalSymmetriesOfCube

Multiplying r by an element of rotationalSymmetriesOfCube results in an element that is in rotationalSymmetriesOfCube.

theorem Cube.s_mul_mem_rotationalSymmetriesOfCube (x : Equiv.Perm (Fin 6)) (hx : x ∈ Cube.rotationalSymmetriesOfCube) : Cube.s * x ∈ Cube.rotationalSymmetriesOfCube

Multiplying s by an element of rotationalSymmetriesOfCube results in an element that is in rotationalSymmetriesOfCube.

theorem Cube.s_pow_r_pow_s_pow_mul_mem_rotationalSymmetriesOfCube (n m k : ℕ) (x : Equiv.Perm (Fin 6)) (hx : x ∈ Cube.rotationalSymmetriesOfCube) : Cube.s ^ n * Cube.r ^ m * Cube.s ^ k * x ∈ Cube.rotationalSymmetriesOfCube

Multiplying sⁿ * rᵐ * sᵏ by an element of rotationalSymmetriesOfCube results in an element that is in rotationalSymmetriesOfCube.

instance Cube.instDecidablePredPermFinOfNatNatMemSubgroupRotationalSymmetriesOfCubeSubgroup : DecidablePred (Membership.mem Cube.RotationalSymmetriesOfCubeSubgroup)

The predicate defined by a ∈ RotationalSymmetriesOfCubeSubgroup is decidable. This instance enables inference of Fintype RotationalSymmetriesOfCubeSubgroup and guarantees that the number of distinct colorings can be computed.

Equations

• Cube.instDecidablePredPermFinOfNatNatMemSubgroupRotationalSymmetriesOfCubeSubgroup p = if h : p ∈ Cube.rotationalSymmetriesOfCube then isTrue h else isFalse h

@[reducible, inline]

abbrev Cube.numDistinctColoringsOfCube (n : ℕ) : ℕ

Number of distinct colorings of the faces of a cube with n colors.

Equations

• Cube.numDistinctColoringsOfCube n = DistinctColorings.numDistinctColorings (Fin 6) (Fin n) ↥Cube.RotationalSymmetriesOfCubeSubgroup

@[reducible, inline]

abbrev Cube.computeNumDistinctColoringsOfCube (n : ℕ) : ℕ

Computes the number of distinct colorings of the faces of a cube with n colors.

Equations

• Cube.computeNumDistinctColoringsOfCube n = ComputationNumberOfDistinctColorings.computeNumDistinctColorings (Fin 6) (Fin n) ↥Cube.RotationalSymmetriesOfCubeSubgroup

theorem Cube.computeNumDistinctColoringsOfCube_eq_numDistinctColoringsOfCube (n : ℕ) : Cube.computeNumDistinctColoringsOfCube n = Cube.numDistinctColoringsOfCube n

computeNumDistinctColoringsOfCube computes the number of distinct colorings of the faces of a cube with n colors.

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.

@[reducible, inline]

abbrev PermutationGroup.numDistinctColoringsOfPerm (n m : ℕ) : ℕ

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

Equations

• PermutationGroup.numDistinctColoringsOfPerm n m = DistinctColorings.numDistinctColorings (Fin n) (Fin m) (Equiv.Perm (Fin n))

def 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

• PermutationGroup.numWeakCompositions 0 0 = 1
• PermutationGroup.numWeakCompositions n.succ 0 = 0
• PermutationGroup.numWeakCompositions x m.succ = (x + m).choose m

def PermutationGroup.contractCodomain {n m : ℕ} {f : Fin n → Fin (m + 1)} (h : ∀ (i : Fin n), ↑(f i) ≠ m) : Fin n → Fin m

A function that takes a function f : Fin n → Fin (m + 1) and a proof that f maps no element to m and returns a function of type Fin n → Fin m that behaves exactly the same as f on all inputs.

Equations

• PermutationGroup.contractCodomain h i = ⟨↑(f i), ⋯⟩

def PermutationGroup.expandCodomain {n m : ℕ} (f : Fin n → Fin m) : Fin n → Fin (m + 1)

A function that takes a function f : Fin n → Fin m and returns a function of type Fin n → Fin (m + 1) that behaves exactly the same as f on all inputs.

Equations

• PermutationGroup.expandCodomain f i = ⟨↑(f i), ⋯⟩

def PermutationGroup.contractDomain {n m : ℕ} (f : Fin (n + 1) → Fin m) : Fin n → Fin m

A function that takes a function f : Fin (n + 1) → Fin m and returns a function of type Fin n → Fin m that behaves exactly the same as f on all inputs except for n, which is no longer a valid input.

Equations

• PermutationGroup.contractDomain f i = f ⟨↑i, ⋯⟩

def PermutationGroup.expandDomain {n m : ℕ} (f : Fin n → Fin (m + 1)) : Fin (n + 1) → Fin (m + 1)

A function that takes a function f : Fin n → Fin (m + 1) and returns a function of type Fin (n + 1) → Fin (m + 1) that behaves exactly the same as f on all inputs except at n, where it returns m.

Equations

• PermutationGroup.expandDomain f i = if h : ↑i = n then ⟨m, ⋯⟩ else f ⟨↑i, ⋯⟩

theorem PermutationGroup.numDistinctColoringsOfPerm_succ_succ {n m : ℕ} : PermutationGroup.numDistinctColoringsOfPerm (n + 1) (m + 1) = PermutationGroup.numDistinctColoringsOfPerm (n + 1) m + PermutationGroup.numDistinctColoringsOfPerm n (m + 1)

A recurrence formula for the number of distinct colorings of a set of n + 1 unordered, indistinguishable objects with m + 1 colors. It equals the sum of the number of distinct colorings of a set of n + 1 unordered, indistinguishable objects with m colors and the number of distinct colorings of a set of n unordered, indistinguishable objects with m + 1 colors.

theorem PermutationGroup.numDistinctColoringsOfPerm_eq_numWeakCompositions {n m : ℕ} : PermutationGroup.numDistinctColoringsOfPerm n m = PermutationGroup.numWeakCompositions n m

The number of distinct colorings of n unordered, indistinguishable objects with m colors is equal to the number of weak compositions of n into m parts.