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

The forward permutation p (old vertex to image) is an isomorphism from G to H: it transports adjacency.

Equations

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

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

Two graphs are isomorphic when some forward permutation transports one onto the other.

Equations

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

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

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

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

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

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

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

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

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

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

theorem Hex.GraphIso.IsIso.graph {n k : Nat} {A B : Colored n k} {p : Perm n} (h : IsIso A B p) : A.graph.IsIso B.graph p

A coloured isomorphism transports the underlying graphs.

theorem Hex.GraphIso.Isomorphic.graph {n k : Nat} {A B : Colored n k} (h : Isomorphic A B) : A.graph.Isomorphic B.graph

Coloured isomorphic graphs are isomorphic.

theorem Hex.GraphIso.Colored.ext_graph {n : Nat} {A B : Colored n 1} (h : A.graph = B.graph) : A = B

At one colour there is nothing to compare but the graph: colour vectors into Fin 1 are constant.

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

Colouring every vertex alike neither adds nor removes isomorphisms: the colour clause of the coloured predicate is vacuous at one colour.

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

The equivalence every uncoloured theorem below is transported along.

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

The canonical form of a graph: the underlying graph of the one-cell coloured canonical form.

Equations

• G.canon h = (Hex.GraphIso.canon (G.singleColor h)).graph

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

The label producing the canonical form.

Equations

• G.label h = Hex.GraphIso.label (G.singleColor h)

def Hex.Graph.findIso {n : Nat} (G H : Graph n) (h : 0 < n := by first | decide | omega) : Option (GraphIso.Perm n)

Find one isomorphism from G to H when one exists.

Equations

• G.findIso H h = Hex.GraphIso.findIso (G.singleColor h) (H.singleColor h)

def Hex.Graph.isIso {n : Nat} (G H : Graph n) (h : 0 < n := by first | decide | omega) : Bool

The Boolean isomorphism decision.

Equations

• G.isIso H h = Hex.GraphIso.isIso (G.singleColor h) (H.singleColor h)

theorem Hex.Graph.relabel_label {n : Nat} (G : Graph n) (h : 0 < n) : G.relabel (G.label h).get = G.canon h

Relabelling by the canonical label produces the canonical form.

theorem Hex.Graph.canon_iso {n : Nat} (G : Graph n) (h : 0 < n) : G.Isomorphic (G.canon h)

Every graph is isomorphic to its canonical form.

theorem Hex.Graph.iso_iff_canon_eq {n : Nat} (G H : Graph n) (h : 0 < n) : G.Isomorphic H ↔ G.canon h = H.canon h

Two graphs are isomorphic exactly when their canonical forms are equal.

theorem Hex.Graph.canon_invariant {n : Nat} {G H : Graph n} (h : 0 < n) (hiso : G.Isomorphic H) : G.canon h = H.canon h

Isomorphic graphs have equal canonical forms.

theorem Hex.Graph.findIso_sound {n : Nat} {G H : Graph n} {p : GraphIso.Perm n} {h : 0 < n} (hp : G.findIso H h = some p) : G.IsIso H p

Soundness of the search: any permutation it returns really is an isomorphism.

theorem Hex.Graph.findIso_isSome_iff {n : Nat} (G H : Graph n) (h : 0 < n) : (G.findIso H h).isSome = true ↔ G.Isomorphic H

Completeness of the search: it returns a permutation exactly when one exists.

theorem Hex.Graph.isIso_eq_true_iff {n : Nat} (G H : Graph n) (h : 0 < n) : G.isIso H h = true ↔ G.Isomorphic H

The decision answers true exactly on isomorphic pairs.

theorem Hex.Graph.isIso_eq_false_iff {n : Nat} (G H : Graph n) (h : 0 < n) : G.isIso H h = false ↔ ¬G.Isomorphic H

The decision answers false exactly on non-isomorphic pairs.

theorem Hex.Graph.isomorphic_of_isIso {n : Nat} {G H : Graph n} {h : 0 < n} (hi : G.isIso H h = true) : G.Isomorphic H

A positive answer proves isomorphism.

def Hex.Graph.SameOrbit {n : Nat} (G : Graph n) (u v : Fin n) : Prop

Two vertices lie in one orbit of the automorphism group.

Equations

• G.SameOrbit u v = ∃ (p : Hex.GraphIso.Perm n), G.IsIso G p ∧ p.get u = v

theorem Hex.Graph.sameOrbit_singleColor_iff {n : Nat} (G : Graph n) (u v : Fin n) (h : 0 < n) : GraphIso.SameOrbit (G.singleColor h) u v ↔ G.SameOrbit u v

The one-cell view carries the orbit relation both ways: at one colour the coloured and uncoloured automorphism groups coincide.

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

Generators of the automorphism group of a graph, with the vertex orbits, the orbit count and the orbit-stabilizer product for the group order, with the guarantees of the coloured Hex.GraphIso.autos.

Equations

• G.autos h = Hex.GraphIso.autos (G.singleColor h)

theorem Hex.Graph.autos_isIso {n : Nat} {G : Graph n} {h : 0 < n} {p : GraphIso.Perm n} (hp : p ∈ (G.autos h).gens) : G.IsIso G p

Membership: every returned generator is an automorphism.

theorem Hex.Graph.size_autos_orbits {n : Nat} (G : Graph n) (h : 0 < n) : (G.autos h).orbits.size = n

The orbit array has one entry per vertex.

theorem Hex.Graph.autos_orbits_lt {n : Nat} (G : Graph n) (h : 0 < n) {v : Nat} (hv : v < n) : (G.autos h).orbits[v]! < n

Every orbit representative is a vertex.

theorem Hex.Graph.autos_sameOrbit_of_eq {n : Nat} (G : Graph n) (h : 0 < n) (u v : Fin n) (hu : (G.autos h).orbits[↑u]! = (G.autos h).orbits[↑v]!) : G.SameOrbit u v

Vertices sharing a reported representative lie in the same orbit.