Bounded minimal free chain resolutions

Over a Noetherian local ring (R, 𝔪), a finite module of projective dimension at most n has a projective resolution by finite free modules, zero above degree n, with every unaugmented differential landing in 𝔪 times its target. Such resolutions are used to compare Koszul complexes with resolutions of the residue field: reduction modulo 𝔪 kills all the resolution differentials.

This file identifies the recursive minimality condition on a finite resolution with the condition on the differentials of its spliced chain complex. It then converts the minimal finite projective resolution into Mathlib's CategoryTheory.ProjectiveResolution, retaining both minimality and the length bound.

References

• The Stacks Project, Lemma 10.102.2 (00MT), minimal finite free resolutions.
• Winfried Bruns and Jürgen Herzog, Cohen–Macaulay Rings, Section 1.3.

theorem TauCeti.ExactStructure.FiniteResolution.IsMinimal.range_d_le {R : Type u} [CommRing R] [IsLocalRing R] {E : ExactStructure (ModuleCat R)} {P : CategoryTheory.ObjectProperty (ModuleCat R)} {M : ModuleCat R} {r : E.FiniteResolution P M} (hr : r.IsMinimal) (n : ℕ) : (ModuleCat.Hom.hom (r.d n)).range ≤ IsLocalRing.maximalIdeal R • ⊤

Every differential of a minimal finite resolution lands in the maximal ideal times its target. The augmentation is not included.

theorem TauCeti.ExactStructure.FiniteResolution.isMinimal_iff_forall_range_d_le {R : Type u} [CommRing R] [IsLocalRing R] {E : ExactStructure (ModuleCat R)} {P : CategoryTheory.ObjectProperty (ModuleCat R)} {M : ModuleCat R} (r : E.FiniteResolution P M) : r.IsMinimal ↔ ∀ (n : ℕ), (ModuleCat.Hom.hom (r.d n)).range ≤ IsLocalRing.maximalIdeal R • ⊤

Recursive minimality is equivalent to the differential condition on the associated chain complex, for any exact structure on modules.

theorem TauCeti.ExactStructure.FiniteResolution.IsMinimal.isMinimal_toProjectiveResolution_complex {R : Type u} [CommRing R] [IsLocalRing R] {P : CategoryTheory.ObjectProperty (ModuleCat R)} {M : ModuleCat R} {r : (abelian (ModuleCat R)).FiniteResolution P M} (hr : r.IsMinimal) (hP : P ≤ CategoryTheory.isProjective (ModuleCat R)) : HomologicalComplex.IsMinimal (toProjectiveResolution hP r).complex

Converting a minimal finite resolution by projective modules to a projective resolution preserves minimality of its complex.

theorem ModuleCat.exists_projectiveResolution_finite_free_minimal {R : Type u} [CommRing R] [IsLocalRing R] [IsNoetherianRing R] (M : ModuleCat R) [Module.Finite R ↑M] {n : ℕ} (hM : CategoryTheory.HasProjectiveDimensionLE M n) : ∃ (F : CategoryTheory.ProjectiveResolution M), (∀ (i : ℕ), Module.Finite R ↑(F.complex.X i) ∧ Module.Free R ↑(F.complex.X i)) ∧ (∀ (i : ℕ), n < i → CategoryTheory.Limits.IsZero (F.complex.X i)) ∧ HomologicalComplex.IsMinimal F.complex

A finite module over a Noetherian local ring with projective dimension at most n has a minimal finite free projective resolution of length at most n: all terms are finite free, all terms above degree n vanish, and every differential lands in the maximal ideal times its target.