Line-graph colourings and decompositions into matchings

The vertices of Mathlib's line graph are actual graph edges. A colour class therefore defines a matching subgraph with precisely the incident vertices, not a spanning subgraph with isolated vertices. Conversely, a partition of the edges into matching subgraphs defines a proper colouring of the line graph.

Neither construction requires a finite graph, a finite palette, or a default colour. Empty classes are allowed. These are classical equivalences of representations, not new graph-theoretic bounds.

structure SimpleGraph.MatchingDecomposition {V : Type u_1} (G : SimpleGraph V) (C : Type u_3) : Type (max u_1 u_3)

A palette-indexed partition of the actual edges into Mathlib matchings. Distinct matchings may share vertices, but every edge belongs to exactly one.

• matching : C → G.Subgraph

  The matching assigned to a colour; it may be empty.

• isMatching (c : C) : (self.matching c).IsMatching

  Each colour class is a matching with no isolated vertices.

• partition (e : ↑G.edgeSet) : ∃! c : C, ↑e ∈ (self.matching c).edgeSet

  Every actual edge has a unique colour class.

theorem SimpleGraph.MatchingDecomposition.ext_iff {V : Type u_1} {G : SimpleGraph V} {C : Type u_3} {x y : G.MatchingDecomposition C} : x = y ↔ x.matching = y.matching

theorem SimpleGraph.MatchingDecomposition.ext {V : Type u_1} {G : SimpleGraph V} {C : Type u_3} {x y : G.MatchingDecomposition C} (matching : x.matching = y.matching) : x = y

def SimpleGraph.Coloring.edgeMatching {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (K : G.lineGraph.Coloring C) (c : C) : G.Subgraph

The subgraph formed by the edges with one specified line-graph colour.

Equations

• K.edgeMatching c = { verts := {v : V | ∃ (w : V) (h : G.Adj v w), K ⟨s(v, w), h⟩ = c}, Adj := fun (v w : V) => ∃ (h : G.Adj v w), K ⟨s(v, w), h⟩ = c, adj_sub := ⋯, edge_vert := ⋯, symm := ⋯ }

@[simp]

theorem SimpleGraph.Coloring.mem_edgeMatching_edgeSet {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (K : G.lineGraph.Coloring C) (c : C) (e : ↑G.edgeSet) : ↑e ∈ (K.edgeMatching c).edgeSet ↔ K e = c

Membership in a matching class is exactly equality of the edge's colour.

theorem SimpleGraph.Coloring.edgeMatching_isMatching {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (K : G.lineGraph.Coloring C) (c : C) : (K.edgeMatching c).IsMatching

Edges of the same colour have unique neighbours at each incident vertex.

def SimpleGraph.Coloring.matchingDecomposition {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (K : G.lineGraph.Coloring C) : G.MatchingDecomposition C

A line-graph colouring partitions the original edges into matching subgraphs.

Equations

• K.matchingDecomposition = { matching := K.edgeMatching, isMatching := ⋯, partition := ⋯ }

noncomputable def SimpleGraph.MatchingDecomposition.edgeColour {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) (e : ↑G.edgeSet) : C

The unique class containing an actual edge. No default colour is required.

Equations

• D.edgeColour e = Classical.choose ⋯

theorem SimpleGraph.MatchingDecomposition.mem_edgeColour_matching {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) (e : ↑G.edgeSet) : ↑e ∈ (D.matching (D.edgeColour e)).edgeSet

The chosen colour class contains the edge.

theorem SimpleGraph.MatchingDecomposition.mem_matching_iff {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) (e : ↑G.edgeSet) (c : C) : ↑e ∈ (D.matching c).edgeSet ↔ D.edgeColour e = c

The edge belongs to a specified class precisely when it has that colour.

noncomputable def SimpleGraph.MatchingDecomposition.edgeEquivSigma {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) : ↑G.edgeSet ≃ (c : C) × ↑(D.matching c).edgeSet

Each original edge is equivalent to its colour and its edge in that matching.

Equations

• D.edgeEquivSigma = { toFun := fun (e : ↑G.edgeSet) => ⟨D.edgeColour e, ⟨↑e, ⋯⟩⟩, invFun := fun (e : (c : C) × ↑(D.matching c).edgeSet) => ⟨↑e.snd, ⋯⟩, left_inv := ⋯, right_inv := ⋯ }

theorem SimpleGraph.MatchingDecomposition.edgeSet_disjoint {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) {a b : C} (hab : a ≠ b) : Disjoint (D.matching a).edgeSet (D.matching b).edgeSet

The edge classes of distinct colours are disjoint, even when their vertices overlap.

theorem SimpleGraph.MatchingDecomposition.iUnion_edgeSet {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) : ⋃ (c : C), (D.matching c).edgeSet = G.edgeSet

The union of all matching classes is exactly the original edge set.

noncomputable def SimpleGraph.MatchingDecomposition.lineGraphColoring {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) : G.lineGraph.Coloring C

A decomposition into matchings gives a proper colouring of the line graph.

Equations

• D.lineGraphColoring = SimpleGraph.Coloring.mk D.edgeColour ⋯

@[simp]

theorem SimpleGraph.MatchingDecomposition.edgeMatching_lineGraphColoring {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) (c : C) : D.lineGraphColoring.edgeMatching c = D.matching c

Converting a decomposition to a colouring preserves each matching exactly.

@[simp]

theorem SimpleGraph.MatchingDecomposition.matchingDecomposition_lineGraphColoring {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (D : G.MatchingDecomposition C) : D.lineGraphColoring.matchingDecomposition = D

The decomposition-to-colouring-to-decomposition round trip is exact.

@[simp]

theorem SimpleGraph.Coloring.lineGraphColoring_matchingDecomposition {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} (K : G.lineGraph.Coloring C) : K.matchingDecomposition.lineGraphColoring = K

The colouring-to-decomposition-to-colouring round trip is exact.

noncomputable def SimpleGraph.lineGraphColoringEquivMatchingDecomposition {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} : G.lineGraph.Coloring C ≃ G.MatchingDecomposition C

Proper line-graph colourings are equivalent to palette-indexed matching partitions.

Equations

• One or more equations did not get rendered due to their size.

theorem SimpleGraph.nonempty_lineGraphColoring_iff_matchingDecomposition {V : Type u_1} {C : Type u_2} {G : SimpleGraph V} : Nonempty (G.lineGraph.Coloring C) ↔ Nonempty (G.MatchingDecomposition C)

Existence of a colouring on any palette is equivalent to a matching partition.

theorem SimpleGraph.lineGraph_colorable_iff_matchingDecomposition {V : Type u_1} {G : SimpleGraph V} (k : ℕ) : G.lineGraph.Colorable k ↔ Nonempty (G.MatchingDecomposition (Fin k))

Edge colourability with at most k colours is equivalent to a decomposition into k matchings; unused colours are represented by empty matchings.