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 0 if it cannot be colored 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.

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

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.

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.

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) : ¬SimpleGraph.Adj G 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 α)

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

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

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

The coloring of an empty graph.

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.

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. If G isn't colorable with finitely many colors, this will be 0.

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.

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.

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

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

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, ∀ (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.chromaticNumber_le_of_colorable {V : Type u} {G : SimpleGraph V} {n : ℕ} (hc : SimpleGraph.Colorable G n) : SimpleGraph.chromaticNumber 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 (SimpleGraph.chromaticNumber G)

theorem SimpleGraph.colorable_chromaticNumber_of_fintype {V : Type u} (G : SimpleGraph V) [Finite V] : SimpleGraph.Colorable G (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_pos {V : Type u} {G : SimpleGraph V} (h : 0 < SimpleGraph.chromaticNumber G) : SimpleGraph.Colorable G (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.Colorable.chromaticNumber_le_of_forall_imp {V : Type u} {G : SimpleGraph V} {V' : Type u_1} {G' : SimpleGraph V'} {m : ℕ} (hc : SimpleGraph.Colorable G' m) (h : ∀ (n : ℕ), SimpleGraph.Colorable G' n → SimpleGraph.Colorable G n) : SimpleGraph.chromaticNumber G ≤ SimpleGraph.chromaticNumber G'

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

theorem SimpleGraph.Colorable.chromaticNumber_mono_of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_1} {G' : SimpleGraph V'} {n : ℕ} (h : SimpleGraph.Colorable G' n) (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_zero_of_infinite (V : Type u_1) [Infinite V] : SimpleGraph.chromaticNumber ⊤ = 0

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.

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 α) : Finset.card s ≤ 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) : Finset.card s ≤ n

theorem SimpleGraph.IsClique.card_le_chromaticNumber {V : Type u} {G : SimpleGraph V} [Finite V] {s : Finset V} (h : SimpleGraph.IsClique G ↑s) : Finset.card s ≤ 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} [Finite V] {n : ℕ} (hc : SimpleGraph.chromaticNumber G < n) : SimpleGraph.CliqueFree G n