Finite representation type passes to subquivers

If a quiver Q' embeds in a quiver Q (TauCeti.QuiverEmbedding) and Q has finite representation type, then so does Q' (TauCeti.IsFiniteRepType.of_quiverEmbedding): extension by zero along the embedding carries the finite-dimensional indecomposable representations of Q' to finite-dimensional indecomposable representations of Q, and it reflects isomorphism, so it embeds the isomorphism classes of the one into those of the other.

Read contrapositively, a quiver containing a subquiver of infinite representation type has infinite representation type itself. This is the reduction by which the non-Dynkin half of Gabriel's theorem is proved: a finite connected quiver whose underlying graph is not a Dynkin diagram contains a subquiver whose graph is an extended Dynkin diagram, and each has infinitely many indecomposables. Applications to loops and parallel arrows are in TauCeti.RepresentationTheory.Quiver.FiniteRepType.Obstructions.

Main results

• TauCeti.IsFiniteRepType.of_quiverEmbedding: finite representation type passes to subquivers.
• TauCeti.isFiniteRepType_iff_of_homEquiv: finite representation type is invariant under isomorphism of quivers.

References

• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Volume I, Chapter VII.
• H. Derksen, J. Weyman, An Introduction to Quiver Representations, Chapter 4.

theorem TauCeti.IsFiniteRepType.of_quiverEmbedding {k : Type u} [Field k] {Q' : Type v'} [Quiver Q'] {Q : Type v} [Quiver Q] (h : IsFiniteRepType k Q) (φ : QuiverEmbedding Q' Q) : IsFiniteRepType k Q'

Finite representation type passes to subquivers. If Q' embeds in a quiver Q of finite representation type then Q' has finite representation type: extension by zero carries the finite-dimensional indecomposables of Q' to finite-dimensional indecomposables of Q, and non-isomorphic ones to non-isomorphic ones.

The representations of Q are taken with vertex spaces in the universe max v' t, where those of Q' live in t and the vertices of Q' in v'; the extension by zero lands there.

theorem TauCeti.isFiniteRepType_iff_of_homEquiv {k : Type u} [Field k] {V : Type v} {q q' : Quiver V} (e : (a b : V) → (a ⟶ b) ≃ (a ⟶ b)) : IsFiniteRepType k V ↔ IsFiniteRepType k V

Finite representation type is invariant under isomorphism of quivers. Two quiver structures on the same vertices whose arrows between any two vertices correspond have finite representation type together.