31.2. Explicit actions and stabilizer chains
Perm n stores all n images, including fixed points. Composition is the
left-action convention (p.comp q) x = p (q x). Group.ofGenerators builds a
complete checked stabilizer chain; order and negative membership become
mathematical facts only after that check succeeds.
open Hex Hex.PermGroup
namespace HexPermGroupChapter
def rotation : Perm 4 :=
⟨#v[1, 2, 3, 0], ⊢ #v[1, 2, 3, 0].toList.Nodup All goals completed! 🐙, ⊢ ∀ (i : Fin 4), i ∈ #v[1, 2, 3, 0].toList All goals completed! 🐙⟩
def reflection : Perm 4 :=
⟨#v[0, 3, 2, 1], ⊢ #v[0, 3, 2, 1].toList.Nodup All goals completed! 🐙, ⊢ ∀ (i : Fin 4), i ∈ #v[0, 3, 2, 1].toList All goals completed! 🐙⟩
def polygon : Group 4 :=
Group.ofGenerators #[rotation, reflection]
#guard polygon.order = 8
#guard (polygon.orbit 0).size = 4
#guard (polygon.stabilizer 0).order = 2
#guard (polygon.word? (rotation.comp reflection)).isSome
The returned membership program is expressed in the original presentation and
is accepted by checkWord. Different presentations can be compared as
subgroups rather than by generator-array equality. Left cosets are used
throughout; for a nonnormal subgroup they must not be interchanged with right
cosets.
For graph automorphisms, constructing a group from known automorphism generators proves only that subgroup. The graph-isomorphism completeness certificate is the additional boundary needed to identify it with the whole automorphism group.
def cyclicA : Group 4 := Group.ofGenerators #[rotation]
def cyclicB : Group 4 := Group.ofGenerators #[rotation.inv]
#guard cyclicA.sameGroup cyclicB
def swap3 : Perm 3 := ⟨#v[1, 0, 2], ⊢ #v[1, 0, 2].toList.Nodup All goals completed! 🐙, ⊢ ∀ (i : Fin 3), i ∈ #v[1, 0, 2].toList All goals completed! 🐙⟩
def cycle3 : Perm 3 := ⟨#v[1, 2, 0], ⊢ #v[1, 2, 0].toList.Nodup All goals completed! 🐙, ⊢ ∀ (i : Fin 3), i ∈ #v[1, 2, 0].toList All goals completed! 🐙⟩
def symmetric3 : Group 3 :=
Group.ofGenerators #[swap3, cycle3]
def pointFixer : Group 3 := symmetric3.stabilizer 2
example : pointFixer.IsSubgroup symmetric3 := ⊢ pointFixer.IsSubgroup symmetric3
p:Perm 3hp:Generated pointFixer.generators p⊢ Generated symmetric3.generators p
All goals completed! 🐙
#guard (symmetric3.leftCosetsWith 3 pointFixer (⊢ pointFixer.IsSubgroup symmetric3
p:Perm 3hp:Generated pointFixer.generators p⊢ Generated symmetric3.generators p
All goals completed! 🐙)).isOk