Components and shortest paths

The two prerequisites of the relative ear decomposition (lem:relative-ear) that no earlier module builds: the component of a vertex, and a shortest walk between two vertices. Both are then spent on the geometric heart of that lemma — a component of G - S has two distinct neighbours in S, and a path between two of them whose interior lies outside S.

The component is a comprehension

G.component u = {v | G.Reaches u v}, exactly as connectedComponentIn collects the points a space reaches. Nothing restricts the comprehension to V(G): the empty walk already demands a vertex of the graph (Graph.IsWalk.nil), so G.Reaches u v carries v ∈ V(G) with it, and a clause v ∈ V(G) ∧ … would be redundant noise at every use site. When u ∉ V(G) the component is empty, which is the convention that makes the covering statement Graph.iUnion_component true with no side condition.

Reachability is an equivalence relation on V(G), so the component is closed under Reaches, two components are equal or disjoint, and the components cover V(G). The one statement that is not pure equivalence-relation bookkeeping is that the induced subgraph on a component is connected: a walk between two vertices of a component never leaves it (Graph.IsWalk.walkVertices_subset_component), so it is already a walk of the induced subgraph, by Graph.IsWalk.anti.

Shortest walks need no finiteness

The set of lengths of walks from u to v is a nonempty set of naturals, so it has a least element — Nat.find, with no Graph.Finite hypothesis anywhere. That is worth noticing: the blueprint says "in a finite graph", but finiteness is used there only to terminate the ear process, never to find one shortest path.

A minimum-length walk is automatically a path (Graph.IsWalk.isPath_of_minLength). The proof is the induction of Graph.IsWalk.contains_path run once more, with lengths attached: if the step's source were revisited later, Graph.IsPath.from_visited would cut the tail down to a strictly shorter walk with the same ends, and a path's edge list repeats nothing (Graph.IsPath.nodup), so the cut piece really is no longer than what it came from (List.subperm_of_subset).

The two neighbours, without a contradiction

The blueprint argues by contradiction: "otherwise its unique neighbour would be a cut vertex". Here the two neighbours are constructed, in the shape Graph.IsTwoConnected.no_bridge already uses. A walk from the component out to a vertex of S crosses the boundary (Graph.IsWalk.crossing), and the crossing edge's far end is in S — because a neighbour outside S would still be in the component. That is the first neighbour c. For the second, delete c: the big graph is still connected, so the same crossing argument runs inside G - c, and its crossing edge's far end is a neighbour that is not c.

Two distinct vertices of S are needed, and used exactly once: the walk of the second step must aim at a vertex of S other than c. In the application S is the vertex set of a 2-connected subgraph, which has three.

Blueprint

• Graph.component, Graph.induce_component_connected — "a component L of G - V(H₀)" in the proof of lem:relative-ear.
• Graph.exists_minLength_isPath — "a shortest path through L", same proof.
• Graph.IsTwoConnected.component_two_neighbors — "if a component L of G - V(H₀) contains a vertex, it has at least two distinct neighbors in H₀; otherwise its unique neighbor would be a cut vertex of G".
• Graph.IsTwoConnected.exists_path_through_component — "a shortest path through L between two such neighbors is an ear": a path of G between two distinct vertices of S, whose every other vertex is outside S, which has at least one such vertex, and each of whose edges has an end outside S. The word ear is not used here and nothing about ears is assumed; this is the raw path that a consumer recognises as one.

Namespace

Root Graph, as fixed by Schoenflies/Graph/Walk.lean.

Components

def Graph.component {α : Type u_1} {β : Type u_2} (G : Graph α β) (u : α) : Set α

The component of u in G: the vertices u reaches. A comprehension over the vertices, not an indexed union of connected subgraphs; the membership test is Graph.Reaches itself, which is why every closure property below is one line of the reachability API.

No v ∈ V(G) clause: Graph.Reaches already carries it, since the empty walk demands a vertex of the graph. For u ∉ V(G) the component is empty.

Equations

• G.component u = {v : α | G.Reaches u v}

theorem Graph.mem_component_iff {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} : v ∈ G.component u ↔ G.Reaches u v

theorem Graph.component_subset_vertexSet {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} : G.component u ⊆ G.vertexSet

theorem Graph.mem_component_self {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∈ G.vertexSet) : u ∈ G.component u

theorem Graph.component_nonempty {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∈ G.vertexSet) : (G.component u).Nonempty

