35.8. Graph automorphisms
The Petersen graph, as constructed in the
HexGraphIso chapter, has vertices 0, …, 9: an outer
5-cycle on 0, …, 4, an inner pentagram on 5, …, 9, and an edge from i
to i + 5 for each i < 5. HexGraphIso computes a list of four generators
for its automorphism group. Here they are in cycle notation, followed by a
check that they are the generators HexGraphIso computes:
open Hex.GraphIso in
def petersen : Hex.Graph 10 := Families.gpetersen 5 2
def σ₁ : Equiv.Perm (Fin 10) :=
c[3, 7] * c[4, 5] * c[8, 9]
def σ₂ : Equiv.Perm (Fin 10) :=
c[2, 6] * c[3, 8] * c[4, 5] * c[7, 9]
def σ₃ : Equiv.Perm (Fin 10) :=
c[1, 4] * c[2, 3] * c[6, 9] * c[7, 8]
def σ₄ : Equiv.Perm (Fin 10) :=
c[0, 1] * c[2, 4] * c[5, 6] * c[7, 9]
#guard (Hex.Graph.autos petersen).gens.map
Hex.Perm.toEquiv = [σ₁, σ₂, σ₃, σ₄]
Each of them maps edges to edges and non-edges to non-edges, which decide
checks, so the subgroup they generate consists of automorphisms:
example : ∀ i j,
petersen.adj (σ₁ i) (σ₁ j) = petersen.adj i j := ⊢ ∀ (i j : Fin 10), petersen.adj (σ₁ i) (σ₁ j) = petersen.adj i j
All goals completed! 🐙
example : ∀ i j,
petersen.adj (σ₂ i) (σ₂ j) = petersen.adj i j := ⊢ ∀ (i j : Fin 10), petersen.adj (σ₂ i) (σ₂ j) = petersen.adj i j
All goals completed! 🐙
example : ∀ i j,
petersen.adj (σ₃ i) (σ₃ j) = petersen.adj i j := ⊢ ∀ (i j : Fin 10), petersen.adj (σ₃ i) (σ₃ j) = petersen.adj i j
All goals completed! 🐙
example : ∀ i j,
petersen.adj (σ₄ i) (σ₄ j) = petersen.adj i j := ⊢ ∀ (i j : Fin 10), petersen.adj (σ₄ i) (σ₄ j) = petersen.adj i j
All goals completed! 🐙
The perm_group tactic shows that this subgroup has 120 elements. It also
shows that the list is not minimal: σ₂ lies in the subgroup generated by
the other three. Those three are enough, and none of them can be omitted,
since none lies in the subgroup generated by the other two:
example : Nat.card (Subgroup.closure
({σ₁, σ₂, σ₃, σ₄} : Set (Equiv.Perm (Fin 10)))) =
120 := ⊢ Nat.card ↥(Subgroup.closure {σ₁, σ₂, σ₃, σ₄}) = 120
All goals completed! 🐙
example : σ₂ ∈ Subgroup.closure
({σ₁, σ₃, σ₄} : Set (Equiv.Perm (Fin 10))) := ⊢ σ₂ ∈ Subgroup.closure {σ₁, σ₃, σ₄}
All goals completed! 🐙
example : σ₁ ∉ Subgroup.closure
({σ₃, σ₄} : Set (Equiv.Perm (Fin 10))) := ⊢ σ₁ ∉ Subgroup.closure {σ₃, σ₄}
All goals completed! 🐙
example : σ₃ ∉ Subgroup.closure
({σ₁, σ₄} : Set (Equiv.Perm (Fin 10))) := ⊢ σ₃ ∉ Subgroup.closure {σ₁, σ₄}
All goals completed! 🐙
example : σ₄ ∉ Subgroup.closure
({σ₁, σ₃} : Set (Equiv.Perm (Fin 10))) := ⊢ σ₄ ∉ Subgroup.closure {σ₁, σ₃}
All goals completed! 🐙
The graph_aut tactic checks the graph search with a point-stabilizer
certificate and combines its upper bound with the perm_group certificate.
Thus the kernel proves both that this particular subgroup is the whole
automorphism group and that the full group has order 120:
example : Subgroup.closure
({σ₁, σ₂, σ₃, σ₄} : Set (Equiv.Perm (Fin 10))) =
Hex.GraphIso.Aut.equivGroup petersen.singleColor := ⊢ Subgroup.closure {σ₁, σ₂, σ₃, σ₄} = GraphIso.Aut.equivGroup (petersen.singleColor ⋯)
All goals completed! 🐙
example :
Nat.card (Hex.GraphIso.Aut.equivGroup
petersen.singleColor) = 120 := ⊢ Nat.card ↥(GraphIso.Aut.equivGroup (petersen.singleColor ⋯)) = 120
All goals completed! 🐙
The compiled search only proposes the certificates. Small Boolean checkers replay the graph-refinement and permutation-group evidence in the kernel.