Vizing's theorem, upper bound

Iterating the extension step colours all edges, giving a proper edge colouring with Δ + 1 colours; equivalently, the line graph is (Δ + 1)-colourable.

def LeanPool.Vizing.PEC.empty {V : Type u_1} (G : SimpleGraph V) (C : Type u_3) : PEC G C

The colouring that colours nothing.

Equations

• LeanPool.Vizing.PEC.empty G C = { col := fun (x x_1 : V) => none, col_symm := ⋯, col_adj := ⋯, col_proper := ⋯ }

noncomputable def LeanPool.Vizing.PEC.uncoloured {V : Type u_1} [Fintype V] {C : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] (c : PEC G C) : Finset (V × V)

The set of (ordered) uncoloured edges.

Equations

• c.uncoloured = {p : V × V | G.Adj p.1 p.2 ∧ c.col p.1 p.2 = none}

theorem LeanPool.Vizing.PEC.mem_uncoloured {V : Type u_1} [Fintype V] {C : Type u_2} {G : SimpleGraph V} [DecidableRel G.Adj] (c : PEC G C) (p : V × V) : p ∈ c.uncoloured ↔ G.Adj p.1 p.2 ∧ c.col p.1 p.2 = none

theorem LeanPool.Vizing.PEC.exists_total {V : Type u_1} [Fintype V] {C : Type u_2} [Fintype C] {G : SimpleGraph V} [DecidableRel G.Adj] (hcard : G.maxDegree < Fintype.card C) : ∃ (c : PEC G C), ∀ (u v : V), G.Adj u v → c.col u v ≠ none

Every graph has a proper edge colouring with more than Δ colours.

From total colourings to colourings of the line graph

def LeanPool.Vizing.PEC.edgeOption {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (e : Sym2 V) : Option C

The optional colour on an unordered pair.

Equations

• c.edgeOption e = Sym2.lift ⟨c.col, ⋯⟩ e

@[simp]

theorem LeanPool.Vizing.PEC.edgeOption_mk {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (u v : V) : c.edgeOption s(u, v) = c.col u v

theorem LeanPool.Vizing.PEC.edgeOption_ne_none {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (htot : ∀ (u v : V), G.Adj u v → c.col u v ≠ none) (e : ↑G.edgeSet) : c.edgeOption ↑e ≠ none

Totality supplies a colour on every actual edge, even for an empty palette.

noncomputable def LeanPool.Vizing.PEC.edgeColor {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (htot : ∀ (u v : V), G.Adj u v → c.col u v ≠ none) (e : ↑G.edgeSet) : C

The colour of an actual edge, extracted from totality without a default colour.

Equations

• c.edgeColor htot e = Classical.choose ⋯

theorem LeanPool.Vizing.PEC.edgeOption_eq_some_edgeColor {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (htot : ∀ (u v : V), G.Adj u v → c.col u v ≠ none) (e : ↑G.edgeSet) : c.edgeOption ↑e = some (c.edgeColor htot e)

noncomputable def LeanPool.Vizing.PEC.lineGraphColoring {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (htot : ∀ (u v : V), G.Adj u v → c.col u v ≠ none) : G.lineGraph.Coloring C

A total proper partial colouring gives a colouring of the line graph.

Equations

• c.lineGraphColoring htot = SimpleGraph.Coloring.mk (c.edgeColor htot) ⋯

theorem LeanPool.Vizing.lineGraph_colorable {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.lineGraph.Colorable (G.maxDegree + 1)

Vizing's theorem (upper bound): the line graph of a finite simple graph G is (Δ(G) + 1)-colourable, i.e. G has a proper edge colouring with Δ(G) + 1 colours.

theorem SimpleGraph.lineGraph_chromaticNumber_le_maxDegree_succ {V : Type u_1} [Fintype V] (G : SimpleGraph V) [DecidableRel G.Adj] : G.lineGraph.chromaticNumber ≤ ↑G.maxDegree + 1

Vizing's theorem (upper bound), edge-chromatic-number form: χ'(G) ≤ Δ(G) + 1, phrased via the line graph.