The reachability order on strongly connected components

The strongly connected components of a quiver are the classes of vertices joined by paths in both directions. Reachability descends to them: one component is below another when some, equivalently every, vertex of the first has a path to some, equivalently every, vertex of the second. This relation is a partial order, the reachability order of the condensation of the quiver, and the components are finite in number when the vertices are. This order organizes, for instance, the minimum cuts of a network through the strongly connected components of its residual network.

Main results

• Quiver.StronglyConnectedComponent.instPartialOrder: strongly connected components are partially ordered by reachability.
• Quiver.StronglyConnectedComponent.mk_le_mk: the component of a is below that of b exactly when there is a path from a to b.
• Quiver.StronglyConnectedComponent.mk_surjective: every component contains a vertex.

theorem Quiver.StronglyConnectedComponent.mk_surjective {V : Type u_1} [Quiver V] : Function.Surjective StronglyConnectedComponent.mk

Every strongly connected component contains a vertex.

instance Quiver.StronglyConnectedComponent.instFinite_tauCeti {V : Type u_1} [Quiver V] [Finite V] : Finite (StronglyConnectedComponent V)

@[instance_reducible]

instance Quiver.StronglyConnectedComponent.instPartialOrder {V : Type u_1} [Quiver V] : PartialOrder (StronglyConnectedComponent V)

Strongly connected components are partially ordered by reachability: C ≤ D when a vertex of C has a path to a vertex of D.

@[simp]

theorem Quiver.StronglyConnectedComponent.mk_le_mk {V : Type u_1} [Quiver V] {a b : V} : StronglyConnectedComponent.mk a ≤ StronglyConnectedComponent.mk b ↔ Nonempty (Path a b)

The component of a is below the component of b exactly when there is a path from a to b.