@[instance_reducible]

def Hex.PermGroup.Action.toMulAction {n : ℕ} {G : Group n} {α : Type u} (a : Action G α) : MulAction (Element G) α

Interpret the executable action as a Mathlib action, preserving its values.

Equations

• a.toMulAction = { smul := a.act, mul_smul := ⋯, one_smul := ⋯ }

@[simp]

theorem Hex.PermGroup.Action.smul_spec {n : ℕ} {G : Group n} {α : Type u} (a : Action G α) (p : Element G) (x : α) : have x_1 := a.toMulAction; p • x = a.act p x

def Hex.PermGroup.Action.Image.hom {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) : Element G →* Element image.group

The checked image map is a surjective group homomorphism.

Equations

• image.hom = { toFun := image.map, map_one' := ⋯, map_mul' := ⋯ }

theorem Hex.PermGroup.Action.Image.hom_surjective {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) : Function.Surjective ⇑image.hom

theorem Hex.PermGroup.Action.Image.mem_ker {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (p : Element G) : p ∈ image.hom.ker ↔ ∀ x ∈ objects, a.act p x = x

theorem Hex.PermGroup.Action.Image.contains_spec {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) (q : Perm objects.size) : q.toEquiv ∈ closure image.group.generators ↔ ∃ (p : Element G), (⋯.perm p).toEquiv = q.toEquiv

The image subgroup is exactly Mathlib's image of the induced action.

theorem Hex.PermGroup.Action.Image.order_eq {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) : G.order = Nat.card ↥image.hom.ker * image.group.order

The finite homomorphism theorem identifies the exact image order even for nonfaithful actions. The kernel here fixes every recorded domain object.

theorem Hex.PermGroup.Action.Image.injective_iff {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (image : a.Image objects) : Function.Injective ⇑image.hom ↔ ∀ (p : Element G), (∀ x ∈ objects, a.act p x = x) → p = Element.id G

theorem Hex.PermGroup.Action.Orbit.mem_spec {n : ℕ} {G : Group n} {α : Type u} {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (y : α) : have x_1 := a.toMulAction; y ∈ c.objects ↔ y ∈ MulAction.orbit (Element G) x

theorem Hex.PermGroup.Action.Orbit.stabilizer_spec {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {x : α} {c : Orbit G α} (h : Valid a x c) (p : Element G) : have x_1 := a.toMulAction; (↑p).toEquiv ∈ closure (stabilizer h).generators ↔ p ∈ MulAction.stabilizer (Element G) x

def Hex.PermGroup.Action.Kernel.equiv {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (kernel : a.Kernel objects) (image : a.Image objects) : Element kernel.group ≃ ↥image.hom.ker

The computed common stabilizer is exactly the kernel of the image map.

Equations

• kernel.equiv image = { toFun := fun (p : Hex.PermGroup.Element kernel.group) => ⟨⟨↑p, ⋯⟩, ⋯⟩, invFun := fun (p : ↥image.hom.ker) => ⟨↑↑p, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem Hex.PermGroup.Action.Kernel.card_ker {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (kernel : a.Kernel objects) (image : a.Image objects) : Nat.card ↥image.hom.ker = kernel.group.order

theorem Hex.PermGroup.Action.Kernel.order_mul_image {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (kernel : a.Kernel objects) (image : a.Image objects) : G.order = kernel.group.order * image.group.order

Exact order factorization for the two executable constructions.

theorem Hex.PermGroup.Action.Kernel.injective_iff {n : ℕ} {G : Group n} {α : Type u} [DecidableEq α] {a : Action G α} {objects : Array α} (kernel : a.Kernel objects) (image : a.Image objects) : Function.Injective ⇑image.hom ↔ kernel.group.order = 1

@[instance_reducible]

def Hex.PermGroup.Partition.toSetoid {n : ℕ} (p : Partition n) : Setoid (Fin n)

Canonical block labels encode an equivalence relation on all points.

Equations

• p.toSetoid = { r := p.Same, iseqv := ⋯ }

theorem Hex.PermGroup.Partition.toSetoid_injective {n : ℕ} : Function.Injective toSetoid

theorem Hex.PermGroup.Partition.permute_spec {n : ℕ} (s : Perm n) (p : Partition n) (x y : Fin n) : (permute s p).toSetoid x y ↔ p.toSetoid (s.toEquiv.symm x) (s.toEquiv.symm y)