Concrete colorings of common graphs

This file defines colorings for some common graphs.

Main declarations

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

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

Bicoloring of a path graph

Equations

• SimpleGraph.pathGraph.bicoloring n = SimpleGraph.Coloring.mk (fun (u : Fin n) => decide (↑u % 2 = 0)) ⋯

theorem SimpleGraph.IsBipartite.pathGraph (n : ℕ) : (SimpleGraph.pathGraph n).IsBipartite

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

Equations

• SimpleGraph.pathGraph_two_embedding n h = { toFun := fun (v : Fin 2) => ⟨↑v, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

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

Equations

• SimpleGraph.cycleGraph.bicoloring_of_even n h = SimpleGraph.Coloring.mk (fun (u : Fin n) => decide (↑u % 2 = 0)) ⋯

theorem SimpleGraph.IsBipartite.cycleGraph_of_even {n : ℕ} (h : Even n) : (cycleGraph n).IsBipartite

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

Equations

• SimpleGraph.cycleGraph.tricoloring n h = SimpleGraph.Coloring.mk (fun (u : Fin n) => if ↑u = n - 1 then 2 else ⟨↑u % 2, ⋯⟩) ⋯

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 ·.

Equations

• SimpleGraph.Coloring.completeEquipartiteGraph = { toFun := Prod.fst, map_rel' := ⋯ }

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

The completeEquipartiteGraph r t is always r-colorable.

def SimpleGraph.Coloring.turanGraph (n r : ℕ) [NeZero r] : (turanGraph n r).Coloring (Fin r)

Taking the remainder upon dividing by r produces an r-coloring of turanGraph n r for nonzero r.

Equations

• SimpleGraph.Coloring.turanGraph n r = { toFun := fun (x : Fin n) => Fin.ofNat r ↑x, map_rel' := ⋯ }

@[simp]

theorem SimpleGraph.Coloring.turanGraph_apply (n r : ℕ) [NeZero r] (x✝ : Fin n) : (Coloring.turanGraph n r) x✝ = Fin.ofNat r ↑x✝

theorem SimpleGraph.Colorable.turanGraph (n r : ℕ) [NeZero r] : (turanGraph n r).Colorable r

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