The edge connectivity of a simple graph

Mathlib's SimpleGraph.IsEdgeConnected G k says that G stays preconnected after deleting any set of fewer than k edges. This file introduces the numerical invariant G.edgeConnectivity : ℕ∞, the supremum of the natural thresholds at which G is edge-connected, and bounds it by vertex degrees. As for multigraphs, a graph on at most one vertex has edge connectivity ⊤. It also lifts walks and trails in G with toSubgraph ≤ K to reachability in edge-deleted subgraphs of K.coe, showing without finiteness assumptions that every closed trail (and in particular every cycle) traces a 2-edge-connected subgraph.

The supremum definition and the degree bounds follow the proposal mathlib4#42494, and the invariant matches the multigraph Graph.edgeConnectivity on Graph.ofSimpleGraph.

Main definitions

• SimpleGraph.edgeConnectivity G: the supremum in ℕ∞ of the natural thresholds k at which G is k-edge-connected.

Main results

• SimpleGraph.isEdgeConnected_iff_le_edgeConnectivity: the invariant records exactly the thresholds in ℕ∞ at which G is edge-connected.
• SimpleGraph.edgeConnectivity_le_degree, SimpleGraph.edgeConnectivity_le_minDegree: on at least two vertices, edge connectivity is at most every degree, hence at most the minimum degree.
• SimpleGraph.edgeConnectivity_eq_top_iff: on a finite vertex type, edge connectivity is ⊤ exactly when there is at most one vertex.
• SimpleGraph.Walk.reachable_deleteEdges_coe, SimpleGraph.Walk.IsTrail.reachable_deleteEdges_coe_or_reachable_deleteEdges_coe: lifting walks and trails in G with toSubgraph ≤ K to reachability in edge-deleted subgraphs of K.coe.
• SimpleGraph.Walk.IsTrail.isEdgeConnected_two_toSubgraph, SimpleGraph.Walk.IsCycle.isEdgeConnected_two_toSubgraph: the subgraph traced by a closed trail (in particular, a cycle) is 2-edge-connected.

noncomputable def SimpleGraph.edgeConnectivity {V : Type u_1} (G : SimpleGraph V) : ℕ∞

The edge connectivity of a simple graph: the supremum in ℕ∞ of the natural thresholds k at which it is k-edge-connected. It is ⊤ when there is at most one vertex.

theorem SimpleGraph.isEdgeConnected_iff_le_edgeConnectivity {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} : G.IsEdgeConnected k ↔ k ≤ G.edgeConnectivity

Edge connectivity records exactly the thresholds at which the graph is edge-connected.

theorem SimpleGraph.edgeConnectivity_mono {V : Type u_1} {G H : SimpleGraph V} (hGH : G ≤ H) : G.edgeConnectivity ≤ H.edgeConnectivity

Edge connectivity is monotone in the graph.

@[simp]

theorem SimpleGraph.edgeConnectivity_eq_top_of_subsingleton {V : Type u_1} {G : SimpleGraph V} [Subsingleton V] : G.edgeConnectivity = ⊤

A graph on at most one vertex has edge connectivity ⊤.

Degree bounds

theorem SimpleGraph.edgeConnectivity_le_degree {V : Type u_1} {G : SimpleGraph V} [Nontrivial V] (u : V) [Fintype ↑(G.neighborSet u)] : G.edgeConnectivity ≤ ↑(G.degree u)

On at least two vertices, edge connectivity is at most the degree of every vertex of finite degree.

theorem SimpleGraph.IsEdgeConnected.le_minDegree {V : Type u_1} {G : SimpleGraph V} {k : ℕ∞} [Fintype V] [DecidableRel G.Adj] [Nontrivial V] (h : G.IsEdgeConnected k) : k ≤ ↑G.minDegree

On a finite vertex type with at least two vertices, a k-edge-connected graph has minimum degree at least k.

theorem SimpleGraph.edgeConnectivity_le_minDegree {V : Type u_1} {G : SimpleGraph V} [Fintype V] [DecidableRel G.Adj] [Nontrivial V] : G.edgeConnectivity ≤ ↑G.minDegree

On a finite vertex type with at least two vertices, edge connectivity is at most the minimum degree.

theorem SimpleGraph.edgeConnectivity_eq_top_iff {V : Type u_1} {G : SimpleGraph V} [Finite V] : G.edgeConnectivity = ⊤ ↔ Subsingleton V

On a finite vertex type, edge connectivity is ⊤ exactly when there is at most one vertex.

Subgraph walks and cycle connectivity

theorem SimpleGraph.Walk.reachable_deleteEdges_coe {V : Type u_1} {G : SimpleGraph V} {K : G.Subgraph} {s : Set (Sym2 ↑K.verts)} {u v : V} (p : G.Walk u v) (hpK : p.toSubgraph ≤ K) (hps : ∀ e ∈ s, Sym2.map Subtype.val e ∉ p.edges) : (K.coe.deleteEdges s).Reachable ⟨u, ⋯⟩ ⟨v, ⋯⟩

If a walk p in G has p.toSubgraph ≤ K and uses none of the underlying edges of s : Set (Sym2 K.verts), then its endpoints are reachable in K.coe.deleteEdges s.

theorem SimpleGraph.Walk.IsTrail.reachable_deleteEdges_coe_or_reachable_deleteEdges_coe {V : Type u_1} {G : SimpleGraph V} {K : G.Subgraph} {u v : V} {p : G.Walk u v} (hp : p.IsTrail) (hpK : p.toSubgraph ≤ K) (f : Sym2 ↑K.verts) {w : V} (hw : w ∈ p.support) : (K.coe.deleteEdges {f}).Reachable ⟨w, ⋯⟩ ⟨u, ⋯⟩ ∨ (K.coe.deleteEdges {f}).Reachable ⟨w, ⋯⟩ ⟨v, ⋯⟩

Along a trail p : G.Walk u v with p.toSubgraph ≤ K, deleting any single edge f of K.coe leaves every vertex on p reachable from u or from v in K.coe.deleteEdges {f}.

theorem SimpleGraph.Walk.IsTrail.isEdgeConnected_two_toSubgraph {V : Type u_1} {G : SimpleGraph V} {u : V} {c : G.Walk u u} (hc : c.IsTrail) : c.toSubgraph.coe.IsEdgeConnected 2

The subgraph traced by any closed trail in a simple graph is 2-edge-connected, with no finiteness assumption.

theorem SimpleGraph.Walk.IsCycle.isEdgeConnected_two_toSubgraph {V : Type u_1} {G : SimpleGraph V} {u : V} {c : G.Walk u u} (hc : c.IsCycle) : c.toSubgraph.coe.IsEdgeConnected 2

The subgraph traced by any cycle in a simple graph is 2-edge-connected, with no finiteness assumption.