Graph Coloring

This module defines colorings of simple graphs (also known as proper colorings in the literature). A graph coloring is the attribution of "colors" to all of its vertices such that adjacent vertices have different colors. A coloring can be represented as a homomorphism into a complete graph, whose vertices represent the colors.

Main definitions

• G.Coloring α is the type of α-colorings of a simple graph G, with α being the set of available colors. The type is defined to be homomorphisms from G into the complete graph on α, and colorings have a coercion to V → α.

• G.Colorable n is the proposition that G is n-colorable, which is whether there exists a coloring with at most n colors.

• G.chromaticNumber is the minimal n such that G is n-colorable, or ⊤ if it cannot be colored with finitely many colors. (Cardinal-valued chromatic numbers are more niche, so we stick to ℕ∞.) We write G.chromaticNumber ≠ ⊤ to mean a graph is colorable with finitely many colors.

• C.colorClass c is the set of vertices colored by c : α in the coloring C : G.Coloring α.

• C.colorClasses is the set containing all color classes.

TODO

• Gather material from:

  • https://github.com/leanprover-community/mathlib/blob/simple_graph_matching/src/combinatorics/simple_graph/coloring.lean
  • https://github.com/kmill/lean-graphcoloring/blob/master/src/graph.lean

• Trees

• Planar graphs

• Chromatic polynomials

• develop API for partial colorings, likely as colorings of subgraphs (H.coe.Coloring α)

@[reducible, inline]

abbrev SimpleGraph.Coloring {V : Type u} (G : SimpleGraph V) (α : Type v) : Type (max u v)

An α-coloring of a simple graph G is a homomorphism of G into the complete graph on α. This is also known as a proper coloring.

theorem SimpleGraph.Coloring.valid {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) {v w : V} (h : G.Adj v w) : C v ≠ C w

theorem SimpleGraph.Coloring.injective_comp_of_pairwise_adj {V : Type u} {G : SimpleGraph V} {ι : Type u_1} {α : Type u_2} (C : G.Coloring α) (f : ι → V) (hf : Pairwise fun (i j : ι) => G.Adj (f i) (f j)) : Function.Injective (⇑C ∘ f)

@[match_pattern]

def SimpleGraph.Coloring.mk {V : Type u} {G : SimpleGraph V} {α : Type u_2} (color : V → α) (valid : ∀ {v w : V}, G.Adj v w → color v ≠ color w) : G.Coloring α

Construct a term of SimpleGraph.Coloring using a function that assigns vertices to colors and a proof that it is as proper coloring.

(Note: this is a definitionally the constructor for SimpleGraph.Hom, but with a syntactically better proper coloring hypothesis.)

def SimpleGraph.Coloring.colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (c : α) : Set V

The color class of a given color.

def SimpleGraph.Coloring.colorClasses {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) : Set (Set V)

The set containing all color classes.

theorem SimpleGraph.Coloring.mem_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (v : V) : v ∈ C.colorClass (C v)

theorem SimpleGraph.Coloring.colorClasses_isPartition {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) : Setoid.IsPartition C.colorClasses

theorem SimpleGraph.Coloring.mem_colorClasses {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) {v : V} : C.colorClass (C v) ∈ C.colorClasses

theorem SimpleGraph.Coloring.colorClasses_finite {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) [Finite α] : C.colorClasses.Finite

theorem SimpleGraph.Coloring.card_colorClasses_le {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) [Fintype α] [Fintype ↑C.colorClasses] : Fintype.card ↑C.colorClasses ≤ Fintype.card α

theorem SimpleGraph.Coloring.not_adj_of_mem_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) {c : α} {v w : V} (hv : v ∈ C.colorClass c) (hw : w ∈ C.colorClass c) : ¬G.Adj v w

theorem SimpleGraph.Coloring.isIndepSet_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (c : α) : G.IsIndepSet (C.colorClass c)

@[deprecated SimpleGraph.Coloring.isIndepSet_colorClass (since := "2026-02-07")]

theorem SimpleGraph.Coloring.color_classes_independent {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) (c : α) : IsAntichain G.Adj (C.colorClass c)

@[implicit_reducible]

noncomputable instance SimpleGraph.instFintypeColoring {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Fintype V] [Fintype α] : Fintype (G.Coloring α)

@[implicit_reducible]

