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

A forward permutation preserving adjacency and each ordered colour.

Equations

• Hex.GraphIso.Sparse.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)

theorem Hex.GraphIso.Sparse.isIso_toDense {n k : Nat} (G H : Colored n k) (p : Perm n) : GraphIso.IsIso G.toDense H.toDense p ↔ IsIso G H p

Explicit dense conversion preserves the isomorphism relation.

theorem Hex.GraphIso.Sparse.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

theorem Hex.GraphIso.Sparse.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.Sparse.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.Sparse.IsIso.refl {n k : Nat} (G : Colored n k) : IsIso G G (Perm.id n)

theorem Hex.GraphIso.Sparse.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.Sparse.IsIso.trans {n k : Nat} {G H K : Colored n k} {p q : Perm n} (hp : IsIso G H p) (hq : IsIso H K q) : IsIso G K (q.comp p)

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

Two sparse coloured graphs are isomorphic if a transporter exists.

Equations

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

theorem Hex.GraphIso.Sparse.isomorphic_toDense {n k : Nat} (G H : Colored n k) : GraphIso.Isomorphic G.toDense H.toDense ↔ Isomorphic G H

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

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

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

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

theorem Hex.GraphIso.Sparse.Isomorphic.trans {n k : Nat} {G H K : Colored n k} (h : Isomorphic G H) (h' : Isomorphic H K) : Isomorphic G K

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

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

theorem Hex.GraphIso.Sparse.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

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

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

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

Check a given transporter by native sparse relabelling and equality. This operation constructs no dense adjacency matrix and does no search.

Equations

• Hex.GraphIso.Sparse.checkIso G H p = (G.relabel p.toLabel == H)

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

@[instance_reducible]

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

Equations

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