theorem Graph.component_eq_empty {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∉ G.vertexSet) : G.component u = ∅

A vertex the graph does not have reaches nothing.

theorem Graph.mem_component_of_reaches {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v w : α} (hv : v ∈ G.component u) (h : G.Reaches v w) : w ∈ G.component u

A component is closed under reachability, which is the property every consumer uses: whatever a vertex of the component reaches is in the component.

theorem Graph.mem_component_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {e : β} (hx : x ∈ G.component u) (hl : G.IsLink e x y) : y ∈ G.component u

A component is closed under taking an edge.

theorem Graph.mem_component_comm {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} : v ∈ G.component u ↔ u ∈ G.component v

theorem Graph.component_eq_of_mem {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (hv : v ∈ G.component u) : G.component v = G.component u

A vertex of a component has the same component.

theorem Graph.component_eq_or_disjoint {α : Type u_1} {β : Type u_2} {G : Graph α β} (u v : α) : G.component u = G.component v ∨ Disjoint (G.component u) (G.component v)

Two components are equal or disjoint.

theorem Graph.iUnion_component {α : Type u_1} {β : Type u_2} (G : Graph α β) : ⋃ u ∈ G.vertexSet, G.component u = G.vertexSet

The components cover the vertex set.

The subgraph induced on a component

theorem Graph.induce_component_le {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} : G.induce (G.component u) ≤ G

theorem Graph.mem_vertexSet_induce_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} : v ∈ (G.induce (G.component u)).vertexSet ↔ G.Reaches u v

theorem Graph.IsWalk.walkVertices_subset_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {W : List β} (h : G.IsWalk x W y) (hx : x ∈ G.component u) : G.walkVertices x W ⊆ G.component u

A walk out of a component stays in it: every vertex it visits is reachable from the component's base point, one step at a time.

theorem Graph.IsWalk.induce_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {u x y : α} {W : List β} (h : G.IsWalk x W y) (hx : x ∈ G.component u) : (G.induce (G.component u)).IsWalk x W y

A walk that starts in a component is a walk of the subgraph induced on it. Both ends of each of its edges are vertices it visits, so the edges survive the induction.

theorem Graph.induce_component_connected {α : Type u_1} {β : Type u_2} {G : Graph α β} {u : α} (hu : u ∈ G.vertexSet) : (G.induce (G.component u)).Connected

The subgraph induced on a component is connected, with the base point as hub.

Shortest walks and shortest paths

