mathlib3 documentation

combinatorics.simple_graph.coloring

Graph Coloring #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.chromatic_number is the minimal n such that G is n-colorable, or 0 if it cannot be colored with finitely many colors.
C.color_class c is the set of vertices colored by c : α in the coloring C : G.coloring α.
C.color_classes 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]

def simple_graph.coloring {V : Type u} (G : simple_graph 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 simple_graph.coloring.valid {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) {v w : V} (h : G.adj v w) :

⇑C v ≠ ⇑C w

def simple_graph.coloring.mk {V : Type u} {G : simple_graph V} {α : Type v} (color : V → α) (valid : ∀ {v w : V}, G.adj v w → color v ≠ color w) :

Construct a term of simple_graph.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 simple_graph.hom, but with a syntactically better proper coloring hypothesis.)

Equations

simple_graph.coloring.mk color valid = {to_fun := color, map_rel' := valid}

def simple_graph.coloring.color_class {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) (c : α) :

The color class of a given color.

Equations

C.color_class c = {v : V | ⇑C v = c}

def simple_graph.coloring.color_classes {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :

The set containing all color classes.

Equations

C.color_classes = (setoid.ker ⇑C).classes

theorem simple_graph.coloring.mem_color_class {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) (v : V) :

v ∈ C.color_class (⇑C v)

theorem simple_graph.coloring.color_classes_is_partition {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :

setoid.is_partition C.color_classes

theorem simple_graph.coloring.mem_color_classes {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) {v : V} :

C.color_class (⇑C v) ∈ C.color_classes

theorem simple_graph.coloring.color_classes_finite {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) [finite α] :

C.color_classes.finite

theorem simple_graph.coloring.card_color_classes_le {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) [fintype α] [fintype ↥(C.color_classes)] :

fintype.card ↥(C.color_classes) ≤ fintype.card α

theorem simple_graph.coloring.not_adj_of_mem_color_class {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) {c : α} {v w : V} (hv : v ∈ C.color_class c) (hw : w ∈ C.color_class c) :

¬G.adj v w

theorem simple_graph.coloring.color_classes_independent {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) (c : α) :

is_antichain G.adj (C.color_class c)

@[protected, instance]

noncomputable def simple_graph.coloring.fintype {V : Type u} {G : simple_graph V} {α : Type v} [fintype V] [fintype α] :

fintype (G.coloring α)

Equations

simple_graph.coloring.fintype = id (fintype.of_injective coe_fn simple_graph.coloring.fintype._proof_1)

def simple_graph.colorable {V : Type u} (G : simple_graph V) (n : ℕ) :

Prop

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

Equations

G.colorable n = nonempty (G.coloring (fin n))

def simple_graph.coloring_of_is_empty {V : Type u} (G : simple_graph V) {α : Type v} [is_empty V] :

The coloring of an empty graph.

Equations

G.coloring_of_is_empty = simple_graph.coloring.mk is_empty_elim _

theorem simple_graph.colorable_of_is_empty {V : Type u} (G : simple_graph V) [is_empty V] (n : ℕ) :

theorem simple_graph.is_empty_of_colorable_zero {V : Type u} (G : simple_graph V) (h : G.colorable 0) :

def simple_graph.self_coloring {V : Type u} (G : simple_graph V) :

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

Equations

G.self_coloring = simple_graph.coloring.mk id _

noncomputable def simple_graph.chromatic_number {V : Type u} (G : simple_graph 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.

Equations

G.chromatic_number = has_Inf.Inf {n : ℕ | G.colorable n}

def simple_graph.recolor_of_embedding {V : Type u} (G : simple_graph V) {α : Type u_1} {β : Type u_2} (f : α ↪ β) :

G.coloring α ↪ G.coloring β

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

Equations

G.recolor_of_embedding f = {to_fun := λ (C : G.coloring α), (simple_graph.embedding.complete_graph f).to_hom.comp C, inj' := _}

def simple_graph.recolor_of_equiv {V : Type u} (G : simple_graph V) {α : Type u_1} {β : Type u_2} (f : α ≃ β) :

G.coloring α ≃ G.coloring β

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

Equations

G.recolor_of_equiv f = {to_fun := ⇑(G.recolor_of_embedding f.to_embedding), inv_fun := ⇑(G.recolor_of_embedding f.symm.to_embedding), left_inv := _, right_inv := _}

noncomputable def simple_graph.recolor_of_card_le {V : Type u} (G : simple_graph V) {α : Type u_1} {β : Type u_2} [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.recolor_of_card_le hn = G.recolor_of_embedding _.some

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

theorem simple_graph.coloring.to_colorable {V : Type u} {G : simple_graph V} {α : Type v} [fintype α] (C : G.coloring α) :

G.colorable (fintype.card α)

theorem simple_graph.colorable_of_fintype {V : Type u} (G : simple_graph V) [fintype V] :

G.colorable (fintype.card V)

noncomputable def simple_graph.colorable.to_coloring {V : Type u} {G : simple_graph V} {α : Type v} [fintype α] {n : ℕ} (hc : G.colorable n) (hn : n ≤ fintype.card α) :

Noncomputably get a coloring from colorability.

Equations

hc.to_coloring hn = ⇑(G.recolor_of_card_le _) (nonempty.some hc)

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

theorem simple_graph.colorable_iff_exists_bdd_nat_coloring {V : Type u} {G : simple_graph V} (n : ℕ) :

G.colorable n ↔ ∃ (C : G.coloring ℕ), ∀ (v : V), ⇑C v < n

theorem simple_graph.colorable_set_nonempty_of_colorable {V : Type u} {G : simple_graph V} {n : ℕ} (hc : G.colorable n) :

{n : ℕ | G.colorable n}.nonempty

theorem simple_graph.chromatic_number_bdd_below {V : Type u} {G : simple_graph V} :

bdd_below {n : ℕ | G.colorable n}

theorem simple_graph.chromatic_number_le_of_colorable {V : Type u} {G : simple_graph V} {n : ℕ} (hc : G.colorable n) :

G.chromatic_number ≤ n

theorem simple_graph.chromatic_number_le_card {V : Type u} {G : simple_graph V} {α : Type v} [fintype α] (C : G.coloring α) :

G.chromatic_number ≤ fintype.card α

theorem simple_graph.colorable_chromatic_number {V : Type u} {G : simple_graph V} {m : ℕ} (hc : G.colorable m) :

G.colorable G.chromatic_number

theorem simple_graph.colorable_chromatic_number_of_fintype {V : Type u} (G : simple_graph V) [finite V] :

G.colorable G.chromatic_number

theorem simple_graph.chromatic_number_le_one_of_subsingleton {V : Type u} (G : simple_graph V) [subsingleton V] :

G.chromatic_number ≤ 1

theorem simple_graph.chromatic_number_eq_zero_of_isempty {V : Type u} (G : simple_graph V) [is_empty V] :

G.chromatic_number = 0

theorem simple_graph.is_empty_of_chromatic_number_eq_zero {V : Type u} (G : simple_graph V) [finite V] (h : G.chromatic_number = 0) :

theorem simple_graph.chromatic_number_pos {V : Type u} {G : simple_graph V} [nonempty V] {n : ℕ} (hc : G.colorable n) :

0 < G.chromatic_number

theorem simple_graph.colorable_of_chromatic_number_pos {V : Type u} {G : simple_graph V} (h : 0 < G.chromatic_number) :

G.colorable G.chromatic_number

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

theorem simple_graph.colorable.chromatic_number_le_of_forall_imp {V : Type u} {G : simple_graph V} {V' : Type u_1} {G' : simple_graph V'} {m : ℕ} (hc : G'.colorable m) (h : ∀ (n : ℕ), G'.colorable n → G.colorable n) :

G.chromatic_number ≤ G'.chromatic_number

theorem simple_graph.colorable.chromatic_number_mono {V : Type u} {G : simple_graph V} (G' : simple_graph V) {m : ℕ} (hc : G'.colorable m) (h : G ≤ G') :

G.chromatic_number ≤ G'.chromatic_number

theorem simple_graph.colorable.chromatic_number_mono_of_embedding {V : Type u} {G : simple_graph V} {V' : Type u_1} {G' : simple_graph V'} {n : ℕ} (h : G'.colorable n) (f : G ↪g G') :

G.chromatic_number ≤ G'.chromatic_number

theorem simple_graph.chromatic_number_eq_card_of_forall_surj {V : Type u} {G : simple_graph V} {α : Type v} [fintype α] (C : G.coloring α) (h : ∀ (C' : G.coloring α), function.surjective ⇑C') :

G.chromatic_number = fintype.card α

theorem simple_graph.chromatic_number_bot {V : Type u} [nonempty V] :

⊥.chromatic_number = 1

@[simp]

theorem simple_graph.chromatic_number_top {V : Type u} [fintype V] :

⊤.chromatic_number = fintype.card V

theorem simple_graph.chromatic_number_top_eq_zero_of_infinite (V : Type u_1) [infinite V] :

⊤.chromatic_number = 0

def simple_graph.complete_bipartite_graph.bicoloring (V : Type u_1) (W : Type u_2) :

(complete_bipartite_graph V W).coloring bool

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

Equations

simple_graph.complete_bipartite_graph.bicoloring V W = simple_graph.coloring.mk (λ (v : V ⊕ W), v.is_right) _

theorem simple_graph.complete_bipartite_graph.chromatic_number {V : Type u_1} {W : Type u_2} [nonempty V] [nonempty W] :

(complete_bipartite_graph V W).chromatic_number = 2

Cliques #

theorem simple_graph.is_clique.card_le_of_coloring {V : Type u} {G : simple_graph V} {α : Type v} {s : finset V} (h : G.is_clique ↑s) [fintype α] (C : G.coloring α) :

s.card ≤ fintype.card α

theorem simple_graph.is_clique.card_le_of_colorable {V : Type u} {G : simple_graph V} {s : finset V} (h : G.is_clique ↑s) {n : ℕ} (hc : G.colorable n) :

theorem simple_graph.is_clique.card_le_chromatic_number {V : Type u} {G : simple_graph V} [finite V] {s : finset V} (h : G.is_clique ↑s) :

s.card ≤ G.chromatic_number

@[protected]

theorem simple_graph.colorable.clique_free {V : Type u} {G : simple_graph V} {n m : ℕ} (hc : G.colorable n) (hm : n < m) :

G.clique_free m

theorem simple_graph.clique_free_of_chromatic_number_lt {V : Type u} {G : simple_graph V} [finite V] {n : ℕ} (hc : G.chromatic_number < n) :

G.clique_free n