A positive definite Tits form forces acyclicity

A directed cycle is an obstruction to positive definiteness of the Tits form. Let p be a closed path of positive length and let d be the indicator vector of the set S of vertices it visits. Every vertex of p is the source of an arrow of p, and that arrow lands in S again, so the arrow term of TauCeti.eulerForm at d already absorbs the whole diagonal term: titsForm d ≤ 0 while d ≠ 0. Hence a finite quiver whose Tits form is positive definite is acyclic (TauCeti.isAcyclic_of_titsForm_posDef).

The counting is with distinct arrows, not with the arrows of p listed in order: a closed path may traverse the same arrow twice, and the Euler form counts each arrow of the quiver once. The injection that survives that is v ↦ (an arrow of p out of v), whose injectivity is only that distinct vertices are distinct sources; it appears below as the bound "each row of the arrow sum, indexed by a vertex of S, is at least one".

The length-one case is the looplessness TauCeti.isEmpty_hom_self_of_titsForm_posDef that the reflection identities need, proved there directly from the arrow count at a single vertex.

The generic path facts used in the counting argument are TauCeti.exists_hom_mem_path_vertices_of_mem_dropLast and TauCeti.exists_hom_mem_path_vertices, from TauCeti.RepresentationTheory.Quiver.FirstArrow.

Main result

• TauCeti.isAcyclic_of_titsForm_posDef: a finite quiver whose Tits form is positive definite is acyclic.

References

The positive definiteness of the Tits form is the numerical side of the ADE condition in Gabriel's theorem, Layer 5 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md; this file supplies the acyclicity that the reflection-functor induction there assumes separately. See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. VII.

theorem TauCeti.isAcyclic_of_titsForm_posDef {V : Type u} [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (hpd : (titsForm V).PosDef) : Quiver.IsAcyclic V

A finite quiver whose Tits form is positive definite is acyclic. The indicator vector of the vertices visited by a closed path of positive length has Tits value at most zero: each of its vertices contributes 1 to the diagonal sum and, being the source of an arrow of the path, at least 1 to the arrow sum as well.