Finite projective dimension and the graded Cartan map

A finitely generated graded module over a left Noetherian graded algebra has a finite resolution by finitely generated graded projectives whenever its underlying module has finite projective dimension. The resolution has length at most the underlying projective-dimension bound. Finite graded free surjections retain the internal grading at every step; Noetherianity keeps the syzygies finitely generated, and ungraded dimension shifting makes the last syzygy projective.

Thus a pointwise finite projective-dimension hypothesis on the underlying modules suffices for the graded Cartan isomorphism over ℤ[q,q⁻¹]. No uniform bound, nonnegative grading, or semisimplicity of the degree-zero algebra is required.

References

• C. Năstăsescu and F. Van Oystaeyen, Methods of Graded Rings, Section 2.3, for graded free presentations and graded projectives.
• Charles A. Weibel, The K-book, Chapter II, Section 7, for the resolution theorem.
• Charles A. Weibel, An Introduction to Homological Algebra, Section 4.1, for dimension shifting.

The induction refines Mathlib's CategoryTheory.ObjectProperty.hasFiniteResolutionOfLength.iff_hasProjectiveDimensionLE by using TauCeti.GradedModuleCat.exists_finite_free_surjection and retaining finite generation and internal degrees. Dimension shifting uses CategoryTheory.ShortComplex.ShortExact.hasProjectiveDimensionLT_X₃_iff on the underlying short exact sequence.

theorem TauCeti.exists_gradedFiniteProjectiveResolution_of_hasProjectiveDimensionLE {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsNoetherianRing A] {M : GradedModuleCat 𝒜} [Module.Finite A M.carrier] {n : ℕ} (hM : CategoryTheory.HasProjectiveDimensionLE (GradedModuleCat.toModuleCat.obj M) n) : ∃ (r : (gradedModuleCanonicalExactStructure 𝒜).FiniteResolution (gradedFiniteProjectiveModules 𝒜) M), r.length ≤ n

A projective-dimension bound on the underlying module is realized by a finite resolution with finitely generated graded-projective terms and the same length bound.

theorem TauCeti.gradedFiniteModules_le_admitsFiniteResolution_of_finite_projectiveDimension {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsNoetherianRing A] (h : ∀ (M : GradedModuleCat 𝒜), Module.Finite A M.carrier → ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (GradedModuleCat.toModuleCat.obj M) n) : gradedFiniteModules 𝒜 ≤ (gradedModuleCanonicalExactStructure 𝒜).admitsFiniteResolution (gradedFiniteProjectiveModules 𝒜)

Pointwise finite projective dimension of the underlying finite graded modules supplies the finite graded-resolution hypothesis of the graded Cartan comparison theorem.

theorem TauCeti.gradedCartanMap_bijective_of_finite_projectiveDimension {k : Type uk} [CommRing k] {A : Type uA} [Ring A] [Algebra k A] {𝒜 : ℤ → Submodule k A} [GradedAlgebra 𝒜] [IsNoetherianRing A] (h : ∀ (M : GradedModuleCat 𝒜), Module.Finite A M.carrier → ∃ (n : ℕ), CategoryTheory.HasProjectiveDimensionLE (GradedModuleCat.toModuleCat.obj M) n) : Function.Bijective ⇑(gradedCartanMap 𝒜)

The graded Cartan map is bijective when the underlying finite graded modules have finite projective dimension over the left Noetherian algebra. Finite ungraded global dimension suffices; no separate bound on graded projective dimension is assumed.