Digraphs as arrow families

The adjacency arrow family Digraph.AdjHom D of a digraph D has a single arrow from v to w exactly when D.Adj v w; loops are retained, and at most one arrow runs from any vertex to any other. Directed walks along it (TauCeti.ArrowWalk) are the objects on which the network theory runs, including the directed forms of Menger's theorem, so this family is how statements about arrow families specialize to digraphs.

This file identifies the notions of the arrow-family theory with their digraph counterparts. The arrows are the ordered pairs of adjacent vertices, and a walk is determined by its vertex sequence, which can be any list of vertices in which consecutive vertices are adjacent. Directed reachability along the family is the reflexive transitive closure of D.Adj. Deleting a set X of vertices corresponds to avoiding it: reachability in the digraph induced on the complement of X is reachability along the family through walks visiting no vertex of X. Deleting the arrows of a digraph E corresponds to avoiding the arrows joining pairs adjacent in E: reachability in D \ E is reachability along the family without those arrows. Finally, the zigzags of arrows, which define the weakly connected components, are the walks of the simple graph D.toSimpleGraphInclusive obtained by forgetting orientations.

Main definitions

• Digraph.AdjHom D: the adjacency arrow family of D.
• Digraph.sigmaAdjHomEquiv: the arrows of the family are the ordered pairs of adjacent vertices.
• Digraph.arrowWalkEquiv: the walks from s to t are the lists of vertices from s to t in which consecutive vertices are adjacent.

Main results

• Digraph.nonempty_arrowWalk_iff_reflTransGen: reachability along the adjacency arrow family is the reflexive transitive closure of D.Adj.
• Digraph.isStronglyConnected_iff: the family is strongly connected exactly when every vertex reaches every other vertex along D.Adj.
• Digraph.reflTransGen_induce_compl_iff: reachability after deleting a set X of vertices is reachability along the family avoiding X.
• Digraph.reflTransGen_sdiff_iff: reachability after deleting the arrows of a digraph E is reachability along the family without the arrows joining pairs adjacent in E.
• Digraph.weaklyConnectedComponent_mk_eq_mk_iff: two vertices lie in the same weakly connected component of the family exactly when they are reachable in D.toSimpleGraphInclusive.

@[reducible, inline]

abbrev Digraph.AdjHom {V : Type u} (D : Digraph V) (v w : V) : Type

The adjacency arrow family of a digraph: a single arrow from v to w exactly when D.Adj v w.

theorem Digraph.nonempty_adjHom_iff {V : Type u} {D : Digraph V} {v w : V} : Nonempty (D.AdjHom v w) ↔ D.Adj v w

Some arrow of the adjacency arrow family runs from v to w exactly when D.Adj v w.

theorem Digraph.isEmpty_adjHom_iff {V : Type u} {D : Digraph V} {v w : V} : IsEmpty (D.AdjHom v w) ↔ ¬D.Adj v w

No arrow of the adjacency arrow family runs from v to w exactly when ¬D.Adj v w.

Arrows and walks

