Uniform graded Ext bounds from simple modules

A cohomological bound on graded Ext can be uniform both in internal degree and in the pair of objects. For finite modules it suffices to test such a bound on simple modules. For an exhaustive family of graded simples up to shift, it suffices to test the chosen representatives: arbitrary internal shifts do not change a cohomological bound.

In particular, pointwise graded Euler-admissibility on a finite exhaustive family gives one cohomological bound for all finite graded modules. Finiteness of internal support remains a separate condition; it is not asserted by the uniform-bound predicate.

References

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

theorem TauCeti.isGradedExtBoundedBy_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 𝒜) (N : ℕ) (h : ∀ (S : GradedModuleCat 𝒜), Module.Finite k S.carrier → CategoryTheory.Simple S → IsGradedExtBoundedBy e S Y N) (X : GradedModuleCat 𝒜) [Module.Finite k X.carrier] : IsGradedExtBoundedBy e X Y N

A fixed bound against all finite-dimensional simple graded sources bounds every finite-dimensional graded source, without increasing the bound.

theorem TauCeti.isGradedExtBoundedBy_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 𝒜) (N : ℕ) (h : ∀ (T : GradedModuleCat 𝒜), Module.Finite k T.carrier → CategoryTheory.Simple T → IsGradedExtBoundedBy e X T N) (Y : GradedModuleCat 𝒜) [Module.Finite k Y.carrier] : IsGradedExtBoundedBy e X Y N

A fixed bound against all finite-dimensional simple graded targets bounds every finite-dimensional graded target, without increasing the bound.

theorem TauCeti.isGradedExtBoundedOn_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) (N : ℕ) : IsGradedExtBoundedOn (GradedModuleCat.shift 𝒜) (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜) N ↔ ∀ (i j : I), IsGradedExtBoundedBy (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj N

A uniform cohomological bound on finite graded modules is detected on any exhaustive family of graded simples up to shift, with the very same bound.

theorem TauCeti.exists_isGradedExtBoundedOn_of_forall_simple {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 𝒜)] [Finite I] {S : I → (gradedFiniteModules 𝒜).FullSubcategory} (hS : IsExhaustiveGradedSimpleFamily S) (h : ∀ (i j : I), IsGradedExtBounded (GradedModuleCat.shift 𝒜) (S i).obj (S j).obj) : ∃ (N : ℕ), IsGradedExtBoundedOn (GradedModuleCat.shift 𝒜) (gradedFiniteModules 𝒜) (gradedFiniteModules 𝒜) N

Pointwise eventual graded Ext-vanishing on a finite exhaustive family of simples supplies one cohomological bound for every pair of finite graded modules and every internal degree.