def Hex.PermGroup.Orbit.index {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin n) (hx : x ∈ c.points) : Fin c.points.size

Read the orbit index of a point known to belong to the checked orbit.

Equations

• Hex.PermGroup.Orbit.index h x hx = c.lookup[↑x].get ⋯

@[simp]

theorem Hex.PermGroup.Orbit.point_index {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin n) (hx : x ∈ c.points) : c.points[↑(index h x hx)] = x

theorem Hex.PermGroup.Orbit.point_injective {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {i j : Fin c.points.size} (he : c.points[↑i] = c.points[↑j]) : i = j

def Hex.PermGroup.Orbit.act {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (p : Perm n) (hp : Generated S p) (x : Fin c.points.size) : Fin c.points.size

The action of a generated permutation on the stored orbit indices.

Equations

• Hex.PermGroup.Orbit.act h p hp x = Hex.PermGroup.Orbit.index h (p.get c.points[↑x]) ⋯

@[simp]

theorem Hex.PermGroup.Orbit.point_act {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (p : Perm n) (hp : Generated S p) (x : Fin c.points.size) : c.points[↑(act h p hp x)] = p.get c.points[↑x]

@[simp]

theorem Hex.PermGroup.Orbit.act_id {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin c.points.size) : act h (Perm.id n) ⋯ x = x

theorem Hex.PermGroup.Orbit.act_comp {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p q : Perm n} (hp : Generated S p) (hq : Generated S q) (x : Fin c.points.size) : act h (p.comp q) ⋯ x = act h p hp (act h q hq x)

@[simp]

theorem Hex.PermGroup.Orbit.act_inv {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p : Perm n} (hp : Generated S p) (x : Fin c.points.size) : act h p hp (act h p.inv ⋯ x) = x

@[simp]

theorem Hex.PermGroup.Orbit.rep_apply {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin c.points.size) : c.reps[↑x].get a = c.points[↑x]

theorem Hex.PermGroup.Orbit.rep_generated {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin c.points.size) : Generated S c.reps[↑x]

def Hex.PermGroup.Orbit.schreier {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (p : Perm n) (hp : Generated S p) (x : Fin c.points.size) : Perm n

The Schreier element t_(p(x))⁻¹ * p * t_x, in left-action order.

Equations

• Hex.PermGroup.Orbit.schreier h p hp x = c.reps[↑(Hex.PermGroup.Orbit.act h p hp x)].inv.comp (p.comp c.reps[↑x])

def Hex.PermGroup.Orbit.schreierImpl {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (p : Perm n) (hp : Generated S p) (x : Fin c.points.size) : Perm n

schreier for compiled code, using the stored inverse representative.

Equations

• Hex.PermGroup.Orbit.schreierImpl h p hp x = c.invs[↑(Hex.PermGroup.Orbit.act h p hp x)].comp (p.comp c.reps[↑x])

@[csimp]

theorem Hex.PermGroup.Orbit.schreier_eq_schreierImpl : @schreier = @schreierImpl

@[simp]

theorem Hex.PermGroup.Orbit.schreier_id {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (x : Fin c.points.size) : schreier h (Perm.id n) ⋯ x = Perm.id n

theorem Hex.PermGroup.Orbit.schreier_comp {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p q : Perm n} (hp : Generated S p) (hq : Generated S q) (x : Fin c.points.size) : schreier h (p.comp q) ⋯ x = (schreier h p hp (act h q hq x)).comp (schreier h q hq x)

Multiplication of Schreier elements follows the successive point images.

theorem Hex.PermGroup.Orbit.schreier_inv {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p : Perm n} (hp : Generated S p) (x : Fin c.points.size) : schreier h p.inv ⋯ x = (schreier h p hp (act h p.inv ⋯ x)).inv

theorem Hex.PermGroup.Orbit.schreier_generated {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p : Perm n} (hp : Generated S p) (x : Fin c.points.size) : Generated S (schreier h p hp x)

@[simp]

theorem Hex.PermGroup.Orbit.schreier_fixes {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) {p : Perm n} (hp : Generated S p) (x : Fin c.points.size) : (schreier h p hp x).get a = a

theorem Hex.PermGroup.Orbit.schreier_mem {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} {T : Array (Perm n)} (h : Valid S a c) (hs : ∀ (i : Fin S.size) (x : Fin c.points.size), Generated T (schreier h S[↑i] ⋯ x)) {p : Perm n} (hp : Generated S p) (x : Fin c.points.size) : Generated T (schreier h p hp x)

If a subgroup contains the Schreier elements for all input generators, it contains those for every generated permutation.

def Hex.PermGroup.Orbit.stabilizerGens {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) : Array (Perm n)

The complete Schreier family for the supplied generators and checked orbit. The chain builder supplies its normalized symmetric array here.

Equations

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

theorem Hex.PermGroup.Orbit.stabilizerGens_spec {n : Nat} {S : Array (Perm n)} {a : Fin n} {c : Orbit n} (h : Valid S a c) (p : Perm n) : Generated (stabilizerGens h) p ↔ Generated S p ∧ p.get a = a

Schreier's lemma: these generators give the entire point stabilizer.