Minimal graded projective surjections and resolutions

Let A be a nonnegatively graded algebra whose degree-zero part A₀ = 𝒜 0 is a semisimple ring, as for the path-length grading of a path algebra of a finite acyclic quiver, of a zigzag algebra, or of any Koszul algebra in the sense of Beilinson--Ginzburg--Soergel. Write A₊ for the sum of the pieces of A of positive degree.

A graded module M vanishing below some degree is the target of a minimal projective surjection: a degree-zero surjection P ⟶ M from a direct sum P of shifted projectives A f, with f idempotents of degree zero, whose kernel lies in A₊ P, minimal in the sense of TauCeti.GradedProjectiveResolution.IsMinimal. Its generators lift a decomposition of each homogeneous piece of M / A₊ M into simple A₀-modules. Over the semisimple ring A₀ every simple summand, generated by any nonzero element v, is isomorphic to A₀ f for an idempotent f fixing v (IsSemisimpleRing.exists_isIdempotentElem_smul_eq_zero_iff). Graded Nakayama makes the lifted generators generate, and because the degree-zero part of A f is A₀ f, the kernel lies in A₊ P.

Iterating along successive kernels gives a minimal graded projective resolution, with finite-dimensional terms when A and M are finite-dimensional. With the diagonal Ext criterion for minimal resolutions this gives the elementary characterisation of linearity: M has a linear graded projective resolution exactly when Extⁿ(M, N) vanishes for every graded module N concentrated in a single degree p ≠ n. In the finite-dimensional case it suffices to test finite-dimensional simple modules N; for M a graded simple this is the diagonal vanishing of the bigraded Ext between graded simples. Dropping the diagonal restriction, vanishing of Extⁿ(M, N) against all finite-dimensional simples from some degree on truncates the minimal resolution and so bounds the projective dimension of the underlying module of M.

Main results

• TauCeti.GradedModuleCat.exists_minimal_projective_surjection: minimal projective surjections onto bounded-below graded modules.
• TauCeti.GradedModuleCat.exists_minimal_projective_surjection_of_finite: finite-dimensional sources for finite-dimensional graded modules over a finite-dimensional algebra.
• TauCeti.GradedProjectiveResolution.exists_isMinimal: minimal graded projective resolutions of bounded-below graded modules.
• TauCeti.GradedProjectiveResolution.exists_isMinimal_of_finite: minimal resolutions with finite-dimensional terms.
• TauCeti.GradedProjectiveResolution.exists_isLinear_iff_subsingleton_ext: a bounded-below graded module has a linear resolution exactly when Ext against concentrated modules vanishes off the diagonal.
• TauCeti.GradedProjectiveResolution.exists_isLinear_iff_subsingleton_ext_simple: the same criterion for finite-dimensional modules, tested against simple modules.
• TauCeti.GradedProjectiveResolution.hasProjectiveDimensionLT_of_subsingleton_ext_simple: eventual vanishing of Ext against simple modules bounds the ungraded projective dimension.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded projective modules and graded Nakayama.
• I. Assem, D. Simson, A. Skowroński, Elements of the Representation Theory of Associative Algebras, Vol. 1, Section I.5, for projective covers built from idempotents.
• A. Beilinson, V. Ginzburg and W. Soergel, Koszul duality patterns in representation theory, Section 1.2, for minimal and linear resolutions over a positively graded ring with semisimple degree-zero part, and the diagonal Ext criterion.

theorem TauCeti.GradedModuleCat.exists_minimal_projective_surjection {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] (hneg : ∀ p < 0, 𝒜 p = ⊥) (M : GradedModuleCat 𝒜) (b : ℤ) (hb : ∀ p < b, M.grading.piece ℤ p = ⊥) : ∃ (P : GradedModuleCat 𝒜) (π : P ⟶ M), Module.Projective A P.carrier ∧ Function.Surjective ⇑π.hom ∧ (∀ (x : P.carrier), π.hom x = 0 → x ∈ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤) ∧ ∀ p < b, P.grading.piece ℤ p = ⊥

Minimal projective surjections. Let A be a nonnegatively graded algebra whose degree-zero part is a semisimple ring. Every graded module M vanishing below degree b is the image of a projective graded module P under a degree-zero surjection whose kernel lies in A₊ P. The source P also vanishes below degree b.

theorem TauCeti.GradedModuleCat.exists_minimal_projective_surjection_of_finite {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] (hneg : ∀ p < 0, 𝒜 p = ⊥) [Module.Finite k A] (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] : ∃ (P : GradedModuleCat 𝒜) (π : P ⟶ M), Module.Projective A P.carrier ∧ Function.Surjective ⇑π.hom ∧ (∀ (x : P.carrier), π.hom x = 0 → x ∈ (⨆ (i : ℤ), ⨆ (_ : 0 < i), 𝒜 i) • ⊤) ∧ Module.Finite k P.carrier