instance SimpleGraph.instDecidablePredMemSetColorClassOfDecidableEq {V : Type u} {G : SimpleGraph V} {α : Type u_2} (C : G.Coloring α) [DecidableEq α] {c : α} : DecidablePred fun (x : V) => x ∈ C.colorClass c

instance SimpleGraph.instNontrivialColoringOfNonempty {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Nonempty (G.Coloring α)] [Nontrivial α] [Nonempty V] : Nontrivial (G.Coloring α)

instance SimpleGraph.instInfiniteColoringOfNonempty {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Nonempty (G.Coloring α)] [Infinite α] [Nonempty V] : Infinite (G.Coloring α)

def SimpleGraph.Colorable {V : Type u} (G : SimpleGraph V) (n : ℕ) : Prop

Whether a graph can be colored by at most n colors.

def SimpleGraph.Coloring.ofIsEmpty {V : Type u} {G : SimpleGraph V} {α : Type u_2} [IsEmpty V] : G.Coloring α

The coloring of an empty graph.

theorem SimpleGraph.Colorable.of_isEmpty {V : Type u} {G : SimpleGraph V} [IsEmpty V] (n : ℕ) : G.Colorable n

@[deprecated SimpleGraph.Coloring.ofIsEmpty (since := "2026-01-03")]

def SimpleGraph.coloringOfIsEmpty {V : Type u} {G : SimpleGraph V} {α : Type u_2} [IsEmpty V] : G.Coloring α

Alias of SimpleGraph.Coloring.ofIsEmpty.

---

The coloring of an empty graph.

@[deprecated SimpleGraph.Colorable.of_isEmpty (since := "2026-01-03")]

theorem SimpleGraph.colorableOfIsEmpty {V : Type u} {G : SimpleGraph V} [IsEmpty V] (n : ℕ) : G.Colorable n

Alias of SimpleGraph.Colorable.of_isEmpty.

theorem SimpleGraph.isEmpty_of_colorable_zero {V : Type u} {G : SimpleGraph V} (h : G.Colorable 0) : IsEmpty V

@[simp]

theorem SimpleGraph.colorable_zero_iff {V : Type u} {G : SimpleGraph V} : G.Colorable 0 ↔ IsEmpty V

theorem SimpleGraph.Colorable.map {V : Type u} {G : SimpleGraph V} {n : ℕ} {β : Type u_3} (f : V ↪ β) [NeZero n] (hc : G.Colorable n) : (SimpleGraph.map (⇑f) G).Colorable n

If G is n-colorable, then mapping the vertices of G produces an n-colorable simple graph.

theorem SimpleGraph.Colorable.card_le_of_pairwise_adj {V : Type u} {G : SimpleGraph V} {n : ℕ} {ι : Type u_1} (hG : G.Colorable n) (f : ι → V) (hf : Pairwise fun (i j : ι) => G.Adj (f i) (f j)) : Nat.card ι ≤ n

def SimpleGraph.selfColoring {V : Type u} (G : SimpleGraph V) : G.Coloring V

The "tautological" coloring of a graph, using the vertices of the graph as colors.

noncomputable def SimpleGraph.chromaticNumber {V : Type u} (G : SimpleGraph V) : ℕ∞

The chromatic number of a graph is the minimal number of colors needed to color it. This is ⊤ (infinity) iff G isn't colorable with finitely many colors.

If G is colorable, then ENat.toNat G.chromaticNumber is the ℕ-valued chromatic number.

theorem SimpleGraph.le_chromaticNumber_iff_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} : ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ), G.Colorable m → n ≤ m

theorem SimpleGraph.le_chromaticNumber_iff_coloring {V : Type u} {G : SimpleGraph V} {n : ℕ} : ↑n ≤ G.chromaticNumber ↔ ∀ (m : ℕ) (a : G.Coloring (Fin m)), n ≤ m

theorem SimpleGraph.le_chromaticNumber_of_pairwise_adj {V : Type u} {G : SimpleGraph V} {n : ℕ} {ι : Type u_1} (hn : n ≤ Nat.card ι) (f : ι → V) (hf : Pairwise fun (i j : ι) => G.Adj (f i) (f j)) : ↑n ≤ G.chromaticNumber

theorem SimpleGraph.chromaticNumber_eq_biInf {V : Type u} (G : SimpleGraph V) : G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, ↑n

