Concrete colorings of common graphs

This file defines colorings for some common graphs.

Main declarations

• SimpleGraph.pathGraph.bicoloring: Bicoloring of a path graph.

theorem SimpleGraph.chromaticNumber_le_two_iff_isBipartite {V : Type u_1} {G : SimpleGraph V} : G.chromaticNumber ≤ 2 ↔ G.IsBipartite

theorem SimpleGraph.chromaticNumber_eq_two_iff {V : Type u_1} {G : SimpleGraph V} : G.chromaticNumber = 2 ↔ G.IsBipartite ∧ G ≠ ⊥

def SimpleGraph.pathGraph.bicoloring (n : ℕ) : (pathGraph n).Coloring Bool

Bicoloring of a path graph

def SimpleGraph.pathGraph_two_embedding (n : ℕ) (h : 2 ≤ n) : pathGraph 2 ↪g pathGraph n

Embedding of pathGraph 2 into the first two elements of pathGraph n for 2 ≤ n

theorem SimpleGraph.chromaticNumber_pathGraph (n : ℕ) (h : 2 ≤ n) : (pathGraph n).chromaticNumber = 2

theorem SimpleGraph.Coloring.even_length_iff_congr {α : Type u_1} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) : Even p.length ↔ (c u = true ↔ c v = true)

theorem SimpleGraph.Coloring.odd_length_iff_not_congr {α : Type u_1} {G : SimpleGraph α} (c : G.Coloring Bool) {u v : α} (p : G.Walk u v) : Odd p.length ↔ (¬c u = true ↔ c v = true)

theorem SimpleGraph.Walk.three_le_chromaticNumber_of_odd_loop {α : Type u_1} {G : SimpleGraph α} {u : α} (p : G.Walk u u) (hOdd : Odd p.length) : 3 ≤ G.chromaticNumber

def SimpleGraph.cycleGraph.bicoloring_of_even (n : ℕ) (h : Even n) : (cycleGraph n).Coloring Bool

Bicoloring of a cycle graph of even size

theorem SimpleGraph.chromaticNumber_cycleGraph_of_even (n : ℕ) (h : 2 ≤ n) (hEven : Even n) : (cycleGraph n).chromaticNumber = 2

def SimpleGraph.cycleGraph.tricoloring (n : ℕ) (h : 2 ≤ n) : (cycleGraph n).Coloring (Fin 3)

Tricoloring of a cycle graph

theorem SimpleGraph.chromaticNumber_cycleGraph_of_odd (n : ℕ) (h : 2 ≤ n) (hOdd : Odd n) : (cycleGraph n).chromaticNumber = 3

def SimpleGraph.Coloring.completeEquipartiteGraph {r t : ℕ} : (SimpleGraph.completeEquipartiteGraph r t).Coloring (Fin r)

The injection (x₁, x₂) ↦ x₁ is always an r-coloring of a completeEquipartiteGraph r ·.

theorem SimpleGraph.completeEquipartiteGraph_colorable {r t : ℕ} : (completeEquipartiteGraph r t).Colorable r

The completeEquipartiteGraph r t is always r-colorable.

theorem SimpleGraph.two_colorable_iff_forall_loop_even {α : Type u_1} {G : SimpleGraph α} : G.Colorable 2 ↔ ∀ (u : α) (w : G.Walk u u), Even w.length