Connected components of doubled graph quivers

Graph walks become directed paths in the doubled quiver by replacing each traversed edge with its corresponding arrow. Conversely, a doubled-quiver path gives a graph walk by forgetting the lifted adjacency proofs. These constructions identify graph reachability with directed reachability in the doubled quiver and with zigzag reachability in its symmetrification.

It follows that the connected components of a graph are canonically equivalent to the weakly connected components of its doubled quiver. This is the component bridge used by the componentwise definition and decomposition of zigzag algebras.

Main definitions

• TauCeti.DoubledQuiver.walkToPath: turn a graph walk into a doubled-quiver path.
• TauCeti.DoubledQuiver.pathToWalk: turn a doubled-quiver path into a graph walk.
• TauCeti.DoubledQuiver.connectedComponentEquiv: identify the two component types.

Main results

• TauCeti.DoubledQuiver.pathToWalk_walkToPath and TauCeti.DoubledQuiver.walkToPath_pathToWalk: the two conversions are mutually inverse.
• TauCeti.DoubledQuiver.reachable_iff: graph and doubled-quiver reachability agree.
• TauCeti.DoubledQuiver.preconnected_iff_isStronglyConnected: graph preconnectedness is strong connectivity of the doubled quiver.
• TauCeti.DoubledQuiver.connected_iff: graph connectedness is nonemptiness together with strong connectivity of the doubled quiver.

References

See Huerfano--Khovanov, A category for the adjoint representation, Section 3.

def TauCeti.DoubledQuiver.walkToPath {V : Type u} (G : SimpleGraph V) {i j : V} : G.Walk i j → Quiver.Path (vertex G i) (vertex G j)

Convert a graph walk to the path through the corresponding arrows of the doubled quiver.

def TauCeti.DoubledQuiver.pathToWalk {V : Type u} (G : SimpleGraph V) {i j : V} (p : Quiver.Path (vertex G i) (vertex G j)) : G.Walk i j

Convert a path in the doubled quiver between graph-labelled vertices to a graph walk.

@[simp]

theorem TauCeti.DoubledQuiver.walkToPath_nil {V : Type u} (G : SimpleGraph V) (i : V) : walkToPath G SimpleGraph.Walk.nil = Quiver.Path.nil

@[simp]

theorem TauCeti.DoubledQuiver.walkToPath_cons {V : Type u} (G : SimpleGraph V) {i j k : V} (h : G.Adj i j) (p : G.Walk j k) : walkToPath G (SimpleGraph.Walk.cons h p) = (arrow G h).toPath.comp (walkToPath G p)

@[simp]

theorem TauCeti.DoubledQuiver.walkToPath_append {V : Type u} (G : SimpleGraph V) {i j k : V} (p : G.Walk i j) (q : G.Walk j k) : walkToPath G (p.append q) = (walkToPath G p).comp (walkToPath G q)

Converting appended graph walks gives the composite doubled-quiver paths.

