Documentation

TauCeti.Combinatorics.Quiver.Reachable

Directed and zigzag reachability in a quiver #

A vertex b of a quiver is reachable from a (Quiver.Reachable a b) when some directed path runs from a to b. This is the reflexive transitive closure of the relation "some arrow runs from x to y", which turns statements about reachability into statements about relations, where the arrows themselves no longer appear.

Two vertices lie in the same weakly connected component when a zigzag of arrows, each traversed in either direction, joins them, that is, a path in the symmetrized quiver. Since loops and the multiplicity of arrows play no role, this is reachability in the simple graph underlying the quiver (TauCeti.Quiver.underlyingGraph), and the weakly connected components of a quiver are the connected components of its underlying graph.

Main results #

source
theorem Quiver.reachable_iff_reflTransGen {V : Type u} [Quiver V] {a b : V} :
Reachable a b ↔ Relation.ReflTransGen (fun (x y : V) => Nonempty (x ⟶ y)) a b

Directed reachability is the reflexive transitive closure of the relation "some arrow runs from x to y".

source
theorem Quiver.nonempty_path_symmetrify_iff_eqvGen {V : Type u} [Quiver V] {a b : V} :
Nonempty (Path a b) ↔ Relation.EqvGen (fun (x y : V) => Nonempty (x ⟶ y)) a b

Two vertices are joined by a zigzag of arrows, a path in the symmetrized quiver, exactly when they are related by the equivalence relation generated by the relation "some arrow runs from x to y". A zigzag is thus a proof-relevant witness of Relation.EqvGen.

source
theorem TauCeti.Quiver.nonempty_path_symmetrify_iff_reachable {V : Type u} [Quiver V] {a b : V} :
Nonempty (Quiver.Path a b) ↔ (underlyingGraph V).Reachable a b

Two vertices are joined by a zigzag of arrows, a path in the symmetrized quiver, exactly when they are reachable in the underlying graph.

source
theorem TauCeti.Quiver.weaklyConnectedComponent_mk_eq_mk_iff {V : Type u} [Quiver V] {a b : V} :
Quiver.WeaklyConnectedComponent.mk a = Quiver.WeaklyConnectedComponent.mk b ↔ (underlyingGraph V).Reachable a b

Two vertices lie in the same weakly connected component exactly when they are reachable in the underlying graph.

source
def TauCeti.Quiver.weaklyConnectedComponentEquiv (V : Type u) [Quiver V] :
Quiver.WeaklyConnectedComponent V ≃ (underlyingGraph V).ConnectedComponent

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

Instances For
    source
    @[simp]
    theorem TauCeti.Quiver.weaklyConnectedComponentEquiv_mk {V : Type u} [Quiver V] (a : V) :
    (weaklyConnectedComponentEquiv V) (Quiver.WeaklyConnectedComponent.mk a) = (underlyingGraph V).connectedComponentMk a
    source
    @[simp]
    theorem TauCeti.Quiver.weaklyConnectedComponentEquiv_symm_mk {V : Type u} [Quiver V] (a : V) :
    (weaklyConnectedComponentEquiv V).symm ((underlyingGraph V).connectedComponentMk a) = Quiver.WeaklyConnectedComponent.mk a
    source
    @[reducible, inline]
    abbrev TauCeti.Quiver.ComponentVertex {V : Type u} (Q : V → V → Type v) (C : Quiver.WeaklyConnectedComponent V) :
    Type u

    The vertices in a fixed weakly connected component of an explicit arrow family.

    Instances For
      source
      @[reducible, inline]
      abbrev TauCeti.Quiver.ComponentHom {V : Type u} (Q : V → V → Type v) (C : Quiver.WeaklyConnectedComponent V) :
      ComponentVertex Q C → ComponentVertex Q C → Type v

      The restriction of an explicit arrow family to a fixed weakly connected component.

      Instances For
        source
        @[instance_reducible]
        noncomputable instance TauCeti.Quiver.instFintypeComponentVertex {V : Type u} {Q : V → V → Type v} [Fintype V] (C : Quiver.WeaklyConnectedComponent V) :
        Fintype (ComponentVertex Q C)

        A component of a finite vertex type has finitely many vertices.

        source
        theorem TauCeti.Quiver.weaklyConnectedComponent_mk_eq_of_hom {V : Type u} {Q : V → V → Type v} {x y : V} (e : Q x y) :
        Quiver.WeaklyConnectedComponent.mk x = Quiver.WeaklyConnectedComponent.mk y

        The endpoints of an arrow lie in the same weakly connected component.

        source
        @[reducible, inline]
        abbrev TauCeti.Quiver.componentIncomingEquiv {V : Type u} {Q : V → V → Type v} (C : Quiver.WeaklyConnectedComponent V) (x : ComponentVertex Q C) :
        (y : ComponentVertex Q C) × Q ↑y ↑x ≃ (y : V) × Q y ↑x

        The arrows entering a vertex from within its component are exactly all arrows entering that vertex.

        Instances For
          source
          @[simp]
          theorem TauCeti.Quiver.componentIncomingEquiv_apply {V : Type u} {Q : V → V → Type v} (C : Quiver.WeaklyConnectedComponent V) (x : ComponentVertex Q C) (a : (y : ComponentVertex Q C) × Q ↑y ↑x) :
          (componentIncomingEquiv C x) a = ⟨↑a.fst, a.snd⟩

          The incoming-arrow equivalence retains the vertex and arrow.

          source
          @[reducible, inline]
          abbrev TauCeti.Quiver.componentOutgoingEquiv {V : Type u} {Q : V → V → Type v} (C : Quiver.WeaklyConnectedComponent V) (x : ComponentVertex Q C) :
          (y : ComponentVertex Q C) × Q ↑x ↑y ≃ (y : V) × Q (↑x) y

          The arrows leaving a vertex for vertices within its component are exactly all arrows leaving that vertex.

          Instances For
            source
            @[simp]
            theorem TauCeti.Quiver.componentOutgoingEquiv_apply {V : Type u} {Q : V → V → Type v} (C : Quiver.WeaklyConnectedComponent V) (x : ComponentVertex Q C) (a : (y : ComponentVertex Q C) × Q ↑x ↑y) :
            (componentOutgoingEquiv C x) a = ⟨↑a.fst, a.snd⟩

            The outgoing-arrow equivalence retains the vertex and arrow.