Edge coloring

DefinitionProper edge coloring#✓fully proved

Let \(G\) be a simple graph on \(V\). An edge labeling \(C\) of \(G\) with colors in \(K\) is a proper edge coloring when any two distinct edges of \(G\) that share a vertex receive different colors: whenever a vertex \(v\) is adjacent to \(w_1\) and to \(w_2\) with \(w_1 \ne w_2\), the edges \(v w_1\) and \(v w_2\) have different colors under \(C\).

def IsProperEdgeColoring {V K : Type*} {G : _root_.SimpleGraph V}
    (C : G.EdgeLabeling K) : Prop :=
  ∀ {v w₁ w₂ : V} (h₁ : G.Adj v w₁) (h₂ : G.Adj v w₂), w₁ ≠ w₂ →
    C ⟨Sym2.mk v w₁, G.mem_edgeSet.mpr h₁⟩ ≠ C ⟨Sym2.mk v w₂, G.mem_edgeSet.mpr h₂⟩

Used by 3

Used byProper colorings of unordered pairs restrict to proper edge colorings · König's line coloring theorem · Vizing's theorem

TheoremKönig's edge coloring theorem for regular bipartite multigraphs#✓fully proved

König's line coloring, regular multigraph case: a d-regular bipartite multigraph (given by endpoint projections) is d-edge-colorable. The proof extracts a perfect matching by Hall's theorem and inducts. Shared API also used by the multigraph Galvin development.

theorem multigraph_regular_color.{u, v} (d : ℕ) (A B : Type u) (E : Type v)
    [Finite A] [DecidableEq A] [Finite B] [DecidableEq B]
    [Fintype E]
    (l : E → A) (r : E → B)
    (hL : ∀ a, (Finset.univ.filter (fun e => l e = a)).card = d)
    (hR : ∀ b, (Finset.univ.filter (fun e => r e = b)).card = d) :
    ∃ C : E → Fin d,
      (∀ e₁ e₂, l e₁ = l e₂ → C e₁ = C e₂ → e₁ = e₂) ∧
      (∀ e₁ e₂, r e₁ = r e₂ → C e₁ = C e₂ → e₁ = e₂)

Used by 1

Used byKönig's edge coloring theorem for bounded-degree bipartite multigraphs

TheoremKönig's edge coloring theorem for bounded-degree bipartite multigraphs#✓fully proved

König's line coloring, bounded-degree multigraph case: a bipartite multigraph of maximum degree at most d is d-edge-colorable. The proof pads both sides with dummy edges to reach the regular case. Shared API also used by the multigraph Galvin development.

theorem multigraph_bounded_color.{u, v} (d : ℕ) (A B : Type u) (E : Type v)
    [Finite A] [DecidableEq A] [Finite B] [DecidableEq B]
    [Fintype E]
    (l : E → A) (r : E → B)
    (hL : ∀ a, (Finset.univ.filter (fun e => l e = a)).card ≤ d)
    (hR : ∀ b, (Finset.univ.filter (fun e => r e = b)).card ≤ d) :
    ∃ C : E → Fin d,
      (∀ e₁ e₂, l e₁ = l e₂ → C e₁ = C e₂ → e₁ = e₂) ∧
      (∀ e₁ e₂, r e₁ = r e₂ → C e₁ = C e₂ → e₁ = e₂)

Uses 1 · Used by 1

Proof usesKönig's edge coloring theorem for regular bipartite multigraphs

Used byKönig's line coloring theorem

TheoremKönig's line coloring theorem#✓fully proved

Every finite bipartite simple graph \(G\) has a proper edge coloring with \(\Delta(G)\) colors, where \(\Delta(G)\) is the maximum degree of \(G\).

Since every proper edge coloring of \(G\) needs at least \(\Delta(G)\) colors, the edge chromatic number of \(G\) equals \(\Delta(G)\).

