Walks of a simple graph as directed walks of its adjacency arrow family

The adjacency arrow family SimpleGraph.AdjHom G of a simple graph G has a single arrow from v to w exactly when v and w are adjacent, so every edge gives one arrow in each direction. Directed walks along it (TauCeti.ArrowWalk) are the objects on which the network theory runs, including the directed forms of Menger's theorem.

This file identifies the walks of G with the directed walks of its adjacency arrow family (SimpleGraph.Walk.arrowWalkEquiv). The identification preserves the length and the vertex sequence, hence paths. Deleting a set X of vertices corresponds to avoiding it: reachability in the subgraph induced on the complement of X is reachability along the adjacency arrow family through walks visiting no vertex of X. This is what transports the vertex forms of Menger's theorem from arrow families to simple graphs.

Main definitions

• SimpleGraph.AdjHom G: the adjacency arrow family of G.
• SimpleGraph.Walk.toArrowWalk: a walk of G as a directed walk.
• TauCeti.ArrowWalk.toWalk: a directed walk of the adjacency arrow family as a walk of G.
• SimpleGraph.Walk.arrowWalkEquiv: these maps are inverse equivalences.

Main results

• SimpleGraph.Walk.vertices_toArrowWalk and TauCeti.ArrowWalk.support_toWalk: the identification preserves vertex sequences.
• SimpleGraph.Walk.isPath_toArrowWalk_iff and TauCeti.ArrowWalk.isPath_toWalk_iff: it preserves and reflects paths.
• SimpleGraph.reachable_iff_nonempty_arrowWalk: reachability in G is reachability along the adjacency arrow family.
• SimpleGraph.reachable_induce_iff: two vertices of a vertex set S are reachable in the subgraph induced on S exactly when some walk between them stays in S.
• SimpleGraph.reachableAvoiding_singleton_adjHom_iff: avoiding one vertex along the adjacency arrow family is witnessed by a simple-graph walk whose support avoids that vertex.
• TauCeti.ReachableAvoiding.reachable: avoiding vertices still implies ordinary simple-graph reachability.
• SimpleGraph.reachable_induce_compl_iff: reachability after deleting a set X of vertices is reachability along the adjacency arrow family avoiding X.

@[reducible, inline]

abbrev SimpleGraph.AdjHom {V : Type u} (G : SimpleGraph V) (v w : V) : Type

The adjacency arrow family of a simple graph: a single arrow from v to w exactly when v and w are adjacent, so every edge gives one arrow in each direction.

def SimpleGraph.Walk.toArrowWalk {V : Type u} {G : SimpleGraph V} {u v : V} : G.Walk u v → TauCeti.ArrowWalk G.AdjHom u v

A walk of G as a directed walk of the adjacency arrow family, visiting the same vertices in the same order.

@[simp]

theorem SimpleGraph.Walk.toArrowWalk_nil {V : Type u} {G : SimpleGraph V} {u : V} : nil.toArrowWalk = TauCeti.ArrowWalk.nil u

@[simp]

theorem SimpleGraph.Walk.toArrowWalk_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (h : G.Adj u v) (p : G.Walk v w) : (cons h p).toArrowWalk = ((TauCeti.ArrowWalk.nil u).cons { down := h }).comp p.toArrowWalk

@[simp]

theorem SimpleGraph.Walk.toArrowWalk_append {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w) : (p.append q).toArrowWalk = p.toArrowWalk.comp q.toArrowWalk

The directed walk of a concatenation is the composite of the directed walks.

@[simp]

