Line-graph colourings as literal proper edge colourings

Any colouring of the line graph induces a proper colour assignment on G.edgeFinset. This connects the fan proof of Vizing's theorem to equitable recolouring on a fixed finite palette.

noncomputable def LeanPool.Vizing.LineGraphColouring.edgeColourOfLineGraph {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [Inhabited Color] {G : SimpleGraph V} [DecidableRel G.Adj] (C : G.lineGraph.Coloring Color) : Sym2 V → Color

Extend a line-graph colouring to all unordered pairs; values off the literal edge finset are irrelevant to ProperOn.

Equations

• LeanPool.Vizing.LineGraphColouring.edgeColourOfLineGraph C e = if he : e ∈ G.edgeFinset then C ⟨e, ⋯⟩ else default

theorem LeanPool.Vizing.LineGraphColouring.properOn_of_lineGraph_colouring {V : Type u_1} {Color : Type u_2} [Fintype V] [DecidableEq V] [Inhabited Color] {G : SimpleGraph V} [DecidableRel G.Adj] (C : G.lineGraph.Coloring Color) : ColourClasses.ProperOn G.edgeFinset (edgeColourOfLineGraph C)

A line-graph colouring is a proper colour assignment on literal graph edges in the exact ColourClasses.ProperOn sense.

noncomputable def LeanPool.Vizing.LineGraphColouring.vizingEdgeColour {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : Sym2 V → Fin (G.maxDegree + 1)

The colour assignment supplied by Vizing's theorem, extended to unordered pairs.

Equations

• LeanPool.Vizing.LineGraphColouring.vizingEdgeColour G = LeanPool.Vizing.LineGraphColouring.edgeColourOfLineGraph (Classical.choice ⋯)

theorem LeanPool.Vizing.LineGraphColouring.properOn_vizingEdgeColour {V : Type u_1} [Fintype V] [DecidableEq V] (G : SimpleGraph V) [DecidableRel G.Adj] : ColourClasses.ProperOn G.edgeFinset (vizingEdgeColour G)