def Hex.GraphIso.Perm.toEquiv {n : ℕ} (p : Perm n) : Fin n ≃ Fin n

The equivalence of Fin n given by a forward permutation: p.get one way, p.inv.get the other.

Equations

• p.toEquiv = { toFun := p.get, invFun := p.inv.get, left_inv := ⋯, right_inv := ⋯ }

@[simp]

theorem Hex.GraphIso.Perm.toEquiv_apply {n : ℕ} (p : Perm n) (i : Fin n) : p.toEquiv i = p.get i

def Hex.GraphIso.Perm.ofEquiv {n : ℕ} (e : Fin n ≃ Fin n) : Perm n

The forward permutation with the same action as an equivalence of Fin n.

Equations

• Hex.GraphIso.Perm.ofEquiv e = Hex.GraphIso.Perm.ofFn ⇑e ⋯ ⋯

@[simp]

theorem Hex.GraphIso.Perm.get_ofEquiv {n : ℕ} (e : Fin n ≃ Fin n) (i : Fin n) : (ofEquiv e).get i = e i

def Hex.GraphIso.Mathlib.encode {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : GraphIso.Colored n k

The executable image of a coloured Mathlib graph along a chosen finite enumeration.

Equations

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

theorem Hex.GraphIso.Mathlib.encode_adj {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (v w : V) : (encode e G).graph.adj (e v) (e w) = true ↔ G.graph.Adj v w

theorem Hex.GraphIso.Mathlib.encode_adj' {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (i j : Fin n) : (encode e G).graph.adj i j = true ↔ G.graph.Adj (e.symm i) (e.symm j)

The general-index form of encode_adj.

theorem Hex.GraphIso.Mathlib.encode_color {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (v : V) : (encode e G).coloring.cells[e v] = G.color v

theorem Hex.GraphIso.Mathlib.encode_color' {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (i : Fin n) : (encode e G).coloring.cells[i] = G.color (e.symm i)

The general-index form of encode_color.

def Hex.GraphIso.Mathlib.decodePerm {V : Type u} {W : Type v} {n : ℕ} (eV : V ≃ Fin n) (eW : W ≃ Fin n) (p : Perm n) : V ≃ W

Decode an executable forward permutation into an equivalence of the two vertex types, conjugating by the chosen enumerations.

Equations

• Hex.GraphIso.Mathlib.decodePerm eV eW p = eV.trans (p.toEquiv.trans eW.symm)

@[simp]

theorem Hex.GraphIso.Mathlib.decodePerm_apply {V : Type u} {W : Type v} {n : ℕ} (eV : V ≃ Fin n) (eW : W ≃ Fin n) (p : Perm n) (v : V) : (decodePerm eV eW p) v = eW.symm (p.get (eV v))

def Hex.GraphIso.Mathlib.isoOfIsIso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k n : ℕ} {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 : IsIso (encode eV G) (encode eW H) p) : G.Iso H

Decode a checked executable transporter into a colour-preserving isomorphism of the Mathlib graphs.

Equations

• Hex.GraphIso.Mathlib.isoOfIsIso eV eW h = { graphIso := let __Equiv := Hex.GraphIso.Mathlib.decodePerm eV eW p; { toEquiv := __Equiv, map_rel_iff' := ⋯ }, map_color := ⋯ }

theorem Hex.GraphIso.Mathlib.isIso_of_iso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k n : ℕ} {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (eV : V ≃ Fin n) (eW : W ≃ Fin n) (h : G.Iso H) : IsIso (encode eV G) (encode eW H) (Perm.ofEquiv (eV.symm.trans (h.graphIso.trans eW)))

Every colour-preserving Mathlib isomorphism encodes to an executable colour-preserving forward permutation.

theorem Hex.GraphIso.Mathlib.encode_iso_iff {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k n : ℕ} {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 ↔ Isomorphic (encode eV G) (encode eW H)

The finite encoding preserves the isomorphism verdict, for any choice of enumerations.

theorem Hex.GraphIso.Mathlib.colored_iso_iff_canon_eq {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k n : ℕ} {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 ↔ canon (encode eV G) = canon (encode eW H)

Two coloured Mathlib graphs are isomorphic exactly when their encodings have equal canonical forms. The right-hand side is a decidable equality of executable values, so this reduces a Mathlib isomorphism question to running the canonical labelling.

def Hex.GraphIso.Mathlib.autos {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : List (G.Iso G)

The automorphism generators found by Hex.GraphIso.Aut.gens on the encoding, decoded as colour-preserving self-isomorphisms of the Mathlib graph. Each entry is an automorphism, by Hex.GraphIso.Aut.gens_isIso and isoOfIsIso. autos_complete proves that this list generates the full automorphism group.

Equations

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

def Hex.GraphIso.Mathlib.autOrder {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : ℕ

The full colour-preserving automorphism group order, computed by Hex.GraphIso.Aut.order on the encoding. autOrder_card proves its equality with the group's cardinality.

Equations

• Hex.GraphIso.Mathlib.autOrder e G = Hex.GraphIso.Aut.order (Hex.GraphIso.Mathlib.encode e G)

def Hex.GraphIso.Mathlib.autNumOrbits {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] : ℕ

The number of vertex orbits reported by Hex.GraphIso.Aut.numOrbits on the encoding. autNumOrbits_card identifies it with the cardinality of the full automorphism orbit quotient.

Equations

• Hex.GraphIso.Mathlib.autNumOrbits e G = Hex.GraphIso.Aut.numOrbits (Hex.GraphIso.Mathlib.encode e G)

theorem Hex.GraphIso.Mathlib.sameOrbit_of_autos {V : Type u} [Fintype V] {k n : ℕ} (e : V ≃ Fin n) (G : Colored V k) [DecidableRel G.graph.Adj] (v w : V) (h : (Aut.orbits (encode e G))[↑(e v)]! = (Aut.orbits (encode e G))[↑(e w)]!) : ∃ (f : G.Iso G), f.graphIso v = w

Vertices the reported orbit array puts together are carried onto each other by a colour-preserving automorphism.

theorem Hex.GraphIso.Mathlib.isEmpty_iso_of_card_ne {V : Type u} {W : Type v} [Fintype V] [Fintype W] (G : SimpleGraph V) (H : SimpleGraph W) (h : Fintype.card V ≠ Fintype.card W) : IsEmpty (G ≃g H)

Unequal vertex cardinalities forbid any graph isomorphism.

theorem Hex.GraphIso.Mathlib.card_color_class_eq {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k : ℕ} {G : Colored V k} {H : Colored W k} (h : G.Iso H) (c : Fin k) [DecidableEq (Fin k)] : Fintype.card { v : V // G.color v = c } = Fintype.card { w : W // H.color w = c }

A colour-preserving isomorphism induces equal colour-class cardinalities.

theorem Hex.GraphIso.Mathlib.not_isomorphic_of_card_color_ne {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k : ℕ} {G : Colored V k} {H : Colored W k} [DecidableEq (Fin k)] {c : Fin k} (h : Fintype.card { v : V // G.color v = c } ≠ Fintype.card { w : W // H.color w = c }) : ¬G.Isomorphic H

Unequal ordered cell sizes forbid coloured isomorphism.