theorem Graph.exists_minLength_isWalk {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Reaches u v) : ∃ (W : List β), G.IsWalk u W v ∧ ∀ (W' : List β), G.IsWalk u W' v → W.length ≤ W'.length

A shortest walk exists between any two vertices one of which reaches the other: the lengths of such walks form a nonempty set of naturals. No finiteness is needed.

theorem Graph.IsWalk.isPath_of_minLength {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} (h : G.IsWalk u W v) (hmin : ∀ (W' : List β), G.IsWalk u W' v → W.length ≤ W'.length) : G.IsPath u W v

A shortest walk is a path. If the vertex a step departs from were visited again, the tail could be cut there (Graph.IsPath.from_visited) and the result would be a strictly shorter walk with the same ends — strictly, because a path repeats no edge and the cut piece is a sublist-up-to-permutation of what it came from.

theorem Graph.exists_minLength_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Reaches u v) : ∃ (P : List β), G.IsPath u P v ∧ ∀ (W : List β), G.IsWalk u W v → P.length ≤ W.length

A shortest path exists: among all walks between two vertices, one of least length, and it is a path. This is the blueprint's "shortest path".

theorem Graph.Connected.exists_minLength_isPath {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} (h : G.Connected) (hu : u ∈ G.vertexSet) (hv : v ∈ G.vertexSet) : ∃ (P : List β), G.IsPath u P v ∧ ∀ (W : List β), G.IsWalk u W v → P.length ≤ W.length

Components of a vertex deletion

From here on S : Set α is a set of vertices to be deleted, and the component in question is one of G.deleteVerts S. Only two facts about the deletion are used, and both are about where its walks can go.

theorem Graph.IsWalk.walkVertices_subset_of_deleteVerts {α : Type u_1} {β : Type u_2} {G : Graph α β} {u v : α} {W : List β} {S : Set α} (h : (G.deleteVerts S).IsWalk u W v) : G.walkVertices u W ⊆ G.vertexSet \ S

A walk of G - S visits only vertices of G outside S — computed in G, which is the form the freshness clause of a path of G reads.

theorem Graph.component_deleteVerts_subset {α : Type u_1} {β : Type u_2} {G : Graph α β} {x : α} {S : Set α} : (G.deleteVerts S).component x ⊆ G.vertexSet \ S

The component of G - S at x, seen in G: outside S, and inside V(G).

theorem Graph.mem_component_deleteVerts_of_isLink {α : Type u_1} {β : Type u_2} {G : Graph α β} {x p q : α} {e : β} {S : Set α} (hp : p ∈ (G.deleteVerts S).component x) (hl : G.IsLink e p q) (hq : q ∉ S) : q ∈ (G.deleteVerts S).component x

A neighbour of a component of G - S that is outside S is in the component. The edge joining them survives the deletion, so it extends the walk.

theorem Graph.exists_isLink_out_of_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {v x : α} {W : List β} {S : Set α} {K : Graph α β} (hKG : K ≤ G) (h : K.IsWalk x W v) (hx : x ∈ (G.deleteVerts S).component x) (hv : v ∈ S) : ∃ p ∈ (G.deleteVerts S).component x, ∃ g ∈ W, ∃ t ∈ S, K.IsLink g p t

Walking out of a component of G - S meets S along an edge. The walk may live in any subgraph K of G — it is run inside G - c once — but the component is always the one of G - S, which is what makes the conclusion usable twice.

This is Graph.IsWalk.crossing plus the previous lemma: the crossing edge's far end is outside the component, so it cannot be outside S.

The two neighbours of a component, and the path through it

theorem Graph.IsTwoConnected.component_two_neighbors {α : Type u_1} {β : Type u_2} {G : Graph α β} {x a b : α} {S : Set α} (hG : G.IsTwoConnected) (hS : S ⊆ G.vertexSet) (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) (hx : x ∈ G.vertexSet) (hxS : x ∉ S) : ∃ c ∈ S, ∃ d ∈ S, c ≠ d ∧ (∃ p ∈ (G.deleteVerts S).component x, ∃ (g : β), G.IsLink g p c) ∧ ∃ q ∈ (G.deleteVerts S).component x, ∃ (g : β), G.IsLink g q d

A component of G - S has two distinct neighbours in S — the first half of lem:relative-ear, with the blueprint's contradiction turned into a construction.

S must contain two distinct vertices; in the application it is the vertex set of a 2-connected subgraph, which has three. The first neighbour c comes from a walk of G out of the component to a vertex of S; the second from the same walk run inside G - c, which is still connected because G is 2-connected, and aimed at a vertex of S other than c.

theorem Graph.mem_walkVertices_append_singleton {α : Type u_1} {β : Type u_2} {G : Graph α β} {u y : α} {e : β} {W : List β} (hy : y ∈ G.walkVertices u (W ++ [e])) : y ∈ G.walkVertices u W ∨ G.Inc e y

Reading off the vertices of a walk with one edge appended at the far end. Purely about lists; used to check the freshness clause when a path inside a component is capped with an edge back into S.

theorem Graph.IsTwoConnected.exists_path_through_component {α : Type u_1} {β : Type u_2} {G : Graph α β} {x a b : α} {S : Set α} (hG : G.IsTwoConnected) (hS : S ⊆ G.vertexSet) (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) (hx : x ∈ G.vertexSet) (hxS : x ∉ S) : ∃ c ∈ S, ∃ d ∈ S, ∃ (P : List β), c ≠ d ∧ G.IsPath c P d ∧ (∀ y ∈ G.walkVertices c P, y ≠ c → y ≠ d → y ∉ S) ∧ (∃ y ∈ G.walkVertices c P, y ∉ S) ∧ ∀ f ∈ P, ∃ (y : α), G.Inc f y ∧ y ∉ S

The path through a component — the second half of lem:relative-ear, without the word ear: in a 2-connected G, from a vertex outside a set S that has two distinct vertices, one gets a path of G whose two endpoints are distinct vertices of S, whose every other vertex is outside S, which has at least one vertex outside S, and each of whose edges has an end outside S.

The last two clauses are what make the ear process terminate and what make the path new: it really does add a vertex, and none of its edges belongs to a subgraph whose vertices all lie in S.

The path is built from the two neighbours of the component: the edge into the component, a path across the component (in G - S, hence never touching S), and the edge back out.