theorem SimpleGraph.chromaticNumber_eq_iInf {V : Type u} (G : SimpleGraph V) : G.chromaticNumber = ⨅ (n : ↑{m : ℕ | G.Colorable m}), ↑↑n

theorem SimpleGraph.Colorable.chromaticNumber_eq_sInf {V : Type u} {G : SimpleGraph V} {n : ℕ} (h : G.Colorable n) : G.chromaticNumber = ↑(sInf {n' : ℕ | G.Colorable n'})

def SimpleGraph.recolorOfEmbedding {V : Type u} (G : SimpleGraph V) {α : Type u_4} {β : Type u_5} (f : α ↪ β) : G.Coloring α ↪ G.Coloring β

Given an embedding, there is an induced embedding of colorings.

@[simp]

theorem SimpleGraph.coe_recolorOfEmbedding {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} (f : α ↪ β) : ⇑(G.recolorOfEmbedding f) = (Embedding.completeGraph f).toHom.comp

def SimpleGraph.recolorOfEquiv {V : Type u} (G : SimpleGraph V) {α : Type u_4} {β : Type u_5} (f : α ≃ β) : G.Coloring α ≃ G.Coloring β

Given an equivalence, there is an induced equivalence between colorings.

@[simp]

theorem SimpleGraph.coe_recolorOfEquiv {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} (f : α ≃ β) : ⇑(G.recolorOfEquiv f) = (Embedding.completeGraph f.toEmbedding).toHom.comp

noncomputable def SimpleGraph.recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_4} {β : Type u_5} [Fintype α] [Fintype β] (hn : Fintype.card α ≤ Fintype.card β) : G.Coloring α ↪ G.Coloring β

There is a noncomputable embedding of α-colorings to β-colorings if β has at least as large a cardinality as α.

@[simp]

theorem SimpleGraph.coe_recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) : ⇑(G.recolorOfCardLE hαβ) = (Embedding.completeGraph ⋯.some).toHom.comp

theorem SimpleGraph.Colorable.mono {V : Type u} {G : SimpleGraph V} {n m : ℕ} (h : n ≤ m) (hc : G.Colorable n) : G.Colorable m

theorem SimpleGraph.Coloring.colorable {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Fintype α] (C : G.Coloring α) : G.Colorable (Fintype.card α)

theorem SimpleGraph.colorable_of_fintype {V : Type u} (G : SimpleGraph V) [Fintype V] : G.Colorable (Fintype.card V)

noncomputable def SimpleGraph.Colorable.toColoring {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Fintype α] {n : ℕ} (hc : G.Colorable n) (hn : n ≤ Fintype.card α) : G.Coloring α

Noncomputably get a coloring from colorability.

theorem SimpleGraph.Colorable.of_hom {V : Type u} {G : SimpleGraph V} {V' : Type u_4} {G' : SimpleGraph V'} (f : G →g G') {n : ℕ} (h : G'.Colorable n) : G.Colorable n

theorem SimpleGraph.colorable_iff_exists_bdd_nat_coloring {V : Type u} {G : SimpleGraph V} (n : ℕ) : G.Colorable n ↔ ∃ (C : G.Coloring ℕ), ∀ (v : V), C v < n

theorem SimpleGraph.colorable_iff_forall_connectedComponents {V : Type u} {G : SimpleGraph V} {n : ℕ} : G.Colorable n ↔ ∀ (c : G.ConnectedComponent), c.toSimpleGraph.Colorable n

theorem SimpleGraph.colorable_set_nonempty_of_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} (hc : G.Colorable n) : {n : ℕ | G.Colorable n}.Nonempty

theorem SimpleGraph.chromaticNumber_bddBelow {V : Type u} {G : SimpleGraph V} : BddBelow {n : ℕ | G.Colorable n}

theorem SimpleGraph.Colorable.chromaticNumber_le {V : Type u} {G : SimpleGraph V} {n : ℕ} (hc : G.Colorable n) : G.chromaticNumber ≤ ↑n

theorem SimpleGraph.chromaticNumber_ne_top_iff_exists {V : Type u} {G : SimpleGraph V} : G.chromaticNumber ≠ ⊤ ↔ ∃ (n : ℕ), G.Colorable n

theorem SimpleGraph.chromaticNumber_le_iff_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} : G.chromaticNumber ≤ ↑n ↔ G.Colorable n

theorem SimpleGraph.chromaticNumber_eq_iff_colorable_not_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} : G.chromaticNumber = ↑n + 1 ↔ G.Colorable (n + 1) ∧ ¬G.Colorable n

