# mathlibdocumentation

combinatorics.simple_graph.coloring

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

• 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 wcolor 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
def simple_graph.coloring.color_class {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) (c : α) :
set V

The color class of a given color.

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

The set containing all color classes.

Equations
theorem simple_graph.coloring.mem_color_class {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) (v : V) :
theorem simple_graph.coloring.color_classes_is_partition {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) :
theorem simple_graph.coloring.mem_color_classes {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) {v : V} :
theorem simple_graph.coloring.color_classes_finite {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) [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)] :
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) :
theorem simple_graph.coloring.color_classes_independent {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) (c : α) :
@[protected, instance]
noncomputable def simple_graph.coloring.fintype {V : Type u} {G : simple_graph V} {α : Type v} [fintype V] [fintype α] :
Equations
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
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
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
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
def simple_graph.recolor_of_embedding {V : Type u} (G : simple_graph V) {α : Type u_1} {β : Type u_2} (f : α β) :

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

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

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

Equations
noncomputable def simple_graph.recolor_of_card_le {V : Type u} (G : simple_graph V) {α : Type u_1} {β : Type u_2} [fintype α] [fintype β] (hn : ) :

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

Equations
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 α) :
noncomputable def simple_graph.colorable.to_coloring {V : Type u} {G : simple_graph V} {α : Type v} [fintype α] {n : } (hc : G.colorable n) (hn : n ) :

Noncomputably get a coloring from colorability.

Equations
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_le_of_colorable {V : Type u} {G : simple_graph V} {n : } (hc : G.colorable n) :
theorem simple_graph.chromatic_number_le_card {V : Type u} {G : simple_graph V} {α : Type v} [fintype α] (C : G.coloring α) :
theorem simple_graph.colorable_chromatic_number {V : Type u} {G : simple_graph V} {m : } (hc : G.colorable m) :
theorem simple_graph.chromatic_number_pos {V : Type u} {G : simple_graph V} [nonempty V] {n : } (hc : G.colorable n) :
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 nG.colorable n) :
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') :
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') :
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 α), ) :
theorem simple_graph.chromatic_number_bot {V : Type u} [nonempty V] :
@[simp]
theorem simple_graph.chromatic_number_top {V : Type u} [fintype V] :
def simple_graph.complete_bipartite_graph.bicoloring (V : Type u_1) (W : Type u_2) :

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

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

### 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 α) :
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) :
s.card 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) :
@[protected]
theorem simple_graph.colorable.clique_free {V : Type u} {G : simple_graph V} {n m : } (hc : G.colorable n) (hm : n < m) :