Simple quotients of finite graded modules

A nonzero graded module finite-dimensional over its scalar field admits a graded surjection onto a simple object. No finite-dimensionality or positivity assumption on the algebra is needed. These quotients detect nonzero finite graded modules, in particular the degree quotients of terms of minimal resolutions.

References

• TauCeti.span_range_laurentK0_of_eq_top, for the graded simple-class spanning argument.
• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3.

theorem TauCeti.GradedModuleCat.exists_mono_cokernel_finrank_lt {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] (hM : ¬CategoryTheory.Limits.IsZero M) (hs : ¬CategoryTheory.Simple M) : ∃ (Y : GradedModuleCat 𝒜) (i : Y ⟶ M), CategoryTheory.Mono i ∧ Module.Finite k Y.carrier ∧ Module.Finite k (cokernelObj i).carrier ∧ ¬CategoryTheory.Limits.IsZero (cokernelObj i) ∧ Module.finrank k Y.carrier < Module.finrank k M.carrier ∧ Module.finrank k (cokernelObj i).carrier < Module.finrank k M.carrier

A nonzero finite-dimensional graded module which is not simple has a proper subobject and a nonzero cokernel, both finite-dimensional and of strictly smaller dimension.

theorem TauCeti.GradedModuleCat.finite_induction {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (X : GradedModuleCat 𝒜) [Module.Finite k X.carrier] (P : CategoryTheory.ObjectProperty (GradedModuleCat 𝒜)) (hzero : ∀ (M : GradedModuleCat 𝒜), CategoryTheory.Limits.IsZero M → P M) (hsimple : ∀ (M : GradedModuleCat 𝒜), Module.Finite k M.carrier → CategoryTheory.Simple M → P M) (hext : ∀ {S : CategoryTheory.ShortComplex (GradedModuleCat 𝒜)} [Module.Finite k S.X₁.carrier] [Module.Finite k S.X₃.carrier], S.ShortExact → P S.X₁ → P S.X₃ → P S.X₂) : P X

An extension-closed property holding on zero objects and finite-dimensional simple objects holds on every finite-dimensional graded module. Only extensions with finite-dimensional ends are needed.

theorem TauCeti.GradedModuleCat.exists_simple_quotient {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] (hM : ¬CategoryTheory.Limits.IsZero M) : ∃ (N : GradedModuleCat 𝒜) (f : M ⟶ N), Module.Finite k N.carrier ∧ CategoryTheory.Simple N ∧ CategoryTheory.Epi f

Every nonzero finite-dimensional graded module has a simple graded quotient. The quotient is finite-dimensional over the same field and lies in the same universe as the source.