The Coxeter transformation drives a dimension vector out of the positive cone

Let Q be a finite quiver whose Tits form is positive definite, the numerical side of the ADE condition in Gabriel's theorem. This file proves that the Coxeter transformation c, the composite of the simple reflections along a repetition-free word running over every vertex, moves every nonzero dimension vector out of the positive cone: for every d ≠ 0 some iterate cᴺ d has a negative coordinate (TauCeti.exists_vertexPreReflectionList_pow_apply_neg).

This is the descent that the Bernstein-Gelfand-Ponomarev proof of Gabriel's theorem runs on the representation side. A finite-dimensional representation has a nonnegative dimension vector, and TauCeti.indecomposable_and_dimVector_coxeterFunctor_or_isZero says that a pass of the Coxeter functor over an indecomposable either applies c to its dimension vector or annihilates it. Since c cannot keep a nonzero dimension vector nonnegative forever, some pass must annihilate the representation, that is, must meet the vertex simple at the sink it is reflecting; iterating that observation is the induction that carries an indecomposable down to a vertex simple, and its dimension vector down to a simple root.

Main results

• TauCeti.isEmpty_hom_self_of_titsForm_posDef: a positive definite Tits form forces every vertex to be loopless, so the reflection identities are available without a separate hypothesis.
• TauCeti.exists_vertexPreReflectionList_pow_apply_neg: the descent. No nonzero dimension vector stays nonnegative under all iterates of the Coxeter transformation.

Implementation notes

The proof is the finite-orbit argument, and it needs no root-system combinatorics. The iterates cᴺ d all have the same Tits value, and a positive definite integral quadratic form takes each value only finitely often (QuadraticMap.PosDef.finite_setOf_apply_eq), so the orbit repeats: cᵖ x = x for some x = cᴺ d and some p > 0. Were every iterate nonnegative, the sum x + c x + ⋯ + cᵖ⁻¹ x over one period would be a nonzero vector fixed by c, which TauCeti.vertexPreReflectionList_eq_self_iff_of_anisotropic forbids.

The word is an explicit argument rather than a chosen sink-admissible ordering, matching TauCeti.vertexPreReflectionList and TauCeti.coxeterFunctor: the transformation depends on the ordering, so a consumer that names one must be able to pass it.

References

This is the "descent by height" milestone of the reflection induction in Layer 5, Gabriel's theorem, of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md. See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Assem--Simson-- Skowroński, Elements of the Representation Theory of Associative Algebras I, VII.5.

theorem TauCeti.exists_vertexPreReflectionList_pow_apply_neg (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hpd : (titsForm Q).PosDef) {l : List Q} (hnd : l.Nodup) (hmem : ∀ (i : Q), i ∈ l) {d : Q → ℤ} (hd0 : d ≠ 0) : ∃ (N : ℕ) (i : Q), (vertexPreReflectionList Q l ^ N) d i < 0

The Coxeter transformation drives every nonzero dimension vector out of the positive cone. For a quiver with positive definite Tits form and a repetition-free word l running over all the vertices, no nonzero d has all of its iterates under the reflection product along l nonnegative. Nonnegativity of d itself is not assumed: at N = 0 the conclusion is just that d has a negative coordinate.

On the representation side this is the descent of the Bernstein-Gelfand-Ponomarev induction: a dimension vector is nonnegative, so an indecomposable representation cannot survive arbitrarily many passes of the Coxeter functor, and the pass that kills it meets a vertex simple.