theorem konig_line_coloring :
    ∀ {V : Type*} (G : _root_.SimpleGraph V) [Fintype V] [DecidableRel G.Adj],
      G.IsBipartite → ∃ C : G.EdgeLabeling (Fin G.maxDegree), IsProperEdgeColoring C

Sources

• D. Konig, Theorie der endlichen und unendlichen Graphen, Akademische Verlagsgesellschaft (1936).

Uses 2

Statement usesProper edge coloring

Proof usesKönig's edge coloring theorem for bounded-degree bipartite multigraphs

DefinitionProper coloring of unordered pairs#✓fully proved

Let \(G\) be a simple graph on \(V\). A map \(c\) that assigns a color in \(K\) to every unordered pair of elements of \(V\) is a proper coloring of unordered pairs for \(G\) when, for all vertices \(x, y, z\) such that \(x\) is adjacent to both \(y\) and \(z\) and \(y \ne z\), the pairs \(\{x, y\}\) and \(\{x, z\}\) receive different colors under \(c\).

Only pairs that are edges of \(G\) are constrained, so the same map \(c\) can be compared across different graphs on \(V\).

def IsProperSym2Coloring {V K : Type*} (G : _root_.SimpleGraph V)
    (c : Sym2 V → K) : Prop :=
  ∀ {x y z : V}, G.Adj x y → G.Adj x z → y ≠ z →
    c (Sym2.mk x y) ≠ c (Sym2.mk x z)

Used by 3

Used byProper colorings of unordered pairs restrict to proper edge colorings · Proper colorings of unordered pairs pass to subgraphs · Vizing's theorem

TheoremProper colorings of unordered pairs restrict to proper edge colorings#✓fully proved

Let \(G\) be a simple graph on \(V\) and let \(c\) assign a color in \(K\) to every unordered pair of elements of \(V\). If \(c\) is a proper coloring of unordered pairs for \(G\), then the edge labeling of \(G\) that gives each edge \(e\) the color \(c(e)\) is a proper edge coloring of \(G\).

theorem isProperEdgeColoring_of_isProperSym2Coloring {V K : Type*}
    {G : _root_.SimpleGraph V} {c : Sym2 V → K}
    (hc : IsProperSym2Coloring G c) :
    IsProperEdgeColoring (fun e : G.edgeSet => c e.val)

Uses 2 · Used by 1

Statement usesProper edge coloring · Proper coloring of unordered pairs

Used byVizing's theorem

TheoremProper colorings of unordered pairs pass to subgraphs#✓fully proved

Let \(G\) and \(H\) be simple graphs on \(V\) such that every edge of \(H\) is an edge of \(G\). If a map \(c\) from unordered pairs of elements of \(V\) to \(K\) is a proper coloring of unordered pairs for \(G\), then it is also a proper coloring of unordered pairs for \(H\).

theorem IsProperSym2Coloring.mono {V K : Type*}
    {G H : _root_.SimpleGraph V}
    {c : Sym2 V → K} (hc : IsProperSym2Coloring G c) (hle : H ≤ G) :
    IsProperSym2Coloring H c

Uses 1

Statement usesProper coloring of unordered pairs

TheoremVizing's theorem#✓fully proved

Let \(G\) be a simple graph on a finite vertex set and let \(\Delta\) be its maximum degree. Then \(G\) has a proper edge coloring with \(\Delta + 1\) colors: there is an assignment of colors from \(\{0, 1, \dots, \Delta\}\) to the edges of \(G\) such that any two distinct edges sharing a vertex receive different colors.

theorem vizing :
    ∀ {V : Type*} (G : _root_.SimpleGraph V) [Fintype V] [DecidableRel G.Adj],
      ∃ C : G.EdgeLabeling (Fin (G.maxDegree + 1)), IsProperEdgeColoring C

Sources

• V. G. Vizing, Diskret. Analiz 3 (1964), 25-30.

Uses 3

Statement usesProper edge coloring

Proof usesProper coloring of unordered pairs · Proper colorings of unordered pairs restrict to proper edge colorings

8 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.