def Hex.PermGroup.Action.Orbit.schreier {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p : Element G) (i : Fin c.objects.size) : Element G

Schreier elements stay in the original permutation group. The action on objects is used only to select the representative at the new orbit index.

Equations

• Hex.PermGroup.Action.Orbit.schreier h p i = c.reps[↑(⋯.act p i)].inv.comp (p.comp c.reps[↑i])

@[simp]

theorem Hex.PermGroup.Action.Orbit.schreier_id {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (i : Fin c.objects.size) : schreier h (Element.id G) i = Element.id G

theorem Hex.PermGroup.Action.Orbit.schreier_comp {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p q : Element G) (i : Fin c.objects.size) : schreier h (p.comp q) i = (schreier h p (⋯.act q i)).comp (schreier h q i)

theorem Hex.PermGroup.Action.Orbit.schreier_inv {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p : Element G) (i : Fin c.objects.size) : schreier h p.inv i = (schreier h p (⋯.act p.inv i)).inv

@[simp]

theorem Hex.PermGroup.Action.Orbit.schreier_fixes {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p : Element G) (i : Fin c.objects.size) : a.act (schreier h p i) x = x

theorem Hex.PermGroup.Action.Orbit.schreier_mem {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) {T : Array (Perm n)} (hs : ∀ (j : Fin G.generators.size) (i : Fin c.objects.size), Generated T (schreier h ⟨G.generators[↑j], ⋯⟩ i).val) (p : Element G) (i : Fin c.objects.size) : Generated T (schreier h p i).val

Generator Schreier elements suffice for all elements, by the multiplication and inverse identities above. This proof does not assume a faithful action.

def Hex.PermGroup.Action.Orbit.stabilizerGens {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) : Array (Perm n)

Full Schreier family, in original-generator then orbit-discovery order.

Equations

• One or more equations did not get rendered due to their size.

theorem Hex.PermGroup.Action.Orbit.stabilizerGens_spec {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p : Perm n) : Generated (stabilizerGens h) p ↔ ∃ (hp : Generated G.generators p), a.act ⟨p, hp⟩ x = x

The Schreier family generates exactly the object stabilizer in the original group, including every element in the action kernel.

def Hex.PermGroup.Action.Orbit.stabilizer {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) : Group n

Rebuild a checked chain for the complete object stabilizer, keeping only the Schreier generators that are not generated by earlier ones.

Equations

• Hex.PermGroup.Action.Orbit.stabilizer h = Hex.PermGroup.Group.ofGenerators (Hex.PermGroup.sieve (Hex.PermGroup.Action.Orbit.stabilizerGens h))

theorem Hex.PermGroup.Action.Orbit.mem_stabilizer {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p : Perm n) : Generated (stabilizer h).generators p ↔ ∃ (hp : Generated G.generators p), a.act ⟨p, hp⟩ x = x

theorem Hex.PermGroup.Action.Orbit.stabilizer_subgroup {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) : (stabilizer h).IsSubgroup G

def Hex.PermGroup.Action.Orbit.schreierWord {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (j : Fin G.generators.size) (i : Fin c.objects.size) : Program

A Schreier generator has a checked program in the original inputs.

Equations

• Hex.PermGroup.Action.Orbit.schreierWord h j i = c.words[↑(⋯.act ⟨G.generators[↑j], ⋯⟩ i)].inv.comp ({ nodes := #[Hex.PermGroup.Node.generator ↑j], root := 0 }.comp c.words[↑i])

theorem Hex.PermGroup.Action.Orbit.check_schreierWord {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (j : Fin G.generators.size) (i : Fin c.objects.size) : checkWord G.generators (schreier h ⟨G.generators[↑j], ⋯⟩ i).val (schreierWord h j i) = true