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 #

Todo: #

@[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
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.mem_color_classes {V : Type u} {G : simple_graph V} {α : Type v} (C : G.coloring α) {v : V} :
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 : α) :
@[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

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 : fintype.card α fintype.card β) :

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 fintype.card α) :

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

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

Equations

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