theorem Hex.PermGroup.Action.Domain.restrict {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {objects : Array α} (hd : a.Domain objects) (H : Group n) (hi : H.IsSubgroup G) : (a.restrict H hi).Domain objects

structure Hex.PermGroup.Action.Kernel {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (objects : Array α) : Type

A checked subgroup consisting exactly of elements fixing every supplied object. Its elements retain the original action degree.

• group : Group n
• spec (p : Perm n) : Generated self.group.generators p ↔ ∃ (hp : Generated G.generators p), ∀ (y : α), y ∈ objects → a.act ⟨p, hp⟩ y = y

theorem Hex.PermGroup.Action.Kernel.subgroup {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {objects : Array α} (kernel : a.Kernel objects) : kernel.group.IsSubgroup G

def Hex.PermGroup.Action.Kernel.prepend {n : Nat} {G : Group n} {α : Type u} {a : Action G α} (H : Group n) (hi : H.IsSubgroup G) (x : α) (points : List α) (hs : ∀ (p : Perm n), Generated H.generators p ↔ ∃ (hp : Generated G.generators p), a.act ⟨p, hp⟩ x = x) (child : (a.restrict H hi).Kernel points.toArray) : a.Kernel (x :: points).toArray

Add the first fixed-object condition to a kernel in its stabilizer.

Equations

• Hex.PermGroup.Action.Kernel.prepend H hi x points hs child = { group := child.group, spec := ⋯ }

def Hex.PermGroup.Action.Kernel.fromDomain {n : Nat} {α : Type u} [DecidableEq α] {G : Group n} (a : Action G α) (domain : Array α) (hd : a.Domain domain) (points : List α) (hp : ∀ (y : α), y ∈ points → y ∈ domain) : a.Kernel points.toArray

Successive full Schreier stabilizers compute the common fixed subgroup. The domain remains invariant after each restriction and bounds every orbit.

Equations

• One or more equations did not get rendered due to their size.
• Hex.PermGroup.Action.Kernel.fromDomain a domain hd [] hp_2 = { group := G, spec := ⋯ }

def Hex.PermGroup.Action.actionKernel {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (cap : Nat) (objects : Array α) : Except ImageError (a.Kernel objects)

Validate the explicit domain budget and invariance, then intersect complete object stabilizers. On an empty domain this returns the original group.

Equations

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

theorem Hex.PermGroup.Action.actionKernel_ok {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (cap : Nat) (objects : Array α) : (∃ (kernel : a.Kernel objects), a.actionKernel cap objects = Except.ok kernel) ↔ objects.size ≤ cap ∧ a.Domain objects

@[simp]

theorem Hex.PermGroup.Action.actionKernel_empty {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (cap : Nat) : Except.map Kernel.group (a.actionKernel cap #[]) = Except.ok G