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 #

TODO #

@[reducible, inline]
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.

Equations
theorem SimpleGraph.Coloring.valid {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {v w : V} (h : G.Adj v w) :
C v C w
@[match_pattern]
def SimpleGraph.Coloring.mk {V : Type u} {G : SimpleGraph V} {α : Type u_1} (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
def SimpleGraph.Coloring.colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) (c : α) :
Set V

The color class of a given color.

Equations
def SimpleGraph.Coloring.colorClasses {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) :
Set (Set V)

The set containing all color classes.

Equations
theorem SimpleGraph.Coloring.mem_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) (v : V) :
v C.colorClass (C v)
theorem SimpleGraph.Coloring.mem_colorClasses {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {v : V} :
theorem SimpleGraph.Coloring.not_adj_of_mem_colorClass {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) {c : α} {v w : V} (hv : v C.colorClass c) (hw : w C.colorClass c) :
¬G.Adj v w
theorem SimpleGraph.Coloring.color_classes_independent {V : Type u} {G : SimpleGraph V} {α : Type u_1} (C : G.Coloring α) (c : α) :
noncomputable instance SimpleGraph.instFintypeColoring {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype V] [Fintype α] :
Equations
def SimpleGraph.Colorable {V : Type u} (G : SimpleGraph V) (n : ) :

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

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

The coloring of an empty graph.

Equations

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

Equations
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. 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
theorem SimpleGraph.chromaticNumber_eq_iInf {V : Type u} {G : SimpleGraph V} :
G.chromaticNumber = ⨅ (n : {m : | G.Colorable m}), n
def SimpleGraph.recolorOfEmbedding {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} (f : α β) :

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

Equations
@[simp]
theorem SimpleGraph.coe_recolorOfEmbedding {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} (f : α β) :
def SimpleGraph.recolorOfEquiv {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} (f : α β) :

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

Equations
@[simp]
theorem SimpleGraph.coe_recolorOfEquiv {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} (f : α β) :
noncomputable def SimpleGraph.recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (hn : Fintype.card α Fintype.card β) :

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

Equations
@[simp]
theorem SimpleGraph.coe_recolorOfCardLE {V : Type u} (G : SimpleGraph V) {α : Type u_1} {β : Type u_2} [Fintype α] [Fintype β] (hαβ : Fintype.card α Fintype.card β) :
theorem SimpleGraph.Colorable.mono {V : Type u} {G : SimpleGraph V} {n m : } (h : n m) (hc : G.Colorable n) :
theorem SimpleGraph.Coloring.colorable {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] (C : G.Coloring α) :
noncomputable def SimpleGraph.Colorable.toColoring {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] {n : } (hc : G.Colorable n) (hn : n Fintype.card α) :

Noncomputably get a coloring from colorability.

Equations
theorem SimpleGraph.Colorable.of_embedding {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {G' : SimpleGraph V'} (f : G ↪g G') {n : } (h : G'.Colorable n) :
theorem SimpleGraph.colorable_iff_exists_bdd_nat_coloring {V : Type u} {G : SimpleGraph V} (n : ) :
G.Colorable n ∃ (C : G.Coloring ), ∀ (v : V), C v < n
theorem SimpleGraph.Colorable.mono_left {V : Type u} {G G' : SimpleGraph V} (h : G G') {n : } (hc : G'.Colorable n) :
theorem SimpleGraph.chromaticNumber_le_of_forall_imp {V : Type u} {G : SimpleGraph V} {V' : Type u_3} {G' : SimpleGraph V'} (h : ∀ (n : ), G'.Colorable nG.Colorable n) :

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

Equations

Cliques #

theorem SimpleGraph.IsClique.card_le_of_coloring {V : Type u} {G : SimpleGraph V} {α : Type u_1} {s : Finset V} (h : G.IsClique s) [Fintype α] (C : G.Coloring α) :
theorem SimpleGraph.IsClique.card_le_of_colorable {V : Type u} {G : SimpleGraph V} {s : Finset V} (h : G.IsClique s) {n : } (hc : G.Colorable n) :
s.card n
theorem SimpleGraph.Colorable.cliqueFree {V : Type u} {G : SimpleGraph V} {n m : } (hc : G.Colorable n) (hm : n < m) :
theorem SimpleGraph.Coloring.surjOn_of_card_le_isClique {V : Type u} {G : SimpleGraph V} {α : Type u_1} [Fintype α] {s : Finset V} (h : G.IsClique s) (hc : Fintype.card α s.card) (C : G.Coloring α) :
Set.SurjOn (⇑C) (↑s) Set.univ

Given a colouring α of G, and a clique of size at least the number of colours, the clique contains a vertex of each colour.

The canonical ι-coloring of a completeMultipartiteGraph with parts indexed by ι

Equations