mathlib documentation

combinatorics.quiver.connected_component

Weakly connected components #

For a quiver V, we build a quiver symmetrify V by adding a reversal of every edge. Informally, a path in symmetrify V corresponds to a 'zigzag' in V. This lets us define the type weakly_connected_component V as the quotient of V by the relation which identifies a with b if there is a path from a to b in symmetrify V. (These zigzags can be seen as a proof-relevant analogue of eqv_gen.)

Strongly connected components have not yet been defined.

source
@[nolint]
def quiver.symmetrify (V : Type u) :
Type u

A type synonym for the symmetrized quiver (with an arrow both ways for each original arrow). NB: this does not work for Prop-valued quivers. It requires [quiver.{v+1} V].

Equations
source
@[protected, instance]
def quiver.symmetrify_quiver (V : Type u) [quiver V] :
quiver (quiver.symmetrify V)
Equations
source
@[class]
structure quiver.has_reverse (V : Type u) [quiver V] :
Type (max u v)
  • reverse' : Π {a b : V}, (a ⟶ b) → (b ⟶ a)

A quiver has_reverse if we can reverse an arrow p from a to b to get an arrow p.reverse from b to a.

Instances
source
@[protected, instance]
def quiver.symmetrify.has_reverse (V : Type u) [quiver V] :
quiver.has_reverse (quiver.symmetrify V)
Equations
source
def quiver.reverse {V : Type u} [quiver V] [quiver.has_reverse V] {a b : V} :
(a ⟶ b) → (b ⟶ a)

Reverse the direction of an arrow.

Equations
source
def quiver.path.reverse {V : Type u} [quiver V] [quiver.has_reverse V] {a b : V} :
quiver.path a b → quiver.path b a

Reverse the direction of a path.

Equations
source
def quiver.zigzag_setoid (V : Type u) [quiver V] :
setoid V

Two vertices are related in the zigzag setoid if there is a zigzag of arrows from one to the other.

Equations
source
def quiver.weakly_connected_component (V : Type u) [quiver V] :
Type u

The type of weakly connected components of a directed graph. Two vertices are in the same weakly connected component if there is a zigzag of arrows from one to the other.

Equations
source
@[protected]
def quiver.weakly_connected_component.mk {V : Type u} [quiver V] :
V → quiver.weakly_connected_component V

The weakly connected component corresponding to a vertex.

Equations
source
@[protected, instance]
def quiver.weakly_connected_component.has_coe_t {V : Type u} [quiver V] :
has_coe_t V (quiver.weakly_connected_component V)
Equations
source
@[protected, instance]
def quiver.weakly_connected_component.inhabited {V : Type u} [quiver V] [inhabited V] :
inhabited (quiver.weakly_connected_component V)
Equations
source
@[protected]
theorem quiver.weakly_connected_component.eq {V : Type u} [quiver V] (a b : V) :
↑a = ↑b ↔ nonempty (quiver.path a b)
source
def quiver.wide_subquiver_symmetrify {V : Type u} [quiver V] (H : wide_subquiver (quiver.symmetrify V)) :
wide_subquiver V

A wide subquiver H of G.symmetrify determines a wide subquiver of G, containing an an arrow e if either e or its reversal is in H.

Equations