theorem Hex.GraphIso.Mathlib.Sparse.iso_iff_canon_eq {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) : G.Isomorphic H ↔ Sparse.canon (encode eV G) = Sparse.canon (encode eW H)

Equality of native sparse canonical forms characterizes Mathlib coloured graph isomorphism for any two finite enumerations.

theorem Hex.GraphIso.Mathlib.Sparse.canon_encode_eq {V : Type u} [Fintype V] {n k : ℕ} {G : Colored V k} [DecidableRel G.graph.Adj] (e e' : V ≃ Fin n) : Sparse.canon (encode e G) = Sparse.canon (encode e' G)

Changing the finite enumeration does not change the canonical form computed by the actual sparse search. This includes the empty graph.

theorem Hex.GraphIso.Mathlib.Sparse.isIso_iff {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) : Sparse.isIso (encode eV G) (encode eW H) = true ↔ G.Isomorphic H

The executable sparse decision is a complete Mathlib isomorphism test.

theorem Hex.GraphIso.Mathlib.Sparse.findIso_eq_none_iff {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) : Sparse.findIso (encode eV G) (encode eW H) = none ↔ ¬G.Isomorphic H

def Hex.GraphIso.Mathlib.Sparse.isoOfFindIso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) {p : Perm n} (h : Sparse.findIso (encode eV G) (encode eW H) = some p) : G.Iso H

Decode the transporter returned by the total native sparse search.

Equations

• Hex.GraphIso.Mathlib.Sparse.isoOfFindIso eV eW h = Hex.GraphIso.Mathlib.Sparse.isoOfIsIso eV eW ⋯