Finite paths in acyclic quivers

This file proves that a finite quiver with finitely many arrows between any two vertices has only finitely many paths exactly when it is acyclic. The forward half supplies the finiteness hypothesis needed for the finite-dimensionality of its path algebra. The bound that makes the count finite is the acyclic one: every path has length below the number of vertices, so the count reduces to the bounded-length count of TauCeti.Combinatorics.Quiver.BoundedPaths.

The converse needs no finiteness of the quiver at all: an oriented cycle has infinitely many powers (Quiver.Path.infinite_of_ne_nil), so a quiver with finitely many paths has none — the form the proof uses is the contrapositive Quiver.Path.eq_nil_of_finite.

Main results

• TauCeti.finite_paths_of_isAcyclic: a finite acyclic quiver with finite arrow types has finitely many paths.
• TauCeti.isAcyclic_of_finite_paths: a quiver with finitely many paths is acyclic.
• TauCeti.isAcyclic_iff_finite_paths: the two together, the extensional form of acyclicity that the finite-dimensionality of the path algebra is read off.

References

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. II.

theorem TauCeti.Quiver.IsAcyclic.length_lt_card {V : Type u} [Quiver V] (h : IsAcyclic V) [Fintype V] {a b : V} (p : Quiver.Path a b) : p.length < Fintype.card V

Every path in an acyclic finite quiver has length strictly below the number of vertices.

theorem TauCeti.finite_paths_of_isAcyclic {V : Type u} [Quiver V] [Finite V] [∀ (a b : V), Finite (a ⟶ b)] (h : Quiver.IsAcyclic V) : Finite ((a : V) × (b : V) × Quiver.Path a b)

A finite acyclic quiver with finite arrow types has finitely many paths.

theorem TauCeti.isAcyclic_of_finite_paths {V : Type u} [Quiver V] (h : Finite ((a : V) × (b : V) × Quiver.Path a b)) : Quiver.IsAcyclic V

A quiver with finitely many paths is acyclic: the powers of an oriented cycle are already infinitely many paths. No finiteness of the vertices or of the arrows is needed.

theorem TauCeti.isAcyclic_iff_finite_paths {V : Type u} [Quiver V] [Finite V] [∀ (a b : V), Finite (a ⟶ b)] : Quiver.IsAcyclic V ↔ Finite ((a : V) × (b : V) × Quiver.Path a b)

For a finite quiver with finite arrow types, acyclicity is finiteness of the path space. This is the extensional form of acyclicity, the hypothesis under which the path algebra is a finite module.