Finite representation type of a quiver and of its path algebra

For a quiver with finitely many paths, the quiver has finite representation type (TauCeti.IsFiniteRepType) exactly when its path algebra is representation-finite (TauCeti.IsRepresentationFinite). The equivalence TauCeti.quiverRepEquivalence between representations and path-algebra modules matches pointwise finite-dimensional representations with finitely generated modules, and preserves indecomposability, so it identifies the two skeletons of indecomposables.

With Gabriel's theorem (TauCeti.isFiniteRepType_iff_titsForm_posDef) this gives the classification of the representation-finite path algebras: for a connected quiver with finitely many paths, the path algebra is representation-finite exactly when the Tits form is positive definite (TauCeti.isRepresentationFinite_pathAlgebra_iff_titsForm_posDef).

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. I (2006), Chapters III and VII.
• P. Gabriel, Unzerlegbare Darstellungen I, Manuscripta Math. 6 (1972), 71--103.

theorem TauCeti.isFiniteRepType_iff_isRepresentationFinite_pathAlgebra (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] : IsFiniteRepType k Q ↔ IsRepresentationFinite (pathAlgebra k Q)

A quiver with finitely many paths has finite representation type exactly when its path algebra is representation-finite.

theorem TauCeti.isRepresentationFinite_pathAlgebra_iff_titsForm_posDef (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite (Quiver.TotalPath Q)] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (hconn : (Quiver.underlyingGraph Q).Connected) : IsRepresentationFinite (pathAlgebra k Q) ↔ (titsForm Q).PosDef

Gabriel's theorem for path algebras. For a finite connected quiver with finitely many paths, the path algebra is representation-finite exactly when the Tits form is positive definite.