35.2. Permutations and groups🔗

A permutation p : Perm n (Hex.Perm) is the vector of the images of 0, 1, …, n - 1, together with proofs that every point occurs exactly once. These proofs default to by decide, so a permutation given by a literal vector is written Perm.mk #v[…]. Composition follows Mathlib: p.comp q applies q first, so (p.comp q) x = p (q x).

Hex.PermGroup.Group.ofGenerators takes an array of permutations and returns the group G : Group n (Hex.PermGroup.Group) that they generate. Here is the dihedral group of order 8, acting on the vertices 0, 1, 2, 3 of a square:

open Hex Hex.PermGroup

namespace HexPermGroupChapter

def rotation : Perm 4 := Perm.mk #v[1, 2, 3, 0]
def reflection : Perm 4 := Perm.mk #v[0, 3, 2, 1]
def square : Group 4 :=
  Group.ofGenerators #[rotation, reflection]

#guard square.order = 8
#guard (square.orbit 0).size = 4
#guard (square.stabilizer 0).order = 2

The group has eight elements and the orbit of a vertex has four, so the stabilizer of a vertex has order two. Hex.PermGroup.Group.orbit returns the orbit of a point in increasing order, and Hex.PermGroup.Group.stabilizer returns the stabilizer of a point as a new group.

The same generators support kernel-checked proofs using only import HexPermGroup. Hex.PermGroup.HasOrder expresses exact order by mutually inverse maps between the generated permutations and a finite index type. The perm_group tactic proves that order, membership and nonmembership without importing Mathlib:

example : HasOrder #[rotation, reflection] 8 := by⊢ HasOrder #[rotation, reflection] 8
  perm_groupAll goals completed! 🐙
example : Generated #[rotation, reflection]
    (rotation.comp reflection) := by⊢ Generated #[rotation, reflection] (rotation.comp reflection)
  perm_groupAll goals completed! 🐙
example : ¬ Generated #[rotation, reflection]
    (Perm.mk #v[1, 0, 2, 3]) := by⊢ ¬Generated #[rotation, reflection] { vec := #v[1, 0, 2, 3], nodup := ⋯, complete := ⋯ }
  perm_groupAll goals completed! 🐙

These proofs check a packed stabilizer-chain certificate in the kernel; they use the same certificate machinery as the Mathlib examples below.

Hex.PermGroup.Group.word? decides whether a permutation lies in the group, and if it does, expresses it in terms of the generators, as a straight-line program described below. Hex.PermGroup.Program.toWord? writes that program out as a word, and Hex.PermGroup.Word.toString displays the word with g0, g1, … standing for the generators in the order they were given. As with comp, the rightmost letter acts first. For the square, g0 is rotation and g1 is reflection:

def squareWord (p : Perm 4) : Option String := do
  let program ← square.word? p
  let w ← program.toWord? square.generators
  return w.toString

[some "g0 * g1", some "g0⁻¹ * g1", none]#eval [rotation.comp reflection,
  reflection.comp rotation,
  Perm.mk #v[1, 0, 2, 3]].map squareWord

[some "g0 * g1", some "g0⁻¹ * g1", none]

Reflecting and then rotating gives g0 * g1. Rotating and then reflecting gives the same as reflecting and then rotating backwards, g0⁻¹ * g1. The last permutation swaps two adjacent vertices, which is not a symmetry of the square, so there is no word.

Words grow quickly with the size of the group: for the Rubik's cube they run to hundreds of millions of letters. Hex.PermGroup.Program.toWordCapped computes the length from the program first and refuses, without writing the word out, when it is over a given cap.

35.2.1. What a group contains🔗

A group consists of its array of generators and a stabilizer chain for the subgroup they generate, built by the Schreier–Sims algorithm. The chain has a level for each point i = 0, 1, …, n - 1. Level i records generators for the subgroup Gᵢ fixing 0, …, i - 1, the orbit of i under Gᵢ, and for each point of that orbit an element of Gᵢ carrying i to it, called its representative.

The structure also contains a proof that the Boolean function checkChain returns true on the generators and the chain. checkChain checks the orbits and representatives at every level, and checks that every Schreier generator of every level reduces to the identity through the levels after it. This is what makes the chain correct for the subgroup generated by the array, whatever algorithm produced it.

The order of the group is the product of the orbit lengths. To decide whether a permutation lies in the group, multiply it on the left by the inverse of the representative for its image of 0, then the result by the inverse of the representative for its image of 1, and so on; the permutation lies in the group exactly when this ends at the identity. Recording the representatives used expresses the permutation in terms of the original generators. Hex.PermGroup.Group.word? returns this expression as a Hex.PermGroup.Program, a straight-line program whose steps are generators, inverses and products of earlier steps, and Hex.PermGroup.checkWord evaluates a program and compares the result with a given permutation.