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

Isomorphism of bare sparse graphs, in the forward permutation direction.

Equations

• G.IsIso H p = ∀ (i j : Fin n), H.adj (p.get i) (p.get j) = G.adj i j

def Hex.SparseGraph.Isomorphic {n : Nat} (G H : SparseGraph n) : Prop

Equations

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

theorem Hex.SparseGraph.IsIso.refl {n : Nat} (G : SparseGraph n) : G.IsIso G (Perm.id n)

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

theorem Hex.SparseGraph.IsIso.trans {n : Nat} {G H K : SparseGraph n} {p q : Perm n} (h : G.IsIso H p) (h' : H.IsIso K q) : G.IsIso K (q.comp p)

theorem Hex.SparseGraph.Isomorphic.refl {n : Nat} (G : SparseGraph n) : G.Isomorphic G

theorem Hex.SparseGraph.Isomorphic.symm {n : Nat} {G H : SparseGraph n} (h : G.Isomorphic H) : H.Isomorphic G

theorem Hex.SparseGraph.Isomorphic.trans {n : Nat} {G H K : SparseGraph n} (h : G.Isomorphic H) (h' : H.Isomorphic K) : G.Isomorphic K

theorem Hex.SparseGraph.isIso_iff_relabel {n : Nat} (G H : SparseGraph n) (p : Perm n) : G.IsIso H p ↔ G.relabel p.inv = H

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

Verify a supplied transporter without adding a colour or a dense matrix. This also covers the empty graph, where the colour count is zero.

Equations

• G.checkIso H p = (G.relabel p.inv == H)

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

@[instance_reducible]

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

Equations

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

def Hex.SparseGraph.singleColor {n : Nat} (G : SparseGraph n) (h : 0 < n) : GraphIso.Sparse.Colored n 1

Equations

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

theorem Hex.SparseGraph.isIso_singleColor_iff {n : Nat} (G H : SparseGraph n) (p : Perm n) (h : 0 < n) : GraphIso.Sparse.IsIso (G.singleColor h) (H.singleColor h) p ↔ G.IsIso H p

theorem Hex.SparseGraph.isomorphic_singleColor_iff {n : Nat} (G H : SparseGraph n) (h : 0 < n) : GraphIso.Sparse.Isomorphic (G.singleColor h) (H.singleColor h) ↔ G.Isomorphic H