Cut vertices of multigraphs

A vertex of a multigraph is a cut vertex when deleting it separates two other vertices that were previously reachable. This definition is insensitive to loops and parallel edges, but is phrased in the native walk-based connectivity API for Graph.

The map Graph.deleteVertexComponentMap sends each component after deleting a vertex to its original component. A vertex is a cut vertex exactly when this map is not injective. With the relevant component types finite, this gives the component-count characterization Graph.isCutVertex_iff_componentCount_lt_componentCount_deleteVerts: deleting a cut vertex increases the number of connected components, while deleting a non-cut vertex does not increase it.

The definition follows R. Diestel, Graph Theory, 5th ed., Graduate Texts in Mathematics 173, Springer, 2017, Section 1.4; the other characterizations are proved here.

Definition and component map

def Graph.IsCutVertex {α : Type u} {β : Type v} (G : Graph α β) (v : α) : Prop

A vertex is a cut vertex if deleting it separates two other vertices that were reachable in the original graph.

theorem Graph.isCutVertex_def {α : Type u} {β : Type v} {G : Graph α β} {v : α} : G.IsCutVertex v ↔ ∃ (u : α) (w : α), u ≠ v ∧ w ≠ v ∧ G.Reachable u w ∧ ¬(G.deleteVerts {v}).Reachable u w

The reachability characterization of a cut vertex.

noncomputable def Graph.deleteVertexComponentMap {α : Type u} {β : Type v} (G : Graph α β) (v : α) : (G.deleteVerts {v}).ConnectedComponent → G.ConnectedComponent

The map from components after deleting v to components of the original graph.

@[simp]

theorem Graph.deleteVertexComponentMap_connectedComponentOf {α : Type u} {β : Type v} (G : Graph α β) (v x : α) (hx : x ∈ (G.deleteVerts {v}).vertexSet) : G.deleteVertexComponentMap v ((G.deleteVerts {v}).connectedComponentOf x hx) = G.connectedComponentOf x ⋯

The component of a vertex after deletion maps to its component in the original graph.

theorem Graph.exists_deleteVertexComponentMap_eq_of_mem {α : Type u} {β : Type v} {G : Graph α β} {v : α} {C : G.ConnectedComponent} {z : α} (hzC : z ∈ (↑C).vertexSet) (hzv : z ≠ v) : ∃ (D : (G.deleteVerts {v}).ConnectedComponent), G.deleteVertexComponentMap v D = C

A component containing a vertex other than v lies in the range of the component map after deleting v.

theorem Graph.isCutVertex_iff_not_injective_deleteVertexComponentMap {α : Type u} {β : Type v} {G : Graph α β} {v : α} : G.IsCutVertex v ↔ ¬Function.Injective (G.deleteVertexComponentMap v)

A vertex is a cut vertex exactly when two components created by its deletion map to the same original component.

theorem Graph.deleteVertexComponentMap_surjective {α : Type u} {β : Type v} {G : Graph α β} {v : α} (h : ∃ (u : α), u ≠ v ∧ G.Reachable u v) : Function.Surjective (G.deleteVertexComponentMap v)

The component map after deleting v is surjective if another vertex is reachable from v.

theorem Graph.IsCutVertex.exists_ne_and_reachable {α : Type u} {β : Type v} {G : Graph α β} {v : α} (h : G.IsCutVertex v) : ∃ (u : α), u ≠ v ∧ G.Reachable u v

A cut vertex is reachable from one of the two vertices it separates.

theorem Graph.IsCutVertex.mem_vertexSet {α : Type u} {β : Type v} {G : Graph α β} {v : α} (h : G.IsCutVertex v) : v ∈ G.vertexSet

A cut vertex is an actual vertex of the graph.

theorem Graph.not_isCutVertex_of_compl_subsingleton {α : Type u} {β : Type v} (G : Graph α β) (v : α) (hsub : (G.vertexSet \ {v}).Subsingleton) : ¬G.IsCutVertex v

A vertex is not a cut vertex when all other actual vertices form a subsingleton set.

Component counts

theorem Graph.isCutVertex_iff_componentCount_lt_componentCount_deleteVerts {α : Type u} {β : Type v} {G : Graph α β} {v : α} [Finite (G.deleteVerts {v}).ConnectedComponent] : G.IsCutVertex v ↔ G.componentCount < (G.deleteVerts {v}).componentCount

Cut vertices by component counts. If deletion leaves finitely many components, a vertex is a cut vertex exactly when deleting it strictly increases the number of connected components.

theorem Graph.componentCount_deleteVerts_singleton_le_of_not_isCutVertex {α : Type u} {β : Type v} {G : Graph α β} {v : α} (h : ¬G.IsCutVertex v) : (G.deleteVerts {v}).componentCount ≤ G.componentCount

Deleting a non-cut vertex cannot increase the number of connected components.