structure Hex.PermGroup.Partition (n : Nat) : Type

A partition of all declared points. Each point is labelled by the least point in its block; block order is therefore not additional structure.

• labels : Vector (Fin n) n
• least (i : Fin n) : self.labels[↑i] ≤ i
• idem (i : Fin n) : self.labels[↑self.labels[↑i]] = self.labels[↑i]

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

Equations

• p.Same x y = (p.labels[↑x] = p.labels[↑y])

@[instance_reducible]

instance Hex.PermGroup.Partition.instDecidableSame {n : Nat} (p : Partition n) (x y : Fin n) : Decidable (p.Same x y)

Equations

• p.instDecidableSame x y = { decide := decide (↑p.labels[↑x] = ↑p.labels[↑y]), reflects_decide := ⋯ }

theorem Hex.PermGroup.Partition.ext_labels {n : Nat} {p q : Partition n} (h : p.labels = q.labels) : p = q

@[instance_reducible]

instance Hex.PermGroup.Partition.instDecidableEq {n : Nat} : DecidableEq (Partition n)

Equations

• p.instDecidableEq q = if h : p.labels = q.labels then isTrue ⋯ else isFalse ⋯

theorem Hex.PermGroup.Partition.ext {n : Nat} {p q : Partition n} (h : ∀ (x y : Fin n), p.Same x y ↔ q.Same x y) : p = q

A canonical partition is determined solely by which pairs share a block.

theorem Hex.PermGroup.Partition.ext_iff {n : Nat} {p q : Partition n} : p = q ↔ ∀ (x y : Fin n), p.Same x y ↔ q.Same x y

def Hex.PermGroup.Partition.label {n : Nat} {α : Type u} [DecidableEq α] (values : Vector α n) (x : Fin n) : Fin n

Find the least occurrence of the input label at a point.

Equations

• Hex.PermGroup.Partition.label values x = Fin.cast ⋯ (Hex.PermGroup.Action.Domain.index values[↑x] ⋯)

@[simp]

theorem Hex.PermGroup.Partition.value_label {n : Nat} {α : Type u} [DecidableEq α] (values : Vector α n) (x : Fin n) : values[↑(label values x)] = values[↑x]

theorem Hex.PermGroup.Partition.label_le {n : Nat} {α : Type u} [DecidableEq α] (values : Vector α n) (x : Fin n) : label values x ≤ x

theorem Hex.PermGroup.Partition.label_eq {n : Nat} {α : Type u} [DecidableEq α] (values : Vector α n) {x y : Fin n} (h : values[↑x] = values[↑y]) : label values x = label values y

def Hex.PermGroup.Partition.ofValues {n : Nat} {α : Type u} [DecidableEq α] (values : Vector α n) : Partition n

Canonicalize arbitrary block labels without enumerating any partitions.

Equations

• Hex.PermGroup.Partition.ofValues values = { labels := Hex.Vector.ofFn' (Hex.PermGroup.Partition.label values), least := ⋯, idem := ⋯ }

theorem Hex.PermGroup.Partition.ofValues_same {n : Nat} {α : Type u} [DecidableEq α] (values : Vector α n) (x y : Fin n) : (ofValues values).Same x y ↔ values[↑x] = values[↑y]

@[simp]

theorem Hex.PermGroup.Partition.ofValues_labels {n : Nat} (p : Partition n) : ofValues p.labels = p

def Hex.PermGroup.Partition.ofLabels? {n : Nat} (labels : Vector (Fin n) n) : Option (Partition n)

Canonical labels must name their own block's least member. This rejects noncanonical arrays rather than treating arbitrary numeric labels as canonical.

Equations

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

theorem Hex.PermGroup.Partition.ofLabels?_isSome {n : Nat} (labels : Vector (Fin n) n) : (ofLabels? labels).isSome = true ↔ (∀ (i : Fin n), labels[↑i] ≤ i) ∧ ∀ (i : Fin n), labels[↑labels[↑i]] = labels[↑i]

def Hex.PermGroup.Partition.permute {n : Nat} (s : Perm n) (p : Partition n) : Partition n

Move the points of every block, then assign the new least-member labels. The blocks themselves form an unordered family.

Equations

• Hex.PermGroup.Partition.permute s p = Hex.PermGroup.Partition.ofValues (Hex.Vector.ofFn' fun (x : Fin n) => p.labels[↑(s.inv.get x)])

theorem Hex.PermGroup.Partition.permute_same {n : Nat} (s : Perm n) (p : Partition n) (x y : Fin n) : (permute s p).Same x y ↔ p.Same (s.inv.get x) (s.inv.get y)

@[simp]

theorem Hex.PermGroup.Partition.permute_id {n : Nat} (p : Partition n) : permute (Perm.id n) p = p

theorem Hex.PermGroup.Partition.permute_comp {n : Nat} (s t : Perm n) (p : Partition n) : permute (s.comp t) p = permute s (permute t p)

def Hex.PermGroup.Action.partitions {n : Nat} (G : Group n) : Action G (Partition n)

Equations

• Hex.PermGroup.Action.partitions G = { act := fun (p : Hex.PermGroup.Element G) (x : Hex.PermGroup.Partition n) => Hex.PermGroup.Partition.permute p.val x, id_act := ⋯, comp_act := ⋯ }