Documentation

TauCeti.RepresentationTheory.Quiver.FiniteRepType.PosDef

A positive definite Tits form forces finite representation type #

Let V 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 V has finite representation type (TauCeti.isFiniteRepType_of_titsForm_posDef).

The result comes from one map. The dimension vector is constant on isomorphism classes, so it descends to the skeleton of the finite-dimensional indecomposables as TauCeti.isoClassDimVector. That map lands in the positive roots, by TauCeti.titsForm_dimVector_eq_one_of_indecomposable_of_isAcyclic, and is injective, by TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable_of_isAcyclic; a positive definite integral quadratic form takes the value 1 only finitely often, by QuadraticMap.PosDef.finite_setOf_apply_eq, so the skeleton is finite.

No acyclicity hypothesis appears, although both consumed theorems ask for one: a directed cycle would already contradict positive definiteness, by TauCeti.isAcyclic_of_titsForm_posDef.

This is the affirming half of Gabriel's dichotomy, and the half that the earlier work leaves to be read off: the two theorems it consumes were proved for their own sake, one saying that a dimension vector of an indecomposable is a root and one that it determines the indecomposable, and neither draws the finiteness conclusion. The refuting half, that a quiver outside Dynkin type has infinitely many indecomposables, is TauCeti.not_isFiniteRepType_of_infinite applied to an explicit family, as in TauCeti.not_isFiniteRepType_kronecker.

Main definitions #

Main results #

Implementation notes #

The isomorphism classes are Mathlib's CategoryTheory.Skeleton of the full subcategory of finite-dimensional indecomposable representations, spelled out rather than abbreviated, exactly as in TauCeti.IsFiniteRepType and in TauCeti.card_skeleton_indecomposable_kronecker.

TauCeti.isoClassDimVector reads its representation off through CategoryTheory.fromSkeleton rather than by a quotient lift. The skeleton is a quotient by definition, but that definition is not part of its interface; CategoryTheory.toSkeleton_fromSkeleton_obj returns the chosen representative to its own class, which is all a map out of the skeleton needs.

The vertex spaces live in max v w x because that is the universe in which the reflection functors of TauCeti.RepresentationTheory.Quiver.Reflection.Basic produce them: the reflected vertex space at a sink is cut out of a product indexed by the arrows there.

References #

This is the affirming direction of Gabriel's theorem: positive definiteness of the Tits form is what forces the indecomposables to be finite in number. See Bernstein--Gelfand--Ponomarev, Coxeter functors and Gabriel's theorem, and Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Ch. VII.

source
theorem TauCeti.titsForm_isoClassDimVector_eq_one {k : Type u} {V : Type v} [Field k] [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (hpd : (titsForm V).PosDef) (X : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M)) :
(titsForm V) (isoClassDimVector X) = 1

The dimension vector of a class of indecomposables is a root of the Tits form, the class form of TauCeti.titsForm_dimVector_eq_one_of_indecomposable_of_isAcyclic.

source
theorem TauCeti.isoClassDimVector_injective {k : Type u} {V : Type v} [Field k] [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (hpd : (titsForm V).PosDef) :
Function.Injective isoClassDimVector

The Gabriel injection. Over a finite quiver with positive definite Tits form, two isomorphism classes of finite-dimensional indecomposable representations with the same dimension vector coincide. This is TauCeti.nonempty_iso_of_dimVector_eq_of_indecomposable_of_isAcyclic, transported to the skeleton.

source
noncomputable def TauCeti.isoClassDimVectorEmbedding {k : Type u} {V : Type v} [Field k] [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (hpd : (titsForm V).PosDef) :
CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M) ↪ { d : V → ℤ // 0 ≤ d ∧ (titsForm V) d = 1 }

The isomorphism classes of finite-dimensional indecomposable representations embed into the positive roots of the Tits form, by the dimension vector. This is the injective half of the Gabriel correspondence, packaged; its surjectivity, that every positive root is the dimension vector of an indecomposable, is not proved here.

Instances For
    source
    @[simp]
    theorem TauCeti.coe_isoClassDimVectorEmbedding_apply {k : Type u} {V : Type v} [Field k] [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (hpd : (titsForm V).PosDef) (X : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M)) :
    ↑((isoClassDimVectorEmbedding hpd) X) = isoClassDimVector X

    The vector underlying the Gabriel injection is the dimension vector of the isomorphism class.

    source
    theorem TauCeti.isFiniteRepType_of_titsForm_posDef {k : Type u} {V : Type v} [Field k] [Quiver V] [Fintype V] [(a b : V) → Fintype (a ⟶ b)] (hpd : (titsForm V).PosDef) :
    IsFiniteRepType k V

    A finite quiver whose Tits form is positive definite has finite representation type. This is the affirming direction of Gabriel's dichotomy: the dimension vector embeds the isomorphism classes of finite-dimensional indecomposables into the roots of the Tits form, of which a positive definite form has only finitely many.

    The refuting direction is TauCeti.not_isFiniteRepType_of_infinite, which asks instead for an infinite family of pairwise non-isomorphic indecomposables.