Dimension vectors of isomorphism classes of indecomposables

The dimension vector is constant on isomorphism classes, so it descends to the skeleton of the finite-dimensional indecomposable representations as TauCeti.isoClassDimVector. This file gives the generic map and its computation rules; results requiring a positive definite Tits form live in TauCeti.RepresentationTheory.Quiver.FiniteRepType.PosDef.

Main definitions

• TauCeti.isoClassDimVector: the dimension vector of an isomorphism class of finite-dimensional indecomposable representations, as an integer vector.

Main results

• TauCeti.isoClassDimVector_toSkeleton: the map sends the class of a representation to that representation's dimension vector.
• TauCeti.isoClassDimVector_nonneg: the resulting integer vector is nonnegative.

Implementation notes

TauCeti.isoClassDimVector reads its representation 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 remain in max v w x, matching the universe in which the reflection functors produce them and preserving the common API used by the finite-representation-type results.

References

This supports the dimension-vector map in the Gabriel correspondence of Layer 5 of TauCetiRoadmap/RepresentationTheory/QuiverRepresentations/README.md.

noncomputable def TauCeti.isoClassDimVector {k : Type u} {V : Type v} [Field k] [Quiver V] (X : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M)) : V → ℤ

The dimension vector of an isomorphism class of finite-dimensional indecomposable representations, as a vector of integers, the shape in which the Tits form reads it.

It is computed on a class by TauCeti.isoClassDimVector_toSkeleton; the chosen representative of the class, supplied by CategoryTheory.fromSkeleton, is isomorphic to any other, and the dimension vector does not see the difference.

@[simp]

theorem TauCeti.isoClassDimVector_apply {k : Type u} {V : Type v} [Field k] [Quiver V] (X : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M)) (j : V) : isoClassDimVector X j = ↑(dimVector ((CategoryTheory.fromSkeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M)).obj X).obj j)

The dimension vector of a class is read off the representative that CategoryTheory.fromSkeleton chooses.

@[simp]

theorem TauCeti.isoClassDimVector_toSkeleton {k : Type u} {V : Type v} [Field k] [Quiver V] (M : QuiverRep k V) (hfd : ∀ (j : CategoryTheory.Paths V), FiniteDimensional k ↑(M.obj j)) (hM : CategoryTheory.Indecomposable M) : isoClassDimVector (CategoryTheory.toSkeleton { obj := M, property := ⋯ }) = fun (j : V) => ↑(dimVector M j)

The dimension vector of a class is the dimension vector of any of its members.

theorem TauCeti.isoClassDimVector_nonneg {k : Type u} {V : Type v} [Field k] [Quiver V] (X : CategoryTheory.Skeleton (CategoryTheory.ObjectProperty.FullSubcategory fun (M : QuiverRep k V) => IsFinDim k V M ∧ CategoryTheory.Indecomposable M)) : 0 ≤ isoClassDimVector X

The dimension vector of a class of indecomposables is nonnegative, being a vector of dimensions.