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 α)

@[inline, reducible]

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

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

theorem SimpleGraph.Coloring.valid {V : Type u} {G : SimpleGraph V} {α : Type v} (C : SimpleGraph.Coloring G α) {v : 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 v} (color : V → α) (valid : ∀ {v w : V}, G.Adj v w → color v ≠ color w) : SimpleGraph.Coloring G α

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 v} (C : SimpleGraph.Coloring G α) (c : α) : Set V

The color class of a given color.

Equations

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

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

The set containing all color classes.

Equations

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

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

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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

The coloring of an empty graph.

Equations

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

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

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

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

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

Equations

• SimpleGraph.selfColoring G = 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

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

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

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

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

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

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

Equations

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

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

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

Equations

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

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

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

Equations

• SimpleGraph.recolorOfCardLE G hn = SimpleGraph.recolorOfEmbedding G (Nonempty.some ⋯)

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

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

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

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

Noncomputably get a coloring from colorability.

Equations

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

theorem SimpleGraph.Colorable.of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_1} {G' : SimpleGraph V'} (f : G ↪g G') {n : ℕ} (h : SimpleGraph.Colorable G' n) : SimpleGraph.Colorable G n

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem SimpleGraph.chromaticNumber_mono_of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_1} {G' : SimpleGraph V'} (f : G ↪g G') : SimpleGraph.chromaticNumber G ≤ SimpleGraph.chromaticNumber G'

theorem SimpleGraph.chromaticNumber_eq_card_of_forall_surj {V : Type u} {G : SimpleGraph V} {α : Type v} [Fintype α] (C : SimpleGraph.Coloring G α) (h : ∀ (C' : SimpleGraph.Coloring G α), Function.Surjective ⇑C') : SimpleGraph.chromaticNumber G = ↑(Fintype.card α)

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

@[simp]

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

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

def SimpleGraph.CompleteBipartiteGraph.bicoloring (V : Type u_1) (W : Type u_2) : SimpleGraph.Coloring (completeBipartiteGraph V W) 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) => Sum.isRight v) ⋯

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

Cliques

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

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

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

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

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