Graded Euler-admissibility from simple modules

For a fixed target, graded Euler-admissibility of finite-dimensional sources can be tested on simple graded modules, and dually for a fixed source it can be tested on simple targets. Both internal finiteness and eventual cohomological vanishing propagate through graded composition series. The algebra need not itself be finite-dimensional for these two criteria.

Together with the shift-admissibility results in TauCeti.Algebra.Homology.EulerCharacteristic.ExtEuler.Graded.Shift, they let an exhaustive family of simples up to shift supply the finiteness data for a q-Euler form: over a finite-dimensional graded algebra, every pair of finite graded modules is graded Euler-admissible exactly when every pair of members of the family is.

Main results

• TauCeti.isGradedEulerAdmissible_of_finite_of_forall_simple: admissibility against a fixed target can be tested on finite-dimensional simple sources.
• TauCeti.isGradedEulerAdmissible_of_finite_of_forall_simple_right: admissibility from a fixed source can be tested on finite-dimensional simple targets.
• TauCeti.isGradedEulerAdmissibleOn_gradedFiniteModules_iff: every pair of finite graded modules is graded Euler-admissible exactly when every pair drawn from an exhaustive family of graded simples is.

References

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

The composition-series inductions use GradedModuleCat.finite_induction; the extension steps use IsGradedEulerAdmissible.of_shortExact₂' and IsGradedEulerAdmissible.of_shortExact₂.

theorem TauCeti.isGradedEulerAdmissible_of_finite_of_forall_simple {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (e : GradedModuleCat 𝒜 ≌ GradedModuleCat 𝒜) (Y : GradedModuleCat 𝒜) (h : ∀ (S : GradedModuleCat 𝒜), Module.Finite k S.carrier → CategoryTheory.Simple S → IsGradedEulerAdmissible k e S Y) (X : GradedModuleCat 𝒜) [Module.Finite k X.carrier] : IsGradedEulerAdmissible k e X Y

Admissibility against every finite-dimensional simple source implies admissibility against all finite-dimensional graded sources, for any chosen internal-shift autoequivalence.

theorem TauCeti.isGradedEulerAdmissible_of_finite_of_forall_simple_right {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (e : GradedModuleCat 𝒜 ≌ GradedModuleCat 𝒜) (X : GradedModuleCat 𝒜) (h : ∀ (T : GradedModuleCat 𝒜), Module.Finite k T.carrier → CategoryTheory.Simple T → IsGradedEulerAdmissible k e X T) (Y : GradedModuleCat 𝒜) [Module.Finite k Y.carrier] : IsGradedEulerAdmissible k e X Y

Admissibility from a fixed source against every finite-dimensional simple target implies admissibility against all finite-dimensional graded targets, for any chosen internal-shift autoequivalence. This is the target counterpart of TauCeti.isGradedEulerAdmissible_of_finite_of_forall_simple.

Exhaustive families of graded simples

theorem TauCeti.isGradedEulerAdmissibleOn_gradedFiniteModules_iff {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} {I : Type u_1} [Module.Finite k A] [CategoryTheory.HasExt (GradedModuleCat 𝒜)] {S : I → (gradedFiniteModules 𝒜).FullSubcategory} (hS : IsExhaustiveGradedSimpleFamily S) : IsGradedEulerAdmissibleOn (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜) ↔ ∀ (i j : I), IsGradedEulerAdmissible k (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj

Graded Euler-admissibility of finite graded modules is decided on simples. Over a finite-dimensional graded algebra, let S be an exhaustive family of graded simples up to internal shift. Every pair of finite graded modules is graded Euler-admissible exactly when every pair (S i, S j) is.