The dimension vector of an indecomposable representation is a root

Let Q be a finite quiver whose Tits form is positive definite, the numerical side of the ADE condition in Gabriel's theorem, and fix a sink-admissible ordering of its vertices. This file proves that every finite-dimensional indecomposable representation M of Q satisfies q(dim M) = 1, so that its dimension vector is a root of the Tits form (TauCeti.titsForm_dimVector_eq_one_of_indecomposable).

This is the half of the Gabriel correspondence saying that the dimension vector of an indecomposable is a positive root: dim M is nonnegative by construction and nonzero by TauCeti.dimVector_ne_zero_of_indecomposable, and the theorem below supplies q(dim M) = 1.

The argument

The Bernstein-Gelfand-Ponomarev induction runs the Coxeter functor C⁺ at M. A pass either carries an indecomposable to an indecomposable and applies the Coxeter transformation to its dimension vector, or annihilates it (TauCeti.indecomposable_and_dimVector_coxeterFunctor_or_isZero). Dimension vectors are nonnegative, and TauCeti.exists_vertexPreReflectionList_pow_apply_neg forbids a nonzero nonnegative vector from surviving every iterate of the Coxeter transformation, so some pass must annihilate M: this is TauCeti.exists_isZero_coxeterFunctor_iterate, that every finite-dimensional indecomposable is killed by a power of C⁺.

The Tits form is unchanged by each pass, so it suffices to compute it at the last surviving representation, that is, at an indecomposable the Coxeter functor annihilates. Such a representation is caught by a single stage of the pass, and TauCeti.titsForm_dimVector_eq_one_of_isZero_reflectionFunctorList reads the answer off there: the stage that annihilates finds the representation concentrated at its own sink i, hence a line there, so its dimension vector is the simple αᵢ, of Tits norm 1; every earlier stage only applies a simple reflection, which preserves the Tits form, as does the reflection of the quiver itself.

Main results

• TauCeti.titsForm_dimVector_eq_one_of_isZero_reflectionFunctorList: a finite-dimensional indecomposable representation annihilated by a composite of reflection functors has a dimension vector of Tits norm one.
• TauCeti.exists_isZero_coxeterFunctor_iterate: a positive definite Tits form forces a power of the Coxeter functor to annihilate every finite-dimensional indecomposable representation.
• TauCeti.titsForm_dimVector_eq_one_of_indecomposable: the dimension vector of a finite-dimensional indecomposable representation is a root of the Tits form, with TauCeti.titsForm_dimVector_eq_one_of_indecomposable_of_isAcyclic the same statement over an acyclic quiver, where the ordering is chosen internally and so does not appear.

Implementation notes

As in TauCeti.coxeterFunctor and TauCeti.exists_vertexPreReflectionList_pow_apply_neg, the sink-admissible ordering is an explicit argument rather than a chosen one: the Coxeter functor and the transformation it realizes both depend on the ordering. Every finite acyclic quiver has one, by TauCeti.Quiver.IsAcyclic.exists_isSinkAdmissible.

For the indecomposable projectives over an acyclic quiver the same Tits value is computed directly, and without positive definiteness, by TauCeti.titsForm_dimVector_indecProjRep_of_isAcyclic; the theorems here reach every indecomposable, at the price of that hypothesis.

References

This is the step of the reflection induction for Gabriel's theorem showing that the dimension vector of an indecomposable is a positive root. 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.

The stage that annihilates an indecomposable representation

theorem TauCeti.titsForm_dimVector_eq_one_of_isZero_reflectionFunctorList {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (l : List V) (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) (hl : Quiver.IsSinkAdmissible q l) (M : QuiverRep k V) : CategoryTheory.Indecomposable M → IsFinDim k V M → CategoryTheory.Limits.IsZero ((reflectionFunctorList k l q hq hl).obj M) → ((titsForm V) fun (j : V) => ↑(dimVector M j)) = 1

A finite-dimensional indecomposable representation annihilated by a composite of reflection functors has a dimension vector of Tits norm one.

The induction is on the list of sinks. A stage that does not meet the vertex simple at its own sink preserves indecomposability and reflects the dimension vector, and neither reflecting the quiver (TauCeti.titsForm_reflect) nor reflecting the dimension vector (TauCeti.titsForm_vertexPreReflection) changes the Tits form. The stage that does meet it finds the representation concentrated at that sink, hence a line there (TauCeti.exists_ne_zero_span_eq_top_of_forall_subsingleton), so its dimension vector is the simple αᵢ, whose Tits norm is one because a sink carries no loop.

Every indecomposable representation is annihilated by a power of the Coxeter functor

theorem TauCeti.exists_isZero_coxeterFunctor_iterate {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (hpd : (titsForm V).PosDef) (M : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hfd : IsFinDim k V M) : ∃ (N : ℕ), CategoryTheory.Limits.IsZero ((coxeterFunctor k q hq hnd hall hl).obj^[N] M)

A power of the Coxeter functor annihilates every finite-dimensional indecomposable representation of a quiver with positive definite Tits form.

Were the iterates all nonzero they would all be indecomposable, with dimension vectors the successive Coxeter transforms of dim M; those are nonnegative, which TauCeti.exists_vertexPreReflectionList_pow_apply_neg forbids for a nonzero vector.

The dimension vector of an indecomposable is a root

theorem TauCeti.titsForm_dimVector_eq_one_of_indecomposable {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] (q : Quiver V) (hq : (a b : V) → Fintype (a ⟶ b)) {l : List V} (hnd : l.Nodup) (hall : ∀ (v : V), v ∈ l) (hl : Quiver.IsSinkAdmissible q l) (hpd : (titsForm V).PosDef) (M : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hfd : IsFinDim k V M) : ((titsForm V) fun (j : V) => ↑(dimVector M j)) = 1

The dimension vector of a finite-dimensional indecomposable representation is a root of the Tits form. For a quiver with positive definite Tits form -- the numerical form of the ADE condition -- and any sink-admissible ordering of its vertices, an indecomposable representation with finite-dimensional vertex spaces has q(dim M) = 1. Since a dimension vector is nonnegative, and is nonzero because an indecomposable is not the zero object, dim M is a positive root.

This is the half of Gabriel's correspondence that produces a positive root from an indecomposable; the nonvanishing half is TauCeti.dimVector_ne_zero_of_indecomposable.

theorem TauCeti.titsForm_dimVector_eq_one_of_indecomposable_of_isAcyclic {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] [q : Quiver V] [hq : (a b : V) → Fintype (a ⟶ b)] (hac : Quiver.IsAcyclic V) (hpd : (titsForm V).PosDef) (M : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hfd : IsFinDim k V M) : ((titsForm V) fun (j : V) => ↑(dimVector M j)) = 1

The dimension vector of a finite-dimensional indecomposable representation of an acyclic quiver with positive definite Tits form is a root. This is the consumer-facing form of TauCeti.titsForm_dimVector_eq_one_of_indecomposable: acyclicity produces a sink-admissible ordering by TauCeti.Quiver.IsAcyclic.exists_isSinkAdmissible, and since the conclusion does not mention the ordering, the choice is made here rather than by the caller.