Mathlib.Combinatorics.Quiver.Symmetric

Quiver.Symmetrify definition

(V : Type*)

Full source

/-- 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]`. -/
def Symmetrify (V : Type*) := V

Symmetrized quiver

Informal description

The type `Symmetrify V` is a type synonym for a quiver `V` that adds formal inverses to each arrow of `V`, effectively symmetrizing the quiver by including both directions for every original arrow. This construction requires that the original quiver `V` is not `Prop`-valued (i.e., it must be a `Type`-valued quiver).

Quiver.symmetrifyQuiver instance

(V : Type u) [Quiver V] : Quiver (Symmetrify V)

Full source

instance symmetrifyQuiver (V : Type u) [Quiver V] : Quiver (Symmetrify V) :=
  ⟨fun a b : V ↦ (a ⟶ b) ⊕ (b ⟶ a)⟩

Quiver Structure on Symmetrized Quivers

Informal description

For any quiver $V$, the symmetrized quiver $\text{Symmetrify}\, V$ is equipped with a quiver structure where each arrow in $V$ is augmented with a formal inverse arrow.

Quiver.HasReverse structure

Full source

/-- A quiver `HasReverse` if we can reverse an arrow `p` from `a` to `b` to get an arrow
    `p.reverse` from `b` to `a`. -/
class HasReverse where
  /-- the map which sends an arrow to its reverse -/
  reverse' : ∀ {a b : V}, (a ⟶ b) → (b ⟶ a)

Quiver with arrow reversal

Informal description

A quiver $V$ is said to *have reverse* if for every arrow $p$ from vertex $a$ to vertex $b$ in $V$, there exists a corresponding reversed arrow from $b$ to $a$.

Quiver.reverse definition

{V} [Quiver.{v + 1} V] [HasReverse V] {a b : V} : (a ⟶ b) → (b ⟶ a)

Full source

/-- Reverse the direction of an arrow. -/
def reverse {V} [Quiver.{v + 1} V] [HasReverse V] {a b : V} : (a ⟶ b) → (b ⟶ a) :=
  HasReverse.reverse'

Arrow reversal in a quiver

Informal description

Given a quiver $V$ with arrow reversal, the function $\text{reverse}$ maps an arrow $f : a \to b$ to its reversed arrow $\text{reverse}(f) : b \to a$.

Quiver.HasInvolutiveReverse structure

extends HasReverse V

Full source

/-- A quiver `HasInvolutiveReverse` if reversing twice is the identity. -/
class HasInvolutiveReverse extends HasReverse V where
  /-- `reverse` is involutive -/
  inv' : ∀ {a b : V} (f : a ⟶ b), reverse (reverse f) = f

Quiver with involutive reverse

Informal description

A quiver $ V $ is said to have an involutive reverse if it is equipped with an operation that assigns to each arrow $ f : a \to b $ a reverse arrow $ \text{reverse}(f) : b \to a $, and this operation satisfies the involutive property: reversing an arrow twice returns the original arrow, i.e., $ \text{reverse}(\text{reverse}(f)) = f $ for every arrow $ f $.

Quiver.reverse_reverse theorem

[h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) : reverse (reverse f) = f

Full source

@[simp]
theorem reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (f : a ⟶ b) :
    reverse (reverse f) = f := by apply h.inv'

Involutive Property of Arrow Reversal in a Quiver

Informal description

For any quiver $V$ with an involutive reverse operation, and for any arrow $f : a \to b$ in $V$, the reverse of the reverse of $f$ is equal to $f$, i.e., $\text{reverse}(\text{reverse}(f)) = f$.

Quiver.reverse_inj theorem

[h : HasInvolutiveReverse V] {a b : V} (f g : a ⟶ b) : reverse f = reverse g ↔ f = g

Full source

@[simp]
theorem reverse_inj [h : HasInvolutiveReverse V] {a b : V}
    (f g : a ⟶ b) : reversereverse f = reverse g ↔ f = g := by
  constructor
  · rintro h
    simpa using congr_arg Quiver.reverse h
  · rintro h
    congr

Injectivity of Arrow Reversal in a Quiver with Involutive Reverse

Informal description

For any quiver $V$ with an involutive reverse operation, and for any two arrows $f, g : a \to b$ in $V$, the reverses of $f$ and $g$ are equal if and only if $f$ and $g$ are equal, i.e., $\text{reverse}(f) = \text{reverse}(g) \leftrightarrow f = g$.

Prefunctor.MapReverse structure

(φ : U ⥤q V)

Full source

/-- A prefunctor preserving reversal of arrows -/
class _root_.Prefunctor.MapReverse (φ : U ⥤q V) : Prop where
  /-- The image of a reverse is the reverse of the image. -/
  map_reverse' : ∀ {u v : U} (e : u ⟶ v), φ.map (reverse e) = reverse (φ.map e)

Prefunctor preserving arrow reversal

Informal description

A structure indicating that a prefunctor $\phi : U \to V$ between quivers preserves the reversal of arrows, meaning that for any arrow $e : u \to v$ in $U$, the image of the reversed arrow $\text{reverse}(e)$ under $\phi$ is equal to the reversed arrow of the image $\text{reverse}(\phi(e))$ in $V$.

Prefunctor.map_reverse theorem

(φ : U ⥤q V) [φ.MapReverse] {u v : U} (e : u ⟶ v) : φ.map (reverse e) = reverse (φ.map e)

Full source

@[simp]
theorem _root_.Prefunctor.map_reverse (φ : U ⥤q V) [φ.MapReverse]
    {u v : U} (e : u ⟶ v) : φ.map (reverse e) = reverse (φ.map e) :=
  Prefunctor.MapReverse.map_reverse' e

Prefunctor Preserves Arrow Reversal

Informal description

Let $\phi : U \to V$ be a prefunctor between quivers that preserves arrow reversal. Then for any arrow $e : u \to v$ in $U$, the image of the reversed arrow $\text{reverse}(e)$ under $\phi$ equals the reversed arrow of the image $\text{reverse}(\phi(e))$ in $V$, i.e., \[ \phi(\text{reverse}(e)) = \text{reverse}(\phi(e)). \]

Prefunctor.mapReverseComp instance

(φ : U ⥤q V) (ψ : V ⥤q W) [φ.MapReverse] [ψ.MapReverse] : (φ ⋙q ψ).MapReverse

Full source

instance _root_.Prefunctor.mapReverseComp
    (φ : U ⥤q V) (ψ : V ⥤q W) [φ.MapReverse] [ψ.MapReverse] :
    (φ ⋙q ψ).MapReverse where
  map_reverse' e := by
    simp only [Prefunctor.comp_map, Prefunctor.MapReverse.map_reverse']

Composition of Arrow-Reversal-Preserving Prefunctors Preserves Arrow Reversal

Informal description

Given two prefunctors $\phi : U \to V$ and $\psi : V \to W$ between quivers that both preserve arrow reversal, their composition $\phi \circ \psi$ also preserves arrow reversal.

Prefunctor.mapReverseId instance

: (Prefunctor.id U).MapReverse

Full source

instance _root_.Prefunctor.mapReverseId :
    (Prefunctor.id U).MapReverse where
  map_reverse' _ := rfl

Identity Prefunctor Preserves Arrow Reversal

Informal description

The identity prefunctor $\text{id} : U \to U$ preserves arrow reversal, meaning that for any arrow $e : u \to v$ in $U$, the image of the reversed arrow $\text{reverse}(e)$ under $\text{id}$ is equal to the reversed arrow of the image $\text{reverse}(\text{id}(e))$.

Quiver.instHasReverseSymmetrify instance

: HasReverse (Symmetrify V)

Full source

instance : HasReverse (Symmetrify V) :=
  ⟨fun e => e.swap⟩

Existence of Arrow Reversals in Symmetrized Quivers

Informal description

The symmetrized quiver $\text{Symmetrify}\, V$ has a reverse operation, meaning every arrow in $\text{Symmetrify}\, V$ has a formal inverse arrow.

Quiver.instHasInvolutiveReverseSymmetrify instance

: HasInvolutiveReverse (Symmetrify V)

Full source

instance :
    HasInvolutiveReverse
      (Symmetrify V) where
  toHasReverse := ⟨fun e ↦ e.swap⟩
  inv' e := congr_fun Sum.swap_swap_eq e

Involutive Reversal in Symmetrized Quivers

Informal description

The symmetrized quiver $\text{Symmetrify}\, V$ has an involutive reverse operation, meaning that for every arrow $e$ in $\text{Symmetrify}\, V$, the reverse of the reverse of $e$ is equal to $e$ itself.

Quiver.symmetrify_reverse theorem

{a b : Symmetrify V} (e : a ⟶ b) : reverse e = e.swap

Full source

@[simp]
theorem symmetrify_reverse {a b : Symmetrify V} (e : a ⟶ b) : reverse e = e.swap :=
  rfl

Reversal Equals Swap in Symmetrized Quiver

Informal description

For any vertices $a$ and $b$ in the symmetrized quiver $\text{Symmetrify}\, V$, and any arrow $e \colon a \to b$, the reverse of $e$ is equal to the swapped arrow $e.\text{swap}$.

Quiver.Hom.toPos abbrev

{X Y : V} (f : X ⟶ Y) : (Quiver.symmetrifyQuiver V).Hom X Y

Full source

/-- Shorthand for the "forward" arrow corresponding to `f` in `symmetrify V` -/
abbrev Hom.toPos {X Y : V} (f : X ⟶ Y) : (Quiver.symmetrifyQuiver V).Hom X Y :=
  Sum.inl f

Forward Arrow in Symmetrized Quiver

Informal description

For any quiver $V$ and any arrow $f \colon X \to Y$ in $V$, the function $\mathrm{toPos}$ constructs the corresponding "forward" arrow $f \colon X \to Y$ in the symmetrized quiver $\mathrm{Symmetrify}\, V$.

Quiver.Hom.toNeg abbrev

{X Y : V} (f : X ⟶ Y) : (Quiver.symmetrifyQuiver V).Hom Y X

Full source

/-- Shorthand for the "backward" arrow corresponding to `f` in `symmetrify V` -/
abbrev Hom.toNeg {X Y : V} (f : X ⟶ Y) : (Quiver.symmetrifyQuiver V).Hom Y X :=
  Sum.inr f

Formal Inverse Arrow in Symmetrized Quiver

Informal description

For any quiver $V$ and any arrow $f \colon X \to Y$ in $V$, the function `toNeg` constructs the formal inverse arrow $f^{-1} \colon Y \to X$ in the symmetrized quiver $\text{Symmetrify}\, V$.

Quiver.Path.reverse definition

[HasReverse V] {a : V} : ∀ {b}, Path a b → Path b a

Full source

/-- Reverse the direction of a path. -/
@[simp]
def Path.reverse [HasReverse V] {a : V} : ∀ {b}, Path a b → Path b a
  | _, Path.nil => Path.nil
  | _, Path.cons p e => (Quiver.reverse e).toPath.comp p.reverse

Path reversal in a quiver with arrow reversal

Informal description

Given a quiver $V$ with arrow reversal, the function $\mathrm{reverse}$ maps a path $p$ from vertex $a$ to vertex $b$ to its reversed path from $b$ to $a$. The reversal is defined recursively: - The reverse of the empty path is the empty path. - The reverse of a path $p$ followed by an edge $e$ is the composition of the reversed path of $p$ with the reversed edge of $e$.

Quiver.Path.reverse_toPath theorem

[HasReverse V] {a b : V} (f : a ⟶ b) : f.toPath.reverse = (Quiver.reverse f).toPath

Full source

@[simp]
theorem Path.reverse_toPath [HasReverse V] {a b : V} (f : a ⟶ b) :
    f.toPath.reverse = (Quiver.reverse f).toPath :=
  rfl

Reversal of Single-Arrow Path Equals Path of Reversed Arrow

Informal description

For any quiver $V$ with arrow reversal and any arrow $f \colon a \to b$ in $V$, the reversal of the path consisting solely of $f$ equals the path consisting solely of the reversed arrow $\mathrm{reverse}(f)$. In other words, $\mathrm{reverse}(f.\mathrm{toPath}) = (\mathrm{reverse}\, f).\mathrm{toPath}$.

Quiver.Path.reverse_comp theorem

[HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) : (p.comp q).reverse = q.reverse.comp p.reverse

Full source

@[simp]
theorem Path.reverse_comp [HasReverse V] {a b c : V} (p : Path a b) (q : Path b c) :
    (p.comp q).reverse = q.reverse.comp p.reverse := by
  induction q with
  | nil => simp
  | cons _ _ h => simp [h]

Reversal of Composite Path in Quiver with Arrow Reversal

Informal description

Let $V$ be a quiver with arrow reversal. For any vertices $a, b, c$ in $V$ and any paths $p$ from $a$ to $b$ and $q$ from $b$ to $c$, the reversal of the composite path $p \circ q$ equals the composite of the reversed paths in reverse order, i.e., $\mathrm{reverse}(p \circ q) = \mathrm{reverse}(q) \circ \mathrm{reverse}(p)$.

Quiver.Path.reverse_reverse theorem

[h : HasInvolutiveReverse V] {a b : V} (p : Path a b) : p.reverse.reverse = p

Full source

@[simp]
theorem Path.reverse_reverse [h : HasInvolutiveReverse V] {a b : V} (p : Path a b) :
    p.reverse.reverse = p := by
  induction p with
  | nil => simp
  | cons _ _ h =>
    rw [Path.reverse, Path.reverse_comp, h, Path.reverse_toPath, Quiver.reverse_reverse]
    rfl

Involutive Property of Path Reversal in a Quiver

Informal description

For any quiver $V$ with an involutive reverse operation and any path $p$ from vertex $a$ to vertex $b$ in $V$, reversing the path twice yields the original path, i.e., $\mathrm{reverse}(\mathrm{reverse}(p)) = p$.

Quiver.Symmetrify.of definition

: Prefunctor V (Symmetrify V)

Full source

/-- The inclusion of a quiver in its symmetrification -/
@[simps]
def of : Prefunctor V (Symmetrify V) where
  obj := id
  map := Sum.inl

Inclusion of a quiver into its symmetrification

Informal description

The inclusion map of a quiver $V$ into its symmetrification $\text{Symmetrify}\, V$, which sends each arrow in $V$ to itself (as a forward arrow) in the symmetrified quiver.

Quiver.Symmetrify.lift definition

[HasReverse V'] (φ : Prefunctor V V') : Prefunctor (Symmetrify V) V'

Full source

/-- Given a quiver `V'` with reversible arrows, a prefunctor to `V'` can be lifted to one from
    `Symmetrify V` to `V'` -/
