Multigraph walks as directed walks of the bidirected arrow family

The bidirected arrow family Graph.BidirectedHom G of a multigraph G : Graph α β lives on its actual vertices V(G): the arrows from x to y are the edges e with G.IsLink e x y. A nonloop edge therefore gives one arrow in each direction, a loop gives a single loop arrow, and parallel edges give distinct parallel arrows. Directed walks along this family (TauCeti.ArrowWalk) are the objects on which the network theory runs: flows, residual reachability, and the directed forms of Menger's theorem.

This file identifies the edge-labelled walks of G between actual vertices with the directed walks of its bidirected arrow family (Graph.Walk.bidirectedEquiv). The identification preserves the length, the vertex sequence, and the edge sequence, hence paths. A directed cycle of the bidirected family corresponds to an undirected cycle exactly when it traverses no edge twice: the directed cycle x → y → x using the two opposite arrows of a single edge is not an undirected cycle. In particular, reachability in G is reachability along the bidirected arrow family, and reachability after deleting a set of vertices of G is reachability avoiding that set.

Main definitions

• Graph.BidirectedHom G: the bidirected arrow family of G, on its actual vertices.
• Graph.Walk.toBidirected: a walk of G from an actual vertex as a directed walk.
• TauCeti.ArrowWalk.toGraphWalk: a directed walk of the bidirected family as a walk of G.
• Graph.Walk.bidirectedEquiv: these maps are inverse equivalences.

Main results

• Graph.Walk.vertices_toBidirected and Graph.Walk.edges_toBidirected: the identification preserves vertex and edge sequences.
• Graph.Walk.isPath_toBidirected_iff: it preserves and reflects paths.
• TauCeti.ArrowWalk.mem_support_toGraphWalk_iff: the points on the walk of a directed walk are the vertices it visits.
• Graph.Walk.isCycle_iff_isCycle_toBidirected_and_isTrail: an undirected cycle is a directed cycle that is a trail.
• Graph.reachable_iff_nonempty_arrowWalk: reachability between actual vertices is reachability along the bidirected arrow family.
• Graph.reachableAvoiding_bidirectedHom_iff: reachability after deleting a set of vertices is reachability along the bidirected arrow family avoiding that set.
• Graph.reachableWithout_bidirectedHom_iff: reachability after deleting a set of edges is reachability along the bidirected arrow family without the arrows those edges give.
• TauCeti.ArrowWalk.internallyDisjoint_toGraphWalk_iff: the identification preserves and reflects internal disjointness.

@[reducible, inline]

abbrev Graph.BidirectedHom {α : Type u} {β : Type v} (G : Graph α β) (x y : ↑G.vertexSet) : Type v

The bidirected arrow family of a multigraph on its actual vertices: the arrows from x to y are the edges linking x to y. A nonloop edge gives one arrow in each direction and a loop gives a single loop arrow.

instance Graph.instFiniteBidirectedHomOfElemEdgeSet {α : Type u} {β : Type v} (G : Graph α β) [Finite ↑G.edgeSet] (x y : ↑G.vertexSet) : Finite (G.BidirectedHom x y)

A multigraph with finitely many actual edges has finitely many arrows between any two vertices of its bidirected arrow family.

@[simp]

theorem Graph.BidirectedHom.fst_cast {α : Type u} {β : Type v} (G : Graph α β) {x y x' y' : ↑G.vertexSet} (a : G.BidirectedHom x y) (hx : x = x') (hy : y = y') : ↑(Quiver.Hom.cast hx hy a) = ↑a

Changing the endpoints of a bidirected arrow does not change its underlying edge.

@[reducible, inline]

abbrev Graph.IsLink.toBidirectedHom {α : Type u} {β : Type v} {G : Graph α β} {e : β} {x y : α} (h : G.IsLink e x y) : G.BidirectedHom ⟨x, ⋯⟩ ⟨y, ⋯⟩

The arrow of the bidirected arrow family given by an edge linking x to y.

theorem Graph.bidirectedHom_edge_injOn_cut {α : Type u} {β : Type v} {G : Graph α β} (S : Set ↑G.vertexSet) : Set.InjOn (fun (a : (x : ↑G.vertexSet) × (y : ↑G.vertexSet) × G.BidirectedHom x y) => ↑a.snd.snd) {a : (x : ↑G.vertexSet) × (y : ↑G.vertexSet) × G.BidirectedHom x y | a.fst ∈ S ∧ a.snd.fst ∉ S}

The map from bidirected arrows crossing a vertex set in the outward direction to their underlying edges is injective.

def Graph.Walk.toBidirected {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : TauCeti.ArrowWalk G.BidirectedHom ⟨x, hx⟩ ⟨y, ⋯⟩

A walk of G from an actual vertex, as a directed walk of the bidirected arrow family that traverses the arrows given by the same edges in the same order.

@[simp]

theorem Graph.Walk.toBidirected_nil {α : Type u} {β : Type v} {G : Graph α β} {x : α} (hx : x ∈ G.vertexSet) : nil.toBidirected hx = TauCeti.ArrowWalk.nil ⟨x, hx⟩

@[simp]

theorem Graph.Walk.toBidirected_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} {e : β} (h : G.IsLink e x y) (p : G.Walk y z) (hx : x ∈ G.vertexSet) : (cons e h p).toBidirected hx = ((TauCeti.ArrowWalk.nil ⟨x, ⋯⟩).cons h.toBidirectedHom).comp (p.toBidirected ⋯)