Minimal projective surjections onto finite-dimensional modules. Over a finite-dimensional algebra as in TauCeti.GradedModuleCat.exists_minimal_projective_surjection, a finite-dimensional graded module is the target of a minimal projective surjection from a finite-dimensional graded module.

theorem TauCeti.GradedProjectiveResolution.exists_isMinimal {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] (hneg : ∀ p < 0, 𝒜 p = ⊥) (M : GradedModuleCat 𝒜) (b : ℤ) (hb : ∀ p < b, M.grading.piece ℤ p = ⊥) : ∃ (r : GradedProjectiveResolution 𝒜 M.grading), r.IsMinimal ∧ ∀ (n : ℕ), ∀ p < b, (r.grading n).piece ℤ p = ⊥

Minimal graded projective resolutions exist. Let A be a nonnegatively graded algebra whose degree-zero part is a semisimple ring. Every graded module vanishing below degree b has a minimal graded projective resolution all of whose terms vanish below degree b.

theorem TauCeti.GradedProjectiveResolution.exists_isLinear_iff_subsingleton_ext {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] (hneg : ∀ p < 0, 𝒜 p = ⊥) [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (M : GradedModuleCat 𝒜) (b : ℤ) (hb : ∀ p < b, M.grading.piece ℤ p = ⊥) : (∃ (r : GradedProjectiveResolution 𝒜 M.grading), r.IsLinear) ↔ ∀ (n : ℕ) (p : ℤ), ↑n ≠ p → ∀ (N : GradedModuleCat 𝒜), (∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) → Subsingleton (CategoryTheory.Abelian.Ext M N n)

Diagonal Ext detects the existence of a linear resolution. Over an algebra as in TauCeti.GradedProjectiveResolution.exists_isMinimal, a bounded-below graded module has a linear graded projective resolution exactly when Extⁿ(M, N) vanishes for every graded module N concentrated in a single degree p ≠ n.

theorem TauCeti.GradedProjectiveResolution.exists_isMinimal_of_finite {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] (hneg : ∀ p < 0, 𝒜 p = ⊥) (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] : ∃ (r : GradedProjectiveResolution 𝒜 M.grading), r.IsMinimal ∧ ∀ (n : ℕ), Module.Finite k (r.X n)

Finite-dimensional minimal graded projective resolutions exist over a finite-dimensional algebra as in TauCeti.GradedProjectiveResolution.exists_isMinimal: a finite-dimensional graded module has a minimal graded projective resolution with finite-dimensional terms.

theorem TauCeti.GradedProjectiveResolution.exists_isLinear_iff_subsingleton_ext_simple {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] (hneg : ∀ p < 0, 𝒜 p = ⊥) [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] : (∃ (r : GradedProjectiveResolution 𝒜 M.grading), r.IsLinear) ↔ ∀ (n : ℕ) (p : ℤ), ↑n ≠ p → ∀ (N : GradedModuleCat 𝒜), Module.Finite k N.carrier → CategoryTheory.Simple N → (∀ (q : ℤ), q ≠ p → N.grading.piece ℤ q = ⊥) → Subsingleton (CategoryTheory.Abelian.Ext M N n)

Diagonal Ext against simple modules detects the existence of a linear resolution. Over a finite-dimensional algebra as in TauCeti.GradedProjectiveResolution.exists_isMinimal, a finite-dimensional graded module M has a linear graded projective resolution exactly when Extⁿ(M, S) vanishes for every finite-dimensional simple graded module S concentrated in a degree p ≠ n.

theorem TauCeti.GradedProjectiveResolution.hasProjectiveDimensionLT_of_subsingleton_ext_simple {k : Type uk} [Field k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsSemisimpleRing ↥(𝒜 0)] [Module.Finite k A] (hneg : ∀ p < 0, 𝒜 p = ⊥) [CategoryTheory.HasExt (GradedModuleCat 𝒜)] (M : GradedModuleCat 𝒜) [Module.Finite k M.carrier] (d : ℕ) (hExt : ∀ (n : ℕ), d ≤ n → ∀ (N : GradedModuleCat 𝒜), Module.Finite k N.carrier → CategoryTheory.Simple N → Subsingleton (CategoryTheory.Abelian.Ext M N n)) : CategoryTheory.HasProjectiveDimensionLT (GradedModuleCat.toModuleCat.obj M) d

Ext against simple modules bounds the projective dimension. Over a finite-dimensional algebra as in TauCeti.GradedProjectiveResolution.exists_isMinimal, let M be a finite-dimensional graded module such that Extⁿ(M, N) vanishes for every n ≥ d and every finite-dimensional simple graded module N. Then the underlying A-module of M has projective dimension less than d.