LineGraph

Main definitions

• SimpleGraph.lineGraph is the line graph of a simple graph G, with vertices as the edges of G and two vertices of the line graph adjacent if the corresponding edges share a vertex in G.

Tags

line graph

def SimpleGraph.lineGraph {V : Type u_1} (G : SimpleGraph V) : SimpleGraph ↑G.edgeSet

The line graph of a simple graph G has its vertex set as the edges of G, and two vertices of the line graph are adjacent if the corresponding edges share a vertex in G.

Equations

• G.lineGraph = { Adj := fun (e₁ e₂ : ↑G.edgeSet) => e₁ ≠ e₂ ∧ (↑↑e₁ ∩ ↑↑e₂).Nonempty, symm := ⋯, loopless := ⋯ }

theorem SimpleGraph.lineGraph_adj_iff_exists {V : Type u_1} {G : SimpleGraph V} {e₁ e₂ : ↑G.edgeSet} : G.lineGraph.Adj e₁ e₂ ↔ e₁ ≠ e₂ ∧ ∃ v ∈ ↑e₁, v ∈ ↑e₂

@[simp]

theorem SimpleGraph.lineGraph_bot {V : Type u_1} : ⊥.lineGraph = ⊥

def SimpleGraph.Copy.toLineGraphEmbedding {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G.Copy G') : G.lineGraph ↪g G'.lineGraph

Lift a copy between graphs to an embedding between their line graphs

Equations

• f.toLineGraphEmbedding = { toFun := fun (e : ↑G.edgeSet) => ⟨Sym2.map ⇑f ↑e, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }

theorem SimpleGraph.IsIndContained.lineGraph {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (h : G.IsIndContained G') : G.lineGraph.IsIndContained G'.lineGraph

theorem SimpleGraph.IsContained.isIndContained_lineGraph {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (h : G.IsContained G') : G.lineGraph.IsIndContained G'.lineGraph

def SimpleGraph.Copy.lineGraph {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G.Copy G') : G.lineGraph.Copy G'.lineGraph

Lift a copy between graphs to a copy between their line graphs

Equations

• f.lineGraph = f.toLineGraphEmbedding.toCopy

theorem SimpleGraph.IsContained.lineGraph {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (h : G.IsContained G') : G.lineGraph.IsContained G'.lineGraph

def SimpleGraph.Iso.lineGraph {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G ≃g G') : G.lineGraph ≃g G'.lineGraph

Lift an isomorphism between graphs to an isomorphism between their line graphs

Equations

• f.lineGraph = { toFun := ⇑f.toCopy.lineGraph, invFun := ⇑f.symm.toCopy.lineGraph, left_inv := ⋯, right_inv := ⋯, map_rel_iff' := ⋯ }

theorem SimpleGraph.map_lineGraph_le_of_le {V : Type u_1} {G G' : SimpleGraph V} (h : G ≤ G') : SimpleGraph.map (⇑(Function.Embedding.subtype fun (x : Sym2 V) => x ∈ G.edgeSet)) G.lineGraph ≤ SimpleGraph.map (⇑(Function.Embedding.subtype fun (x : Sym2 V) => x ∈ G'.edgeSet)) G'.lineGraph

@[deprecated SimpleGraph.map_lineGraph_le_of_le (since := "2026-03-26")]

theorem SimpleGraph.IsSubgraph.lineGraph {V : Type u_1} {G G' : SimpleGraph V} (h : G ≤ G') : SimpleGraph.map (⇑(Function.Embedding.subtype fun (x : Sym2 V) => x ∈ G.edgeSet)) G.lineGraph ≤ SimpleGraph.map (⇑(Function.Embedding.subtype fun (x : Sym2 V) => x ∈ G'.edgeSet)) G'.lineGraph

Alias of SimpleGraph.map_lineGraph_le_of_le.