Ext-Euler admissibility from simple modules

Euler-admissibility is closed under extensions in either variable, so it propagates along a composition series: a module Y which is Euler-admissible against every simple module is Euler-admissible against every module of finite length. Over an Artinian ring every finitely generated module has finite length, and the criterion becomes a hypothesis on simple first arguments only. This is how admissibility of all pairs of finitely generated modules is obtained for algebras whose simple modules are known, for example path algebras of finite acyclic quivers, when no finite projective resolution is at hand.

Main results

• TauCeti.isEulerAdmissible_of_isFiniteLength: admissibility against every simple module gives admissibility against every module of finite length.
• TauCeti.isEulerAdmissibleOn_isFG_of_forall_isSimpleModule: over an Artinian ring, every pair of finitely generated modules is Euler-admissible as soon as every pair with a simple first argument is.

theorem TauCeti.isEulerAdmissible_of_isFiniteLength (k : Type u_1) [Field k] {R : Type u} [Ring R] [Algebra k R] (Y : ModuleCat R) (h : ∀ (S : ModuleCat R), IsSimpleModule R ↑S → IsEulerAdmissible k S Y) (X : ModuleCat R) (hX : IsFiniteLength R ↑X) : IsEulerAdmissible k X Y

Euler-admissibility descends along composition series. If Y is Euler-admissible against every simple module, it is Euler-admissible against every module of finite length.

theorem TauCeti.isEulerAdmissibleOn_isFG_of_forall_isSimpleModule (k : Type u_1) [Field k] {R : Type u} [Ring R] [Algebra k R] [IsArtinianRing R] (h : ∀ (S Y : ModuleCat R), IsSimpleModule R ↑S → Module.Finite R ↑Y → IsEulerAdmissible k S Y) : IsEulerAdmissibleOn k (ModuleCat.isFG R) (ModuleCat.isFG R)

Euler-admissibility of finitely generated modules is tested on simple first arguments. Over an Artinian ring, if every simple module is Euler-admissible against every finitely generated module, then every pair of finitely generated modules is Euler-admissible.