If the chromatic number of G is n + 1, then G is colorable in no fewer than n + 1 colors.

theorem SimpleGraph.colorable_chromaticNumber {V : Type u} {G : SimpleGraph V} {m : ℕ} (hc : G.Colorable m) : G.Colorable G.chromaticNumber.toNat

theorem SimpleGraph.colorable_chromaticNumber_of_fintype {V : Type u} (G : SimpleGraph V) [Finite V] : G.Colorable G.chromaticNumber.toNat

theorem SimpleGraph.chromaticNumber_le_one_of_subsingleton {V : Type u} (G : SimpleGraph V) [Subsingleton V] : G.chromaticNumber ≤ 1

theorem SimpleGraph.chromaticNumber_pos {V : Type u} {G : SimpleGraph V} [Nonempty V] {n : ℕ} (hc : G.Colorable n) : 0 < G.chromaticNumber

theorem SimpleGraph.colorable_of_chromaticNumber_ne_top {V : Type u} {G : SimpleGraph V} (h : G.chromaticNumber ≠ ⊤) : G.Colorable G.chromaticNumber.toNat

theorem SimpleGraph.chromaticNumber_eq_zero_of_isEmpty {V : Type u} {G : SimpleGraph V} [IsEmpty V] : G.chromaticNumber = 0

theorem SimpleGraph.isEmpty_of_chromaticNumber_eq_zero {V : Type u} {G : SimpleGraph V} (h : G.chromaticNumber = 0) : IsEmpty V

theorem SimpleGraph.Colorable.mono_left {V : Type u} {G G' : SimpleGraph V} (h : G ≤ G') {n : ℕ} (hc : G'.Colorable n) : G.Colorable n

theorem SimpleGraph.chromaticNumber_le_of_forall_imp {V : Type u} {G : SimpleGraph V} {V' : Type u_4} {G' : SimpleGraph V'} (h : ∀ (n : ℕ), G'.Colorable n → G.Colorable n) : G.chromaticNumber ≤ G'.chromaticNumber

theorem SimpleGraph.chromaticNumber_mono {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph V) (h : G ≤ G') : G.chromaticNumber ≤ G'.chromaticNumber

theorem SimpleGraph.chromaticNumber_mono_of_hom {V : Type u} {G : SimpleGraph V} {V' : Type u_4} {G' : SimpleGraph V'} (f : G →g G') : G.chromaticNumber ≤ G'.chromaticNumber

theorem SimpleGraph.card_le_chromaticNumber_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Fintype α] : ↑(Fintype.card α) ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring α), Function.Surjective ⇑C

theorem SimpleGraph.le_chromaticNumber_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {n : ℕ} : ↑n ≤ G.chromaticNumber ↔ ∀ (C : G.Coloring (Fin n)), Function.Surjective ⇑C

theorem SimpleGraph.chromaticNumber_eq_card_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Fintype α] (hG : G.Colorable (Fintype.card α)) : G.chromaticNumber = ↑(Fintype.card α) ↔ ∀ (C : G.Coloring α), Function.Surjective ⇑C

theorem SimpleGraph.chromaticNumber_eq_iff_forall_surjective {V : Type u} {G : SimpleGraph V} {n : ℕ} (hG : G.Colorable n) : G.chromaticNumber = ↑n ↔ ∀ (C : G.Coloring (Fin n)), Function.Surjective ⇑C

theorem SimpleGraph.chromaticNumber_bot {V : Type u} [Nonempty V] : ⊥.chromaticNumber = 1

@[simp]

theorem SimpleGraph.chromaticNumber_top {V : Type u} [Fintype V] : ⊤.chromaticNumber = ↑(Fintype.card V)

theorem SimpleGraph.chromaticNumber_top_eq_top_of_infinite (V : Type u_4) [Infinite V] : ⊤.chromaticNumber = ⊤

theorem SimpleGraph.eq_top_of_chromaticNumber_eq_card {V : Type u} {G : SimpleGraph V} [Fintype V] (h : G.chromaticNumber = ↑(Fintype.card V)) : G = ⊤

theorem SimpleGraph.chromaticNumber_eq_card_iff {V : Type u} {G : SimpleGraph V} [Fintype V] : G.chromaticNumber = ↑(Fintype.card V) ↔ G = ⊤

