Every positive root of a positive definite Tits form is a reflection of a simple root

Let Q be a finite quiver whose Tits form is positive definite. A positive root is a nonzero d : Q → ℤ with 0 ≤ d and titsForm Q d = 1; the dimension vector of a finite-dimensional indecomposable representation is one, by TauCeti.titsForm_dimVector_eq_one_of_indecomposable. This file proves the root-lattice statement that every positive root is carried to a simple root αⱼ = Pi.single j 1 by finitely many simple reflections read along a repetition-free word running over all the vertices. Equivalently, every positive root lies in the Weyl orbit of a simple one.

This is a prerequisite for the reflection induction in Gabriel's theorem. The reduction records that every intermediate vector remains nonnegative, so the reverse word can be transported through source reflection functors. It does not assert that the reflection word is sink- or source-admissible for the evolving quivers; that property comes from choosing the full word to be a sink-admissible ordering.

Main results

• TauCeti.vertexPreReflection_apply_self_neg_iff_eq_single: a positive root is simple exactly when the reflection at that vertex makes its coordinate there negative.
• TauCeti.exists_vertexPreReflectionList_take_apply_eq_single_and_nonneg: some number of full passes of the reflection product followed by an initial segment of the word carries a positive root to the simple root at the next vertex of the word, without leaving the nonnegative cone before reaching that root.
• TauCeti.titsForm_eq_one_iff_exists_vertexPreReflectionList_single: consequently the positive roots are exactly the nonnegative reflection images of the simple roots.

References

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.

One reflection detects the simple roots

@[simp]

theorem TauCeti.vertexPreReflection_apply_self_neg_iff_eq_single (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hpd : (titsForm Q).PosDef) {i : Q} {d : Q → ℤ} (hd : 0 ≤ d) (hroot : (titsForm Q) d = 1) : (vertexPreReflection Q i) d i < 0 ↔ d = Pi.single i 1

A single reflection turns a positive root negative exactly at a simple root. For a positive definite Tits form and a nonnegative d with q(d) = 1, the coordinate of sᵢ d at i is negative precisely when d is the simple dimension vector αᵢ.

Thus a positive root can leave the positive cone under a simple reflection only when it is the corresponding simple root.

@[simp]

theorem TauCeti.vertexPreReflection_nonneg_iff_ne_single (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hpd : (titsForm Q).PosDef) {i : Q} {d : Q → ℤ} (hd : 0 ≤ d) (hroot : (titsForm Q) d = 1) : 0 ≤ (vertexPreReflection Q i) d ↔ d ≠ Pi.single i 1

A simple reflection keeps a positive root nonnegative unless it is that simple root. For a positive definite Tits form and a nonnegative d with q(d) = 1, the reflected vector sᵢ d is nonnegative precisely when d is not the simple dimension vector αᵢ.

Reduction of a positive root to a simple root

theorem TauCeti.exists_vertexPreReflectionList_take_apply_eq_single_of_not_nonneg (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hpd : (titsForm Q).PosDef) {l : List Q} {x : Q → ℤ} (hx : 0 ≤ x) (hroot : (titsForm Q) x = 1) {m : ℕ} (hm : ¬0 ≤ (vertexPreReflectionList Q (List.take m l)) x) : ∃ (k : ℕ) (j : Q), l[k]? = some j ∧ (vertexPreReflectionList Q (List.take k l)) x = Pi.single j 1 ∧ ∀ r ≤ k, 0 ≤ (vertexPreReflectionList Q (List.take r l)) x

The first initial segment of a word leaving the positive cone meets a simple root. For a positive definite Tits form, let x be a nonnegative vector with q(x) = 1 and let l be a word. If some initial segment of l carries x out of the nonnegative cone, then some initial segment l.take k, followed in l by a vertex j, carries x to the simple root αⱼ, and every initial segment of length at most k keeps x nonnegative.

theorem TauCeti.exists_vertexPreReflectionList_take_apply_eq_single_and_nonneg (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 → ℤ} (hd : 0 ≤ d) (hroot : (titsForm Q) d = 1) : ∃ (N : ℕ) (m : ℕ) (j : Q), l[m]? = some j ∧ (vertexPreReflectionList Q (List.take m l)) ((vertexPreReflectionList Q l ^ N) d) = Pi.single j 1 ∧ (∀ p < N, ∀ r ≤ l.length, 0 ≤ (vertexPreReflectionList Q (List.take r l)) ((vertexPreReflectionList Q l ^ p) d)) ∧ ∀ r ≤ m, 0 ≤ (vertexPreReflectionList Q (List.take r l)) ((vertexPreReflectionList Q l ^ N) d)

Weyl-orbit reduction with nonnegative intermediate vectors. For a quiver with positive definite Tits form and a repetition-free word l running over all the vertices, every positive root d is carried to a simple root by finitely many full passes of the reflection product followed by an initial segment of l: the simple root is the one at the vertex l reaches next.

Every intermediate vector in each earlier pass, and every intermediate vector up to the returned initial segment in the final pass, is nonnegative. This is the condition needed to reverse the word using source reflection functors: none of the intermediate vectors asks for a representation with a negative vertex dimension.

No admissibility property of the word for successive reflected quivers is asserted. Reading the word backwards exhibits d in the Weyl orbit of a simple root, as recorded by TauCeti.titsForm_eq_one_iff_exists_vertexPreReflectionList_single.

theorem TauCeti.titsForm_eq_one_iff_exists_vertexPreReflectionList_single (Q : Type u) [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hpd : (titsForm Q).PosDef) {d : Q → ℤ} (hd : 0 ≤ d) : (titsForm Q) d = 1 ↔ ∃ (w : List Q) (j : Q), (vertexPreReflectionList Q w) (Pi.single j 1) = d

The positive roots are exactly the nonnegative reflection images of the simple roots. For a quiver with positive definite Tits form, a nonnegative dimension vector has Tits norm one if and only if it is obtained from a simple dimension vector by a product of simple reflections.

Combined with TauCeti.titsForm_dimVector_eq_one_of_indecomposable, this places the dimension vector of every finite-dimensional indecomposable representation in the Weyl orbit of a simple dimension vector.