def Hex.PermGroup.Action.Domain {n : Nat} {G : Group n} {α : Type u} (a : Action G α) (objects : Array α) : Prop

A recorded enumeration of an invariant domain. Closure is checked on the signed original generators before any index permutation is constructed.

Equations

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

@[instance_reducible]

instance Hex.PermGroup.Action.instDecidableDomain {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (objects : Array α) : Decidable (a.Domain objects)

Equations

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

theorem Hex.PermGroup.Action.Domain.invariant {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) (x : α) : x ∈ objects ↔ a.act p x ∈ objects

def Hex.PermGroup.Action.Domain.index {α : Type u} [DecidableEq α] {objects : Array α} (x : α) (hx : x ∈ objects) : Fin objects.size

Linear lookup uses decidable equality; no unchecked hash or ordering is used.

Equations

• Hex.PermGroup.Action.Domain.index x hx = ⟨Array.findIdx (fun (y : α) => decide (y = x)) objects, ⋯⟩

@[simp]

theorem Hex.PermGroup.Action.Domain.object_index {α : Type u} [DecidableEq α] {objects : Array α} (x : α) (hx : x ∈ objects) : objects[↑(index x hx)] = x

theorem Hex.PermGroup.Action.Domain.object_injective {n : Nat} {G : Group n} {α : Type u} {a : Action G α} {objects : Array α} (h : a.Domain objects) {i j : Fin objects.size} (he : objects[↑i] = objects[↑j]) : i = j

def Hex.PermGroup.Action.Domain.act {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) (i : Fin objects.size) : Fin objects.size

The induced action on the recorded domain indices.

Equations

• h.act p i = Hex.PermGroup.Action.Domain.index (a.act p objects[↑i]) ⋯

@[simp]

theorem Hex.PermGroup.Action.Domain.object_act {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) (i : Fin objects.size) : objects[↑(h.act p i)] = a.act p objects[↑i]

@[simp]

theorem Hex.PermGroup.Action.Domain.act_id {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (i : Fin objects.size) : h.act (Element.id G) i = i

theorem Hex.PermGroup.Action.Domain.act_comp {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p q : Element G) (i : Fin objects.size) : h.act (p.comp q) i = h.act p (h.act q i)

@[simp]

theorem Hex.PermGroup.Action.Domain.act_inv {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) (i : Fin objects.size) : h.act p (h.act p.inv i) = i

@[simp]

theorem Hex.PermGroup.Action.Domain.inv_act {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) (i : Fin objects.size) : h.act p.inv (h.act p i) = i

def Hex.PermGroup.Action.Domain.perm {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) : Perm objects.size

Every group element induces an executable permutation of the domain.

Equations

• h.perm p = Hex.Perm.ofFn (h.act p) ⋯ ⋯

@[simp]

theorem Hex.PermGroup.Action.Domain.get_perm {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) (i : Fin objects.size) : (h.perm p).get i = h.act p i

@[simp]

theorem Hex.PermGroup.Action.Domain.perm_id {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) : h.perm (Element.id G) = Perm.id objects.size

theorem Hex.PermGroup.Action.Domain.perm_comp {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p q : Element G) : h.perm (p.comp q) = (h.perm p).comp (h.perm q)

@[simp]

theorem Hex.PermGroup.Action.Domain.perm_inv {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) : h.perm p.inv = (h.perm p).inv

theorem Hex.PermGroup.Action.Domain.perm_eq_id {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (p : Element G) : h.perm p = Perm.id objects.size ↔ ∀ (x : α), x ∈ objects → a.act p x = x

Identity in the image means every recorded object is fixed.