# 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 : ) (α : 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
Instances For
theorem SimpleGraph.Coloring.valid {V : Type u} {G : } {α : Type v} (C : ) {v : V} {w : V} (h : G.Adj v w) :
C v C w
@[match_pattern]
def SimpleGraph.Coloring.mk {V : Type u} {G : } {α : Type v} (color : Vα) (valid : ∀ {v w : V}, G.Adj v wcolor 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.)

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

The color class of a given color.

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

The set containing all color classes.

Equations
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} [] [] :
Equations
def SimpleGraph.Colorable {V : Type u} (G : ) (n : ) :

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

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

The coloring of an empty graph.

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
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. 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
• = ⨅ n ∈ , n
Instances For
theorem SimpleGraph.chromaticNumber_eq_biInf {V : Type u} {G : } :
= ⨅ n ∈ , n
theorem SimpleGraph.chromaticNumber_eq_iInf {V : Type u} {G : } :
= ⨅ (n : {m : | }), n
theorem SimpleGraph.Colorable.chromaticNumber_eq_sInf {V : Type u} {G : } {n : } (h : ) :
= (sInf {n' : | })
def SimpleGraph.recolorOfEmbedding {V : Type u} (G : ) {α : Type u_1} {β : Type u_2} (f : α β) :

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

Equations
• One or more equations did not get rendered due to their size.
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.

Equations
• One or more equations did not get rendered due to their size.
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 α.

Equations
Instances For
theorem SimpleGraph.Colorable.mono {V : Type u} {G : } {n : } {m : } (h : n m) (hc : ) :
theorem SimpleGraph.Coloring.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.

Equations
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 : ) :
Set.Nonempty {n : | }
theorem SimpleGraph.Colorable.chromaticNumber_le {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.chromaticNumber_le_of_forall_imp {V : Type u} {G : } {V' : Type u_1} {G' : } (h : ∀ (n : ), ) :
theorem SimpleGraph.chromaticNumber_mono {V : Type u} {G : } (G' : ) (h : G G') :
theorem SimpleGraph.chromaticNumber_mono_of_embedding {V : Type u} {G : } {V' : Type u_1} {G' : } (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.

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

### Cliques #

theorem SimpleGraph.IsClique.card_le_of_coloring {V : Type u} {G : } {α : Type v} {s : } (h : ) [] (C : ) :
s.card
theorem SimpleGraph.IsClique.card_le_of_colorable {V : Type u} {G : } {s : } (h : ) {n : } (hc : ) :
s.card n
theorem SimpleGraph.IsClique.card_le_chromaticNumber {V : Type u} {G : } {s : } (h : ) :
s.card
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 : ) :