An indecomposable representation is determined by its dimension vector

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 two finite-dimensional indecomposable representations of Q with the same dimension vector are isomorphic (TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable), so that TauCeti.dimVector is injective on the isomorphism classes of indecomposables (TauCeti.nonempty_iso_iff_dimVector_eq_of_indecomposable).

Together with TauCeti.titsForm_dimVector_eq_one_of_indecomposable, which says that the dimension vector of an indecomposable is a positive root of the Tits form, this is the injective half of the Gabriel correspondence: M ↦ dim M is an injection from the isomorphism classes of finite-dimensional indecomposables into the positive roots. Its surjectivity, that every positive root is realized, is TauCeti.exists_indecomposable_dimVector_eq in TauCeti.RepresentationTheory.Quiver.Reflection.Existence.

The argument

The Bernstein-Gelfand-Ponomarev induction is run at M and N in parallel. The reflection functor at a sink i is fully faithful on the representations whose incoming sum at i is onto (TauCeti.reflectionFunctor_map_bijective), and a fully faithful functor reflects isomorphisms: this is TauCeti.nonempty_iso_of_nonempty_iso_reflectRep. An indecomposable representation fails that hypothesis only by being concentrated at i (TauCeti.incomingSum_surjective_or_forall_subsingleton), and a representation with the same dimension vector then vanishes wherever it does and has a vertex space of the same dimension at i; two such representations are isomorphic, by TauCeti.nonempty_iso_of_isZero_away_of_linearEquiv.

The comparison at such a stage is made directly, rather than through the vertex simple Sᵢ and TauCeti.nonempty_iso_simpleRep_of_forall_subsingleton: the vertex space of Sᵢ is the field itself, so naming it would force the universe of the vertex spaces to be that of the field, below the generality at which TauCeti.titsForm_dimVector_eq_one_of_indecomposable states the other half of the correspondence.

So at each stage of a sink-admissible list, either both representations are concentrated at the current sink and are therefore already identified, or both reflect, with equal dimension vectors again. The induction terminates because a power of the Coxeter functor annihilates M (TauCeti.exists_isZero_coxeterFunctor_iterate), and the stage that annihilates it is a stage where it is concentrated at the sink.

Main results

• TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable: two finite-dimensional indecomposable representations with the same dimension vector are isomorphic, with TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable_of_isAcyclic the same statement over an acyclic quiver, where the sink-admissible ordering is chosen internally.
• TauCeti.nonempty_iso_iff_dimVector_eq_of_indecomposable: the resulting characterization of isomorphism of indecomposables by equality of dimension vectors.

References

This is the uniqueness step of the reflection induction for Gabriel's theorem. See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Derksen--Weyman, An Introduction to Quiver Representations, Ch. 2.

Uniqueness along a sink-admissible list

Uniqueness

theorem TauCeti.nonempty_iso_of_dimVector_eq_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 N : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hN : CategoryTheory.Indecomposable N) (hfdM : IsFinDim k V M) (hfdN : IsFinDim k V N) (hd : dimVector M = dimVector N) : Nonempty (M ≅ N)

An indecomposable representation is determined by its dimension vector. For a quiver with positive definite Tits form -- the numerical form of the ADE condition -- and any sink-admissible ordering of its vertices, two indecomposable representations with finite-dimensional vertex spaces and the same dimension vector are isomorphic.

This is the injectivity half of the Gabriel correspondence; that the dimension vector of an indecomposable is a positive root is TauCeti.titsForm_dimVector_eq_one_of_indecomposable.

theorem TauCeti.nonempty_iso_of_dimVector_eq_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 N : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hN : CategoryTheory.Indecomposable N) (hfdM : IsFinDim k V M) (hfdN : IsFinDim k V N) (hd : dimVector M = dimVector N) : Nonempty (M ≅ N)

An indecomposable representation of an acyclic quiver with positive definite Tits form is determined by its dimension vector. This is the consumer-facing form of TauCeti.nonempty_iso_of_dimVector_eq_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.

theorem TauCeti.nonempty_iso_iff_dimVector_eq_of_indecomposable {k : Type u} {V : Type v} [fld : Field k] [fV : Fintype V] [Quiver V] [(a b : V) → Fintype (a ⟶ b)] (hac : Quiver.IsAcyclic V) (hpd : (titsForm V).PosDef) (M N : QuiverRep k V) (hM : CategoryTheory.Indecomposable M) (hN : CategoryTheory.Indecomposable N) (hfdM : IsFinDim k V M) (hfdN : IsFinDim k V N) : Nonempty (M ≅ N) ↔ dimVector M = dimVector N

Indecomposable representations of an acyclic quiver with positive definite Tits form are isomorphic exactly when their dimension vectors agree. The forward direction is TauCeti.dimVector_eq_of_iso and needs none of the hypotheses; the converse is TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable_of_isAcyclic.