Quiver representations · The Lumenary

Lens

MotivationH

Classifying configurations of linear maps

Many classical problems of linear algebra ask for normal forms of a few linear maps between a few vector spaces.

One map $V \to W$ . Up to changes of basis in $V$ and $W$ , a linear map is determined by its rank: it is the matrix $\left(\begin{smallmatrix} I_r & 0 \\ 0 & 0 \end{smallmatrix}\right)$ .
One map $V \to V$ . Up to a single change of basis, this is the Jordan normal form problem: infinitely many normal forms, depending on continuous parameters (the eigenvalues).
Two maps $V \rightrightarrows W$ . Pairs of matrices up to $(A, B) \mapsto (gAh^{-1}, gBh^{-1})$ , the theory of matrix pencils solved by Weierstrass (1868) and Kronecker (1890).
Three or four subspaces of a vector space. Triples of subspaces have finitely many indecomposable configurations up to isomorphism; for quadruples they come in one-parameter families (the cross-ratio appears), solved by Gelfand and Ponomarev (1970); five or more subspaces lead to problems containing all the others.

All of these are representations of quivers: directed graphs with a vector space at each vertex and a linear map on each arrow. The striking discovery of Pierre Gabriel (1972) was that the problems with only finitely many indecomposable answers are exactly those whose underlying graph is a Dynkin diagram of type $A$ , $D$ or $E$ — and that the indecomposables then correspond to the positive roots of the corresponding root system from Lie theory.

IntuitionH

Pictures, dimension vectors, indecomposables

Draw the quiver; at each vertex write the dimension of the space placed there. This dimension vector is the first invariant of a representation. Two representations can be added (direct sum, vertex by vertex), and every finite-dimensional representation is a direct sum of indecomposable ones, uniquely up to order and isomorphism (the Krull–Schmidt theorem: endomorphism rings of indecomposables are local). So classification means: list the indecomposables.

For the quiver $1 \to 2$ there are exactly three, with dimension vectors $(1, 0)$ , $(0, 1)$ , $(1, 1)$ :

k \to 0, \qquad 0 \to k, \qquad k \xrightarrow{\;1\;} k,

and a map $f : V \to W$ of rank $r$ decomposes as $r$ copies of $k \xrightarrow{1} k$ , $\dim \ker f$ copies of $k \to 0$ and $\dim \operatorname{coker} f$ copies of $0 \to k$ . These three vectors are precisely the positive roots of the root system $A_2$ (the vectors with $x_1^2 + x_2^2 - x_1 x_2 = 1$ ). That is Gabriel's theorem in its smallest case.

DefinitionsH

Definitions

Definition— quiver and representation

A quiver $Q = (Q_0, Q_1, s, t)$ is a finite set $Q_0$ of vertices, a finite set $Q_1$ of arrows, and source and target maps $s, t : Q_1 \to Q_0$ . A representation $V$ over a field $k$ assigns a finite-dimensional vector space $V_i$ to each vertex and a linear map $V_a : V_{s(a)} \to V_{t(a)}$ to each arrow. A morphism $\varphi : V \to W$ is a family of linear maps $\varphi_i : V_i \to W_i$ with $\varphi_{t(a)} V_a = W_a \varphi_{s(a)}$ for every arrow $a$ . The dimension vector is $\underline{\dim}\, V = (\dim V_i)_{i \in Q_0} \in \N^{Q_0}$ .

The category $\mathrm{rep}_k(Q)$ is equivalent to the category of finite-dimensional modules over the path algebra $kQ$ (see quivers and path algebras); it is abelian and hereditary: $\operatorname{Ext}^2$ vanishes. Each vertex $i$ gives a simple representation $S(i)$ ( $k$ at $i$ , zero elsewhere), a projective $P(i)$ with $P(i)_j$ the span of the paths from $i$ to $j$ , and an injective $I(i)$ with $I(i)_j$ dual to the span of the paths from $j$ to $i$ .

Definition— Euler form and Tits form

The Euler form of $Q$ is the bilinear form on $\Z^{Q_0}$

\langle x, y \rangle = \sum_{i \in Q_0} x_i y_i - \sum_{a \in Q_1} x_{s(a)} y_{t(a)},

