@[reducible, inline]

abbrev Hex.PermGroup.Partition.Block {n : Nat} (p : Partition n) : Type

A block is identified by its least point.

Equations

• p.Block = { x : Fin n // p.labels[↑x] = x }

def Hex.PermGroup.Partition.block {n : Nat} (p : Partition n) (x : Fin n) : p.Block

The block containing a point.

Equations

• p.block x = ⟨p.labels[↑x], ⋯⟩

theorem Hex.PermGroup.Partition.block_eq {n : Nat} (p : Partition n) (x y : Fin n) : p.block x = p.block y ↔ p.Same x y

def Hex.PermGroup.Partition.blocks {n : Nat} (p : Partition n) : Array p.Block

Canonical block order is increasing least-point order.

Equations

• p.blocks = (List.map (fun (x : { x : Fin n // x ∈ p.roots }) => ⟨x.val, ⋯⟩) p.roots.attach).toArray

@[simp]

theorem Hex.PermGroup.Partition.blocks_size {n : Nat} (p : Partition n) : p.blocks.size = p.roots.length

theorem Hex.PermGroup.Partition.mem_blocks {n : Nat} (p : Partition n) (b : p.Block) : b ∈ p.blocks

theorem Hex.PermGroup.Partition.blocks_nodup {n : Nat} (p : Partition n) : p.blocks.toList.Nodup

def Hex.PermGroup.Action.blocks {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) : Action G p.Block

The action on least-point block representatives. Invariance is required; transitivity and equal block sizes are not.

Equations

• Hex.PermGroup.Action.blocks G p hp = { act := fun (g : Hex.PermGroup.Element G) (b : p.Block) => p.block (g.val.get b.val), id_act := ⋯, comp_act := ⋯ }

theorem Hex.PermGroup.Action.blocks_image {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) (g : Element G) (x : Fin n) : (blocks G p hp).act g (p.block x) = p.block (g.val.get x)

theorem Hex.PermGroup.Action.blocks_domain {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) : (blocks G p hp).Domain p.blocks

theorem Hex.PermGroup.Action.blocks_fixed {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) (g : Element G) : (∀ (b : p.Block), b ∈ p.blocks → (blocks G p hp).act g b = b) ↔ ∀ (x : Fin n), p.Same (g.val.get x) x

Fixing each block permits arbitrary permutations within that block.

structure Hex.PermGroup.BlockAction {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) : Type

The induced permutation image on canonically numbered blocks, together with its exact kernel in the original action degree.

• image : (Action.blocks G p hp).Image p.blocks
• kernel : (Action.blocks G p hp).Kernel p.blocks

theorem Hex.PermGroup.BlockAction.mem_kernel {n : Nat} {G : Group n} {p : Partition n} {hp : p.IsInvariant G} (a : BlockAction G p hp) (g : Perm n) : Generated a.kernel.group.generators g ↔ Generated G.generators g ∧ ∀ (x : Fin n), p.Same (g.get x) x

theorem Hex.PermGroup.BlockAction.map_block {n : Nat} {G : Group n} {p : Partition n} {hp : p.IsInvariant G} (a : BlockAction G p hp) (g : Element G) (i : Fin p.blocks.size) : p.blocks[↑((a.image.map g).val.get i)] = p.block (g.val.get p.blocks[↑i].val)

The image map uses the recorded canonical block numbering.

def Hex.PermGroup.Group.blockAction {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) (cap : Nat) : Except Action.ImageError (BlockAction G p hp)

Construct the full image and kernel after checking the block-count budget. The domain consists of all blocks, including fixed blocks and unequal sizes.

Equations

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

theorem Hex.PermGroup.Group.blockAction_ok {n : Nat} (G : Group n) (p : Partition n) (hp : p.IsInvariant G) (cap : Nat) : (∃ (a : BlockAction G p hp), G.blockAction p hp cap = Except.ok a) ↔ p.roots.length ≤ cap