theorem TauCeti.DoubledQuiver.walkToPath_toWalk {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : walkToPath G h.toWalk = (arrow G h).toPath

Converting the one-edge walk gives the corresponding doubled-quiver arrow.

@[simp]

theorem TauCeti.DoubledQuiver.pathToWalk_nil {V : Type u} (G : SimpleGraph V) (i : V) : pathToWalk G Quiver.Path.nil = SimpleGraph.Walk.nil

Converting the empty doubled-quiver path gives the empty graph walk.

@[simp]

theorem TauCeti.DoubledQuiver.pathToWalk_comp {V : Type u} (G : SimpleGraph V) {i j k : V} (p : Quiver.Path (vertex G i) (vertex G j)) (q : Quiver.Path (vertex G j) (vertex G k)) : pathToWalk G (p.comp q) = (pathToWalk G p).append (pathToWalk G q)

Converting composite doubled-quiver paths gives the appended graph walks.

@[simp]

theorem TauCeti.DoubledQuiver.pathToWalk_toPath {V : Type u} (G : SimpleGraph V) {i j : V} (h : G.Adj i j) : pathToWalk G (arrow G h).toPath = h.toWalk

Converting the one-arrow doubled-quiver path gives the one-edge graph walk.

@[simp]

theorem TauCeti.DoubledQuiver.pathToWalk_walkToPath {V : Type u} (G : SimpleGraph V) {i j : V} (p : G.Walk i j) : pathToWalk G (walkToPath G p) = p

Turning a graph walk into a doubled-quiver path and back gives the original walk.

@[simp]

theorem TauCeti.DoubledQuiver.walkToPath_pathToWalk {V : Type u} (G : SimpleGraph V) {i j : V} (p : Quiver.Path (vertex G i) (vertex G j)) : walkToPath G (pathToWalk G p) = p

Turning a doubled-quiver path into a graph walk and back gives the original path.

@[simp]

theorem TauCeti.DoubledQuiver.length_walkToPath {V : Type u} (G : SimpleGraph V) {i j : V} (p : G.Walk i j) : (walkToPath G p).length = p.length

Turning a graph walk into a doubled-quiver path preserves its length.

@[simp]

theorem TauCeti.DoubledQuiver.length_pathToWalk {V : Type u} (G : SimpleGraph V) {i j : V} (p : Quiver.Path (vertex G i) (vertex G j)) : (pathToWalk G p).length = p.length

Turning a doubled-quiver path into a graph walk preserves its length.

theorem TauCeti.DoubledQuiver.reachable_iff {V : Type u} (G : SimpleGraph V) {i j : V} : G.Reachable i j ↔ Quiver.Reachable (vertex G i) (vertex G j)

Graph reachability is directed reachability in the doubled quiver.

theorem TauCeti.DoubledQuiver.reachable_iff_nonempty_symmetrify_path {V : Type u} (G : SimpleGraph V) {i j : V} : G.Reachable i j ↔ Nonempty (Quiver.Path (vertex G i) (vertex G j))

Graph reachability is zigzag reachability in the doubled quiver.

theorem TauCeti.DoubledQuiver.reachable_vertexEquiv_symm_iff {V : Type u} (G : SimpleGraph V) (i j : DoubledQuiver G) : G.Reachable ((vertexEquiv G).symm i) ((vertexEquiv G).symm j) ↔ Quiver.Reachable i j

Reachability of two doubled-quiver vertices is graph reachability of the vertices they come from.

theorem TauCeti.DoubledQuiver.weaklyConnectedComponent_eq_iff {V : Type u} (G : SimpleGraph V) (i j : DoubledQuiver G) : Quiver.WeaklyConnectedComponent.mk i = Quiver.WeaklyConnectedComponent.mk j ↔ G.Reachable ((vertexEquiv G).symm i) ((vertexEquiv G).symm j)

Two doubled-quiver vertices have the same weakly connected component exactly when the graph vertices they come from are reachable.

def TauCeti.DoubledQuiver.connectedComponentEquiv {V : Type u} (G : SimpleGraph V) : G.ConnectedComponent ≃ Quiver.WeaklyConnectedComponent (DoubledQuiver G)

The connected components of a graph are the weakly connected components of its doubled quiver.

@[simp]

theorem TauCeti.DoubledQuiver.connectedComponentEquiv_mk {V : Type u} (G : SimpleGraph V) (i : V) : (connectedComponentEquiv G) (G.connectedComponentMk i) = Quiver.WeaklyConnectedComponent.mk (vertex G i)

@[simp]

theorem TauCeti.DoubledQuiver.connectedComponentEquiv_symm_mk {V : Type u} (G : SimpleGraph V) (i : DoubledQuiver G) : (connectedComponentEquiv G).symm (Quiver.WeaklyConnectedComponent.mk i) = G.connectedComponentMk ((vertexEquiv G).symm i)

theorem TauCeti.DoubledQuiver.preconnected_iff_isStronglyConnected {V : Type u} (G : SimpleGraph V) : G.Preconnected ↔ Quiver.IsStronglyConnected (DoubledQuiver G)

A graph is preconnected exactly when its doubled quiver is strongly connected.

theorem TauCeti.DoubledQuiver.connected_iff {V : Type u} (G : SimpleGraph V) : G.Connected ↔ Nonempty (DoubledQuiver G) ∧ Quiver.IsStronglyConnected (DoubledQuiver G)

A graph is connected exactly when its doubled quiver is nonempty and strongly connected.