structure Hex.GraphIso.Coloring (n k : Nat) : Type

An ordered vertex colouring of Fin n by colours Fin k in which every colour is used.

• cells : Vector (Fin k) n

  The colour of each vertex.

• onto : Function.Surjective self.cells.get

  Every colour is used.

theorem Hex.Vector.get_eq_getElem {α : Type u} {m : Nat} (v : Vector α m) (i : Fin m) : v.get i = v[i]

Vector.get agrees with element access. The Lean standard library states its Vector lemmas about getElem rather than about Vector.get, so uses of the onto field rewrite with this equation first.

theorem Hex.GraphIso.Coloring.ext_cells {n k : Nat} {c d : Coloring n k} (h : c.cells = d.cells) : c = d

theorem Hex.GraphIso.Coloring.ext {n k : Nat} {c d : Coloring n k} (h : ∀ (i : Fin n), c.cells[i] = d.cells[i]) : c = d

theorem Hex.GraphIso.Coloring.ext_iff {n k : Nat} {c d : Coloring n k} : c = d ↔ ∀ (i : Fin n), c.cells[i] = d.cells[i]

@[instance_reducible]

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

Equations

• c.instDecidableEq d = if h : c.cells = d.cells then isTrue ⋯ else isFalse ⋯

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

Checked construction: accepts exactly the colour vectors using every colour.

Equations

• Hex.GraphIso.Coloring.ofVector? v = if h : ∀ (c : Fin k), ∃ (i : Fin n), v.get i = c then some { cells := v, onto := ⋯ } else none

theorem Hex.GraphIso.Coloring.isSome_ofVector? {n k : Nat} (v : Vector (Fin k) n) : (ofVector? v).isSome = true ↔ ∀ (c : Fin k), ∃ (i : Fin n), v.get i = c

def Hex.GraphIso.Coloring.trivial (n : Nat) (h : 0 < n := by first | decide | omega) : Coloring n 1

The constant zero colouring: the one-cell colouring of a nonempty vertex set.

Equations

