def Hex.GraphIso.Mathlib.listEquiv {V : Type u} [Fintype V] [DecidableEq V] (l : List V) (hlen : l.length = Fintype.card V) (hnodup : l.Nodup) (hcompl : ∀ (v : V), v ∈ l) : V ≃ Fin (Fintype.card V)

The enumeration equivalence induced by a duplicate-free list of all the vertices: v maps to its position in the list. Both directions are structural list operations, so a ground instance reduces in the kernel. The tactic obtains the list by reducing Finset.univ.val, and proves the three side conditions by decide.

Equations

• Hex.GraphIso.Mathlib.listEquiv l hlen hnodup hcompl = { toFun := fun (v : V) => ⟨List.idxOf v l, ⋯⟩, invFun := fun (i : Fin (Fintype.card V)) => l[↑i], left_inv := ⋯, right_inv := ⋯ }

def Hex.GraphIso.Mathlib.onecell {V : Type u} [Fintype V] (G : SimpleGraph V) (h : 0 < Fintype.card V) : Colored V 1

The colouring of an uncoloured graph over a nonempty vertex type that gives every vertex colour 0. A G ≃g H goal is encoded through this colouring, since a one-cell colouring constrains nothing.

Equations

• Hex.GraphIso.Mathlib.onecell G h = { graph := G, color := fun (x : V) => 0, onto := ⋯ }

@[instance_reducible]

instance Hex.GraphIso.Mathlib.instDecidableRelAdjGraphOnecell {V : Type u} [Fintype V] {G : SimpleGraph V} [DecidableRel G.Adj] (h : 0 < Fintype.card V) : DecidableRel (onecell G h).graph.Adj

Equations

• Hex.GraphIso.Mathlib.instDecidableRelAdjGraphOnecell h = Hex.GraphIso.Mathlib.instDecidableRelAdjGraphOnecell._aux_1 h

theorem Hex.GraphIso.Mathlib.onecell_isomorphic_iff {V : Type u} {W : Type v} [Fintype V] [Fintype W] {G : SimpleGraph V} {H : SimpleGraph W} (hV : 0 < Fintype.card V) (hW : 0 < Fintype.card W) : (onecell G hV).Isomorphic (onecell H hW) ↔ Nonempty (G ≃g H)

One-cell colourings are isomorphic exactly when the graphs are.

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

The coloured isomorphism a kernel-checked transporter of the encodings yields.

Equations

• Hex.GraphIso.Mathlib.coloredIsoOfIsIso eV eW p h = Hex.GraphIso.Mathlib.isoOfIsIso eV eW h

def Hex.GraphIso.Mathlib.graphIsoOfIsIso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n : ℕ} (eV : V ≃ Fin n) (eW : W ≃ Fin n) {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj] (hV : 0 < Fintype.card V) (hW : 0 < Fintype.card W) (p : Perm n) (h : IsIso (encode eV (onecell G hV)) (encode eW (onecell H hW)) p) : G ≃g H

The graph isomorphism a kernel-checked transporter of the one-cell encodings yields.

Equations

• Hex.GraphIso.Mathlib.graphIsoOfIsIso eV eW hV hW p h = (Hex.GraphIso.Mathlib.coloredIsoOfIsIso eV eW p h).graphIso

def Hex.GraphIso.Mathlib.isoOfCardZero {V : Type u} {W : Type v} [Fintype V] [Fintype W] (G : SimpleGraph V) (H : SimpleGraph W) (hV : Fintype.card V = 0) (hW : Fintype.card W = 0) : G ≃g H

Two graphs on empty vertex types are isomorphic.

Equations

• Hex.GraphIso.Mathlib.isoOfCardZero G H hV hW = { toEquiv := Equiv.equivOfIsEmpty V W, map_rel_iff' := ⋯ }

def Hex.GraphIso.Mathlib.coloredIsoOfCardZero {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k : ℕ} (G : Colored V k) (H : Colored W k) (hV : Fintype.card V = 0) (hW : Fintype.card W = 0) : G.Iso H

Two coloured graphs on empty vertex types are isomorphic.

Equations

• Hex.GraphIso.Mathlib.coloredIsoOfCardZero G H hV hW = { graphIso := Hex.GraphIso.Mathlib.isoOfCardZero G.graph H.graph hV hW, map_color := ⋯ }

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

Non-isomorphism of the encodings refutes coloured isomorphism. The hypothesis is stated about Hex.GraphIso.Isomorphic, so it accepts a negative proof from either the root-separator route or the certificate-replay route.

theorem Hex.GraphIso.Mathlib.isEmpty_coloredIso_of_not_encode_iso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k n : ℕ} (eV : V ≃ Fin n) (eW : W ≃ Fin n) {G : Colored V k} {H : Colored W k} [DecidableRel G.graph.Adj] [DecidableRel H.graph.Adj] (h : ¬Isomorphic (encode eV G) (encode eW H)) : IsEmpty (G.Iso H)

theorem Hex.GraphIso.Mathlib.isEmpty_iso_of_not_encode_iso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n : ℕ} (eV : V ≃ Fin n) (eW : W ≃ Fin n) {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj] (hV : 0 < Fintype.card V) (hW : 0 < Fintype.card W) (h : ¬Isomorphic (encode eV (onecell G hV)) (encode eW (onecell H hW))) : IsEmpty (G ≃g H)

theorem Hex.GraphIso.Mathlib.not_nonempty_iso_of_not_encode_iso {V : Type u} {W : Type v} [Fintype V] [Fintype W] {n : ℕ} (eV : V ≃ Fin n) (eW : W ≃ Fin n) {G : SimpleGraph V} {H : SimpleGraph W} [DecidableRel G.Adj] [DecidableRel H.Adj] (hV : 0 < Fintype.card V) (hW : 0 < Fintype.card W) (h : ¬Isomorphic (encode eV (onecell G hV)) (encode eW (onecell H hW))) : ¬Nonempty (G ≃g H)

theorem Hex.GraphIso.Mathlib.not_nonempty_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) : ¬Nonempty (G ≃g H)

Unequal cardinalities refute nonemptiness of the isomorphism type.

theorem Hex.GraphIso.Mathlib.not_isomorphic_of_card_ne {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k : ℕ} (G : Colored V k) (H : Colored W k) (h : Fintype.card V ≠ Fintype.card W) : ¬G.Isomorphic H

Unequal cardinalities refute coloured isomorphism.

theorem Hex.GraphIso.Mathlib.isEmpty_coloredIso_of_card_ne {V : Type u} {W : Type v} [Fintype V] [Fintype W] {k : ℕ} (G : Colored V k) (H : Colored W k) (h : Fintype.card V ≠ Fintype.card W) : IsEmpty (G.Iso H)