Documentation

TauCeti.Combinatorics.Quiver.BoundedPaths

Finitely many paths of bounded length #

A quiver with finitely many vertices and finitely many arrows between any two of them has only finitely many paths of any given length, because a path of length at most n is a list of at most n arrows. No acyclicity is involved: the bound on the length is what makes the count finite, and an acyclic quiver is exactly one where such a bound is automatic.

Main results #

References #

The unbounded consequence for an acyclic quiver, TauCeti.finite_paths_of_isAcyclic, is in TauCeti.RepresentationTheory.Quiver.Acyclic.FinitePaths; it is the finite_paths_of_isAcyclic target of Layer 0 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. The bounded count here is what the finite dimensionality of a bound quiver algebra rests on (TauCeti.RepresentationTheory.Quiver.AdmissibleIdeal.Basic), where no such bound is automatic.

source
theorem TauCeti.Quiver.finite_boundedPaths {V : Type u} [Quiver V] [Finite V] [∀ (a b : V), Finite (a ⟶ b)] (n : ℕ) (a b : V) :
Finite (Quiver.Path.BoundedPaths a b n)

Paths of bounded length are finite when there are finitely many vertices and finitely many arrows between any two of them: a path of length at most n + 1 is either trivial or an arrow followed by a path of length at most n.

source
theorem TauCeti.Quiver.finite_setOf_length_le {V : Type u} [Quiver V] [Finite V] [∀ (a b : V), Finite (a ⟶ b)] (n : ℕ) :
{x : (a : V) × (b : V) × Quiver.Path a b | x.snd.snd.length ≤ n}.Finite

The paths of length at most n are a finite subset of the total path space.

source
theorem TauCeti.Quiver.finite_setOf_length_lt {V : Type u} [Quiver V] [Finite V] [∀ (a b : V), Finite (a ⟶ b)] (n : ℕ) :
{x : (a : V) × (b : V) × Quiver.Path a b | x.snd.snd.length < n}.Finite

The paths of length less than n are a finite subset of the total path space.