Every positive root is the dimension vector of an indecomposable representation

Let Q be a finite quiver whose Tits form is positive definite, the numerical side of the ADE condition in Gabriel's theorem. TauCeti.titsForm_dimVector_eq_one_of_indecomposable sends a finite-dimensional indecomposable representation of Q to a positive root of the Tits form, and TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable shows that map injective on isomorphism classes. This file proves it surjective: every positive root is realized (TauCeti.exists_indecomposable_dimVector_eq), so M ↦ dim M is a bijection from the isomorphism classes of finite-dimensional indecomposables onto the positive roots. No algebraic closedness is needed anywhere: the Bernstein-Gelfand-Ponomarev reflection functors work over any field.

Where the injective half runs the sink reflection functors forwards until they annihilate the representation, the surjective half runs the source reflection functors backwards from a vertex simple. TauCeti.exists_isSinkAdmissible_vertexPreReflectionList_eq_single_and_nonneg supplies the word to travel along, TauCeti.exists_indecomposable_dimVector_eq_vertexPreReflectionList_single travels along its reverse, and TauCeti.exists_indecomposable_dimVector_eq is their composite.

Implementation notes

The vector computations are all carried out for the original quiver and transferred to the reflected one at the last moment: the reflection product along a word does not depend on the orientation (TauCeti.vertexPreReflectionList_reflectList), so no looplessness or Tits-form hypothesis has to be re-established for a reflected quiver. Arrow-finiteness is transported by TauCeti.Quiver.fintypeHomReflectList.

As in the neighbouring files, the universe of the vertex spaces is chosen large enough for the vertices, arrows, and field. The construction therefore starts from a universe lift of Sⱼ, whose nonzero vertex space remains a one-dimensional copy of the field.

Main results

• TauCeti.exists_isSinkAdmissible_vertexPreReflectionList_eq_single_and_nonneg: the Weyl-orbit reduction of a positive root, as one sink-admissible word with nonnegative intermediate vectors.
• TauCeti.exists_indecomposable_dimVector_eq_vertexPreReflectionList_single: a source-admissible word with nonnegative intermediate vectors turns a vertex simple into an indecomposable with the reflected dimension vector.
• TauCeti.exists_indecomposable_dimVector_eq: every positive root is the dimension vector of a finite-dimensional indecomposable representation, with TauCeti.nonneg_and_titsForm_eq_one_iff_exists_indecomposable the resulting characterization of the positive roots.

References

Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2, and Assem--Simson--Skowronski, Elements of the Representation Theory of Associative Algebras I, VII.5.

A single sink-admissible word carrying a positive root to a simple root

theorem TauCeti.exists_isSinkAdmissible_vertexPreReflectionList_eq_single_and_nonneg (Q : Type v) [q : Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [DecidableEq Q] (hpd : (titsForm Q).PosDef) {d : Q → ℤ} (hd : 0 ≤ d) (hroot : (titsForm Q) d = 1) : ∃ (l : List Q) (j : Q), Quiver.IsSinkAdmissible q l ∧ (vertexPreReflectionList Q l) d = Pi.single j 1 ∧ ∀ r ≤ l.length, 0 ≤ (vertexPreReflectionList Q (List.take r l)) d

The reflection word carrying a positive root to a simple root can be taken sink-admissible. For a quiver with positive definite Tits form, every positive root d is carried to a simple root by a single sink-admissible word, along which no intermediate vector leaves the nonnegative cone.

This is TauCeti.exists_vertexPreReflectionList_take_apply_eq_single_and_nonneg, whose conclusion is phrased as a number of full passes of a sink-admissible ordering followed by an initial segment of it, restated as the one word the reflection induction reads backwards.

Rebuilding an indecomposable from a vertex simple

theorem TauCeti.exists_indecomposable_dimVector_eq_vertexPreReflectionList_single (k : Type u) (Q : Type v) [Field k] [Fintype Q] [DecidableEq Q] (q₀ : Quiver Q) (hq₀ : (a b : Q) → Fintype (a ⟶ b)) (l : List Q) (j : Q) (hadm : Quiver.IsSourceAdmissible q₀ l) (hnn : ∀ r < l.length, 0 ≤ (vertexPreReflectionList Q (List.take (r + 1) l)) (Pi.single j 1)) : ∃ (M : QuiverRep k Q), CategoryTheory.Indecomposable M ∧ IsFinDim k Q M ∧ (fun (t : Q) => ↑(dimVector M t)) = (vertexPreReflectionList Q l) (Pi.single j 1)

A nonnegative source-reflection word turns a vertex simple into an indecomposable with the prescribed dimension vector. Starting from the vertex simple Sⱼ of q₀ and reflecting along a source-admissible word l, all of whose intermediate dimension vectors stay nonnegative, produces an indecomposable representation of TauCeti.Quiver.reflectList q₀ l whose dimension vector is the reflection product along l of the simple dimension vector αⱼ.

theorem TauCeti.exists_indecomposable_dimVector_eq (k : Type u) (Q : Type v) [Field k] [Fintype Q] [q : Quiver Q] [hq : (a b : Q) → Fintype (a ⟶ b)] (hpd : (titsForm Q).PosDef) {d : Q → ℤ} (hd : 0 ≤ d) (hroot : (titsForm Q) d = 1) : ∃ (M : QuiverRep k Q), CategoryTheory.Indecomposable M ∧ IsFinDim k Q M ∧ (fun (t : Q) => ↑(dimVector M t)) = d

Every positive root of a quiver with positive definite Tits form is the dimension vector of a finite-dimensional indecomposable representation. This is the surjective half of the Gabriel correspondence; the injective half — that an indecomposable is determined by its dimension vector — is TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable_of_isAcyclic, and that the dimension vector of an indecomposable is a positive root is TauCeti.titsForm_dimVector_eq_one_of_indecomposable_of_isAcyclic.

theorem TauCeti.nonneg_and_titsForm_eq_one_iff_exists_indecomposable (k : Type u) (Q : Type v) [Field k] [Fintype Q] [q : Quiver Q] [hq : (a b : Q) → Fintype (a ⟶ b)] (hpd : (titsForm Q).PosDef) {d : Q → ℤ} : 0 ≤ d ∧ (titsForm Q) d = 1 ↔ ∃ (M : QuiverRep k Q), CategoryTheory.Indecomposable M ∧ IsFinDim k Q M ∧ (fun (t : Q) => ↑(dimVector M t)) = d

A vector is a nonnegative root exactly when it is realized by an indecomposable representation. The forward direction is TauCeti.exists_indecomposable_dimVector_eq; the reverse is TauCeti.titsForm_dimVector_eq_one_of_indecomposable_of_isAcyclic, nonnegativity being automatic for a dimension vector.