def Hex.GraphIso.IsIso {n k : Nat} (G H : Colored n k) (p : Perm n) : Prop

The forward permutation p is an isomorphism from G to H: it preserves each ordered colour index and transports adjacency.

Equations

• Hex.GraphIso.IsIso G H p = ((∀ (i : Fin n), H.coloring.cells[p.get i] = G.coloring.cells[i]) ∧ ∀ (i j : Fin n), H.graph.adj (p.get i) (p.get j) = G.graph.adj i j)

def Hex.GraphIso.checkIso {n k : Nat} (G H : Colored n k) (p : Perm n) : Bool

Executable isomorphism check, sound and complete for IsIso (checkIso_iff). A plain Boolean fold so the kernel replays it without unfolding Decidable instances.

Equations

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

theorem Hex.GraphIso.checkIso_iff {n k : Nat} (G H : Colored n k) (p : Perm n) : checkIso G H p = true ↔ IsIso G H p

theorem Hex.GraphIso.IsIso.mk {n k : Nat} {G H : Colored n k} {p : Perm n} (hc : ∀ (i : Fin n), H.coloring.cells[p.get i] = G.coloring.cells[i]) (ha : ∀ (i j : Fin n), H.graph.adj (p.get i) (p.get j) = G.graph.adj i j) : IsIso G H p

Introduce IsIso from its two clauses. The definition is not exposed across module boundaries, so consumers use this.

@[instance_reducible]

instance Hex.GraphIso.instDecidableIsIso {n k : Nat} (G H : Colored n k) (p : Perm n) : Decidable (IsIso G H p)

Equations

• Hex.GraphIso.instDecidableIsIso G H p = if h : Hex.GraphIso.checkIso G H p = true then isTrue ⋯ else isFalse ⋯

def Hex.GraphIso.Isomorphic {n k : Nat} (G H : Colored n k) : Prop

Two coloured graphs are isomorphic when some colour-preserving forward permutation transports one onto the other.

Equations

• Hex.GraphIso.Isomorphic G H = ∃ (p : Hex.GraphIso.Perm n), Hex.GraphIso.IsIso G H p

theorem Hex.GraphIso.Isomorphic.intro {n k : Nat} {G H : Colored n k} (p : Perm n) (h : IsIso G H p) : Isomorphic G H

theorem Hex.GraphIso.Isomorphic.elim {n k : Nat} {G H : Colored n k} (h : Isomorphic G H) : ∃ (p : Perm n), IsIso G H p

theorem Hex.GraphIso.IsIso.intro {n k : Nat} {G H : Colored n k} {p : Perm n} (h1 : ∀ (i : Fin n), H.coloring.cells[p.get i] = G.coloring.cells[i]) (h2 : ∀ (i j : Fin n), H.graph.adj (p.get i) (p.get j) = G.graph.adj i j) : IsIso G H p

theorem Hex.GraphIso.IsIso.cells_eq {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) (i : Fin n) : H.coloring.cells[p.get i] = G.coloring.cells[i]

theorem Hex.GraphIso.IsIso.adj_eq {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) (i j : Fin n) : H.graph.adj (p.get i) (p.get j) = G.graph.adj i j

theorem Hex.GraphIso.IsIso.refl {n k : Nat} (G : Colored n k) : IsIso G G (Perm.id n)

theorem Hex.GraphIso.IsIso.symm {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) : IsIso H G p.inv

theorem Hex.GraphIso.IsIso.trans {n k : Nat} {G H K : Colored n k} {p q : Perm n} (hGH : IsIso G H p) (hHK : IsIso H K q) : IsIso G K (q.comp p)

theorem Hex.GraphIso.Isomorphic.refl {n k : Nat} (G : Colored n k) : Isomorphic G G

theorem Hex.GraphIso.Isomorphic.symm {n k : Nat} {G H : Colored n k} (h : Isomorphic G H) : Isomorphic H G

theorem Hex.GraphIso.Isomorphic.trans {n k : Nat} {G H K : Colored n k} (hGH : Isomorphic G H) (hHK : Isomorphic H K) : Isomorphic G K

theorem Hex.GraphIso.isIso_relabel {n k : Nat} (G : Colored n k) (l : Label n) : IsIso G (G.relabel l) l.toPerm

Relabelling produces an isomorphic coloured graph, transported by the forward permutation of the labelling.

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

theorem Hex.GraphIso.relabel_eq_of_isIso {n k : Nat} {G H : Colored n k} {p : Perm n} (h : IsIso G H p) : G.relabel p.toLabel = H

Every isomorphism arises from a labelling: transporting along p relabels by p.toLabel.

theorem Hex.GraphIso.isomorphic_iff_exists_relabel {n k : Nat} {G H : Colored n k} : Isomorphic G H ↔ ∃ (l : Label n), G.relabel l = H

Two coloured graphs are isomorphic exactly when one is a relabelling of the other.