# Documentation

Mathlib.Combinatorics.SimpleGraph.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.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 : ) (α : 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.

Instances For
theorem SimpleGraph.Coloring.valid {V : Type u} {G : } {α : Type v} (C : ) {v : V} {w : V} (h : ) :
C v C w
@[match_pattern]
def SimpleGraph.Coloring.mk {V : Type u} {G : } {α : Type v} (color : Vα) (valid : ∀ {v w : V}, color v color w) :

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

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

The color class of a given color.

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

The set containing all color classes.

Instances For
theorem SimpleGraph.Coloring.mem_colorClass {V : Type u} {G : } {α : Type v} (C : ) (v : V) :
v
theorem SimpleGraph.Coloring.colorClasses_isPartition {V : Type u} {G : } {α : Type v} (C : ) :
theorem SimpleGraph.Coloring.mem_colorClasses {V : Type u} {G : } {α : Type v} (C : ) {v : V} :
theorem SimpleGraph.Coloring.colorClasses_finite {V : Type u} {G : } {α : Type v} (C : ) [] :
theorem SimpleGraph.Coloring.card_colorClasses_le {V : Type u} {G : } {α : Type v} (C : ) [] :
theorem SimpleGraph.Coloring.not_adj_of_mem_colorClass {V : Type u} {G : } {α : Type v} (C : ) {c : α} {v : V} {w : V} (hv : ) (hw : ) :
theorem SimpleGraph.Coloring.color_classes_independent {V : Type u} {G : } {α : Type v} (C : ) (c : α) :
noncomputable instance SimpleGraph.instFintypeColoring {V : Type u} {G : } {α : Type v} [] [] :
def SimpleGraph.Colorable {V : Type u} (G : ) (n : ) :

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

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

The coloring of an empty graph.

Instances For
theorem SimpleGraph.colorable_of_isEmpty {V : Type u} (G : ) [] (n : ) :
theorem SimpleGraph.isEmpty_of_colorable_zero {V : Type u} (G : ) (h : ) :
def SimpleGraph.selfColoring {V : Type u} (G : ) :

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

Instances For
noncomputable def SimpleGraph.chromaticNumber {V : Type u} (G : ) :

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.

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

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

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

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

Instances For
noncomputable def SimpleGraph.recolorOfCardLE {V : Type u} (G : ) {α : Type u_1} {β : Type u_2} [] [] (hn : ) :

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

Instances For
theorem SimpleGraph.Colorable.mono {V : Type u} {G : } {n : } {m : } (h : n m) (hc : ) :
theorem SimpleGraph.Coloring.to_colorable {V : Type u} {G : } {α : Type v} [] (C : ) :
theorem SimpleGraph.colorable_of_fintype {V : Type u} (G : ) [] :
noncomputable def SimpleGraph.Colorable.toColoring {V : Type u} {G : } {α : Type v} [] {n : } (hc : ) (hn : ) :

Noncomputably get a coloring from colorability.

Instances For
theorem SimpleGraph.Colorable.of_embedding {V : Type u} {G : } {V' : Type u_1} {G' : } (f : G ↪g G') {n : } (h : ) :
theorem SimpleGraph.colorable_iff_exists_bdd_nat_coloring {V : Type u} {G : } (n : ) :
C, ∀ (v : V), C v < n
theorem SimpleGraph.colorable_set_nonempty_of_colorable {V : Type u} {G : } {n : } (hc : ) :
theorem SimpleGraph.chromaticNumber_le_of_colorable {V : Type u} {G : } {n : } (hc : ) :
theorem SimpleGraph.chromaticNumber_le_card {V : Type u} {G : } {α : Type v} [] (C : ) :
theorem SimpleGraph.colorable_chromaticNumber {V : Type u} {G : } {m : } (hc : ) :
theorem SimpleGraph.chromaticNumber_pos {V : Type u} {G : } [] {n : } (hc : ) :
theorem SimpleGraph.Colorable.mono_left {V : Type u} {G : } {G' : } (h : G G') {n : } (hc : ) :
theorem SimpleGraph.Colorable.chromaticNumber_le_of_forall_imp {V : Type u} {G : } {V' : Type u_1} {G' : } {m : } (hc : ) (h : ∀ (n : ), ) :
theorem SimpleGraph.Colorable.chromaticNumber_mono {V : Type u} {G : } (G' : ) {m : } (hc : ) (h : G G') :
theorem SimpleGraph.Colorable.chromaticNumber_mono_of_embedding {V : Type u} {G : } {V' : Type u_1} {G' : } {n : } (h : ) (f : G ↪g G') :
theorem SimpleGraph.chromaticNumber_eq_card_of_forall_surj {V : Type u} {G : } {α : Type v} [] (C : ) (h : ∀ (C' : ), ) :
@[simp]

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

Instances For

### Cliques #

theorem SimpleGraph.IsClique.card_le_of_coloring {V : Type u} {G : } {α : Type v} {s : } (h : ) [] (C : ) :
theorem SimpleGraph.IsClique.card_le_of_colorable {V : Type u} {G : } {s : } (h : ) {n : } (hc : ) :
n
theorem SimpleGraph.IsClique.card_le_chromaticNumber {V : Type u} {G : } [] {s : } (h : ) :
theorem SimpleGraph.Colorable.cliqueFree {V : Type u} {G : } {n : } {m : } (hc : ) (hm : n < m) :
theorem SimpleGraph.cliqueFree_of_chromaticNumber_lt {V : Type u} {G : } [] {n : } (hc : ) :