def Digraph.sigmaAdjHomEquiv {V : Type u} (D : Digraph V) : (v : V) × (w : V) × D.AdjHom v w ≃ { p : V × V // D.Adj p.1 p.2 }

The arrows of the adjacency arrow family, recorded with their endpoints, are the ordered pairs of adjacent vertices.

@[simp]

theorem Digraph.sigmaAdjHomEquiv_apply_coe {V : Type u} {D : Digraph V} (a : (v : V) × (w : V) × D.AdjHom v w) : ↑(D.sigmaAdjHomEquiv a) = (a.fst, a.snd.fst)

@[simp]

theorem Digraph.sigmaAdjHomEquiv_symm_apply {V : Type u} {D : Digraph V} (p : { p : V × V // D.Adj p.1 p.2 }) : D.sigmaAdjHomEquiv.symm p = ⟨(↑p).1, ⟨(↑p).2, { down := ⋯ }⟩⟩

theorem Digraph.isChain_vertices {V : Type u} {D : Digraph V} {s t : V} (p : TauCeti.ArrowWalk D.AdjHom s t) : List.IsChain D.Adj p.vertices

Consecutive vertices of a walk along the adjacency arrow family are adjacent.

noncomputable def Digraph.arrowWalkEquiv {V : Type u} (D : Digraph V) (s t : V) : TauCeti.ArrowWalk D.AdjHom s t ≃ { l : List V // List.IsChain D.Adj l ∧ l.head? = some s ∧ l.getLast? = some t }

The walks along the adjacency arrow family from s to t are the lists of vertices starting at s and ending at t in which consecutive vertices are adjacent, through their vertex sequences.

@[simp]

theorem Digraph.arrowWalkEquiv_apply_coe {V : Type u} {D : Digraph V} {s t : V} (p : TauCeti.ArrowWalk D.AdjHom s t) : ↑((D.arrowWalkEquiv s t) p) = p.vertices

@[simp]

theorem Digraph.vertices_arrowWalkEquiv_symm_apply {V : Type u} {D : Digraph V} {s t : V} (l : { l : List V // List.IsChain D.Adj l ∧ l.head? = some s ∧ l.getLast? = some t }) : ((D.arrowWalkEquiv s t).symm l).vertices = ↑l

Reachability

theorem Digraph.nonempty_arrowWalk_iff_reflTransGen {V : Type u} {D : Digraph V} {s t : V} : Nonempty (TauCeti.ArrowWalk D.AdjHom s t) ↔ Relation.ReflTransGen D.Adj s t

Reachability along the adjacency arrow family is the reflexive transitive closure of adjacency.

theorem Digraph.isStronglyConnected_iff {V : Type u} {D : Digraph V} : Quiver.IsStronglyConnected V ↔ ∀ (v w : V), Relation.ReflTransGen D.Adj v w

The adjacency arrow family is strongly connected exactly when every vertex reaches every other vertex along adjacency.

Deleting vertices

theorem Digraph.reflTransGen_induce_iff {V : Type u} {D : Digraph V} {S : Set V} {s t : ↑S} : Relation.ReflTransGen (D.induce S).Adj s t ↔ ∃ (p : TauCeti.ArrowWalk D.AdjHom ↑s ↑t), ∀ v ∈ p.vertices, v ∈ S

Two vertices of a set S are related by the reflexive transitive closure of adjacency in the digraph induced on S exactly when some walk along the adjacency arrow family of D joins them through vertices of S.

theorem Digraph.reflTransGen_induce_compl_iff {V : Type u} {D : Digraph V} {X : Set V} {s t : ↑Xᶜ} : Relation.ReflTransGen (D.induce Xᶜ).Adj s t ↔ TauCeti.ReachableAvoiding D.AdjHom X ↑s ↑t

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

Deleting arrows

def Digraph.deleteArrows {V : Type u} (D : Digraph V) (F : Set ((v : V) × (w : V) × D.AdjHom v w)) : Digraph V

Delete a set of arrows from a digraph. Each arrow retains its ordered endpoints and the adjacency proof witnessing that it belongs to D.

@[simp]

theorem Digraph.deleteArrows_adj {V : Type u} {D : Digraph V} {F : Set ((v : V) × (w : V) × D.AdjHom v w)} {v w : V} : (D.deleteArrows F).Adj v w ↔ ∃ (e : D.AdjHom v w), ⟨v, ⟨w, e⟩⟩ ∉ F

An ordered pair is an arrow after deletion exactly when it was an arrow and was not selected.

@[simp]

theorem Digraph.deleteArrows_empty {V : Type u} {D : Digraph V} : D.deleteArrows ∅ = D

Deleting no arrows leaves a digraph unchanged.

@[simp]

theorem Digraph.deleteArrows_univ {V : Type u} {D : Digraph V} : D.deleteArrows Set.univ = ⊥

Deleting every arrow leaves the empty digraph.

theorem Digraph.deleteArrows_anti {V : Type u} {D : Digraph V} {F F' : Set ((v : V) × (w : V) × D.AdjHom v w)} (hFF' : F ⊆ F') : D.deleteArrows F' ≤ D.deleteArrows F

Deleting a larger set of arrows gives a smaller digraph.

theorem Digraph.reflTransGen_sdiff_iff {V : Type u} {D : Digraph V} {s t : V} {E : Digraph V} : Relation.ReflTransGen (D \ E).Adj s t ↔ TauCeti.ReachableWithout {a : (x : V) × (y : V) × D.AdjHom x y | E.Adj a.fst a.snd.fst} s t

Reachability after deleting the arrows of a digraph E is reachability along the adjacency arrow family of D without the arrows joining pairs adjacent in E.

Weak connectivity

@[simp]

theorem Digraph.underlyingGraph_adjHom {V : Type u} {D : Digraph V} : TauCeti.Quiver.underlyingGraph V = D.toSimpleGraphInclusive

The simple graph underlying the adjacency arrow family is the simple graph obtained from D by forgetting orientations.

theorem Digraph.weaklyConnectedComponent_mk_eq_mk_iff {V : Type u} {D : Digraph V} {v w : V} : Quiver.WeaklyConnectedComponent.mk v = Quiver.WeaklyConnectedComponent.mk w ↔ D.toSimpleGraphInclusive.Reachable v w

Two vertices lie in the same weakly connected component of the adjacency arrow family exactly when they are reachable in the simple graph obtained from D by forgetting orientations.