Cycles in the underlying graph obstruct finite representation type

A cycle x 0, x 1, …, x (n + 2) of pairwise distinct vertices of a quiver Q, with an arrow in one direction or the other between each x i and x (i + 1) and between x (n + 2) and x 0, is the extended Dynkin diagram Ã_{n+2} in some orientation. This file shows that, whatever the orientation, Q then has infinite representation type over every field (TauCeti.not_isFiniteRepType_of_injective_of_nonempty_hom_sum).

The infinite family lives on the full subquiver of Q on the vertices of the cycle. Its r-th member puts the truncated polynomial algebra k[X]/(Xʳ⁺¹) at every vertex of the cycle; an arrow between x (n + 2) and x 0, in either direction, acts by multiplication by X, and every other arrow by the identity. Naturality along the arrows of the cycle other than the closing one forces an endomorphism to have the same component at every vertex, whatever their directions, and naturality along the closing arrow then says that this common component commutes with multiplication by X. So the endomorphism is multiplication by an element of the local ring k[X]/(Xʳ⁺¹), and the representation is indecomposable; its dimension vector is constant equal to r + 1 on the cycle, so different members are non-isomorphic.

Read through the underlying graph, this says that a quiver of finite representation type has a forest as underlying graph (TauCeti.IsFiniteRepType.isAcyclic_underlyingGraph): the cycles of length at least three are the copies of SimpleGraph.cycleGraph, which Mathlib's SimpleGraph.isAcyclic_iff_free_cycleGraph identifies as the obstructions to acyclicity. With the tree case of Gabriel's dichotomy (TauCeti.IsFiniteRepType.posDef_titsForm_of_isTree) this gives the dichotomy's converse half for every finite connected quiver with finitely many arrows between any two vertices (TauCeti.IsFiniteRepType.posDef_titsForm_of_connected).

Main results

• TauCeti.not_isFiniteRepType_of_injective_of_nonempty_hom_sum: a cycle of length at least three, in any orientation, obstructs finite representation type.
• TauCeti.not_isFiniteRepType_of_copy_cycleGraph: so does a copy of SimpleGraph.cycleGraph in the underlying graph.
• TauCeti.IsFiniteRepType.isAcyclic_underlyingGraph: the underlying graph of a quiver of finite representation type is acyclic.
• TauCeti.IsFiniteRepType.posDef_titsForm_of_connected: a finite connected quiver of finite representation type has a positive definite Tits form.

Implementation notes

The cycles here have length at least three because that is what the underlying simple graph can see: a cycle of length two is a pair of opposite arrows a ⟶ b, b ⟶ a, which the underlying graph records as a single edge, and a cycle of length one is a loop, excluded already by TauCeti.IsFiniteRepType.isEmpty_hom_self. The two-cycle obstruction is proved separately in TauCeti.RepresentationTheory.Quiver.FiniteRepType.TwoCycle. Length three is also what the construction below needs: the closing edge must be the only edge of the cycle joining x (n + 2) and x 0, so that the other arrows can act by the identity.

The construction and the indecomposability argument adapt the nilpotent Jordan blocks on the one-loop quiver in TauCeti/RepresentationTheory/Quiver/OneLoop/FiniteRepType.lean (oneLoopNilpotentRepApp_root_mul and TauCeti.indecomposable_oneLoopNilpotentRep), with the loop spread out around the cycle.

The statements are for representations with vertex spaces in the universe of the base field, the universe in which the truncated polynomial algebras live.

References

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

theorem TauCeti.not_isFiniteRepType_of_injective_of_nonempty_hom_sum {k : Type u} [Field k] {Q : Type v} [Quiver Q] {n : ℕ} (x : Fin (n + 3) → Q) (hinj : Function.Injective x) (hx : ∀ (i : Fin (n + 3)), Nonempty ((x i ⟶ x (i + 1)) ⊕ (x (i + 1) ⟶ x i))) : ¬IsFiniteRepType k Q

A cycle of length at least three obstructs finite representation type, in any orientation. If x 0, …, x (n + 2) are pairwise distinct vertices of Q, with an arrow in one direction or the other between x i and x (i + 1) for each i, indices read modulo n + 3, then Q has infinite representation type over every field.

theorem TauCeti.not_isFiniteRepType_of_copy_cycleGraph {k : Type u} [Field k] {Q : Type v} [Quiver Q] {n : ℕ} (f : (SimpleGraph.cycleGraph (n + 3)).Copy (Quiver.underlyingGraph Q)) : ¬IsFiniteRepType k Q

A cycle in the underlying graph obstructs finite representation type. If the underlying graph of Q contains a copy of the cycle graph on n + 3 vertices, then Q has infinite representation type over every field, whatever the directions and multiplicities of the arrows of Q along the copy.

theorem TauCeti.IsFiniteRepType.isAcyclic_underlyingGraph {k : Type u} [Field k] {Q : Type v} [Quiver Q] (h : IsFiniteRepType k Q) : (Quiver.underlyingGraph Q).IsAcyclic

The underlying graph of a quiver of finite representation type is a forest: a cycle in it would obstruct finite representation type (TauCeti.not_isFiniteRepType_of_copy_cycleGraph).

theorem TauCeti.IsFiniteRepType.posDef_titsForm_of_connected {k : Type u} [Field k] {Q : Type v} [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (h : IsFiniteRepType k Q) (hconn : (Quiver.underlyingGraph Q).Connected) : (titsForm Q).PosDef

Finite representation type of a connected quiver forces a positive definite Tits form. A finite quiver of finite representation type whose underlying graph is connected has a positive definite Tits form.

Its underlying graph is acyclic (TauCeti.IsFiniteRepType.isAcyclic_underlyingGraph), hence a tree, and the tree case is TauCeti.IsFiniteRepType.posDef_titsForm_of_isTree. This is the converse of TauCeti.isFiniteRepType_of_titsForm_posDef for such quivers.