@[simp]

theorem Graph.Walk.toBidirected_append {α : Type u} {β : Type v} {G : Graph α β} {x y z : α} (p : G.Walk x y) (q : G.Walk y z) (hx : x ∈ G.vertexSet) : (p.append q).toBidirected hx = (p.toBidirected hx).comp (q.toBidirected ⋯)

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

@[simp]

theorem Graph.IsLink.toBidirected_toWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : α} {e : β} (h : G.IsLink e x y) (hx : x ∈ G.vertexSet) : h.toWalk.toBidirected hx = (TauCeti.ArrowWalk.nil ⟨x, ⋯⟩).cons h.toBidirectedHom

The directed walk of a single edge is the single arrow given by that edge.

def TauCeti.ArrowWalk.toGraphWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} : ArrowWalk G.BidirectedHom x y → G.Walk ↑x ↑y

A directed walk of the bidirected arrow family of G, as a walk of G traversing the edges of its arrows in the same order.

@[simp]

theorem TauCeti.ArrowWalk.toGraphWalk_nil {α : Type u} {β : Type v} {G : Graph α β} (x : ↑G.vertexSet) : (nil x).toGraphWalk = Graph.Walk.nil

@[simp]

theorem TauCeti.ArrowWalk.toGraphWalk_cons {α : Type u} {β : Type v} {G : Graph α β} {x y z : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) (a : G.BidirectedHom y z) : (q.cons a).toGraphWalk = q.toGraphWalk.append ⋯.toWalk

@[simp]

theorem TauCeti.ArrowWalk.toGraphWalk_comp {α : Type u} {β : Type v} {G : Graph α β} {x y z : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) (r : ArrowWalk G.BidirectedHom y z) : (q.comp r).toGraphWalk = q.toGraphWalk.append r.toGraphWalk

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

@[simp]

theorem Graph.Walk.toGraphWalk_toBidirected {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : (p.toBidirected hx).toGraphWalk = p

Returning a walk from the bidirected arrow family recovers it.

@[simp]

theorem Graph.Walk.toBidirected_toGraphWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : TauCeti.ArrowWalk G.BidirectedHom x y) : q.toGraphWalk.toBidirected ⋯ = q

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

def Graph.Walk.bidirectedEquiv {α : Type u} {β : Type v} (G : Graph α β) (x y : ↑G.vertexSet) : G.Walk ↑x ↑y ≃ TauCeti.ArrowWalk G.BidirectedHom x y

The walks of G between two actual vertices are the directed walks of the bidirected arrow family between them, with the same vertex and edge sequences.

@[simp]

theorem Graph.Walk.bidirectedEquiv_apply {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (p : G.Walk ↑x ↑y) : (bidirectedEquiv G x y) p = p.toBidirected ⋯

@[simp]

theorem Graph.Walk.bidirectedEquiv_symm_apply {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : TauCeti.ArrowWalk G.BidirectedHom x y) : (bidirectedEquiv G x y).symm q = q.toGraphWalk

@[simp]

theorem TauCeti.ArrowWalk.toGraphWalk_cast {α : Type u} {β : Type v} {G : Graph α β} {x y x' y' : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) (hx : x = x') (hy : y = y') : toGraphWalk (Quiver.Path.cast hx hy q) = q.toGraphWalk.copy ⋯ ⋯

Changing the endpoints of a directed walk before forgetting directions changes the endpoints of the resulting graph walk by the underlying equalities.

Transport of lengths, vertices, edges, paths, and cycles

@[simp]

theorem Graph.Walk.length_toBidirected {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : (p.toBidirected hx).length = p.length

The directed walk has the same length as the walk.

@[simp]

theorem Graph.Walk.vertices_toBidirected {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : (p.toBidirected hx).vertices.unattach = p.support

The directed walk visits the vertices of the walk in the same order.

@[simp]

theorem Graph.Walk.edges_toBidirected {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : List.map (fun (a : (x : ↑G.vertexSet) × (y : ↑G.vertexSet) × G.BidirectedHom x y) => ↑a.snd.snd) (p.toBidirected hx).arrows = p.edges

The arrows of the directed walk are the edges of the walk, in the same order.

@[simp]

theorem Graph.Walk.isPath_toBidirected_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : α} (p : G.Walk x y) (hx : x ∈ G.vertexSet) : (p.toBidirected hx).IsPath ↔ p.IsPath

The directed walk is a directed path exactly when the walk is a path.

theorem Graph.Walk.isCycle_iff_isCycle_toBidirected_and_isTrail {α : Type u} {β : Type v} {G : Graph α β} {x : α} (p : G.Walk x x) (hx : x ∈ G.vertexSet) : p.IsCycle ↔ (p.toBidirected hx).IsCycle ∧ p.IsTrail

A closed walk is an undirected cycle exactly when its directed walk is a directed cycle and it traverses no edge twice.

@[simp]

theorem TauCeti.ArrowWalk.length_toGraphWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) : q.toGraphWalk.length = q.length

The walk of a directed walk has the same length as the directed walk.

@[simp]

theorem TauCeti.ArrowWalk.support_toGraphWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) : q.toGraphWalk.support = q.vertices.unattach

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

@[simp]

theorem TauCeti.ArrowWalk.edges_toGraphWalk {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) : q.toGraphWalk.edges = List.map (fun (a : (x : ↑G.vertexSet) × (y : ↑G.vertexSet) × G.BidirectedHom x y) => ↑a.snd.snd) q.arrows

The edges of the walk of a directed walk are the edges of its arrows, in the same order.

theorem TauCeti.ArrowWalk.mem_support_toGraphWalk_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) {v : α} : v ∈ q.toGraphWalk.support ↔ ∃ (hv : v ∈ G.vertexSet), ⟨v, hv⟩ ∈ q.vertices