and the Tits form is the quadratic form $q(x) = \langle x, x \rangle = \sum_i x_i^2 - \sum_a x_{s(a)} x_{t(a)}$ , which depends only on the underlying graph. A positive root is a vector $x \in \N^{Q_0} \setminus \{0\}$ with $q(x) = 1$ (for Dynkin graphs; Kac's theorem below uses the more general Kac–Moody roots).

Definition— finite representation type

$Q$ has finite representation type if it has only finitely many indecomposable representations up to isomorphism. (It always has infinitely many representations up to isomorphism, since $S(i)^{\oplus n}$ , $n = 1, 2, \dots$ , are pairwise non-isomorphic.)

Definition— reflections

For a vertex $i$ without loops, the simple reflection $s_i$ of $\Z^{Q_0}$ changes only the $i$ -th coordinate:

s_i(x)_i = \Big(\sum_{j \text{ adjacent to } i} x_j\Big) - x_i

(neighbours counted with the number of edges). It preserves $q$ , and $s_i^2 = \mathrm{id}$ . If $i$ is a sink of $Q$ , the quiver $\sigma_i Q$ reverses every arrow at $i$ , and the reflection functor $S_i^+ : \mathrm{rep}(Q) \to \mathrm{rep}(\sigma_i Q)$ replaces $V_i$ by the kernel of $\bigoplus_{a : j \to i} V_j \to V_i$ (Bernstein–Gelfand–Ponomarev, 1973).

Definition— Auslander–Reiten sequence and quiver

An Auslander–Reiten (almost split) sequence is a non-split short exact sequence $0 \to A \to B \xrightarrow{g} C \to 0$ with $A$ and $C$ indecomposable, such that every map $X \to C$ that is not a split epimorphism factors through $g$ . One writes $A = \tau C$ , the Auslander–Reiten translate. The Auslander–Reiten quiver has the indecomposables as vertices, the irreducible maps as arrows, and the translation $\tau$ recorded by dashed arrows.

Worked examplesH

Examples

Example— Type A₃ and intervals

For the linear quiver $1 \to 2 \to 3$ , the indecomposables are the "interval modules" $[i, j]$ : $k$ at the vertices $i, \dots, j$ joined by identity maps, $0$ elsewhere. There are $6 = \binom{4}{2}$ of them, with dimension vectors $100, 010, 001, 110, 011, 111$ — the positive roots of $A_3$ , i.e. the vectors $e_i + \dots + e_j$ . For $A_n$ there are $n(n+1)/2$ .

Example— Type D₄ and three subspaces

Orient $D_4$ with three arrows into the centre. A representation is three linear maps into a space $V_c$ ; an indecomposable one with all maps injective is a configuration of three subspaces of $V_c$ . There are $12$ indecomposables; the most interesting has dimension vector $(1, 2, 1, 1)$ (centre written second): three distinct lines in a plane. Its Tits form is $1 + 4 + 1 + 1 - 2 - 2 - 2 = 1$ . The positive roots of $D_4$ number $12$ , and the formal section proves that these are exactly the non-negative solutions of $q = 1$ .

Example— The Kronecker quiver: a family

For $1 \rightrightarrows 2$ , a representation of dimension $(1, 1)$ is a pair $(\lambda, \mu) \in k^2$ . If $(\lambda, \mu) \neq (0, 0)$ it is indecomposable, and two such are isomorphic exactly when they are proportional. So the indecomposables of dimension $(1, 1)$ are parametrised by the projective line $\mathbb{P}^1(k)$ : infinitely many when $k$ is infinite, and $|k| + 1$ over a finite field. The Tits form $q(x, y) = (x - y)^2$ vanishes at $(1, 1)$ : an imaginary root. The Kronecker quiver is the first quiver of infinite type, and its classification is the theory of matrix pencils.

Example— Computing Ext with the Euler form

For $1 \to 2$ : $\langle \underline{\dim}\, S(1), \underline{\dim}\, S(2) \rangle = \langle e_1, e_2 \rangle = 0 - 1 = -1$ . Since $\operatorname{Hom}(S(1), S(2)) = 0$ , Theorem 1 below gives $\dim \operatorname{Ext}^1(S(1), S(2)) = 1$ : the non-split extension is $0 \to S(2) \to (k \xrightarrow{1} k) \to S(1) \to 0$ . In the other order, $\langle e_2, e_1 \rangle = 0$ and indeed $\operatorname{Hom}(S(2), S(1)) = \operatorname{Ext}^1(S(2), S(1)) = 0$ .

ProofH

Central theorems

Theorem— Theorem 1 — the Euler form computes Hom minus Ext (Ringel)

For representations $V$ , $W$ of a quiver $Q$ ,

\langle \underline{\dim}\, V, \underline{\dim}\, W \rangle = \dim \operatorname{Hom}(V, W) - \dim \operatorname{Ext}^1(V, W).

Proof

Consider the linear map

\delta : \bigoplus_{i \in Q_0} \operatorname{Hom}_k(V_i, W_i) \longrightarrow \bigoplus_{a \in Q_1} \operatorname{Hom}_k(V_{s(a)}, W_{t(a)}), \qquad \delta(\varphi)_a = \varphi_{t(a)} V_a - W_a \varphi_{s(a)}.

By definition $\ker \delta = \operatorname{Hom}(V, W)$ . Ringel's standard resolution $0 \to \bigoplus_a P(t(a)) \otimes V_{s(a)} \to \bigoplus_i P(i) \otimes V_i \to V \to 0$ is a projective resolution of length $1$ (this is how one sees that $\mathrm{rep}(Q)$ is hereditary); applying $\operatorname{Hom}(-, W)$ and using $\operatorname{Hom}(P(i), W) = W_i$ turns it into $\delta$ , so $\operatorname{coker} \delta \cong \operatorname{Ext}^1(V, W)$ . Hence $\dim \operatorname{Hom} - \dim \operatorname{Ext}^1 = \dim(\text{source}) - \dim(\text{target}) = \sum_i \dim V_i \dim W_i - \sum_a \dim V_{s(a)} \dim W_{t(a)}$ .

∎

Theorem— Theorem 2 — finite type forces a weakly positive Tits form (Tits)

Let $k$ be algebraically closed. If $Q$ has finite representation type, then $q(d) \geq 1$ for every $d \in \N^{Q_0} \setminus \{0\}$ .

Proof

Representations of dimension vector $d$ form the affine space $\mathrm{Rep}(Q, d) = \prod_a \operatorname{Hom}(k^{d_{s(a)}}, k^{d_{t(a)}})$ , of dimension $\sum_a d_{s(a)} d_{t(a)}$ . The group $GL(d) = \prod_i GL_{d_i}(k)$ , of dimension $\sum_i d_i^2$ , acts by change of basis, and its orbits are exactly the isomorphism classes. The scalars $\{(\lambda \cdot I)_i\}$ act trivially, so every orbit has dimension at most $\sum_i d_i^2 - 1$ .

If $Q$ has finite type, Krull–Schmidt gives finitely many isomorphism classes of each dimension vector, so $\mathrm{Rep}(Q, d)$ is a finite union of orbits. An irreducible variety that is a finite union of (locally closed) orbits contains an orbit of full dimension, so $\sum_a d_{s(a)} d_{t(a)} \le \sum_i d_i^2 - 1$ , which says $q(d) \geq 1$ .

∎

Theorem— Corollary 3 — finite type implies Dynkin

Let $k$ be algebraically closed. If a connected quiver has finite representation type over $k$ , its underlying graph is a Dynkin diagram $A_n$ , $D_n$ ( $n \ge 4$ ), $E_6$ , $E_7$ or $E_8$ .

Proof

A connected graph that is not of type $A$ , $D$ , $E$ contains (by an elementary combinatorial argument) a subgraph of extended Dynkin type $\tilde A_n$ (a cycle, including a loop $\tilde A_0$ and a double edge $\tilde A_1$ ), $\tilde D_n$ , $\tilde E_6$ , $\tilde E_7$ or $\tilde E_8$ . Each extended Dynkin graph $\Gamma'$ has a null root $\delta \in \N^{\Gamma'_0}$ with $q_{\Gamma'}(\delta) = 0$ : for instance $\delta = (1, \dots, 1)$ for a cycle and $\delta = (1, 1, 1, 1, 2)$ for $\tilde D_4$ (the star with four leaves, centre last). Extending $\delta$ by zero, extra edges of the full graph can only subtract further terms, so $q(\delta) \le 0$ , contradicting Theorem 2. (Over an arbitrary field the conclusion still holds, by a different argument: for a non-Dynkin graph the reflection functors produce infinitely many pairwise non-isomorphic preprojective indecomposables $\tau^{-m}P(i)$ , as the Kronecker example in the computation section illustrates.)

∎

Conversely, the Tits form of every Dynkin graph is positive definite — for $A_n$ , $2q(x) = x_1^2 + \sum_{i=1}^{n-1} (x_i - x_{i+1})^2 + x_n^2$ , and the formal section proves the $D_4$ case by an explicit sum of squares — so the set of positive roots is finite.

Theorem— Theorem 4 — Gabriel's theorem (1972)

Let $Q$ be a connected quiver and $k$ any field. Then $Q$ has finite representation type if and only if its underlying graph is a Dynkin diagram of type $A$ , $D$ or $E$ . In that case $V \mapsto \underline{\dim}\, V$ is a bijection between isomorphism classes of indecomposable representations and positive roots. In particular the number of indecomposables does not depend on the orientation: it is $n(n+1)/2$ for $A_n$ , $n(n-1)$ for $D_n$ , and $36, 63, 120$ for $E_6, E_7, E_8$ .

Proof

Outline, following Bernstein–Gelfand–Ponomarev. "Only if" is Corollary 3. For "if", let $i$ be a sink and $V$ indecomposable with $V \not\cong S(i)$ . Then $\bigoplus_{a : j \to i} V_j \to V_i$ is surjective (otherwise a complement of its image would split off a copy of $S(i)$ ), so $S_i^+ V$ has dimension vector $s_i(\underline{\dim}\, V)$ ; one checks that $S_i^+V$ is indecomposable and $S_i^- S_i^+ V \cong V$ . Number the vertices so that each is a sink after reflecting at the previous ones, and let $c = s_{i_n} \cdots s_{i_1}$ be the corresponding Coxeter element. Because $q$ is positive definite, $c$ has finite order and no non-zero fixed vector, so for every positive vector $x$ some $c^m x$ fails to be positive. Following an indecomposable $V$ through the reflection functors, its dimension vector stays positive until $V$ becomes a simple $S(i)$ and is killed. Hence every indecomposable is obtained from a simple by inverse reflection functors: it is determined by its dimension vector, which is a root since reflections preserve $q$ and $q(e_i) = 1$ . Conversely every positive root is reached this way from a simple root. (Full proofs: Schiffler, Quiver Representations, Ch. 8; Derksen–Weyman, Ch. 4.)

∎

Theorem— Theorem 5 — Auslander–Reiten sequences and knitting

For a finite-dimensional algebra $A$ and an indecomposable non-projective module $C$ there is an Auslander–Reiten sequence $0 \to \tau C \to E \to C \to 0$ , unique up to isomorphism (Auslander–Reiten, 1975). For $A = kQ$ with $Q$ acyclic, $\underline{\dim}\, \tau C = \Phi\, \underline{\dim}\, C$ , where $\Phi = -E^{-1}E^{T}$ is the Coxeter matrix and $E$ the matrix of the Euler form. For Dynkin $Q$ every indecomposable has the form $\tau^{-m} P(i)$ .

Theorem 5 (whose proof we do not give; see Assem–Simson–Skowroński, Ch. IV and VIII) yields the knitting algorithm. Start from the projectives $P(i)$ , whose dimension vectors are path counts. Each mesh $\tau^{-1}M$ satisfies $\underline{\dim}\, \tau^{-1} M = \Phi^{-1} \underline{\dim}\, M$ (equivalently, the sum of the middle terms of the mesh minus $\underline{\dim}\, M$ ), and the process stops at $M$ exactly when $\Phi^{-1}\underline{\dim}\, M$ has a negative entry, i.e. when $M$ is injective. For $1 \to 2 \to 3$ :

The Auslander–Reiten quiver of 1 → 2 → 3, by dimension vectors: projectives on the left edge, injectives on the right, dashed arrows the translation τ. The meshes encode the AR sequences, e.g. 0 → 011 → 111 ⊕ 010 → 110 → 0.

Theorem— Theorem 6 — Kac's theorem (1980)

Let $k$ be algebraically closed and $Q$ a quiver without loops. The dimension vectors of indecomposable representations are exactly the positive roots of the Kac–Moody root system of the underlying graph, independently of the orientation. For a real root (one in the Weyl group orbit of a simple root) there is exactly one indecomposable up to isomorphism; for an imaginary root $\alpha$ there are infinitely many, in families with $1 - q(\alpha)$ parameters.

The proof (Kac, Inventiones 1980) counts representations over finite fields: the number of absolutely indecomposable representations of dimension $\alpha$ over $\mathbb{F}_q$ is a polynomial $a_\alpha(q)$ with integer coefficients, independent of the orientation. Kac conjectured that its coefficients are non-negative and that $a_\alpha(0)$ is the multiplicity of $\alpha$ as a root. Both conjectures are now theorems: Crawley-Boevey and Van den Bergh (2004) proved the second for indivisible $\alpha$ , Hausel (2010) in general, and Hausel, Letellier and Rodriguez-Villegas (2013) proved positivity. For the Kronecker quiver and $\alpha = (1, 1)$ , $a_\alpha(q) = q + 1$ — the points of $\mathbb{P}^1(\mathbb{F}_q)$ — and $a_\alpha(0) = 1$ is the multiplicity of the imaginary root $\delta$ of $\widehat{\mathfrak{sl}}_2$ .

ExplanationH

The landscape: tame, wild, and the links with Lie theory

Tame and wild. Connected quivers fall into three classes. Dynkin quivers have finite type (Gabriel). Extended Dynkin (Euclidean) quivers are tame: in each dimension, all but finitely many indecomposables lie in finitely many one-parameter families (Donovan–Freislich and Nazarova, 1973); the Kronecker quiver and the four-subspace quiver $\tilde D_4$ are the basic examples. All other connected quivers are wild: their classification contains that of pairs of matrices up to simultaneous conjugation, and with it the module theory of every finite-dimensional algebra. Drozd (1979) proved that every finite-dimensional algebra over an algebraically closed field is tame or wild, never both.

Lie theory. Gabriel's coincidence has an explanation. Ringel (1990) showed that the Hall algebra of $\mathrm{rep}_{\mathbb{F}_q}(Q)$ , whose structure constants count submodules, realises the positive part $U_v^+(\mathfrak{g})$ of the quantum group of the Dynkin type of $Q$ at $v = \sqrt{q}$ ; Green extended this to all quivers. Lusztig (1990–91) constructed the canonical basis of $U_v^+$ from perverse sheaves on the spaces $\mathrm{Rep}(Q, d)$ , and Nakajima's quiver varieties (1994, 1998) realise the integrable representations geometrically — a central source of categorification (see categorical representation theory).

Derived categories. For Dynkin $Q$ , Happel showed that $D^b(\mathrm{rep}\,Q)$ depends only on the underlying graph and is described by the mesh category of the repetitive quiver $\Z Q$ : the AR quiver of the derived category is $\Z Q$ (see derived categories).

Cluster algebras. Fomin and Zelevinsky (2003) classified cluster algebras of finite type by the same Dynkin diagrams, with cluster variables matching almost positive roots. Buan, Marsh, Reineke, Reiten and Todorov (2006) explained this with the cluster category $D^b(kQ)/\tau^{-1}[1]$ , and Caldero and Chapoton (2006) expressed cluster variables through Euler characteristics of quiver Grassmannians.

Quivers with relations. Every basic finite-dimensional algebra over an algebraically closed field is $kQ/I$ for a quiver $Q$ and an admissible ideal $I$ (Gabriel), so quivers with relations model all finite-dimensional algebras. Here genuinely open problems remain, among them the finitistic dimension conjecture (Bass, 1960) and the Nakayama conjecture (1958). For the frontiers closer to this lesson — Hall algebras, cohomological Donaldson–Thomas invariants of quivers, moduli of wild quivers — the state of the art moves quickly; consult a recent survey rather than any list here.

Explore

Explore: Dynkin or not, through walks

For a graph with adjacency matrix $A$ , the Tits form is $q(x) = \tfrac12 x^{T}(2I - A)x$ , so $q$ is positive definite exactly when every eigenvalue of $A$ is less than $2$ . For the Dynkin diagrams the largest eigenvalue is $2\cos(\pi/h)$ , with $h$ the Coxeter number; for the extended Dynkin diagrams it is exactly $2$ . You can see this in walk counts: the number of closed walks of length $2m$ grows like $\lambda_{\max}^{2m}$ .

Try the Matrix tab on the two stars below. On $D_4$ (three leaves), the entry of $A^{2m}$ at the centre is $3^m = (\sqrt{3})^{2m}$ ; on $\tilde D_4$ (four leaves) it is $4^m = 2^{2m}$ , the borderline growth of an extended Dynkin graph, whose null root is $(1, 1, 1, 1, 2)$ . Predict the growth for five leaves before computing it.

D₄: a Dynkin star

Count closed walks at the centre with powers of the adjacency matrix.

|V| = 4|E| = 3Choose a cell of the matrix below.

Walk lengthk = 1

Choose a cell: its row is the start vertex, its column the end vertex.

Each row of A adds up to the degree of its vertex.

A
	c	1	2	3
c
1
2
3

D̃₄: the four-subspace star

Extended Dynkin: the walk counts grow exactly like 2 to the length.

|V| = 5|E| = 4Choose a cell of the matrix below.

Walk lengthk = 1

Choose a cell: its row is the start vertex, its column the end vertex.

Each row of A adds up to the degree of its vertex.

A
	c	1	2	3	4
c
1
2
3
4

Formal mathematicsF

Quiver representations in Lean and Mathlib

Mathlib has quivers (Quiver), prefunctors, paths and the free category Paths Q with its universal property, but not (at this version) a library of quiver representations. A representation is exactly a prefunctor into the category of vector spaces, so we define it that way:

QuiverRepLean 4Formally verified

/-- A representation of a quiver `Q` over a field `k`: a `k`-vector space at each vertex and a
linear map along each arrow. In categorical language this is exactly a prefunctor
`Q ⥤q ModuleCat k` — no relations are imposed, because a quiver has none. -/
abbrev QuiverRep (Q : Type u) [Quiver.{w} Q] (k : Type v) [Field k] :=
  Q ⥤q ModuleCat.{v} k

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

toFunctorLean 4Formally verified

/-- Every representation extends uniquely to a functor out of the path category: a path
`a₁ ⋯ aₙ` acts by the composite of the linear maps along its arrows. (A functor from the path
category to `ModuleCat k` is the same as a module over the path algebra `kQ`.) This uses
Mathlib's `Paths.lift`. -/
noncomputable def QuiverRep.toFunctor {Q : Type u} [Quiver.{w} Q] {k : Type v} [Field k]
    (ρ : QuiverRep Q k) : Paths Q ⥤ ModuleCat.{v} k :=
  Paths.lift ρ

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

toFunctor_restrictsLean 4Applies a library theoremFormally verified

/-- Restricting `ρ.toFunctor` to single arrows gives back `ρ`. This applies Mathlib's
`Paths.lift_spec`. -/
theorem toFunctor_restricts {Q : Type u} [Quiver.{w} Q] {k : Type v} [Field k]
    (ρ : QuiverRep Q k) : Paths.of Q ⋙q ρ.toFunctor.toPrefunctor = ρ :=
  Paths.lift_spec ρ

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

toFunctor_uniqueLean 4Applies a library theoremFormally verified

/-- ... and `ρ.toFunctor` is the only functor with that property: representations of `Q` are
the same as functors `Paths Q ⥤ ModuleCat k`. This applies Mathlib's `Paths.lift_unique`. -/
theorem toFunctor_unique {Q : Type u} [Quiver.{w} Q] {k : Type v} [Field k]
    (ρ : QuiverRep Q k) (Φ : Paths Q ⥤ ModuleCat.{v} k)
    (hΦ : Paths.of Q ⋙q Φ.toPrefunctor = ρ) : Φ = ρ.toFunctor :=
  Paths.lift_unique ρ Φ hΦ

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

Together these say that representations of $Q$ are the same as functors from the path category — the categorical form of $\mathrm{rep}(Q) \simeq kQ\text{-mod}$ . The $A_2$ case of Gabriel's theorem, as a dimension count:

A2_multiplicitiesLean 4Applies a library theoremFormally verified

/-- Gabriel's theorem for `A₂ = (1 → 2)`, in numbers. A representation is a linear map
`f : V → W`; it decomposes as `rank f` copies of `k --1--> k`, `dim ker f` copies of `k → 0`
and `dim coker f` copies of `0 → k`. The dimension count behind this is rank–nullity and the
dimension of a quotient: Mathlib's `LinearMap.finrank_range_add_finrank_ker` and
`Submodule.finrank_quotient_add_finrank`. -/
theorem A2_multiplicities {k : Type v} [Field k] {V W : Type*} [AddCommGroup V] [Module k V]
    [AddCommGroup W] [Module k W] [FiniteDimensional k V] [FiniteDimensional k W]
    (f : V →ₗ[k] W) :
    Module.finrank k V = Module.finrank k (LinearMap.range f) +
        Module.finrank k (LinearMap.ker f) ∧
      Module.finrank k W = Module.finrank k (LinearMap.range f) +
        Module.finrank k (W ⧸ LinearMap.range f) := by
  refine ⟨(LinearMap.finrank_range_add_finrank_ker f).symm, ?_⟩
  rw [← Submodule.finrank_quotient_add_finrank (LinearMap.range f), add_comm]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

Now the arithmetic half of Gabriel's theorem, proved by hand. Positive definiteness for $A_2$ and $D_4$ , via sums of squares:

titsA2Lean 4Formally verified

/-- The Tits form of `A₂ = (1 → 2)`: `q(x, y) = x² + y² - xy`. -/
def titsA2 (x y : ℤ) : ℤ := x ^ 2 + y ^ 2 - x * y

Axioms used: propextformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

titsA2_posLean 4Proved here from basic factsFormally verified

/-- The Tits form of `A₂` is positive definite. Completing the square,
`4q(x, y) = (2x - y)² + 3y²`, which vanishes only when `y = 0` and then `x = 0`. -/
theorem titsA2_pos (x y : ℤ) (h : x ≠ 0 ∨ y ≠ 0) : 0 < titsA2 x y := by
  unfold titsA2
  rcases h with hx | hy
  · have : 0 < x ^ 2 := by positivity
    nlinarith [sq_nonneg (x - y), sq_nonneg y]
  · have : 0 < y ^ 2 := by positivity
    nlinarith [sq_nonneg (x - y), sq_nonneg x]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

titsD4Lean 4Formally verified

/-- The Tits form of a quiver with underlying graph `D₄`: a centre `c` joined to three leaves
`a, b, d`. It does not depend on the orientation of the three arrows:
`q = a² + b² + c² + d² - ac - bc - dc`. -/
def titsD4 (a b c d : ℤ) : ℤ := a ^ 2 + b ^ 2 + c ^ 2 + d ^ 2 - a * c - b * c - d * c

Axioms used: propextformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

titsD4_sum_of_squaresLean 4Proved here from basic factsFormally verified

/-- A sum-of-squares identity for the `D₄` form:
`4q = (2c - a - b - d)² + (a - b)² + (a - d)² + (b - d)² + a² + b² + d²`. -/
theorem titsD4_sum_of_squares (a b c d : ℤ) :
    4 * titsD4 a b c d = (2 * c - a - b - d) ^ 2 + (a - b) ^ 2 + (a - d) ^ 2 + (b - d) ^ 2
      + a ^ 2 + b ^ 2 + d ^ 2 := by
  unfold titsD4
  ring

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

titsD4_posLean 4Proved here from basic factsFormally verified

/-- The Tits form of `D₄` is positive definite: by `titsD4_sum_of_squares`, `q ≤ 0` forces
`a = b = d = 0` and then `2c = 0`. (Positive definiteness of the Tits form characterises the
Dynkin diagrams `A`, `D`, `E` among connected graphs.) -/
theorem titsD4_pos (a b c d : ℤ) (h : a ≠ 0 ∨ b ≠ 0 ∨ c ≠ 0 ∨ d ≠ 0) :
    0 < titsD4 a b c d := by
  have key := titsD4_sum_of_squares a b c d
  by_contra hq
  replace hq := not_lt.mp hq
  have s₁ := sq_nonneg (2 * c - a - b - d)
  have s₂ := sq_nonneg (a - b)
  have s₃ := sq_nonneg (a - d)
  have s₄ := sq_nonneg (b - d)
  have s₅ := sq_nonneg a
  have s₆ := sq_nonneg b
  have s₇ := sq_nonneg d
  have ha : a ^ 2 = 0 := by linarith
  have hb : b ^ 2 = 0 := by linarith
  have hd : d ^ 2 = 0 := by linarith
  have hc : (2 * c - a - b - d) ^ 2 = 0 := by linarith
  have ha' : a = 0 := pow_eq_zero_iff two_ne_zero |>.mp ha
  have hb' : b = 0 := pow_eq_zero_iff two_ne_zero |>.mp hb
  have hd' : d = 0 := pow_eq_zero_iff two_ne_zero |>.mp hd
  have hc' : 2 * c - a - b - d = 0 := pow_eq_zero_iff two_ne_zero |>.mp hc
  have hc'' : c = 0 := by omega
  rcases h with h | h | h | h <;> contradiction

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

Reflections preserve the form:

titsD4_reflect_centreLean 4Proved here from basic factsFormally verified

/-- The simple reflection at the centre, `c ↦ a + b + d - c`, preserves the Tits form. On
dimension vectors this is what the reflection functor at a sink or source does to every
indecomposable other than the simple one. -/
theorem titsD4_reflect_centre (a b c d : ℤ) :
    titsD4 a b (a + b + d - c) d = titsD4 a b c d := by
  unfold titsD4
  ring

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

titsD4_reflect_leafLean 4Proved here from basic factsFormally verified

/-- The simple reflection at the leaf `a`, `a ↦ c - a`, also preserves the Tits form. -/
theorem titsD4_reflect_leaf (a b c d : ℤ) :
    titsD4 (c - a) b c d = titsD4 a b c d := by
  unfold titsD4
  ring

Axioms used: propext, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

And the complete list of positive roots of $D_4$ : the sum-of-squares identity bounds every coordinate, and a finite case check does the rest.

D4_rootsLean 4Formally verified

/-- The twelve positive roots of `D₄`, written `(a, b, c, d)` with `c` the centre. -/
def D4_roots : List (ℕ × ℕ × ℕ × ℕ) :=
  [(1, 0, 0, 0), (0, 1, 0, 0), (0, 0, 1, 0), (0, 0, 0, 1),
   (1, 0, 1, 0), (0, 1, 1, 0), (0, 0, 1, 1),
   (1, 1, 1, 0), (1, 0, 1, 1), (0, 1, 1, 1),
   (1, 1, 1, 1), (1, 1, 2, 1)]

Axioms used: No axiomsformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

D4_positive_rootsLean 4Proved here from basic factsFormally verified

/-- **The positive roots of `D₄`.** A non-negative integer vector has Tits form `1` exactly
when it is one of the twelve vectors in `D4_roots`. Proof: the sum-of-squares identity bounds
`a, b, d ≤ 2` and `c ≤ 4`, leaving finitely many cases to check. By Gabriel's theorem these are
the dimension vectors of the twelve indecomposable representations of any quiver of type `D₄`
(Gabriel's theorem itself is not formalised here). -/
theorem D4_positive_roots (a b c d : ℕ) :
    titsD4 a b c d = 1 ↔ (a, b, c, d) ∈ D4_roots := by
  constructor
  · intro h
    have key := titsD4_sum_of_squares a b c d
    rw [h] at key
    have s₁ := sq_nonneg ((2 : ℤ) * c - a - b - d)
    have s₂ := sq_nonneg ((a : ℤ) - b)
    have s₃ := sq_nonneg ((a : ℤ) - d)
    have s₄ := sq_nonneg ((b : ℤ) - d)
    have s₅ := sq_nonneg (a : ℤ)
    have s₆ := sq_nonneg (b : ℤ)
    have s₇ := sq_nonneg (d : ℤ)
    have ha : a ≤ 2 := by
      have : (a : ℤ) ^ 2 ≤ 4 := by linarith
      have : (a : ℤ) ≤ 2 := by nlinarith
      exact_mod_cast this
    have hb : b ≤ 2 := by
      have : (b : ℤ) ^ 2 ≤ 4 := by linarith
      have : (b : ℤ) ≤ 2 := by nlinarith
      exact_mod_cast this
    have hd : d ≤ 2 := by
      have : (d : ℤ) ^ 2 ≤ 4 := by linarith
      have : (d : ℤ) ≤ 2 := by nlinarith
      exact_mod_cast this
    have hc : c ≤ 4 := by
      have h₀ : ((2 : ℤ) * c - a - b - d) ^ 2 ≤ 4 := by linarith
      have h₁ : (2 : ℤ) * c - a - b - d ≤ 2 := by nlinarith
      have h₂ : (a : ℤ) ≤ 2 := by exact_mod_cast ha
      have h₃ : (b : ℤ) ≤ 2 := by exact_mod_cast hb
      have h₄ : (d : ℤ) ≤ 2 := by exact_mod_cast hd
      have : (c : ℤ) ≤ 4 := by linarith
      exact_mod_cast this
    unfold titsD4 at h
    interval_cases a <;> interval_cases b <;> interval_cases c <;> interval_cases d <;>
      simp_all [D4_roots]
  · intro h
    simp only [D4_roots, List.mem_cons, Prod.mk.injEq, List.not_mem_nil, or_false] at h
    rcases h with ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ |
      ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ |
      ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ |
      ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ | ⟨rfl, rfl, rfl, rfl⟩ <;>
      norm_num [titsD4]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

D4_roots_lengthLean 4Proved here from basic factsFormally verified

/-- There are exactly twelve positive roots of `D₄` — the same as the number of positive roots
`n(n - 1) = 12` of the root system `D₄` in Lie theory. -/
theorem D4_roots_length : D4_roots.length = 12 := by decide

Axioms used: No axiomsformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

Finally, the Kronecker form is semidefinite but not definite — the arithmetic reason the Kronecker quiver has infinite type:

titsKronecker_semidefiniteLean 4Proved here from basic factsFormally verified

/-- The Kronecker quiver `1 ⇉ 2` has Tits form `q(x, y) = x² + y² - 2xy = (x - y)²`: never
negative, but zero at `(1, 1)`. So it is not positive definite, and the Kronecker quiver has
infinite representation type: over an infinite field there is a one-parameter family of
indecomposables of dimension vector `(1, 1)`, one for each point of the projective line. -/
theorem titsKronecker_semidefinite :
    (∀ x y : ℤ, 0 ≤ x ^ 2 + y ^ 2 - 2 * x * y) ∧ (1 : ℤ) ^ 2 + 1 ^ 2 - 2 * 1 * 1 = 0 := by
  refine ⟨fun x y => ?_, by norm_num⟩
  nlinarith [sq_nonneg (x - y)]

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/QuiverRepresentations.leanTry it in the Lean web editor

What is and is not formalised. We formalise the definition of representations (as prefunctors) and their equivalence with functors out of the path category, the $A_2$ dimension count, positive definiteness of the $A_2$ and $D_4$ forms, invariance under reflections, and the exact set of positive roots of $D_4$ . We do not formalise Gabriel's theorem itself (that the indecomposables correspond to these roots), Krull–Schmidt for quiver representations, reflection functors, Tits' orbit argument, Auslander–Reiten theory or Kac's theorem; none of these is in Mathlib at this version.

ComputationC

Three ways to count indecomposables

The experiment counts positive roots of Dynkin quivers in three independent ways: closing the simple roots under reflections; brute force over a box of non-negative vectors with $q = 1$ ; and knitting, iterating the inverse Coxeter matrix on the projectives until injectives are reached (Theorem 5). All three agree with $n(n+1)/2$ , $n(n-1)$ , $36$ , $63$ , $120$ , for two orientations of $A_4$ . For the Kronecker quiver, knitting never stops — the preprojectives $(n, n+1)$ go on forever — and over $\mathbb{F}_p$ there are $p + 1$ indecomposables of dimension $(1, 1)$ .

Quiver roots: reflections, brute force and knittingPythonExact computationExhaustive finite checkComputationally tested

"""Positive roots, Coxeter transformations and knitting for Dynkin quivers.

Gabriel's theorem says that a connected quiver has finitely many
indecomposable representations exactly when its underlying graph is of type
A, D or E, and that dimension vectors then match the positive roots: the
non-negative integer vectors x with Tits form q(x) = 1. We compute these roots
in three independent ways for several Dynkin quivers - by reflecting simple
roots, by brute force in a box, and by "knitting": applying the inverse
Coxeter transformation (which computes dim of tau^-1 M, the inverse
Auslander-Reiten translate) to the projective representations until an
injective is reached. For the Kronecker quiver the knitting never stops, and
the vector (1, 1) has q = 0: over F_p we count its p + 1 indecomposables, one
per point of the projective line. This is exact, exhaustive-finite evidence
for the quivers shown; Gabriel's theorem is the proof for all of them.
"""

from fractions import Fraction
from itertools import product

#: Quivers as (number of vertices, list of arrows i -> j).
QUIVERS = {
    "A4 (linear)": (4, [(0, 1), (1, 2), (2, 3)]),
    "A4 (zigzag)": (4, [(0, 1), (2, 1), (2, 3)]),
    "D4": (4, [(0, 1), (2, 1), (3, 1)]),
    "D5": (5, [(0, 2), (1, 2), (2, 3), (3, 4)]),
    "E6": (6, [(0, 1), (1, 2), (2, 3), (3, 4), (5, 2)]),
    "E7": (7, [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (6, 2)]),
    "E8": (8, [(0, 1), (1, 2), (2, 3), (3, 4), (4, 5), (5, 6), (7, 4)]),
}
KRONECKER = (2, [(0, 1), (0, 1)])

def tits_form(x, arrows):
    """q(x) = sum of x_i^2 minus x_i x_j over arrows i -> j."""
    return sum(v * v for v in x) - sum(x[i] * x[j] for i, j in arrows)

def reflect(x, i, arrows):
    """Simple reflection s_i: x_i becomes (sum over neighbours of x_j) - x_i."""
    nbr = sum(x[b] for a, b in arrows if a == i) + sum(
        x[a] for a, b in arrows if b == i)
    y = list(x)
    y[i] = nbr - x[i]
    return tuple(y)

def roots_by_reflection(n, arrows):
    """Close the simple roots under simple reflections, keeping x >= 0."""
    simple = [tuple(int(k == i) for k in range(n)) for i in range(n)]
    found, todo = set(simple), list(simple)
    while todo:
        x = todo.pop()
        for i in range(n):
            y = reflect(x, i, arrows)
            if min(y) >= 0 and any(y) and y not in found:
                found.add(y)
                todo.append(y)
    return found

def roots_by_brute_force(n, arrows, bound):
    """All x in {0..bound}^n, x != 0, with q(x) = 1."""
    return {x for x in product(range(bound + 1), repeat=n)
            if any(x) and tits_form(x, arrows) == 1}

def euler_matrix(n, arrows):
    """E = I - A, A[i][j] = number of arrows i -> j; <x, y> = x^T E y."""
    e = [[Fraction(int(i == j)) for j in range(n)] for i in range(n)]
    for i, j in arrows:
        e[i][j] -= 1
    return e

def mat_inv(m):
    """Inverse of a square matrix of Fractions (Gauss-Jordan)."""
    n = len(m)
    a = [list(row) + [Fraction(int(i == j)) for j in range(n)]
         for i, row in enumerate(m)]
    for c in range(n):
        p = next(r for r in range(c, n) if a[r][c] != 0)
        a[c], a[p] = a[p], a[c]
        a[c] = [v / a[c][c] for v in a[c]]
        for r in range(n):
            if r != c and a[r][c] != 0:
                a[r] = [u - a[r][c] * v for u, v in zip(a[r], a[c])]
    return [row[n:] for row in a]

def mat_mul(a, b):
    """Matrix product."""
    return [[sum(a[i][k] * b[k][j] for k in range(len(b)))
             for j in range(len(b[0]))] for i in range(len(a))]

def coxeter_inverse(n, arrows):
    """Phi^-1 for Phi = -E^-1 E^T, so dim(tau M) = Phi dim M."""
    e = euler_matrix(n, arrows)
    et = [list(r) for r in zip(*e)]
    phi = [[-v for v in row] for row in mat_mul(mat_inv(e), et)]
    return mat_inv(phi)

def projective_dims(n, arrows):
    """dim P(i)_j = number of paths from i to j (the quiver must be acyclic)."""
    dims = []
    for i in range(n):
        count = [0] * n
        stack = [i]
        while stack:
            v = stack.pop()
            count[v] += 1
            stack.extend(b for a, b in arrows if a == v)
        dims.append(tuple(count))
    return dims

def knit(n, arrows, max_steps=60):
    """Dimension vectors tau^-k P(i), stopping when Phi^-1 leaves x >= 0."""
    cinv = coxeter_inverse(n, arrows)
    found = []
    for p in projective_dims(n, arrows):
        x = p
        for _ in range(max_steps):
            found.append(x)
            y = tuple(int(sum(cinv[i][j] * x[j] for j in range(n)))
                      for i in range(n))
            if min(y) < 0:
                break
            x = y
    return found

def kronecker_family_count(p):
    """Isoclasses of indecomposable Kronecker reps k --a,b--> k over F_p.

    (a, b) and (a', b') are isomorphic when (a', b') = t (a, b), t != 0; the
    pair (0, 0) is decomposable. So we count lines in F_p^2.
    """
    classes = set()
    for a, b in product(range(p), repeat=2):
        if (a, b) != (0, 0):
            classes.add(min(((t * a) % p, (t * b) % p) for t in range(1, p)))
    return len(classes)

def main():
    print("type          refl  brute  knit  (indecomposables = positive roots)")
    for name, (n, arrows) in QUIVERS.items():
        refl = roots_by_reflection(n, arrows)
        bound = max(max(x) for x in refl)
        brute = roots_by_brute_force(n, arrows, bound) if n <= 6 else None
        knitted = knit(n, arrows)
        same = set(knitted) == refl and len(knitted) == len(refl)
        same = same and (brute is None or brute == refl)
        shown = "-" if brute is None else len(brute)
        print(f"{name:<13} {len(refl):>4}  {shown:>5}  "
              f"{len(knitted):>4}  {'agree' if same else 'DISAGREE'}")
    print("(brute force over the box {0..max}^n, run for n <= 6 only)")
    print()
    n, arrows = 4, QUIVERS["D4"][1]
    print("D4, arrows into the centre (vector order: leaf, centre, leaf, leaf):")
    print("  " + " ".join("".join(map(str, x)) for x in knit(n, arrows)))
    print()
    n, arrows = KRONECKER
    print("Kronecker quiver 0 => 1: tau^-1 orbits never reach an injective")
    pre = knit(n, arrows, max_steps=4)
    print("  preprojectives:", ", ".join(str(x) for x in pre))
    print("  Tits form on them:", [tits_form(x, arrows) for x in pre])
    print("  q(1, 1) =", tits_form((1, 1), arrows), "(an imaginary root)")
    counts = [(p, kronecker_family_count(p)) for p in (2, 3, 5, 7)]
    print("  indecomposables of dim (1, 1) over F_p:",
          ", ".join(f"p={p}: {c}" for p, c in counts))
    print()
    print("Epistemic status: exact integer and rational arithmetic, exhaustive")
    print("for the quivers, boxes and primes shown. It checks Gabriel's count")
    print("of indecomposables against the positive roots in these cases (the")
    print("knitting uses the theorem that dim tau^-1 M = Phi^-1 dim M for")
    print("hereditary algebras); it does not prove Gabriel's theorem.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

This is exact, exhaustive evidence for the quivers and primes shown. The knitting step relies on Theorem 5; none of it proves Gabriel's theorem.

Exercises

1. Quiver representations

Warm-upHuman

How many indecomposable representations (up to isomorphism) does the quiver $1 \to 2 \leftarrow 3 \to 4$ have over $\mathbb{C}$ ?

2. Quiver representations

CoreHuman

For $D_4$ with the centre written second, $q(a, c, b, d) = a^2 + c^2 + b^2 + d^2 - ac - bc - dc$ . Which vectors are dimension vectors of indecomposable representations? (Choose all that apply.)

Choose all that apply

(1, 2, 1, 1)

(1, 1, 1, 1)

(1, 2, 1, 0)

(2, 2, 1, 1)

(1, 0, 1, 0)

3. Quiver representations

Warm-upHuman

For the Kronecker quiver $1 \rightrightarrows 2$ (two arrows from $1$ to $2$ ), compute $\dim \operatorname{Ext}^1(S(1), S(2))$ using the Euler form.

4. Quiver representations

CoreHuman

The extended Dynkin graph $\tilde D_4$ is a star with centre $c$ and four leaves. Compute its Tits form at $\delta = (1, 1, 1, 1, 2)$ (leaves first, centre last).

5. Quiver representations

CoreHuman

Two connected quivers $Q$ and $Q'$ have the same underlying graph but different orientations. Which statement is correct?

Choose one

They have the same number of indecomposables, but a given dimension vector may be realised by quite different representationsTheir categories of representations are always equivalentOne may have finite type while the other has infinite typeTheir Tits forms differ

6. Quiver representations

StretchHuman

In Tits' proof that finite type forces $q(d) \ge 1$ , where does the “ $-1$ ” in $\dim(\text{orbit}) \le \sum_i d_i^2 - 1$ come from?

Choose one

The scalar matrices

\lambda \cdot (I_{d_i})_i

act trivially on

\mathrm{Rep}(Q, d)

, so every stabiliser has dimension at least

1

\mathrm{Rep}(Q, d)

is a projective variety of dimension one less than the affine spaceEach indecomposable has a one-dimensional endomorphism ringThe zero representation is a fixed point

7. Quiver representations

CoreHuman

Which statements about the Kronecker quiver $1 \rightrightarrows 2$ over $\mathbb{C}$ are true? (Choose all that apply.)

Choose all that apply

For each

n \ge 0

there is exactly one indecomposable of dimension vector

(n, n+1)

The indecomposables of dimension

(1, 1)

are parametrised by

\mathbb{P}^1(\mathbb{C})

It has finite representation typeIts Tits form is positive definite

8. Quiver representations

CoreFormal

Which Lean statement correctly formalises “the positive roots of $D_4$ are exactly the twelve vectors in D4_roots”? (titsD4 takes four integers, the centre third.)

Choose one

theorem t (a b c d : ℕ) : titsD4 a b c d = 1 ↔ (a, b, c, d) ∈ D4_rootstheorem t (a b c d : ℤ) : titsD4 a b c d = 1 ↔ (a, b, c, d) ∈ D4_rootstheorem t : D4_roots.length = 12theorem t (a b c d : ℤ) : 0 < titsD4 a b c d

9. Quiver representations

StretchComputational

Write positive_roots(n, edges) returning the set of positive roots (as tuples) of a Dynkin graph with vertices 0, …, n-1 and edge list edges, by closing the simple roots under simple reflections $s_i(x)_i = \sum_{j \sim i} x_j - x_i$ and keeping only non-negative, non-zero vectors.

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

"Gabriel's theorem depends on the orientation." Finite type and the bijection with positive roots depend only on the underlying graph: the reflection functors relate all orientations of a tree. What the orientation changes is which representation has a given dimension vector, and the shape of the AR quiver — not how many indecomposables there are.

Misconception

"Finite representation type means finitely many representations." There are always infinitely many representations up to isomorphism ( $S(i)^{\oplus n}$ for every $n$ ), over any field, finite or infinite. Finite type means finitely many indecomposable ones; by Krull–Schmidt every representation is then a direct sum of these.

Misconception

"Every vector with $q(x) = 1$ is a dimension vector of an indecomposable." Only the positive ones: $q(-x) = q(x)$ , so negative roots also satisfy $q = 1$ . And for non-Dynkin quivers, dimension vectors of indecomposables are the positive roots of the Kac–Moody root system, which include imaginary roots with $q(x) \le 0$ .

Misconception

"Over an infinite field the Kronecker quiver has infinitely many indecomposables, but over a finite field it has finitely many." Over $\mathbb{F}_q$ each dimension vector carries finitely many isomorphism classes, but the preprojectives $(n, n+1)$ already give infinitely many indecomposables. Infinite type is a property of the graph.

Misconception

"The Auslander–Reiten translate $\tau$ is a functor on $\mathrm{rep}(Q)$ given by reflection." For path algebras $\tau$ agrees on indecomposable non-projectives with the Coxeter functor, a composite of reflection functors, but it is not an equivalence of $\mathrm{rep}(Q)$ : it kills the projectives. On dimension vectors it acts linearly by $\Phi$ only on indecomposable non-projective modules.

ViewpointsH

Viewpoints

Geometry— Orbits, moduli and quiver varieties

Isomorphism classes of representations of dimension $d$ are the orbits of $GL(d)$ on the affine space $\mathrm{Rep}(Q, d)$ , and Theorem 2 is a statement about orbit dimensions. Finite type means finitely many orbits; then there is a dense open orbit, and degenerations between orbits are studied as a geometric order on representations. For infinite type one builds moduli spaces by geometric invariant theory: King (1994) translated GIT stability into a slope-type condition on subrepresentations, giving projective moduli spaces of stable representations. Nakajima's quiver varieties, hyperkähler quotients built from doubled quivers, carry geometric actions of Kac–Moody algebras on their cohomology. See algebraic geometry.

Topology— The McKay correspondence and the E₈ manifold

The same Dynkin diagrams classify the finite subgroups $G \subset SU(2)$ (McKay, 1980: the irreducible representations of $G$ form the vertices of an extended Dynkin diagram) and the simple surface singularities $\mathbb{C}^2/G$ (Du Val). The minimal resolution of $\mathbb{C}^2/G$ replaces the singular point by a tree of $(-2)$ -spheres whose dual graph is the Dynkin diagram, and their intersection form is minus the Cartan matrix $2I - A$ , i.e. $-2q$ in symmetric form. For $E_8$ this gives a smooth $4$ -manifold with intersection form $-E_8$ whose boundary is the Poincaré homology sphere — a building block in four-dimensional topology (see low-dimensional topology). Grauert's criterion says that a configuration of curves on a surface can be contracted to a point only if its intersection form is negative definite; for a tree of $(-2)$ -spheres this happens exactly when the tree is a Dynkin diagram — the same positivity that singles out Gabriel's quivers.

Algebra— Roots, Hall algebras and hereditary categories

Gabriel's positive roots are the positive roots of the semisimple Lie algebra with the same Dynkin diagram, and Ringel's Hall algebra explains why: the category $\mathrm{rep}_{\mathbb{F}_q}(Q)$ "knows" the quantum group, with indecomposables corresponding to a PBW-type basis. From the point of view of ring theory, path algebras of acyclic quivers are exactly the basic hereditary finite-dimensional algebras over an algebraically closed field, so this lesson is also the representation theory of hereditary algebras. See Lie groups and Lie algebras.

Combinatorics— Counting roots, clusters and walks

The Dynkin classification is itself a combinatorial theorem: a connected graph has positive definite $2I - A$ iff it is $A_n$ , $D_n$ , $E_{6,7,8}$ , iff its largest adjacency eigenvalue is below $2$ . Root counts $n(n+1)/2$ , $n(n-1)$ , $36$ , $63$ , $120$ equal $nh/2$ with $h$ the Coxeter number. For cluster algebras of type $A_n$ the number of clusters is the Catalan number $\frac{1}{n+2}\binom{2n+2}{n+1}$ , and clusters correspond to triangulations of an $(n+3)$ -gon (Fomin–Zelevinsky).

Physics— Quiver gauge theories (heuristic)

In string theory, D-branes at the orbifold singularity $\mathbb{C}^2/G$ are described by a gauge theory whose matter content is encoded by the McKay quiver of $G$ (Douglas–Moore, 1996), and in four-dimensional $\mathcal{N} = 2$ theories the BPS states are counted by stable representations of a quiver with potential, with wall-crossing governed by the Kontsevich–Soibelman formula. These physical pictures motivate much current mathematics (cohomological Hall algebras, Donaldson–Thomas invariants); they are heuristics, and the theorems are proved separately.

Category theory— Functors from a free category

A representation of $Q$ is a functor from the free category $\mathrm{Paths}(Q)$ to $\mathrm{Vect}_k$ (formalised above), so $\mathrm{rep}(Q)$ is a functor category and inherits its abelian structure pointwise; the projective $P(i)$ is the representable functor $k\,\mathrm{Paths}(Q)(i, -)$ , and the Yoneda lemma gives $\operatorname{Hom}(P(i), V) = V_i$ . The reflection functors, the Coxeter functor and $\tau$ are functors between such categories; their derived versions are equivalences of derived categories.

History & global context

History and global context

1868–1890. Karl Weierstrass (elementary divisors) and Leopold Kronecker solve the classification of matrix pencils — in modern terms, representations of the Kronecker quiver.
1960s–70. In Kyiv, Lyudmila Nazarova and Andrei Roiter develop matrix problems and their reduction techniques; in Moscow, Israel Gelfand and V. A. Ponomarev classify quadruples of subspaces (1970).
1972. Pierre Gabriel (France/Switzerland) proves his theorem, in "Unzerlegbare Darstellungen I", and coins the term quiver (Köcher).
1973. Joseph Bernstein, Israel Gelfand and V. A. Ponomarev introduce reflection functors and explain Gabriel's theorem through Coxeter functors. Peter Donovan and Mary Ruth Freislich (Australia) and, independently, Nazarova classify the tame quivers.
1975. Maurice Auslander (USA) and Idun Reiten (Norway) introduce almost split sequences.
1979–80. Yuriy Drozd (Kyiv) proves the tame–wild dichotomy; Victor Kac proves his theorem on dimension vectors.
1990s–2000s. Claus Michael Ringel (Hall algebras), George Lusztig (canonical bases), Hiraku Nakajima (quiver varieties), Sergey Fomin and Andrei Zelevinsky (cluster algebras). The representation theory of algebras has strong schools in many countries, including Mexico, Brazil, China, Japan, Poland and Norway.

Classifying configurations of linear maps

Pictures, dimension vectors, indecomposables

Definitions

Examples

Central theorems

The landscape: tame, wild, and the links with Lie theory

Explore: Dynkin or not, through walks

Quiver representations in Lean and Mathlib

Three ways to count indecomposables

Exercises

Common misconceptions

Viewpoints

History and global context

Further reading