35.4. Blocks and transporters🔗

A block system for G is a partition of the points such that every element of G maps each part onto a part. Hex.PermGroup.Group.blocks takes a list of pairs of points and returns the finest block system in which each pair lies in one block. Hex.PermGroup.Group.blocks_invariant proves that the result is a block system, and Hex.PermGroup.Group.blocks_least that it refines every other equivalence relation preserved by G that relates each pair. HexPermGroupTheory states the same two facts together as Hex.PermGroup.Group.blocks_spec: the result, as a Setoid (Fin n), is the least element of the set of G-invariant equivalence relations relating each pair.

In the square, opposite vertices form blocks of size 2. Hex.PermGroup.Group.blockAction computes the action of G on the blocks: the image, a permutation group on the blocks, and the kernel, the subgroup mapping each block onto itself. Its last argument bounds the number of blocks.

Subsets of the points are written as vectors of booleans. Hex.PermGroup.Group.setTransporter? searches for an element of G mapping one subset onto another, and returns none when there is no such element. In the square, the edge {0, 1} is mapped onto the edge {1, 2}: