Graded Euler admissibility of quiver vertex simples

For a finite quiver with finitely many arrows, the first-arrow resolution of a vertex simple has finitely generated projective terms. Against a finite graded module, their shifted Hom spaces have finite Laurent support. The resolution therefore makes the vertex simple Euler-admissible.

Over a finite-dimensional path algebra, the same resolutions show that every finite graded module has projective dimension at most one in the graded category, so its graded Ext groups vanish from cohomological degree two on.

This is the finiteness step needed before computing the graded Ringel form from the first-arrow resolution. The resolution follows Assem--Simson--Skowroński, Elements of the Representation Theory of Associative Algebras I, Chapter III, Sections 2--3; the q-Euler convention follows Dancso--Licata, Koszul algebras and flow lattices, Section 2.2.

theorem TauCeti.PathAlgebra.isGradedEulerAdmissible_gradedArrowSum (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] (i : Q) (Y : GradedModuleCat (integerGrade k Q)) [Module.Finite k Y.carrier] : IsGradedEulerAdmissible k (GradedModuleCat.shift (integerGrade k Q)) (gradedArrowSum k Q i) Y

The shifted projective sum in the first-arrow resolution is Euler-admissible against every finite-dimensional graded target.

theorem TauCeti.PathAlgebra.isGradedEulerAdmissible_gradedVertexProjective (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] (i : Q) (Y : GradedModuleCat (integerGrade k Q)) [Module.Finite k Y.carrier] : IsGradedEulerAdmissible k (GradedModuleCat.shift (integerGrade k Q)) (gradedVertexProjective k Q i) Y

A graded vertex projective is Euler-admissible against every finite-dimensional graded target, even when the path algebra itself is infinite-dimensional.

theorem TauCeti.PathAlgebra.isGradedEulerAdmissible_gradedVertexSimple (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [∀ (a b : Q), Finite (a ⟶ b)] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] (i : Q) (Y : GradedModuleCat (integerGrade k Q)) [Module.Finite k Y.carrier] : IsGradedEulerAdmissible k (GradedModuleCat.shift (integerGrade k Q)) (gradedVertexSimple k Q i) Y

A graded vertex simple of a finite quiver is Euler-admissible against every finite-dimensional graded target. The first-arrow resolution bounds its cohomological Ext support, while finite generation of the projectives bounds the internal support.

theorem TauCeti.PathAlgebra.isGradedExtBoundedBy_two_of_finite_source (k : Type w) (Q : Type u) [Field k] [Quiver Q] [Finite Q] [CategoryTheory.HasExt (GradedModuleCat (integerGrade k Q))] [FiniteDimensional k (pathAlgebra k Q)] (X Y : GradedModuleCat (integerGrade k Q)) [Module.Finite k X.carrier] : IsGradedExtBoundedBy (GradedModuleCat.shift (integerGrade k Q)) X Y 2

A finite graded module over a finite-dimensional path algebra has projective dimension at most one in the graded category. Equivalently, its graded Ext groups into any target vanish from cohomological degree two on, uniformly in the internal degree.