Extended Dynkin subquivers obstruct finite representation type

The loop quiver has infinitely many nilpotent Jordan block representations (TauCeti.not_isFiniteRepType_oneLoop), and the Kronecker quiver • ⇉ • has infinitely many indecomposable representations (TauCeti.not_isFiniteRepType_kronecker). Finite representation type passes to subquivers (TauCeti.IsFiniteRepType.of_quiverEmbedding), so these families, together with the oriented two-cycle obstruction, show that a quiver of finite representation type has no loops and at most one arrow between any two vertices, counting both directions. These are the two smallest extended Dynkin obstructions, Ã₀ and Ã₁, in the non-Dynkin half of Gabriel's theorem.

The four subspace quiver, whose underlying graph is the extended Dynkin diagram D4~, has infinite representation type as well (TauCeti.not_isFiniteRepType_subspace_fin_four), so a quiver of finite representation type has no vertex receiving arrows from four distinct other vertices.

Main results

• TauCeti.IsFiniteRepType.isEmpty_hom_self: a quiver of finite representation type has no loops.
• TauCeti.IsFiniteRepType.subsingleton_hom: a quiver of finite representation type has no two parallel arrows.
• TauCeti.IsFiniteRepType.isEmpty_hom_reverse: an arrow has no reverse arrow.
• TauCeti.IsFiniteRepType.card_hom_add_card_hom_le_one: there is at most one arrow between two vertices, counting both directions, and no loop.
• TauCeti.not_isFiniteRepType_of_forall_nonempty_hom: a vertex receiving arrows from four distinct other vertices refutes finite representation type.
• TauCeti.not_isFiniteRepType_subspace: a subspace quiver with at least four outer vertices has infinite representation type.

Implementation notes

The consequences are stated for representations with vertex spaces in the universe of the base field, the universe in which the loop-quiver, Kronecker and four subspace families are built.

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.isEmpty_hom_self {k : Type u} [Field k] {Q : Type v} [Quiver Q] (h : IsFiniteRepType k Q) (i : Q) : IsEmpty (i ⟶ i)

A quiver of finite representation type has no loops: a loop embeds the loop quiver, whose nilpotent Jordan blocks are infinitely many pairwise non-isomorphic indecomposables.

theorem TauCeti.IsFiniteRepType.subsingleton_hom {k : Type u} [Field k] {Q : Type v} [Quiver Q] (h : IsFiniteRepType k Q) (i j : Q) : Subsingleton (i ⟶ j)

A quiver of finite representation type has at most one arrow from any vertex to any other: two parallel arrows between distinct vertices embed the Kronecker quiver • ⇉ •, and two loops at one vertex are excluded already by TauCeti.IsFiniteRepType.isEmpty_hom_self.

theorem TauCeti.IsFiniteRepType.isEmpty_hom_reverse {k : Type u} [Field k] {Q : Type v} [Quiver Q] (h : IsFiniteRepType k Q) {a b : Q} (α : a ⟶ b) : IsEmpty (b ⟶ a)

An arrow in a quiver of finite representation type has no reverse arrow.

theorem TauCeti.IsFiniteRepType.card_hom_add_card_hom_le_one {k : Type u} [Field k] {Q : Type v} [Quiver Q] [(a b : Q) → Fintype (a ⟶ b)] (h : IsFiniteRepType k Q) (a b : Q) : Fintype.card (a ⟶ b) + Fintype.card (b ⟶ a) ≤ 1

Over a quiver of finite representation type, two vertices are joined by at most one arrow, counting both directions, and there is no loop.

theorem TauCeti.not_isFiniteRepType_of_forall_nonempty_hom {k : Type u} [Field k] {Q : Type v} [Quiver Q] {c : Q} (x : Fin 4 ↪ Q) (hc : c ∉ Set.range ⇑x) (hα : ∀ (i : Fin 4), Nonempty (x i ⟶ c)) : ¬IsFiniteRepType k Q

Four arrows into one vertex from four other distinct vertices obstruct finite representation type: they embed the four subspace quiver, whose underlying graph is the extended Dynkin diagram D4~ and whose Jordan block configurations are infinitely many pairwise non-isomorphic indecomposables.

theorem TauCeti.not_isFiniteRepType_subspace {k : Type u} [Field k] {ι : Type v} (f : Fin 4 ↪ ι) : ¬IsFiniteRepType k (Quiver.Subspace ι)

A subspace quiver with at least four outer vertices has infinite representation type over every field: four of its arrows already embed the four subspace quiver.