Kempe chains for partial edge colourings

Given a partial proper edge colouring c and two colours a b, the Kempe graph consists of the edges coloured a or b. Swapping the two colours on the connected component of a vertex x produces another partial proper edge colouring, colouring exactly the same edges.

def LeanPool.Vizing.PEC.kempeGraph {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (a b : C) : SimpleGraph V

The subgraph consisting of the edges coloured a or b.

Equations

• c.kempeGraph a b = { Adj := fun (u v : V) => u ≠ v ∧ (c.col u v = some a ∨ c.col u v = some b), symm := ⋯, loopless := ⋯ }

theorem LeanPool.Vizing.PEC.kempeGraph_adj {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} {c : PEC G C} {a b : C} {u v : V} : (c.kempeGraph a b).Adj u v ↔ u ≠ v ∧ (c.col u v = some a ∨ c.col u v = some b)

theorem LeanPool.Vizing.PEC.kempeGraph_adj_of_col {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} {c : PEC G C} {a b : C} {u v : V} (h : c.col u v = some a ∨ c.col u v = some b) : (c.kempeGraph a b).Adj u v

theorem LeanPool.Vizing.PEC.reachable_of_col {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} {c : PEC G C} {a b : C} {x u v : V} (hu : (c.kempeGraph a b).Reachable x u) (h : c.col u v = some a ∨ c.col u v = some b) : (c.kempeGraph a b).Reachable x v

Reachability in the Kempe graph propagates along edges coloured a or b.

noncomputable def LeanPool.Vizing.PEC.kempeSwapFun {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) (x : V) : V → V → Option C

The colour function after swapping a and b on the Kempe component of x.

Equations

• c.kempeSwapFun a b x u v = if (c.kempeGraph a b).Reachable x u ∧ (c.kempeGraph a b).Reachable x v then Option.map (⇑(Equiv.swap a b)) (c.col u v) else c.col u v

theorem LeanPool.Vizing.PEC.kempeSwapFun_of_reachable {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) {x u : V} (hu : (c.kempeGraph a b).Reachable x u) (v : V) : c.kempeSwapFun a b x u v = Option.map (⇑(Equiv.swap a b)) (c.col u v)

theorem LeanPool.Vizing.PEC.kempeSwapFun_of_not_reachable {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) {x u : V} (hu : ¬(c.kempeGraph a b).Reachable x u) (v : V) : c.kempeSwapFun a b x u v = c.col u v

theorem LeanPool.Vizing.PEC.kempeSwapFun_isSome {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) (x u v : V) : c.kempeSwapFun a b x u v = none ↔ c.col u v = none

noncomputable def LeanPool.Vizing.PEC.kempeSwap {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) (x : V) : PEC G C

Swapping the colours a and b on the Kempe component of x.

Equations

• c.kempeSwap a b x = { col := c.kempeSwapFun a b x, col_symm := ⋯, col_adj := ⋯, col_proper := ⋯ }

@[simp]

theorem LeanPool.Vizing.PEC.kempeSwap_col {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) (x : V) : (c.kempeSwap a b x).col = c.kempeSwapFun a b x

theorem LeanPool.Vizing.PEC.extends_kempeSwap {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) (x : V) : c.Extends (c.kempeSwap a b x)

theorem LeanPool.Vizing.PEC.isFree_kempeSwap_of_reachable {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) {x v : V} (hv : (c.kempeGraph a b).Reachable x v) (γ : C) : (c.kempeSwap a b x).IsFree v γ ↔ c.IsFree v ((Equiv.swap a b) γ)

On the Kempe component the free colours get swapped.

theorem LeanPool.Vizing.PEC.isFree_kempeSwap_of_not_reachable {V : Type u_1} {C : Type u_2} [DecidableEq C] {G : SimpleGraph V} (c : PEC G C) (a b : C) {x v : V} (hv : ¬(c.kempeGraph a b).Reachable x v) (γ : C) : (c.kempeSwap a b x).IsFree v γ ↔ c.IsFree v γ

Off the Kempe component the free colours are unchanged.

Degrees in the Kempe graph

theorem LeanPool.Vizing.PEC.kempe_degree_le_two {V : Type u_1} [Fintype V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) (a b : C) [DecidableRel (c.kempeGraph a b).Adj] (v : V) : (c.kempeGraph a b).degree v ≤ 2

theorem LeanPool.Vizing.PEC.kempe_degree_le_one_of_isFree {V : Type u_1} [Fintype V] {C : Type u_2} {G : SimpleGraph V} (c : PEC G C) {a b : C} [DecidableRel (c.kempeGraph a b).Adj] {v : V} {γ : C} (hγ : γ = a ∨ γ = b) (hfree : c.IsFree v γ) : (c.kempeGraph a b).degree v ≤ 1