Partial edge colourings

Basic definitions and extension operations for the fan-and-Kempe proof of Vizing's theorem.

Partial edge colourings

Basic framework for Vizing's theorem: a partial proper edge colouring of a simple graph G is a symmetric partial function on pairs of vertices, defined only on edges, such that two distinct edges sharing a vertex never receive the same colour.

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

A partial proper edge colouring of G with colours in C.

• col : V → V → Option C

  The colour of the edge u v, if it is coloured.

• col_symm (u v : V) : self.col u v = self.col v u
• col_adj {u v : V} {γ : C} : self.col u v = some γ → G.Adj u v
• col_proper {u v w : V} {γ : C} : self.col u v = some γ → self.col u w = some γ → v = w

def LeanPool.Vizing.PEC.IsFree {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (v : V) (γ : C) : Prop

A colour is free at a vertex if no edge at that vertex carries it.

Equations

• c.IsFree v γ = ∀ (u : V), c.col v u ≠ some γ

def LeanPool.Vizing.PEC.Extends {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c c' : PEC G C) : Prop

c' colours at least the edges that c colours.

Equations

• c.Extends c' = ∀ (u v : V), c.col u v ≠ none → c'.col u v ≠ none

theorem LeanPool.Vizing.PEC.Extends.rfl' {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) : c.Extends c

theorem LeanPool.Vizing.PEC.Extends.trans {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} {c₁ c₂ c₃ : PEC G C} (h₁ : c₁.Extends c₂) (h₂ : c₂.Extends c₃) : c₁.Extends c₃

theorem LeanPool.Vizing.PEC.col_self {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (u : V) : c.col u u = none

theorem LeanPool.Vizing.PEC.exists_free {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} [Fintype V] [Fintype C] [DecidableRel G.Adj] (c : PEC G C) (hcard : G.maxDegree < Fintype.card C) (v : V) : ∃ (γ : C), c.IsFree v γ

At every vertex there is a free colour, provided there are more colours than the maximum degree.

Updating a single edge

def LeanPool.Vizing.PEC.updFun {V : Type u_1} [DecidableEq V] {C : Type u_2} (f : V → V → Option C) (x y : V) (o : Option C) : V → V → Option C

Change the colour of the edge x y (in both directions) to o.

Equations

• LeanPool.Vizing.PEC.updFun f x y o u v = if u = x ∧ v = y ∨ u = y ∧ v = x then o else f u v

theorem LeanPool.Vizing.PEC.updFun_of_ne {V : Type u_1} [DecidableEq V] {C : Type u_2} {f : V → V → Option C} {x y u v : V} (o : Option C) (h : ¬(u = x ∧ v = y ∨ u = y ∧ v = x)) : updFun f x y o u v = f u v

@[simp]

theorem LeanPool.Vizing.PEC.updFun_left {V : Type u_1} [DecidableEq V] {C : Type u_2} {f : V → V → Option C} {x y : V} (o : Option C) : updFun f x y o x y = o

@[simp]

theorem LeanPool.Vizing.PEC.updFun_right {V : Type u_1} [DecidableEq V] {C : Type u_2} {f : V → V → Option C} {x y : V} (o : Option C) : updFun f x y o y x = o

def LeanPool.Vizing.PEC.setEdge {V : Type u_1} [DecidableEq V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) {x y : V} (γ : C) (hadj : G.Adj x y) (hx : c.IsFree x γ) (hy : c.IsFree y γ) : PEC G C

Colour the (possibly already coloured) edge x y with a colour free at both endpoints.

Equations

• c.setEdge γ hadj hx hy = { col := LeanPool.Vizing.PEC.updFun c.col x y (some γ), col_symm := ⋯, col_adj := ⋯, col_proper := ⋯ }

@[simp]

theorem LeanPool.Vizing.PEC.setEdge_col {V : Type u_1} [DecidableEq V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) {x y : V} (γ : C) (hadj : G.Adj x y) (hx : c.IsFree x γ) (hy : c.IsFree y γ) : (c.setEdge γ hadj hx hy).col = updFun c.col x y (some γ)

theorem LeanPool.Vizing.PEC.setEdge_col_of_ne_left {V : Type u_1} [DecidableEq V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) {x y : V} (γ : C) (hadj : G.Adj x y) (hx : c.IsFree x γ) (hy : c.IsFree y γ) {w : V} (hwx : w ≠ x) (hwy : w ≠ y) (u : V) : (c.setEdge γ hadj hx hy).col w u = c.col w u

theorem LeanPool.Vizing.PEC.isFree_setEdge_of_ne {V : Type u_1} [DecidableEq V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) {x y : V} (γ : C) (hadj : G.Adj x y) (hx : c.IsFree x γ) (hy : c.IsFree y γ) {w : V} (hwx : w ≠ x) (hwy : w ≠ y) (δ : C) : (c.setEdge γ hadj hx hy).IsFree w δ ↔ c.IsFree w δ

theorem LeanPool.Vizing.PEC.extends_setEdge {V : Type u_1} [DecidableEq V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) {x y : V} (γ : C) (hadj : G.Adj x y) (hx : c.IsFree x γ) (hy : c.IsFree y γ) : c.Extends (c.setEdge γ hadj hx hy)