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.

Equations

• G.Coloring α = (G →g ⊤)

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

@[match_pattern]

def SimpleGraph.Coloring.mk {V : Type u} {G : SimpleGraph V} {α : Type u_1} (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.)

Equations

• SimpleGraph.Coloring.mk color valid = { toFun := color, map_rel' := valid }

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

The color class of a given color.

Equations

• C.colorClass c = {v : V | C v = c}

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

The set containing all color classes.

Equations

• C.colorClasses = (Setoid.ker ⇑C).classes

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

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

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

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

theorem SimpleGraph.Coloring.card_colorClasses_le {V : Type u} {G : SimpleGraph V} {α : Type u_1} (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_1} (C : G.Coloring α) {c : α} {v w : V} (hv : v ∈ C.colorClass c) (hw : w ∈ C.colorClass c) : ¬G.Adj v w

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

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

Equations

• SimpleGraph.instFintypeColoring = id (Fintype.ofInjective (fun (f : G.Adj →r ⊤.Adj) => ⇑f) ⋯)

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

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

Equations

• G.Colorable n = Nonempty (G.Coloring (Fin n))

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

The coloring of an empty graph.

Equations

• G.coloringOfIsEmpty = SimpleGraph.Coloring.mk (fun (a : V) => isEmptyElim a) ⋯

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

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

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.

Equations

• G.selfColoring = SimpleGraph.Coloring.mk id ⋯

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.

Equations

• G.chromaticNumber = ⨅ n ∈ setOf G.Colorable, ↑n

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_3} {β : Type u_4} (f : α ↪ β) : G.Coloring α ↪ G.Coloring β

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

Equations

• G.recolorOfEmbedding f = { toFun := fun (C : G.Coloring α) => (SimpleGraph.Embedding.completeGraph f).toHom.comp C, inj' := ⋯ }

@[simp]

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

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

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

Equations

• G.recolorOfEquiv f = { toFun := ⇑(G.recolorOfEmbedding f.toEmbedding), invFun := ⇑(G.recolorOfEmbedding f.symm.toEmbedding), left_inv := ⋯, right_inv := ⋯ }

@[simp]

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

noncomputable def SimpleGraph.recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} [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 α.

Equations

• G.recolorOfCardLE hn = G.recolorOfEmbedding ⋯.some

@[simp]

theorem SimpleGraph.coe_recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α ≤ Fintype.card β) : ⇑(G.recolorOfCardLE hαβ) = (SimpleGraph.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_1} [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_1} [Fintype α] {n : ℕ} (hc : G.Colorable n) (hn : n ≤ Fintype.card α) : G.Coloring α

Noncomputably get a coloring from colorability.

Equations

• hc.toColoring hn = (G.recolorOfCardLE ⋯) (Nonempty.some hc)

theorem SimpleGraph.Colorable.of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {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_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

@[deprecated SimpleGraph.Colorable.chromaticNumber_le (since := "2024-03-21")]

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

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_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) [Finite V] (h : G.chromaticNumber = 0) : IsEmpty V

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.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_3} {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_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {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_1} [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_1} [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_3) [Infinite V] : ⊤.chromaticNumber = ⊤

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

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

Equations

• SimpleGraph.CompleteBipartiteGraph.bicoloring V W = SimpleGraph.Coloring.mk (fun (v : V ⊕ W) => v.isRight) ⋯

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

Cliques

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

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

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.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