structure Hex.GraphIso.Label (n : Nat) : Type

A canonical-labelling result array in nauty's canonlab convention: l[i] is the old vertex placed at new position i. The underlying data is the same duplicate-free complete vertex array as Perm. The wrapper marks the direction.

• perm : Perm n

  The underlying bijection sending each new position to the old vertex placed there.

@[instance_reducible]

instance Hex.GraphIso.Label.instDecidableEq {n : Nat} : DecidableEq (Label n)

Equations

• l.instDecidableEq m = if h : l.perm = m.perm then isTrue ⋯ else isFalse ⋯

@[inline]

def Hex.GraphIso.Label.get {n : Nat} (l : Label n) (i : Fin n) : Fin n

The old vertex at new position i.

Equations

• l.get i = l.perm.get i

@[instance_reducible]

instance Hex.GraphIso.Label.instGetElemFinTrue {n : Nat} : GetElem (Label n) (Fin n) (Fin n) fun (x : Label n) (x_1 : Fin n) => True

Equations

• Hex.GraphIso.Label.instGetElemFinTrue = { getElem := fun (l : Hex.GraphIso.Label n) (i : Fin n) (x : True) => l.get i }

@[simp]

theorem Hex.GraphIso.Label.getElem_eq_get {n : Nat} (l : Label n) (i : Fin n) : l[i] = l.get i

theorem Hex.GraphIso.Label.ext {n : Nat} {l m : Label n} (h : ∀ (i : Fin n), l.get i = m.get i) : l = m

theorem Hex.GraphIso.Label.ext_iff {n : Nat} {l m : Label n} : l = m ↔ ∀ (i : Fin n), l.get i = m.get i

def Hex.GraphIso.Label.ofVector? {n : Nat} (v : Vector (Fin n) n) : Option (Label n)

Checked construction from a vertex array.

Equations

• Hex.GraphIso.Label.ofVector? v = Option.map Hex.GraphIso.Label.mk (Hex.Perm.ofVector? v)

def Hex.GraphIso.Label.id (n : Nat) : Label n

The identity labelling.

Equations

• Hex.GraphIso.Label.id n = { perm := Hex.Perm.id n }

@[simp]

theorem Hex.GraphIso.Label.get_id {n : Nat} (i : Fin n) : (Label.id n).get i = i

def Hex.GraphIso.Label.comp {n : Nat} (l m : Label n) : Label n

Sequential composition: relabelling by l and then by m is relabelling by l.comp m, with (l.comp m).get i = l.get (m.get i).

Equations

• l.comp m = { perm := l.perm.comp m.perm }

@[simp]

theorem Hex.GraphIso.Label.get_comp {n : Nat} (l m : Label n) (i : Fin n) : (l.comp m).get i = l.get (m.get i)

def Hex.GraphIso.Label.toPerm {n : Nat} (l : Label n) : Perm n

The forward permutation of a labelling: old vertex v moves to the new position where l placed it.

Equations

• l.toPerm = l.perm.inv

@[simp]

theorem Hex.GraphIso.Label.get_toPerm_get {n : Nat} (l : Label n) (i : Fin n) : l.get (l.toPerm.get i) = i

@[simp]

theorem Hex.GraphIso.Label.toPerm_get_get {n : Nat} (l : Label n) (i : Fin n) : l.toPerm.get (l.get i) = i

def Hex.GraphIso.Label.ofArray? (n : Nat) (lab : Array Nat) : Option (Label n)

Checked construction from a raw array of vertex numbers: none unless the array has length n, entries below n, and describes a permutation.

Equations

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

theorem Hex.GraphIso.Label.ofVector?_perm_vec {n : Nat} {v : Vector (Fin n) n} {l : Label n} (h : ofVector? v = some l) : l.perm.vec = v

theorem Hex.GraphIso.Label.ofArray?_bounds {n : Nat} {lab : Array Nat} {l : Label n} (h : ofArray? n lab = some l) : lab.size = n ∧ ∀ (v : Nat), v ∈ lab → v < n

theorem Hex.GraphIso.Label.ofArray?_get {n : Nat} {lab : Array Nat} {l : Label n} (h : ofArray? n lab = some l) (i : Nat) (hi : i < n) : ↑(l.get ⟨i, hi⟩) = lab[i]!

A checked labelling reads back the raw array entrywise.

def Hex.Perm.toLabel {n : Nat} (p : Perm n) : GraphIso.Label n

The labelling of a forward permutation: new position i holds the old vertex mapped to i.

Equations

• p.toLabel = { perm := p.inv }

@[simp]

theorem Hex.Perm.get_toLabel {n : Nat} (p : Perm n) (i : Fin n) : p.toLabel.get i = p.inv.get i

@[simp]

theorem Hex.Perm.toLabel_toPerm {n : Nat} (p : Perm n) : p.toLabel.toPerm = p

@[simp]

theorem Hex.Perm.toPerm_toLabel {n : Nat} (l : GraphIso.Label n) : l.toPerm.toLabel = l