Dimension vectors on Grothendieck groups of quiver representations and path algebra modules

For a finite-dimensional path algebra, a finitely generated module has finite-dimensional vertex spaces. The dimension vector is therefore additive in every short exact sequence of finitely generated modules, and defines a homomorphism from their exact Grothendieck group to the integral dimension lattice. This is the map through which the quiver Euler form can be compared with an Ext-Euler pairing on object classes.

The restriction to finite-dimensional path algebras is essential: Module.finrank has a junk value on infinite-dimensional spaces, and a finitely generated module over a cyclic quiver's path algebra need not be finite-dimensional over the base field.

For a finite quiver, pointwise finite-dimensional representations form an essentially small category, and their exact Grothendieck group has a dimension-vector map. For finite vertex sets with finite arrow types, this map pulls back the Euler form to a pairing on that group.

See Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3, for dimension vectors and the Grothendieck group of finite-dimensional representations.

noncomputable def TauCeti.pathAlgebraDimensionVectorK0 (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q)) →+ Q → ℤ

The integral dimension vector as an additive map on exact K₀ of finitely generated modules over a finite-dimensional path algebra.

@[simp]

theorem TauCeti.pathAlgebraDimensionVectorK0_of (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (M : FGModuleCat (pathAlgebra k Q)) : (pathAlgebraDimensionVectorK0 k Q) (ExactK0.of M) = fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj M.obj) i)

The dimension-vector map sends the class of a module to the dimensions of its vertex components.

theorem TauCeti.pathAlgebraDimensionVectorK0_unique (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] (f : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q)) →+ Q → ℤ) (hf : ∀ (M : FGModuleCat (pathAlgebra k Q)), f (ExactK0.of M) = fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj M.obj) i)) : f = pathAlgebraDimensionVectorK0 k Q

The map on K₀ is characterized by its values on module classes.

noncomputable def TauCeti.pathAlgebraEulerPairingK0 (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [FiniteDimensional k (pathAlgebra k Q)] : LinearMap.BilinForm ℤ (ExactK0 (finiteModulesExactStructure (pathAlgebra k Q)))

The Ringel form pulled back to the exact Grothendieck group of finite-dimensional path algebra modules. This is the integral form against which the Ext-Euler pairing is compared.

@[simp]

theorem TauCeti.pathAlgebraEulerPairingK0_apply (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [FiniteDimensional k (pathAlgebra k Q)] (x y : ExactK0 (finiteModulesExactStructure (pathAlgebra k Q))) : ((pathAlgebraEulerPairingK0 k Q) x) y = ((eulerForm Q) ((pathAlgebraDimensionVectorK0 k Q) x)) ((pathAlgebraDimensionVectorK0 k Q) y)

The pulled-back form is the quiver Euler form of the two dimension-vector images.

theorem TauCeti.pathAlgebraEulerPairingK0_of_of (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [FiniteDimensional k (pathAlgebra k Q)] (M N : FGModuleCat (pathAlgebra k Q)) : ((pathAlgebraEulerPairingK0 k Q) (ExactK0.of M)) (ExactK0.of N) = ((eulerForm Q) fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj M.obj) i)) fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj N.obj) i)

On module classes, the pulled-back form is the quiver Euler form of the two dimension vectors.

theorem TauCeti.pathAlgebraEulerPairingK0_unique (k : Type u) (Q : Type v) [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [FiniteDimensional k (pathAlgebra k Q)] (b : LinearMap.BilinForm ℤ (ExactK0 (finiteModulesExactStructure (pathAlgebra k Q)))) (hb : ∀ (M N : FGModuleCat (pathAlgebra k Q)), (b (ExactK0.of M)) (ExactK0.of N) = ((eulerForm Q) fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj M.obj) i)) fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj N.obj) i)) : b = pathAlgebraEulerPairingK0 k Q

The pulled-back Ringel form is determined by its values on pairs of module classes.

noncomputable def TauCeti.quiverRepDimensionVectorK0 (k : Type u) (Q : Type v) [Field k] [Quiver Q] [CategoryTheory.EssentiallySmall.{t, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))] : ExactK0 (pointwiseFiniteDimensionalQuiverRepresentationsExactStructure k Q) →+ Q → ℤ

The dimension vector as an additive map from the exact Grothendieck group of pointwise finite-dimensional quiver representations to the integral vertex lattice.

@[simp]

theorem TauCeti.quiverRepDimensionVectorK0_of (k : Type u) (Q : Type v) [Field k] [Quiver Q] [CategoryTheory.EssentiallySmall.{t, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))] (M : CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q)) : (quiverRepDimensionVectorK0 k Q) (ExactK0.of M) = fun (i : Q) => ↑(dimVector M.obj i)

The Grothendieck-group dimension map sends an object class to its dimension vector.

theorem TauCeti.quiverRepDimensionVectorK0_unique (k : Type u) (Q : Type v) [Field k] [Quiver Q] [CategoryTheory.EssentiallySmall.{t, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))] (f : ExactK0 (pointwiseFiniteDimensionalQuiverRepresentationsExactStructure k Q) →+ Q → ℤ) (hf : ∀ (M : CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q)), f (ExactK0.of M) = fun (i : Q) => ↑(dimVector M.obj i)) : f = quiverRepDimensionVectorK0 k Q

The dimension-vector map is determined by its values on representation classes.

noncomputable def TauCeti.quiverRepEulerPairingK0 (k : Type u) (Q : Type v) [Field k] [Quiver Q] [CategoryTheory.EssentiallySmall.{t, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] : LinearMap.BilinForm ℤ (ExactK0 (pointwiseFiniteDimensionalQuiverRepresentationsExactStructure k Q))

The Ringel form transported to the exact Grothendieck group of pointwise finite-dimensional quiver representations through their dimension vectors.

@[simp]

theorem TauCeti.quiverRepEulerPairingK0_of_of (k : Type u) (Q : Type v) [Field k] [Quiver Q] [CategoryTheory.EssentiallySmall.{t, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (M N : CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q)) : ((quiverRepEulerPairingK0 k Q) (ExactK0.of M)) (ExactK0.of N) = ((eulerForm Q) fun (i : Q) => ↑(dimVector M.obj i)) fun (i : Q) => ↑(dimVector N.obj i)

On representation classes, the transported pairing is the Ringel form of their dimension vectors.

theorem TauCeti.quiverRepEulerPairingK0_unique (k : Type u) (Q : Type v) [Field k] [Quiver Q] [CategoryTheory.EssentiallySmall.{t, max t v, max (max (max (t + 1) u) v) w} (CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q))] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] (b : LinearMap.BilinForm ℤ (ExactK0 (pointwiseFiniteDimensionalQuiverRepresentationsExactStructure k Q))) (hb : ∀ (M N : CategoryTheory.ObjectProperty.FullSubcategory (IsFinDim k Q)), (b (ExactK0.of M)) (ExactK0.of N) = ((eulerForm Q) fun (i : Q) => ↑(dimVector M.obj i)) fun (i : Q) => ↑(dimVector N.obj i)) : b = quiverRepEulerPairingK0 k Q

The transported pairing is determined by its values on pairs of representation classes.