The graded Ringel formula on all finite graded path-algebra modules

For a finite quiver with finite-dimensional path algebra, every pair of finite graded modules is graded Euler-admissible. The first-arrow resolutions give admissibility on vertex simples; internal shifts and graded composition series extend it to every finite graded source.

The categorical q-Euler form on the Laurent Grothendieck group is the graded Ringel form: if xᵢ and yᵢ are the idempotent graded dimensions, then

χ_q(x,y) = ∑ᵢ invert(xᵢ) yᵢ - q⁻¹ ∑_{a : i ⟶ j} invert(xᵢ) yⱼ.

Rows are source vertices and columns are target vertices. The inverse power of q records the shift of the projectives in the first-arrow resolution, and the involution in the first argument records q-antilinearity. Neither the pairing nor its matrix is generally symmetric.

References

• I. Assem, D. Simson and A. Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Sections 2--3, for the first-arrow resolution and Ringel form.
• Z. Dancso and A. Licata, Koszul algebras and flow lattices, Section 2.2, for the q-antilinear convention.

The object-level entries are those of gradedExtEuler_gradedVertexSimple_gradedVertexSimple; the extension to classes uses gradedVertexSimpleClassBasis and Mathlib's sesquilinear matrix evaluation formula.

theorem TauCeti.PathAlgebra.isGradedEulerAdmissibleOn_gradedFiniteModules (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [Module.Finite k (pathAlgebra k Q)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] : IsGradedEulerAdmissibleOn (gradedFiniteModules (integerGrade k Q)) (gradedFiniteModules (integerGrade k Q))

Every pair of finite graded modules over a finite-dimensional path algebra is graded Euler-admissible. Both cohomological and internal finiteness follow from the first-arrow resolutions and graded composition series.

noncomputable def TauCeti.PathAlgebra.gradedExtEulerForm (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [Module.Finite k (pathAlgebra k Q)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] : LaurentK0 (gradedFiniteModulesExactStructure (integerGrade k Q)) →ₛₗ[LaurentPolynomial.invert.toRingEquiv.toRingHom] LaurentK0 (gradedFiniteModulesExactStructure (integerGrade k Q)) →ₗ[LaurentPolynomial ℤ] LaurentPolynomial ℤ

The categorical q-Euler form on G₀^gr(mod kQ), q-antilinear in the first argument and q-linear in the second. Admissibility is proved for every finite graded module pair.

@[simp]

theorem TauCeti.PathAlgebra.gradedExtEulerForm_of_of (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [Module.Finite k (pathAlgebra k Q)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] (X Y : (gradedFiniteModules (integerGrade k Q)).FullSubcategory) : ((gradedExtEulerForm k Q) (LaurentK0.of (gradedFiniteModulesExactStructure (integerGrade k Q)) X)) (LaurentK0.of (gradedFiniteModulesExactStructure (integerGrade k Q)) Y) = gradedExtEuler k (GradedModuleCat.shift (integerGrade k Q)) ⋯

On object classes the q-Euler form is the graded Ext-Euler characteristic.

theorem TauCeti.PathAlgebra.gradedExtEulerForm_basis (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [Module.Finite k (pathAlgebra k Q)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] [DecidableEq Q] (i j : Q) : ((gradedExtEulerForm k Q) ((gradedVertexSimpleClassBasis k Q) i)) ((gradedVertexSimpleClassBasis k Q) j) = (if i = j then 1 else 0) - LaurentPolynomial.T (-1) * ↑(Nat.card (i ⟶ j))

The q-Euler matrix in the graded vertex-simple basis is I - q⁻¹ A, where the (i,j) entry of A counts arrows i ⟶ j.

theorem TauCeti.PathAlgebra.gradedExtEulerForm_eq_sum (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Fintype Q] [Module.Finite k (pathAlgebra k Q)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] (x y : LaurentK0 (gradedFiniteModulesExactStructure (integerGrade k Q))) : ((gradedExtEulerForm k Q) x) y = ∑ i : Q, LaurentPolynomial.invert (((gradedVertexSimpleClassBasis k Q).repr x) i) * ((gradedVertexSimpleClassBasis k Q).repr y) i - LaurentPolynomial.T (-1) * ∑ i : Q, ∑ j : Q, ↑(Nat.card (i ⟶ j)) * LaurentPolynomial.invert (((gradedVertexSimpleClassBasis k Q).repr x) i) * ((gradedVertexSimpleClassBasis k Q).repr y) j

The graded Ringel formula on Grothendieck classes. The vertex coordinates are the idempotent graded dimensions, and the source coordinates are conjugated by q ↦ q⁻¹.

theorem TauCeti.PathAlgebra.gradedExtEuler_eq_sum_smulGradedDimension (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Fintype Q] [Module.Finite k (pathAlgebra k Q)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] (X Y : GradedModuleCat (integerGrade k Q)) [Module.Finite k X.carrier] [Module.Finite k Y.carrier] (h : IsGradedEulerAdmissible k (GradedModuleCat.shift (integerGrade k Q)) X Y) : gradedExtEuler k (GradedModuleCat.shift (integerGrade k Q)) h = ∑ i : Q, LaurentPolynomial.invert (GradedModuleCat.smulGradedDimension (vertexIdempotent k i) X) * GradedModuleCat.smulGradedDimension (vertexIdempotent k i) Y - LaurentPolynomial.T (-1) * ∑ i : Q, ∑ j : Q, ↑(Nat.card (i ⟶ j)) * LaurentPolynomial.invert (GradedModuleCat.smulGradedDimension (vertexIdempotent k i) X) * GradedModuleCat.smulGradedDimension (vertexIdempotent k j) Y

The graded Ringel formula for finite-dimensional graded modules. The coordinate at vertex i is the graded dimension of the image of its vertex idempotent. The formula holds for any admissibility witness, without choosing a composition series or support bounds.