• Hex.GraphIso.Coloring.trivial n h = { cells := Hex.Vector.ofFn' fun (x : Fin n) => 0, onto := ⋯ }

@[simp]

theorem Hex.GraphIso.Coloring.cells_eq_zero {n : Nat} (c : Coloring n 1) {i : Nat} (hi : i < n) : c.cells[i] = 0

Colour vectors into Fin 1 are constant, so a one-cell colouring carries no information beyond its existence.

def Hex.GraphIso.Coloring.mod (n k : Nat) (hk : 0 < k := by first | decide | omega) (hkn : k ≤ n := by first | decide | omega) : Coloring n k

The colouring i ↦ i % k, onto whenever k ≤ n.

Equations

• Hex.GraphIso.Coloring.mod n k hk hkn = { cells := Hex.Vector.ofFn' fun (i : Fin n) => ⟨↑i % k, ⋯⟩, onto := ⋯ }

def Hex.GraphIso.Coloring.cellSizes {n k : Nat} (c : Coloring n k) : Vector Nat k

The number of vertices with each colour.

Equations

• c.cellSizes = Hex.Vector.ofFn' fun (j : Fin k) => (List.filter (fun (i : Fin n) => c.cells[i] == j) (List.finRange n)).length

structure Hex.GraphIso.Colored (n k : Nat) : Type

A coloured graph: a simple undirected graph on Fin n together with an ordered onto colouring by Fin k.

• graph : Graph n

  The underlying simple graph.

• coloring : Coloring n k

  The ordered vertex colouring.

@[instance_reducible]

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

Equations

• G.instDecidableEq H = if h : G.graph = H.graph ∧ G.coloring = H.coloring then isTrue ⋯ else isFalse ⋯

theorem Hex.GraphIso.Colored.ext {n k : Nat} {G H : Colored n k} (hg : ∀ (i j : Fin n), G.graph.adj i j = H.graph.adj i j) (hc : ∀ (i : Fin n), G.coloring.cells[i] = H.coloring.cells[i]) : G = H

theorem Hex.GraphIso.Colored.ext_iff {n k : Nat} {G H : Colored n k} : G = H ↔ (∀ (i j : Fin n), G.graph.adj i j = H.graph.adj i j) ∧ ∀ (i : Fin n), G.coloring.cells[i] = H.coloring.cells[i]

def Hex.GraphIso.Colored.relabel {n k : Nat} (G : Colored n k) (l : Label n) : Colored n k

Relabel a coloured graph by a labelling l: new vertex i is old vertex l[i], so (relabel G l).graph.adj i j = G.graph.adj l[i] l[j] and (relabel G l).coloring.cells[i] = G.coloring.cells[l[i]].

Equations

• G.relabel l = { graph := G.graph.relabel fun (i : Fin n) => l.get i, coloring := { cells := Hex.Vector.ofFn' fun (i : Fin n) => G.coloring.cells[l.get i], onto := ⋯ } }

@[simp]

theorem Hex.GraphIso.Colored.adj_relabel {n k : Nat} (G : Colored n k) (l : Label n) (i j : Fin n) : (G.relabel l).graph.adj i j = G.graph.adj (l.get i) (l.get j)

@[simp]

theorem Hex.GraphIso.Colored.cells_relabel {n k : Nat} (G : Colored n k) (l : Label n) (i : Nat) (hi : i < n) : (G.relabel l).coloring.cells[i] = G.coloring.cells[l.get ⟨i, hi⟩]

@[simp]

theorem Hex.GraphIso.Colored.relabel_id {n k : Nat} (G : Colored n k) : G.relabel (Label.id n) = G

theorem Hex.GraphIso.Colored.relabel_relabel {n k : Nat} (G : Colored n k) (l m : Label n) : (G.relabel l).relabel m = G.relabel (l.comp m)

def Hex.Graph.singleColor {n : Nat} (G : Graph n) (h : 0 < n := by first | decide | omega) : GraphIso.Colored n 1

The one-cell coloured graph of a bare graph: every vertex takes the single colour zero, so a coloured isomorphism is exactly a graph isomorphism. n = 0 would force k = 0, so this is defined for positive n.

Equations

• G.singleColor h = { graph := G, coloring := Hex.GraphIso.Coloring.trivial n h }

@[simp]

theorem Hex.Graph.graph_singleColor {n : Nat} (G : Graph n) (h : 0 < n) : (G.singleColor h).graph = G

structure Hex.GraphIso.CanonResult (n k : Nat) : Type

A canonical form and the label producing it, kept together.

• form : Colored n k

  The canonical coloured graph.

• label : Label n

  The label producing the canonical form: form = G.relabel label.

def Hex.GraphIso.instDecidableEqCanonResult.decEq {n✝ k✝ : Nat} (x✝ x✝¹ : CanonResult n✝ k✝) : Decidable (x✝ = x✝¹)

Equations

• Hex.GraphIso.instDecidableEqCanonResult.decEq { form := a, label := a_1 } { form := b, label := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Hex.GraphIso.instDecidableEqCanonResult {n✝ k✝ : Nat} : DecidableEq (CanonResult n✝ k✝)

Equations

• Hex.GraphIso.instDecidableEqCanonResult = Hex.GraphIso.instDecidableEqCanonResult.decEq

def Hex.GraphIso.ColorSorted {n k : Nat} (K : Colored n k) : Prop

A coloured graph whose colour classes are contiguous in vertex order: the first cell occupies the least vertices, and so on. Every canonical form satisfies this.

Equations

• Hex.GraphIso.ColorSorted K = ∀ (i j : Fin n), i ≤ j → K.coloring.cells[i] ≤ K.coloring.cells[j]

def Hex.GraphIso.colorSortedCheck {n k : Nat} (K : Colored n k) : Bool

Executable check for ColorSorted, a plain Boolean fold so the kernel replays it without unfolding quantifier instances.

Equations

• Hex.GraphIso.colorSortedCheck K = (List.finRange n).all fun (i : Fin n) => (List.finRange n).all fun (j : Fin n) => !decide (i ≤ j) || decide (K.coloring.cells[i] ≤ K.coloring.cells[j])

theorem Hex.GraphIso.colorSortedCheck_iff {n k : Nat} (K : Colored n k) : colorSortedCheck K = true ↔ ColorSorted K

@[instance_reducible]

instance Hex.GraphIso.instDecidableColorSorted {n k : Nat} (K : Colored n k) : Decidable (ColorSorted K)

Equations

• Hex.GraphIso.instDecidableColorSorted K = if h : Hex.GraphIso.colorSortedCheck K = true then isTrue ⋯ else isFalse ⋯