Ext-Euler admissibility from module resolutions

This file specializes the finite-projective-resolution criterion for Ext-Euler admissibility to finitely generated modules over a finite-dimensional algebra.

Main results

• TauCeti.isEulerAdmissibleOn_isFG: if every finitely generated module has a finite resolution by finitely generated projectives, every pair of finitely generated modules is Euler-admissible.

theorem TauCeti.isEulerAdmissibleOn_isFG (k : Type u_1) [Field k] {A : Type u} [Ring A] [Algebra k A] [FiniteDimensional k A] (h : ModuleCat.isFG A ≤ (ExactStructure.abelian (ModuleCat A)).admitsFiniteResolution (finiteProjectiveModules A)) : IsEulerAdmissibleOn k (ModuleCat.isFG A) (ModuleCat.isFG A)

If every finitely generated module over a finite-dimensional algebra has a finite resolution by finitely generated projectives, then every pair of finitely generated modules is Euler-admissible: the resolution bounds the Ext groups, and the Hom spaces from its terms are finite-dimensional.