theorem SimpleGraph.Walk.vertices_toArrowWalk {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toArrowWalk.vertices = p.support

The directed walk of a walk visits the vertices of its support, in order.

@[simp]

theorem SimpleGraph.Walk.length_toArrowWalk {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toArrowWalk.length = p.length

@[simp]

theorem SimpleGraph.Walk.isPath_toArrowWalk_iff {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v} : p.toArrowWalk.IsPath ↔ p.IsPath

def TauCeti.ArrowWalk.toWalk {V : Type u} {G : SimpleGraph V} {u v : V} : ArrowWalk G.AdjHom u v → G.Walk u v

A directed walk of the adjacency arrow family of G, as a walk of G visiting the same vertices in the same order.

@[simp]

theorem TauCeti.ArrowWalk.toWalk_nil {V : Type u} {G : SimpleGraph V} (u : V) : (nil u).toWalk = SimpleGraph.Walk.nil

@[simp]

theorem TauCeti.ArrowWalk.toWalk_cons {V : Type u} {G : SimpleGraph V} {u v w : V} (q : ArrowWalk G.AdjHom u v) (e : G.AdjHom v w) : (q.cons e).toWalk = q.toWalk.concat ⋯

@[simp]

theorem TauCeti.ArrowWalk.toWalk_comp {V : Type u} {G : SimpleGraph V} {u v w : V} (q : ArrowWalk G.AdjHom u v) (r : ArrowWalk G.AdjHom v w) : (q.comp r).toWalk = q.toWalk.append r.toWalk

The walk of a composite directed walk is the concatenation of the walks.

@[simp]

theorem TauCeti.ArrowWalk.support_toWalk {V : Type u} {G : SimpleGraph V} {u v : V} (q : ArrowWalk G.AdjHom u v) : q.toWalk.support = q.vertices

The walk of a directed walk has the vertices of the directed walk as its support.

@[simp]

theorem TauCeti.ArrowWalk.length_toWalk {V : Type u} {G : SimpleGraph V} {u v : V} (q : ArrowWalk G.AdjHom u v) : q.toWalk.length = q.length

@[simp]

theorem TauCeti.ArrowWalk.isPath_toWalk_iff {V : Type u} {G : SimpleGraph V} {u v : V} {q : ArrowWalk G.AdjHom u v} : q.toWalk.IsPath ↔ q.IsPath

@[simp]

theorem SimpleGraph.Walk.toWalk_toArrowWalk {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : p.toArrowWalk.toWalk = p

Returning a walk from the adjacency arrow family recovers it.

@[simp]

theorem SimpleGraph.Walk.toArrowWalk_toWalk {V : Type u} {G : SimpleGraph V} {u v : V} (q : TauCeti.ArrowWalk G.AdjHom u v) : q.toWalk.toArrowWalk = q

Every directed walk of the adjacency arrow family is the directed walk of its walk in G.

def SimpleGraph.Walk.arrowWalkEquiv {V : Type u} (G : SimpleGraph V) (u v : V) : G.Walk u v ≃ TauCeti.ArrowWalk G.AdjHom u v

The walks of G between two vertices are the directed walks of the adjacency arrow family between them, with the same vertex sequences.

@[simp]

theorem SimpleGraph.Walk.arrowWalkEquiv_apply {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) : (arrowWalkEquiv G u v) p = p.toArrowWalk

@[simp]

theorem SimpleGraph.Walk.arrowWalkEquiv_symm_apply {V : Type u} {G : SimpleGraph V} {u v : V} (q : TauCeti.ArrowWalk G.AdjHom u v) : (arrowWalkEquiv G u v).symm q = q.toWalk

theorem SimpleGraph.Walk.toArrowWalk_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective toArrowWalk

theorem TauCeti.ArrowWalk.toWalk_injective {V : Type u} {G : SimpleGraph V} {u v : V} : Function.Injective toWalk

Reachability

theorem SimpleGraph.reachable_iff_nonempty_arrowWalk {V : Type u} {G : SimpleGraph V} {s t : V} : G.Reachable s t ↔ Nonempty (TauCeti.ArrowWalk G.AdjHom s t)

Reachability in G is reachability along its adjacency arrow family.

theorem SimpleGraph.reachable_induce_iff {V : Type u} {G : SimpleGraph V} {S : Set V} {s t : ↑S} : (induce S G).Reachable s t ↔ ∃ (p : G.Walk ↑s ↑t), ∀ v ∈ p.support, v ∈ S

Two vertices of a set S are reachable in the subgraph induced on S exactly when some walk of G between them visits only vertices of S.

theorem SimpleGraph.reachableAvoiding_adjHom_iff {V : Type u} {G : SimpleGraph V} {s t : V} {X : Set V} : TauCeti.ReachableAvoiding G.AdjHom X s t ↔ ∃ (p : G.Walk s t), ∀ v ∈ p.support, v ∉ X

Reachability along the adjacency arrow family avoiding a set X of vertices is the existence of a walk of G visiting no vertex of X.

theorem SimpleGraph.reachableAvoiding_singleton_adjHom_iff {V : Type u} {G : SimpleGraph V} {s t x : V} : TauCeti.ReachableAvoiding G.AdjHom {x} s t ↔ ∃ (p : G.Walk s t), x ∉ p.support

Avoiding one vertex along the adjacency arrow family is the existence of a simple-graph walk whose support avoids that vertex.

theorem TauCeti.ReachableAvoiding.reachable {V : Type u} {G : SimpleGraph V} {s t : V} {X : Set V} (h : ReachableAvoiding G.AdjHom X s t) : G.Reachable s t

Reachability while avoiding vertices implies ordinary simple-graph reachability.

theorem SimpleGraph.reachable_induce_compl_iff {V : Type u} {G : SimpleGraph V} {X : Set V} {s t : ↑Xᶜ} : (induce Xᶜ G).Reachable s t ↔ TauCeti.ReachableAvoiding G.AdjHom X ↑s ↑t

Reachability after deleting a set X of vertices, in the subgraph induced on its complement, is reachability along the adjacency arrow family avoiding X.