Generators of the automorphism group of a coloured graph, with the
vertex orbits, the orbit count and the orbit-stabilizer product for the
group order. Every returned permutation is an automorphism
(autos_isIso). Vertices sharing an orbit representative are in one
orbit (autos_sameOrbit_of_eq). HexGraphIso.AutComplete supplies the
biconditional autos_sameOrbit and proves in autos_complete that the
list generates the full group. The Mathlib bridge proves exact cardinality
theorems for the orbit count and order.
Computing the order runs one traversal per base point, so a
caller who wants only the generators or the orbits should take
Aut.gens or Aut.orbits.
32.4. The automorphism group
The canonical search discovers automorphisms as it goes: whenever a leaf
of the search tree carries the same refinement codes as an earlier one,
the permutation carrying the earlier labelling onto it is a candidate
automorphism, and the search prunes with the ones that check out. Those
generators are an output in their own right.
autos returns them, in the order the traversal
discovered them, together with the vertex orbits, the number of orbits
and the order of the group. The uncoloured mirror is
Graph.autos.
def
The Petersen graph is the natural first example. Its automorphism group
is the symmetric group on the underlying five-element set, of order
120, and it is vertex-transitive, so there is a single orbit. The
generators below are the four the traversal records; the graph is the
same Families.gpetersen 5 2
used above.
namespace HexGraphIsoAutomorphismExample
open HexGraphIsoChapterExample
#guard (Graph.autos petersen).order = 120
#guard (Graph.autos petersen).numOrbits = 1
#guard (Graph.autos petersen).orbits = #[0, 0, 0, 0, 0, 0, 0, 0, 0, 0]
#guard ((Graph.autos petersen).gens.map
fun p => (List.finRange 10).map fun i => (p.get i).val) =
[[0, 1, 2, 7, 5, 4, 6, 3, 9, 8],
[0, 1, 6, 8, 5, 4, 2, 9, 3, 7],
[0, 4, 3, 2, 1, 5, 9, 8, 7, 6],
[1, 0, 4, 3, 2, 6, 5, 9, 8, 7]]
The list is data, but membership is a theorem: every permutation
autos returns really is an automorphism, and the proof runs the same
check the isomorphism surface runs.
example (p : Perm 10) (h : p ∈ (Graph.autos petersen).gens) :
Graph.IsIso petersen petersen p :=
Graph.autos_isIso h
end HexGraphIsoAutomorphismExample
The returned list generates the full automorphism group, by
Graph.autos_complete. Two vertices have
the same orbit entry if and only if an automorphism carries one onto the
other (Graph.autos_sameOrbit). Thus the
single reported orbit is the full group's vertex orbit. The Mathlib bridge
also proves that the reported orbit count and order are the cardinalities
of the orbit quotient and the full automorphism group, respectively.
Here order = 120 is the group order. Conformance independently compares
these values against nauty.