theorem SimpleGraph.chromaticNumber_le_card {V : Type u} {G : SimpleGraph V} [Fintype V] : G.chromaticNumber ≤ ↑(Fintype.card V)

theorem SimpleGraph.two_le_chromaticNumber_of_adj {V : Type u} {G : SimpleGraph V} {u v : V} (hadj : G.Adj u v) : 2 ≤ G.chromaticNumber

theorem SimpleGraph.chromaticNumber_eq_one_iff {V : Type u} {G : SimpleGraph V} : G.chromaticNumber = 1 ↔ G = ⊥ ∧ Nonempty V

theorem SimpleGraph.two_le_chromaticNumber_iff_ne_bot {V : Type u} {G : SimpleGraph V} : 2 ≤ G.chromaticNumber ↔ G ≠ ⊥

def SimpleGraph.CompleteBipartiteGraph.bicoloring (V : Type u_4) (W : Type u_5) : (completeBipartiteGraph V W).Coloring Bool

The bicoloring of a complete bipartite graph using whether a vertex is on the left or on the right.

theorem SimpleGraph.CompleteBipartiteGraph.chromaticNumber {V : Type u_4} {W : Type u_5} [Nonempty V] [Nonempty W] : (completeBipartiteGraph V W).chromaticNumber = 2

Cliques

theorem SimpleGraph.IsClique.card_le_of_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} {s : Finset V} (h : G.IsClique ↑s) (hc : G.Colorable n) : s.card ≤ n

theorem SimpleGraph.IsClique.card_le_of_coloring {V : Type u} {G : SimpleGraph V} {α : Type u_2} {s : Finset V} (h : G.IsClique ↑s) [Fintype α] (C : G.Coloring α) : s.card ≤ Fintype.card α

theorem SimpleGraph.IsClique.card_le_chromaticNumber {V : Type u} {G : SimpleGraph V} {s : Finset V} (h : G.IsClique ↑s) : ↑s.card ≤ G.chromaticNumber

theorem SimpleGraph.cliqueNum_le_chromaticNumber {V : Type u} {G : SimpleGraph V} : ↑G.cliqueNum ≤ G.chromaticNumber

theorem SimpleGraph.Colorable.cliqueFree {V : Type u} {G : SimpleGraph V} {n m : ℕ} (hc : G.Colorable n) (hm : n < m) : G.CliqueFree m

theorem SimpleGraph.cliqueFree_of_chromaticNumber_lt {V : Type u} {G : SimpleGraph V} {n : ℕ} (hc : G.chromaticNumber < ↑n) : G.CliqueFree n

theorem SimpleGraph.Coloring.surjOn_of_card_le_isClique {V : Type u} {G : SimpleGraph V} {α : Type u_2} [Fintype α] {s : Finset V} (h : G.IsClique ↑s) (hc : Fintype.card α ≤ s.card) (C : G.Coloring α) : Set.SurjOn (⇑C) (↑s) Set.univ

Given a coloring α of G, and a clique of size at least the number of colors, the clique contains a vertex of each color.

def SimpleGraph.completeMultipartiteGraph.coloring {ι : Type u_4} (V : ι → Type u_5) : (completeMultipartiteGraph V).Coloring ι

The canonical ι-coloring of a completeMultipartiteGraph with parts indexed by ι

theorem SimpleGraph.completeMultipartiteGraph.colorable {ι : Type u_4} (V : ι → Type u_5) [Fintype ι] : (completeMultipartiteGraph V).Colorable (Fintype.card ι)

theorem SimpleGraph.completeMultipartiteGraph.chromaticNumber {ι : Type u_4} (V : ι → Type u_5) [Fintype ι] (f : (i : ι) → V i) : (completeMultipartiteGraph V).chromaticNumber = ↑(Fintype.card ι)

theorem SimpleGraph.completeMultipartiteGraph.colorable_of_cliqueFree {n : ℕ} {ι : Type u_4} (V : ι → Type u_5) (f : (i : ι) → V i) (hc : (completeMultipartiteGraph V).CliqueFree n) : (completeMultipartiteGraph V).Colorable (n - 1)

theorem SimpleGraph.free_of_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} {W : Type u_4} {H : SimpleGraph W} (nhc : ¬H.Colorable n) (hc : G.Colorable n) : H.Free G

If H is not n-colorable and G is n-colorable, then G is H.Free.