35.5. Numbering and random elements
An element of G is a permutation together with a proof that it lies in the
subgroup generated by the generators of G; its type is
Hex.PermGroup.Element. The stabilizer chain writes each element of
G uniquely as a product of representatives, one from each level, and so
numbers the elements 0, 1, …, |G| - 1.
Hex.PermGroup.Group.rank computes the number of an element and
Hex.PermGroup.Group.unrank the element with a given number; they are
inverse to each other. Neither lists the elements of G. To unrank k, write
it in the mixed radix whose digits are bounded by the orbit lengths of the
chain, and multiply the representatives that the digits select, one per
level. This costs one product of permutations per level, so about n²
operations for a group on n points, however large G is. Ranking sifts the
element through the chain, at the same cost. Hex.PermGroup.Group.unrank? accepts any
natural number and returns none when it is not below |G|. The numbering
depends on the chain, so two groups with the same elements and different
generators may number them differently.
Here are the eight elements of the square in this order, written as words in
the generators:
#eval (List.range 8).filterMap fun k =>
(square.unrank? k).bind fun g => squareWord g.val
Random elements come from the same numbering.
Hex.PermGroup.Group.sampleFrom takes a function that produces an index
below a given bound, in any functor, calls it once with the bound |G|, and
unranks the index it returns. Drawing an element therefore costs one index and
one unranking. If the index is
uniformly distributed, so is the element: each element has probability
1 / |G|, which is Hex.PermGroup.Group.sample_uniform in
HexPermGroupTheory. HexPermGroup itself contains no random number
generator.
HexPermGroupTheory also provides an instance of Mathlib's
Random m (Element G), so Random.random draws an element using any
Mathlib RandomGen. The index is drawn by
Hex.PermGroup.randomIndex, which uses rejection sampling rather than
reducing a single draw modulo |G|. If the generator's draws are independent
and uniform, each element has probability within 2^-128 of 1 / |G|. With a
fixed seed the draws are reproducible. Here are five random elements of the
square, written as words in the generators, and the number of times each of
the eight elements occurs among 8000 draws:
def draw (k : Nat) : List (Element square) :=
(List.replicate k ()).mapM (fun _ =>
(Random.random : Rand (Element square)))
|>.run' ⟨mkStdGen 2026⟩
#eval (draw 5).filterMap fun g => squareWord g.val
#eval
let ranks := (draw 8000).map (square.rank · |>.val)
(List.range 8).map fun k => ranks.count k