def lift [HasReverse V'] (φ : Prefunctor V V') :
    Prefunctor (Symmetrify V) V' where
  obj := φ.obj
  map
  | Sum.inl g => φ.map g
  | Sum.inr g => reverse (φ.map g)

Lift of a prefunctor to a symmetrized quiver

Informal description

Given a quiver $V'$ with reversible arrows and a prefunctor $\phi : V \to V'$, the function `Symmetrify.lift` constructs a prefunctor from the symmetrized quiver $\text{Symmetrify}\, V$ to $V'$. This prefunctor maps each original arrow $g$ in $V$ to $\phi(g)$ and each formal inverse arrow (added by symmetrization) to the reverse of $\phi(g)$ in $V'$.

Quiver.Symmetrify.lift_spec theorem

[HasReverse V'] (φ : Prefunctor V V') : Symmetrify.of.comp (Symmetrify.lift φ) = φ

Full source

theorem lift_spec [HasReverse V'] (φ : Prefunctor V V') :
    Symmetrify.of.comp (Symmetrify.lift φ) = φ := by
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    rfl

Universal Property of Symmetrify: $\text{Symmetrify.of} \circ \text{Symmetrify.lift}\, \phi = \phi$

Informal description

For any quiver $V'$ with reversible arrows and any prefunctor $\phi \colon V \to V'$, the composition of the inclusion prefunctor $\text{Symmetrify.of} \colon V \to \text{Symmetrify}\, V$ with the lifted prefunctor $\text{Symmetrify.lift}\, \phi \colon \text{Symmetrify}\, V \to V'$ equals $\phi$. In other words, the following diagram commutes: \[ V \xrightarrow{\text{Symmetrify.of}} \text{Symmetrify}\, V \xrightarrow{\text{Symmetrify.lift}\, \phi} V' \]