A point lies on the walk of a directed walk exactly when it is an actual vertex visited by the directed walk.

@[simp]

theorem TauCeti.ArrowWalk.internallyDisjoint_toGraphWalk_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} {p q : ArrowWalk G.BidirectedHom x y} : p.toGraphWalk.InternallyDisjoint q.toGraphWalk ↔ p.InternallyDisjoint q

The walks in G of two directed walks are internally disjoint exactly when the directed walks are.

theorem TauCeti.ArrowWalk.toGraphWalk_injective {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} : Function.Injective toGraphWalk

A directed walk is determined by its walk in G.

@[simp]

theorem TauCeti.ArrowWalk.isPath_toGraphWalk_iff {α : Type u} {β : Type v} {G : Graph α β} {x y : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x y) : q.toGraphWalk.IsPath ↔ q.IsPath

The walk of a directed walk is a path exactly when the directed walk is a directed path.

theorem TauCeti.ArrowWalk.isCycle_toGraphWalk_iff {α : Type u} {β : Type v} {G : Graph α β} {x : ↑G.vertexSet} (q : ArrowWalk G.BidirectedHom x x) : q.toGraphWalk.IsCycle ↔ q.IsCycle ∧ (List.map (fun (a : (x : ↑G.vertexSet) × (y : ↑G.vertexSet) × G.BidirectedHom x y) => ↑a.snd.snd) q.arrows).Nodup

A directed cycle of the bidirected arrow family is an undirected cycle exactly when no two of its arrows come from the same edge.

theorem Graph.reachable_iff_nonempty_arrowWalk {α : Type u} {β : Type v} {G : Graph α β} (x y : ↑G.vertexSet) : G.Reachable ↑x ↑y ↔ Nonempty (TauCeti.ArrowWalk G.BidirectedHom x y)

Two actual vertices are reachable in G exactly when a directed walk of the bidirected arrow family joins them.

theorem Graph.reachableAvoiding_bidirectedHom_iff {α : Type u} {β : Type v} {G : Graph α β} {Y : Set α} {x y : ↑G.vertexSet} : TauCeti.ReachableAvoiding G.BidirectedHom (Subtype.val ⁻¹' Y) x y ↔ (G.deleteVerts Y).Reachable ↑x ↑y

Two actual vertices are reachable after deleting a set Y of vertices of G exactly when a directed walk of the bidirected arrow family joins them avoiding Y.

theorem Graph.reachableWithout_bidirectedHom_iff {α : Type u} {β : Type v} {G : Graph α β} {E : Set β} {x y : ↑G.vertexSet} : TauCeti.ReachableWithout {a : (v : ↑G.vertexSet) × (w : ↑G.vertexSet) × G.BidirectedHom v w | ↑a.snd.snd ∈ E} x y ↔ (G.deleteEdges E).Reachable ↑x ↑y

Two actual vertices are reachable after deleting a set E of edges of G exactly when a directed walk of the bidirected arrow family joins them using no arrow given by an edge of E.

theorem Graph.not_reachable_deleteVerts_map_subtype {α : Type u} {β : Type v} {G : Graph α β} {X : Finset ↑G.vertexSet} {x y : ↑G.vertexSet} (h : ¬TauCeti.ReachableAvoiding G.BidirectedHom (↑X) x y) : ¬(G.deleteVerts ↑(Finset.map (Function.Embedding.subtype fun (x : α) => x ∈ G.vertexSet) X)).Reachable ↑x ↑y

A set of actual vertices that the bidirected arrow family cannot avoid on its way from x to y separates x from y in G.

theorem Graph.isEmpty_bidirectedHom {α : Type u} {β : Type v} {G : Graph α β} {s t : α} (hadj : ¬G.Adj s t) (hs : s ∈ G.vertexSet) (ht : t ∈ G.vertexSet) : IsEmpty (G.BidirectedHom ⟨s, hs⟩ ⟨t, ht⟩)

No arrow of the bidirected arrow family runs between vertices that no edge joins.