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 graphG
, withα
being the set of available colors. The type is defined to be homomorphisms fromG
into the complete graph onα
, and colorings have a coercion toV → α
. -
G.Colorable n
is the proposition thatG
isn
-colorable, which is whether there exists a coloring with at most n colors. -
G.chromaticNumber
is the minimaln
such thatG
isn
-colorable, or0
if it cannot be colored with finitely many colors. -
C.colorClass c
is the set of vertices colored byc : α
in the coloringC : 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 α
)
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
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
The color class of a given color.
Instances For
The set containing all color classes.
Instances For
Whether a graph can be colored by at most n
colors.
Instances For
The coloring of an empty graph.
Instances For
The "tautological" coloring of a graph, using the vertices of the graph as colors.
Instances For
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
Given an embedding, there is an induced embedding of colorings.
Instances For
Given an equivalence, there is an induced equivalence between colorings.
Instances For
There is a noncomputable embedding of α
-colorings to β
-colorings if
β
has at least as large a cardinality as α
.
Instances For
Noncomputably get a coloring from colorability.
Instances For
The bicoloring of a complete bipartite graph using whether a vertex is on the left or on the right.