Quiver.Symmetrify.lift_reverse theorem

 [h : HasInvolutiveReverse V'] (φ : Prefunctor V V') {X Y : Symmetrify V} (f : X ⟶ Y) :
  (Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Symmetrify.lift φ).map f)

Full source

theorem lift_reverse [h : HasInvolutiveReverse V']
    (φ : Prefunctor V V') {X Y : Symmetrify V} (f : X ⟶ Y) :
    (Symmetrify.lift φ).map (Quiver.reverse f) = Quiver.reverse ((Symmetrify.lift φ).map f) := by
  dsimp [Symmetrify.lift]; cases f
  · simp only
    rfl
  · simp only [reverse_reverse]
    rfl

Lifted Prefunctor Preserves Arrow Reversal in Symmetrized Quiver

Informal description

Let $V'$ be a quiver with an involutive reverse operation, and let $\phi \colon V \to V'$ be a prefunctor. For any arrow $f \colon X \to Y$ in the symmetrized quiver $\text{Symmetrify}\, V$, the lifted prefunctor $\text{Symmetrify.lift}\, \phi$ maps the reverse of $f$ to the reverse of $\phi(f)$, i.e., \[ (\text{Symmetrify.lift}\, \phi)(\text{reverse}(f)) = \text{reverse}((\text{Symmetrify.lift}\, \phi)(f)). \]

Quiver.Symmetrify.lift_unique theorem

 [HasReverse V'] (φ : V ⥤q V') (Φ : Symmetrify V ⥤q V') (hΦ : (of ⋙q Φ) = φ)
  (hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y), Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) :
  Φ = Symmetrify.lift φ

Full source

/-- `lift φ` is the only prefunctor extending `φ` and preserving reverses. -/
theorem lift_unique [HasReverse V'] (φ : V ⥤q V') (Φ : SymmetrifySymmetrify V ⥤q V') (hΦ : (ofof ⋙q Φ) = φ)
    (hΦinv : ∀ {X Y : Symmetrify V} (f : X ⟶ Y),
      Φ.map (Quiver.reverse f) = Quiver.reverse (Φ.map f)) :
    Φ = Symmetrify.lift φ := by
  subst_vars
  fapply Prefunctor.ext
  · rintro X
    rfl
  · rintro X Y f
    cases f
    · rfl
    · exact hΦinv (Sum.inl _)

Uniqueness of the Lift of a Prefunctor to a Symmetrized Quiver

Informal description

Let $V'$ be a quiver with arrow reversal, $\phi \colon V \to V'$ a prefunctor, and $\Phi \colon \text{Symmetrify}\, V \to V'$ a prefunctor such that: 1. The composition $\text{Symmetrify.of} \circ \Phi$ equals $\phi$, and 2. For any arrow $f \colon X \to Y$ in $\text{Symmetrify}\, V$, $\Phi$ maps the reverse of $f$ to the reverse of $\Phi(f)$. Then $\Phi$ is equal to the lift of $\phi$, i.e., $\Phi = \text{Symmetrify.lift}\, \phi$.

Prefunctor.symmetrify definition

(φ : U ⥤q V) : Symmetrify U ⥤q Symmetrify V

Full source

/-- A prefunctor canonically defines a prefunctor of the symmetrifications. -/
@[simps]
def _root_.Prefunctor.symmetrify (φ : U ⥤q V) : SymmetrifySymmetrify U ⥤q Symmetrify V where
  obj := φ.obj
  map := Sum.map φ.map φ.map

Symmetrified prefunctor

Informal description

Given a prefunctor $\phi$ from quiver $U$ to quiver $V$, the symmetrified prefunctor $\phi.\text{symmetrify}$ is a prefunctor from $\text{Symmetrify}\, U$ to $\text{Symmetrify}\, V$ that maps objects via $\phi.\text{obj}$ and arrows by applying $\phi.\text{map}$ to both original arrows and their formal inverses.

Prefunctor.symmetrify_mapReverse instance

(φ : U ⥤q V) : Prefunctor.MapReverse φ.symmetrify

Full source

instance _root_.Prefunctor.symmetrify_mapReverse (φ : U ⥤q V) :
    Prefunctor.MapReverse φ.symmetrify :=
  ⟨fun e => by cases e <;> rfl⟩

Symmetrified Prefunctor Preserves Arrow Reversal

Informal description

Given a prefunctor $\phi : U \to V$ between quivers, the symmetrified prefunctor $\phi.\text{symmetrify} : \text{Symmetrify}\, U \to \text{Symmetrify}\, V$ preserves arrow reversal. That is, for any arrow $f$ in $\text{Symmetrify}\, U$, the image of the reversed arrow $\text{reverse}(f)$ under $\phi.\text{symmetrify}$ is equal to the reversed arrow of the image $\text{reverse}(\phi.\text{symmetrify}(f))$ in $\text{Symmetrify}\, V$.

Quiver.Push.instHasReverse instance

[HasReverse V] : HasReverse (Quiver.Push σ)

Full source

instance [HasReverse V] : HasReverse (Quiver.Push σ) where
  reverse' := fun
              | PushQuiver.arrow f => PushQuiver.arrow (reverse f)

Pushforward Quiver Preserves Arrow Reversal

Informal description

Given a quiver $V$ with arrow reversal and a map $\sigma : V \to W$, the pushforward quiver structure on $W$ also has arrow reversal. That is, for every arrow $\sigma(v) \to \sigma(v')$ in $W$ obtained from an arrow $v \to v'$ in $V$, there exists a corresponding reversed arrow $\sigma(v') \to \sigma(v)$ in $W$.

Quiver.Push.instHasInvolutiveReverse instance

[h : HasInvolutiveReverse V] : HasInvolutiveReverse (Push σ)

Full source

instance [h : HasInvolutiveReverse V] :
    HasInvolutiveReverse (Push σ) where
  reverse' := fun
  | PushQuiver.arrow f => PushQuiver.arrow (reverse f)
  inv' := fun
  | PushQuiver.arrow f => by dsimp [reverse]; congr; apply h.inv'

Pushforward Quiver Preserves Involutive Reverse

Informal description

Given a quiver $V$ with an involutive reverse operation and a map $\sigma : V \to W$, the pushforward quiver structure on $W$ also has an involutive reverse operation. That is, for every arrow $\sigma(v) \to \sigma(v')$ in $W$ obtained from an arrow $v \to v'$ in $V$, there exists a corresponding reversed arrow $\sigma(v') \to \sigma(v)$ in $W$, and reversing an arrow twice returns the original arrow.

Quiver.Push.of_reverse theorem

[HasInvolutiveReverse V] (X Y : V) (f : X ⟶ Y) : (reverse <| (Push.of σ).map f) = (Push.of σ).map (reverse f)

Full source

theorem of_reverse [HasInvolutiveReverse V] (X Y : V) (f : X ⟶ Y) :
    (reverse <| (Push.of σ).map f) = (Push.of σ).map (reverse f) :=
  rfl

Pushforward of Arrow Reversal in Quivers with Involutive Reverse

Informal description

Let $V$ be a quiver with an involutive reverse operation, and let $\sigma : V \to W$ be a map. For any vertices $X, Y$ in $V$ and any arrow $f : X \to Y$, the reverse of the pushforward arrow $(Push.of \sigma).map f$ in the pushforward quiver equals the pushforward of the reverse arrow $(Push.of \sigma).map (reverse f)$. That is, \[ \text{reverse}((Push.of \sigma).map f) = (Push.of \sigma).map (\text{reverse} f). \]

Quiver.Push.ofMapReverse instance

[h : HasInvolutiveReverse V] : (Push.of σ).MapReverse

Full source

instance ofMapReverse [h : HasInvolutiveReverse V] : (Push.of σ).MapReverse :=
  ⟨by simp [of_reverse]⟩

Prefunctor Preserves Arrow Reversal in Pushforward Quiver

Informal description

Given a quiver $V$ with an involutive reverse operation and a map $\sigma : V \to W$, the prefunctor $\text{Push.of} \sigma$ preserves the reversal of arrows. That is, for any arrow $f$ in $V$, the reverse of the pushforward arrow $(\text{Push.of} \sigma).map f$ is equal to the pushforward of the reverse arrow $(\text{Push.of} \sigma).map (\text{reverse} f)$.

Quiver.IsPreconnected definition

(V) [Quiver.{u + 1} V]

Full source

/-- A quiver is preconnected iff there exists a path between any pair of
vertices.
Note that if `V` doesn't `HasReverse`, then the definition is stronger than
simply having a preconnected underlying `SimpleGraph`, since a path in one
direction doesn't induce one in the other.
-/
def IsPreconnected (V) [Quiver.{u + 1} V] :=
  ∀ X Y : V, Nonempty (Path X Y)

Preconnected Quiver

Informal description

A quiver $ V $ is called *preconnected* if for any two vertices $ X $ and $ Y $ in $ V $, there exists a directed path from $ X $ to $ Y $. Note that if $ V $ does not have a formal inverse operation for its arrows (i.e., it does not satisfy `HasReverse`), then this definition is stronger than simply requiring the underlying undirected graph to be connected, since the existence of a path in one direction does not imply the existence of a path in the opposite direction.