The Ext-Euler pairing of a finite acyclic quiver is the Ringel form

Let Q be a finite quiver whose path algebra kQ is finite-dimensional, that is, a finite acyclic quiver. Its simple modules are the vertex simples, each of which has a projective resolution of length one, so every pair of finitely generated kQ-modules is Euler-admissible: no Ext group above degree one survives, and every Hom and Ext group is finite-dimensional. The categorical Ext-Euler pairing on the Grothendieck group of finitely generated modules therefore exists, and it is the Ringel form of the dimension vectors,

χ(M, N) = ∑ᵢ dim Mᵢ dim Nᵢ - ∑_{a : i ⟶ j} dim Mᵢ dim Nⱼ.

Both sides are biadditive and the simple classes span, so the identity follows from the vertex simple computation. Its symmetrization is the polarized Tits form; the raw pairing need not be symmetric.

Main results

• TauCeti.isEulerAdmissibleOn_isFG_pathAlgebra: every pair of finitely generated modules over a finite-dimensional path algebra is Euler-admissible.
• TauCeti.extEulerPairing_eq_pathAlgebraEulerPairingK0: the Ext-Euler pairing on G₀(mod kQ) is the Ringel form pulled back along dimension vectors.
• TauCeti.extEuler_eq_eulerForm_dimVector: the object-level Ext-Euler characteristic of two finitely generated modules is the Ringel form of their dimension vectors.
• TauCeti.extEulerPairing_add_flip_eq_titsPolarForm: the symmetrized Ext-Euler pairing is the polarized Tits form of the dimension vectors.

References

• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Section 3, in particular Proposition 3.13.

theorem TauCeti.isEulerAdmissibleOn_isFG_pathAlgebra (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Finite Q] [FiniteDimensional k (pathAlgebra k Q)] : IsEulerAdmissibleOn k (ModuleCat.isFG (pathAlgebra k Q)) (ModuleCat.isFG (pathAlgebra k Q))

Every pair of finitely generated modules over a finite-dimensional path algebra is Euler-admissible. The simple modules are the vertex simples, whose first-arrow resolutions bound Ext above degree one, and admissibility propagates along composition series.

@[simp]

theorem TauCeti.extEulerPairing_eq_pathAlgebraEulerPairingK0 (k : Type (max v w)) (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))) : ((extEulerPairing ⋯ ⋯ ⋯) ((finiteModulesExactK0Equiv (pathAlgebra k Q)) x)) ((finiteModulesExactK0Equiv (pathAlgebra k Q)) y) = ((pathAlgebraEulerPairingK0 k Q) x) y

The Ext-Euler pairing of a finite acyclic quiver is the Ringel form. On the Grothendieck group of finitely generated modules over a finite-dimensional path algebra, the categorical Ext-Euler pairing is the quiver Euler form pulled back along the dimension-vector map.

@[simp]

theorem TauCeti.extEuler_eq_eulerForm_dimVector (k : Type (max v w)) (Q : Type v) [Field k] [Quiver Q] [Fintype Q] [(a b : Q) → Fintype (a ⟶ b)] [FiniteDimensional k (pathAlgebra k Q)] (X Y : ModuleCat (pathAlgebra k Q)) [Module.Finite (pathAlgebra k Q) ↑X] [Module.Finite (pathAlgebra k Q) ↑Y] (h : IsEulerAdmissible k X Y) : extEuler k h = ((eulerForm Q) fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj X) i)) fun (i : Q) => ↑(dimVector ((quiverRepFunctor k Q).obj Y) i)

The Ext-Euler characteristic of two finitely generated modules over a finite-dimensional path algebra is the Ringel form of their dimension vectors.

theorem TauCeti.extEulerPairing_add_flip_eq_titsPolarForm (k : Type (max v w)) (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))) : ((extEulerPairing ⋯ ⋯ ⋯) ((finiteModulesExactK0Equiv (pathAlgebra k Q)) x)) ((finiteModulesExactK0Equiv (pathAlgebra k Q)) y) + ((extEulerPairing ⋯ ⋯ ⋯) ((finiteModulesExactK0Equiv (pathAlgebra k Q)) y)) ((finiteModulesExactK0Equiv (pathAlgebra k Q)) x) = ((titsPolarForm Q) ((pathAlgebraDimensionVectorK0 k Q) x)) ((pathAlgebraDimensionVectorK0 k Q) y)

The symmetrized Ext-Euler pairing is the polarized Tits form of the dimension vectors.