structure Hex.GraphIso.Mathlib.Colored (V : Type u) (k : ℕ) [Fintype V] : Type u

A finite simple graph with an ordered vertex colouring by Fin k in which every colour is used. This is the Mathlib-side counterpart of Hex.GraphIso.Colored: the colouring need not be proper, and an isomorphism has to preserve each colour index.

• graph : SimpleGraph V

  The underlying Mathlib graph.

• color : V → Fin k

  The ordered colour of each vertex.

• onto : Function.Surjective self.color

  Every colour is used.

structure Hex.GraphIso.Mathlib.Colored.Iso {V : Type u} {W : Type v} {k : ℕ} [Fintype V] [Fintype W] (G : Colored V k) (H : Colored W k) : Type (max u v)

A colour-preserving isomorphism of coloured graphs: a graph isomorphism carrying each vertex to a vertex of the same ordered colour.

• graphIso : G.graph ≃g H.graph

  The underlying graph isomorphism.

• map_color (v : V) : H.color (self.graphIso v) = G.color v

  Colour indices are preserved.

def Hex.GraphIso.Mathlib.Colored.Isomorphic {V : Type u} {W : Type v} {k : ℕ} [Fintype V] [Fintype W] (G : Colored V k) (H : Colored W k) : Prop

Two coloured graphs are isomorphic when a colour-preserving graph isomorphism exists.

Equations

• G.Isomorphic H = Nonempty (G.Iso H)

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

theorem Hex.GraphIso.Mathlib.Colored.Isomorphic.elim {V : Type u} {W : Type v} {k : ℕ} [Fintype V] [Fintype W] {G : Colored V k} {H : Colored W k} (h : G.Isomorphic H) : Nonempty (G.Iso H)

def Hex.GraphIso.Mathlib.Colored.ofColor? {V : Type u} {k : ℕ} [Fintype V] [DecidableEq (Fin k)] (graph : SimpleGraph V) (color : V → Fin k) [DecidableEq V] : Option (Colored V k)

Checked construction from a possibly non-onto colour map: none exactly when some colour below k is unused.

Equations

• Hex.GraphIso.Mathlib.Colored.ofColor? graph color = if h : ∀ (c : Fin k), ∃ (v : V), color v = c then some { graph := graph, color := color, onto := h } else none

theorem Hex.GraphIso.Mathlib.Colored.ofColor?_eq_none_iff {V : Type u} {k : ℕ} [Fintype V] [DecidableEq (Fin k)] [DecidableEq V] {graph : SimpleGraph V} {color : V → Fin k} : ofColor? graph color = none ↔ ∃ (c : Fin k), ∀ (v : V), color v ≠ c

Colored.ofColor? returns none exactly when some colour of Fin k is taken by no vertex.