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

An executable left action with laws for every group element. Its argument is a permutation value with membership evidence, independent of word programs.

• act : Element G → α → α
• id_act (x : α) : self.act (Element.id G) x = x
• comp_act (p q : Element G) (x : α) : self.act (p.comp q) x = self.act p (self.act q x)

@[simp]

theorem Hex.PermGroup.Action.act_id {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (x : α) : a.act (Element.id G) x = x

theorem Hex.PermGroup.Action.act_comp {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (p q : Element G) (x : α) : a.act (p.comp q) x = a.act p (a.act q x)

@[simp]

theorem Hex.PermGroup.Action.act_inv {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (p : Element G) (x : α) : a.act p (a.act p.inv x) = x

@[simp]

theorem Hex.PermGroup.Action.inv_act {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (p : Element G) (x : α) : a.act p.inv (a.act p x) = x

theorem Hex.PermGroup.Action.act_injective {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (p : Element G) {x y : α} (h : a.act p x = a.act p y) : x = y

theorem Hex.PermGroup.Action.act_surjective {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (p : Element G) (x : α) : ∃ (y : α), a.act p y = x

def Hex.PermGroup.Action.restrict {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (H : Group n) (h : H.IsSubgroup G) : Action H α

Restrict an action to a checked subgroup, without changing its values.

Equations

• a.restrict H h = { act := fun (p : Hex.PermGroup.Element H) (x : α) => a.act ⟨p.val, ⋯⟩ x, id_act := ⋯, comp_act := ⋯ }

def Hex.PermGroup.Action.vectors {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (k : Nat) : Action G (Vector α k)

Componentwise action on fixed-length tuples; repeated entries are retained.

Equations

• a.vectors k = { act := fun (p : Hex.PermGroup.Element G) (xs : Vector α k) => Vector.map (a.act p) xs, id_act := ⋯, comp_act := ⋯ }

def Hex.PermGroup.Action.natural {n : Nat} (G : Group n) : Action G (Fin n)

The natural action on the declared point domain, including degree zero.

Equations

• Hex.PermGroup.Action.natural G = { act := fun (p : Hex.PermGroup.Element G) (x : Fin n) => p.val.get x, id_act := ⋯, comp_act := ⋯ }

def Hex.PermGroup.Action.tuples {n : Nat} (G : Group n) (k : Nat) : Action G (Vector (Fin n) k)

Equations

• Hex.PermGroup.Action.tuples G k = (Hex.PermGroup.Action.natural G).vectors k

def Hex.PermGroup.Action.subsets {n : Nat} (G : Group n) : Action G (Vector Bool n)

Bit vectors represent subsets. Moving points forward reads their membership at inverse images, so this obeys the same left-action composition convention.

Equations

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

@[simp]

theorem Hex.PermGroup.Action.subsets_apply {n : Nat} (G : Group n) (p : Element G) (xs : Vector Bool n) (x : Fin n) : ((subsets G).act p xs).get (p.val.get x) = xs.get x

A subset element moves to the forward image of its original point.

theorem Hex.PermGroup.Action.invariant {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (P : α → Prop) (h : ∀ (i : Fin G.generators.size) (x : α), P x ↔ P (a.act ⟨G.generators[↑i], ⋯⟩ x)) (p : Element G) (x : α) : P x ↔ P (a.act p x)

A predicate invariant under the signed input generators is invariant under every group element. This also applies when the action has a nontrivial kernel.