def Hex.PermGroup.Partition.discrete (n : Nat) : Partition n

The discrete partition, including the empty partition in degree zero.

Equations

• Hex.PermGroup.Partition.discrete n = { labels := Hex.Vector.ofFn' id, least := ⋯, idem := ⋯ }

@[simp]

theorem Hex.PermGroup.Partition.discrete_same {n : Nat} (x y : Fin n) : (discrete n).Same x y ↔ x = y

def Hex.PermGroup.Partition.indiscrete (n : Nat) : Partition n

The single-block partition; in degree zero there are no blocks.

Equations

• Hex.PermGroup.Partition.indiscrete n = { labels := Hex.Vector.ofFn' fun (x : Fin n) => ⟨0, ⋯⟩, least := ⋯, idem := ⋯ }

@[simp]

theorem Hex.PermGroup.Partition.indiscrete_same {n : Nat} (x y : Fin n) : (indiscrete n).Same x y

theorem Hex.PermGroup.Partition.equivalence {n : Nat} (p : Partition n) : Equivalence p.Same

def Hex.PermGroup.Partition.Refines {n : Nat} (p : Partition n) (R : Fin n → Fin n → Prop) : Prop

Every block of p lies in one equivalence class of R.

Equations

• p.Refines R = ∀ (x y : Fin n), p.Same x y → R x y

def Hex.PermGroup.Partition.roots {n : Nat} (p : Partition n) : List (Fin n)

Block representatives in increasing point order.

Equations

• p.roots = List.filter (fun (x : Fin n) => decide (p.labels[↑x] = x)) (List.finRange n)

@[simp]

theorem Hex.PermGroup.Partition.mem_roots {n : Nat} (p : Partition n) (x : Fin n) : x ∈ p.roots ↔ p.labels[↑x] = x

theorem Hex.PermGroup.Partition.roots_nodup {n : Nat} (p : Partition n) : p.roots.Nodup

theorem Hex.PermGroup.Partition.roots_pos {n : Nat} (p : Partition n) (hn : 0 < n) : 0 < p.roots.length

def Hex.PermGroup.Partition.mergeRoots {n : Nat} (p : Partition n) (a b : Fin n) (ha : p.labels[↑a] = a) (_hb : p.labels[↑b] = b) (hab : a ≤ b) : Partition n

Quick-find union: redirect one root and all its points to a smaller root. The direct label array keeps each find constant-time and each union linear.

Equations

• p.mergeRoots a b ha _hb hab = { labels := Hex.Vector.ofFn' fun (x : Fin n) => if p.labels[↑x] = b then a else p.labels[↑x], least := ⋯, idem := ⋯ }

theorem Hex.PermGroup.Partition.mergeRoots_coarsens {n : Nat} (p : Partition n) (a b : Fin n) (ha : p.labels[↑a] = a) (hb : p.labels[↑b] = b) (hab : a ≤ b) : p.Refines (p.mergeRoots a b ha hb hab).Same

theorem Hex.PermGroup.Partition.mergeRoots_pair {n : Nat} (p : Partition n) (a b : Fin n) (ha : p.labels[↑a] = a) (hb : p.labels[↑b] = b) (hab : a ≤ b) : (p.mergeRoots a b ha hb hab).Same a b

theorem Hex.PermGroup.Partition.mergeRoots_least {n : Nat} (p : Partition n) (a b : Fin n) (ha : p.labels[↑a] = a) (hb : p.labels[↑b] = b) (hab : a ≤ b) {R : Fin n → Fin n → Prop} (hR : Equivalence R) (hp : p.Refines R) (h : R a b) : (p.mergeRoots a b ha hb hab).Refines R

theorem Hex.PermGroup.Partition.mergeRoots_root {n : Nat} (p : Partition n) (a b : Fin n) (ha : p.labels[↑a] = a) (hb : p.labels[↑b] = b) (hab : a ≤ b) (hne : a ≠ b) (x : Fin n) : (p.mergeRoots a b ha hb hab).labels[↑x] = x ↔ p.labels[↑x] = x ∧ x ≠ b

theorem Hex.PermGroup.Partition.roots_mergeRoots {n : Nat} (p : Partition n) (a b : Fin n) (ha : p.labels[↑a] = a) (hb : p.labels[↑b] = b) (hab : a ≤ b) (hne : a ≠ b) : (p.mergeRoots a b ha hb hab).roots = p.roots.erase b

def Hex.PermGroup.Partition.merge {n : Nat} (p : Partition n) (x y : Fin n) : Partition n

Merge the two blocks, preserving canonical least-point labels.

Equations

• p.merge x y = if h : p.labels[↑x] ≤ p.labels[↑y] then p.mergeRoots p.labels[↑x] p.labels[↑y] ⋯ ⋯ h else p.mergeRoots p.labels[↑y] p.labels[↑x] ⋯ ⋯ ⋯

theorem Hex.PermGroup.Partition.merge_coarsens {n : Nat} (p : Partition n) (x y : Fin n) : p.Refines (p.merge x y).Same

theorem Hex.PermGroup.Partition.merge_pair {n : Nat} (p : Partition n) (x y : Fin n) : (p.merge x y).Same x y

theorem Hex.PermGroup.Partition.merge_least {n : Nat} (p : Partition n) (x y : Fin n) {R : Fin n → Fin n → Prop} (hR : Equivalence R) (hp : p.Refines R) (h : R x y) : (p.merge x y).Refines R

Union introduces exactly the equivalences forced by the old blocks and the requested pair, for any target equivalence relation.

theorem Hex.PermGroup.Partition.roots_merge {n : Nat} (p : Partition n) (x y : Fin n) (h : ¬p.Same x y) : (p.merge x y).roots.length + 1 = p.roots.length

Each effective union removes exactly one block.