inductive Hex.GraphIso.Perm.Generated {n : Nat} (gens : List (Perm n)) : Perm n → Prop

Membership in the subgroup generated by a list of permutations. This relation is proof data only; computing generators does not construct it.

• id {n : Nat} {gens : List (Perm n)} : Generated gens (Perm.id n)
• mem {n : Nat} {gens : List (Perm n)} {p : Perm n} : p ∈ gens → Generated gens p
• comp {n : Nat} {gens : List (Perm n)} {p q : Perm n} : Generated gens p → Generated gens q → Generated gens (p.comp q)
• inv {n : Nat} {gens : List (Perm n)} {p : Perm n} : Generated gens p → Generated gens p.inv

theorem Hex.GraphIso.Perm.Generated.induction {n : Nat} {gens : List (Perm n)} {P : Perm n → Prop} (hid : P (Perm.id n)) (hmem : ∀ (p : Perm n), p ∈ gens → P p) (hcomp : ∀ (p q : Perm n), P p → P q → P (p.comp q)) (hinv : ∀ (p : Perm n), P p → P p.inv) {p : Perm n} (hp : Generated gens p) : P p

A subgroup containing the generators contains every generated element.

theorem Hex.GraphIso.Perm.Generated.map {n : Nat} {s t : List (Perm n)} (h : ∀ (p : Perm n), p ∈ s → Generated t p) {p : Perm n} (hp : Generated s p) : Generated t p

Replacing each generator by a word in another list preserves membership.

theorem Hex.GraphIso.Perm.Generated.mono {n : Nat} {s t : List (Perm n)} (h : ∀ (p : Perm n), p ∈ s → p ∈ t) {p : Perm n} (hp : Generated s p) : Generated t p

theorem Hex.GraphIso.Perm.Generated.isIso {n k : Nat} {G : Colored n k} {gens : List (Perm n)} (h : ∀ (p : Perm n), p ∈ gens → IsIso G G p) {p : Perm n} (hp : Generated gens p) : IsIso G G p

Words in automorphisms are automorphisms.

theorem Hex.GraphIso.Perm.Generated.fixes {n : Nat} {gens : List (Perm n)} {v : Fin n} (h : ∀ (p : Perm n), p ∈ gens → p.get v = v) {p : Perm n} (hp : Generated gens p) : p.get v = v

Words in permutations fixing a point also fix that point.

def Hex.GraphIso.Perm.Fixes {n : Nat} (base : List (Fin n)) (p : Perm n) : Prop

The pointwise stabilizer condition for a list of base points.

Equations

• Hex.GraphIso.Perm.Fixes base p = ∀ (v : Fin n), v ∈ base → p.get v = v

theorem Hex.GraphIso.Perm.Fixes.id {n : Nat} (base : List (Fin n)) : Fixes base (Perm.id n)

theorem Hex.GraphIso.Perm.Fixes.comp {n : Nat} {base : List (Fin n)} {p q : Perm n} (hp : Fixes base p) (hq : Fixes base q) : Fixes base (p.comp q)

theorem Hex.GraphIso.Perm.Fixes.inv {n : Nat} {base : List (Fin n)} {p : Perm n} (hp : Fixes base p) : Fixes base p.inv

theorem Hex.GraphIso.Perm.Fixes.cons {n : Nat} {base : List (Fin n)} {p : Perm n} {v : Fin n} : Fixes (v :: base) p ↔ p.get v = v ∧ Fixes base p

theorem Hex.GraphIso.Perm.Fixes.nil {n : Nat} (p : Perm n) : Fixes [] p

theorem Hex.GraphIso.Perm.Generated.of_stabilizer {n k : Nat} {G : Colored n k} {gens : List (Perm n)} {base : List (Fin n)} {v : Fin n} (hnext : ∀ (p : Perm n), IsIso G G p → Fixes (v :: base) p → Generated gens p) (himages : ∀ (p : Perm n), IsIso G G p → Fixes base p → ∃ (q : Perm n), Generated gens q ∧ IsIso G G q ∧ Fixes base q ∧ q.get v = p.get v) {p : Perm n} (hp : IsIso G G p) (hfix : Fixes base p) : Generated gens p

A point-stabilizer step in the generation proof. To generate the stabilizer of base, it suffices to generate the stabilizer of the next point and to represent every image of that point. All membership claims use the same final generator list.