Graded module resolutions supply q-Euler admissibility

Over a finite-dimensional graded algebra, a finite resolution by finitely generated graded projectives supplies both finiteness conditions needed for the q-Euler characteristic against any finite graded module. The graded Hom spaces of the resolving terms are finite-dimensional and have finite Laurent support, and the resolution gives a cohomological vanishing bound uniform in the target's internal shift.

Thus the subcategory of modules admitting finite graded-projective resolutions pairs with all finite graded modules. If every finite graded module admits such a resolution, the module/module q-Euler form can be constructed using this admissibility witness. No uniform bound on all resolution lengths, splitness hypothesis, or positivity of the algebra grading is required.

Main results

• TauCeti.isGradedEulerAdmissible_of_admitsFiniteProjectiveResolution: admissibility for one resolved source and one finite target.
• TauCeti.isGradedEulerAdmissibleOn_admitsFiniteProjectiveResolution_gradedFiniteModules: admissibility on the finite-resolution subcategory against all finite graded modules.
• TauCeti.isGradedEulerAdmissibleOn_gradedFiniteModules: admissibility on all finite graded modules under the finite graded-projective resolution hypothesis.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Sections 2.4--2.7.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.

The graded Hom support input is TauCeti.GradedModuleCat.hasFiniteLaurentSupport_hom_shiftObj; the resolution criterion is TauCeti.ExactStructure.FiniteResolution.isGradedEulerAdmissible.

theorem TauCeti.isGradedEulerAdmissible_of_admitsFiniteProjectiveResolution {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {X Y : GradedModuleCat 𝒜} [Module.Finite k Y.carrier] (hX : (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜) X) : IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) X Y

A finite resolution by finitely generated graded projectives makes the source graded Euler-admissible against every finite-dimensional graded target. The algebra itself need not be finite-dimensional.

theorem TauCeti.isGradedEulerAdmissibleOn_admitsFiniteProjectiveResolution_gradedFiniteModules {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [Module.Finite k A] : IsGradedEulerAdmissibleOn ((gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) (gradedFiniteModules 𝒜)

Modules admitting finite resolutions by finite graded projectives pair with all finite graded modules under the q-Euler characteristic. The cohomological bound may depend on the source, but is uniform in the internal degree.

theorem TauCeti.isGradedEulerAdmissibleOn_gradedFiniteModules {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] [Module.Finite k A] (h : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)) : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜)

If every finite graded module over a finite-dimensional graded algebra has a finite resolution by finite graded projectives, every pair of finite graded modules is graded Euler-admissible. In particular this supplies the finiteness witness for the module/module q-Euler form, without assuming Euler-admissibility separately.