Projective dimension bounds along composition series

A common bound on the projective dimensions of simple modules also bounds every module of finite length. This lets short resolutions of simple modules control higher Ext groups of arbitrary finite-length modules, without choosing resolutions of their successive extensions.

For a module of projective dimension at most one, the standard free presentation has projective kernel and hence is a projective resolution of length one.

theorem ModuleCat.hasProjectiveDimensionLT_of_isFiniteLength {R : Type u} [Ring R] (X : ModuleCat R) (n : ℕ) (h : ∀ (S : ModuleCat R), IsSimpleModule R ↑S → CategoryTheory.HasProjectiveDimensionLT S n) (hX : IsFiniteLength R ↑X) : CategoryTheory.HasProjectiveDimensionLT X n

A bound on the projective dimension of every simple module bounds every module of finite length. Neither Artinianity of the ring nor finite generation of the ring over a field is needed.

theorem TauCeti.projective_projectiveShortComplex_X₁ {R : Type u} [Ring R] [Small.{v, u} R] {M : ModuleCat R} (hM : CategoryTheory.HasProjectiveDimensionLT M 2) : CategoryTheory.Projective M.projectiveShortComplex.X₁

The standard free presentation of a module of projective dimension at most one has projective kernel, so it is a projective resolution of length one.