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

Images of the original generators, in their original order.

Equations

• h.generators = (Hex.Vector.ofFn' fun (i : Fin G.generators.size) => h.perm ⟨G.generators[↑i], ⋯⟩).toArray

@[simp]

theorem Hex.PermGroup.Action.Domain.generators_size {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) : h.generators.size = G.generators.size

theorem Hex.PermGroup.Action.Domain.mem_generators {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (q : Perm objects.size) : q ∈ h.generators ↔ ∃ (i : Fin G.generators.size), h.perm ⟨G.generators[↑i], ⋯⟩ = q

theorem Hex.PermGroup.Action.Domain.generated_iff {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (h : a.Domain objects) (q : Perm objects.size) : Generated h.generators q ↔ ∃ (p : Element G), h.perm p = q

The generated image is exactly the image of all original group elements; no faithfulness assumption is needed.

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

A checked image group, tied to the supplied domain enumeration and retaining the order of the original generators for preimage certificates.

• domain : a.Domain objects
• group : Group objects.size
• generators_eq : self.group.generators = ⋯.generators

def Hex.PermGroup.Action.Image.map {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (p : Element G) : Element image.group

The permutation induced by an original group element belongs to the image.

Equations

• image.map p = ⟨⋯.perm p, ⋯⟩

@[simp]

theorem Hex.PermGroup.Action.Image.map_id {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) : image.map (Element.id G) = Element.id image.group

theorem Hex.PermGroup.Action.Image.map_comp {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (p q : Element G) : image.map (p.comp q) = (image.map p).comp (image.map q)

theorem Hex.PermGroup.Action.Image.map_surjective {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (q : Element image.group) : ∃ (p : Element G), image.map p = q

theorem Hex.PermGroup.Action.Image.contains_iff {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (q : Perm objects.size) : image.group.contains q = true ↔ ∃ (p : Element G), ⋯.perm p = q

def Hex.PermGroup.Action.Image.source {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (i : Fin image.group.generators.size) : Fin G.generators.size

The source generator associated with an image generator.

Equations

• image.source i = ⟨↑i, ⋯⟩

def Hex.PermGroup.Action.Image.preimage {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (i : Fin image.group.generators.size) : Element G

Equations

• image.preimage i = ⟨G.generators[↑(image.source i)], ⋯⟩

def Hex.PermGroup.Action.Image.preimageWord {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (i : Fin image.group.generators.size) : Program

Equations

• image.preimageWord i = { nodes := #[Hex.PermGroup.Node.generator ↑(image.source i)], root := 0 }

theorem Hex.PermGroup.Action.Image.check_preimage {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (i : Fin image.group.generators.size) : checkWord G.generators (image.preimage i).val (image.preimageWord i) = true

theorem Hex.PermGroup.Action.Image.map_preimage {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (i : Fin image.group.generators.size) : (image.map (image.preimage i)).val = image.group.generators[↑i]

theorem Hex.PermGroup.Action.Image.map_eq_id {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (p : Element G) : image.map p = Element.id image.group ↔ ∀ (x : α), x ∈ objects → a.act p x = x

inductive Hex.PermGroup.Action.ImageError : Type

• sizeLimit (limit : SizeLimit) : ImageError
• invalidDomain : ImageError

@[instance_reducible]

instance Hex.PermGroup.Action.instDecidableEqImageError : DecidableEq ImageError

Equations

• Hex.PermGroup.Action.instDecidableEqImageError = Hex.PermGroup.Action.instDecidableEqImageError.decEq

def Hex.PermGroup.Action.instDecidableEqImageError.decEq (x✝ x✝¹ : ImageError) : Decidable (x✝ = x✝¹)

Equations

• Hex.PermGroup.Action.instDecidableEqImageError.decEq (Hex.PermGroup.Action.ImageError.sizeLimit a) (Hex.PermGroup.Action.ImageError.sizeLimit b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Hex.PermGroup.Action.instDecidableEqImageError.decEq (Hex.PermGroup.Action.ImageError.sizeLimit limit) Hex.PermGroup.Action.ImageError.invalidDomain = isFalse ⋯
• Hex.PermGroup.Action.instDecidableEqImageError.decEq Hex.PermGroup.Action.ImageError.invalidDomain (Hex.PermGroup.Action.ImageError.sizeLimit limit) = isFalse ⋯
• Hex.PermGroup.Action.instDecidableEqImageError.decEq Hex.PermGroup.Action.ImageError.invalidDomain Hex.PermGroup.Action.ImageError.invalidDomain = isTrue ⋯

@[instance_reducible]

instance Hex.PermGroup.Action.instReprImageError : Repr ImageError

Equations

• Hex.PermGroup.Action.instReprImageError = { reprPrec := Hex.PermGroup.Action.instReprImageError.repr }

def Hex.PermGroup.Action.instReprImageError.repr : ImageError → Nat → Std.Format

Equations

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

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

Check the explicit allocation bound and signed generator closure before constructing index permutations or an image chain. The empty domain is valid.

Equations

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

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

theorem Hex.PermGroup.Action.actionImage_sizeLimit {n : Nat} {G : Group n} {α : Type u} [DecidableEq α] (a : Action G α) (cap : Nat) (objects : Array α) (h : cap < objects.size) : a.actionImage cap objects = Except.error (ImageError.sizeLimit { required := objects.size, capacity := cap })