Finite-term bounded-above projective replacements

Mathlib constructs strictly bounded-below injective replacements. Opposing a cochain complex and negating its integer degrees gives a strictly bounded-above projective replacement in FGModuleCat R, where finite-free epimorphisms supply enough projectives. The ModuleCat version below transfers the resulting complex and quasi-isomorphism through the finite-module inclusion. No finite lower bound or derived-arrow comparison is asserted.

theorem FGModuleCat.exists_boundedAbove_projective_replacement {R : Type u} [CommRing R] [IsNoetherianRing R] (K : CochainComplex (FGModuleCat R) ℤ) (b : ℤ) [K.IsStrictlyLE b] : ∃ (P : CochainComplex (FGModuleCat R) ℤ) (p : P ⟶ K), P.IsStrictlyLE b ∧ (∀ (i : ℤ), CategoryTheory.Projective (P.X i)) ∧ QuasiIso p

A strictly bounded-above complex of finite modules over a noetherian commutative ring has a strictly bounded-above quasi-isomorphic complex of projective finite modules. Its negative-degree tail may be infinite.

theorem ModuleCat.exists_finite_projective_replacement {R : Type u} [CommRing R] [IsNoetherianRing R] (K : CochainComplex (ModuleCat R) ℤ) (b : ℤ) [K.IsStrictlyLE b] (hfinite : ∀ (i : ℤ), Module.Finite R ↑(K.X i)) : ∃ (P : CochainComplex (ModuleCat R) ℤ) (p : P ⟶ K), P.IsStrictlyLE b ∧ (∀ (i : ℤ), Module.Finite R ↑(P.X i)) ∧ (∀ (i : ℤ), CategoryTheory.Projective (P.X i)) ∧ QuasiIso p

A strictly bounded-above complex of finite modules over a noetherian commutative ring has a strictly bounded-above, termwise finite-projective replacement in ModuleCat. The quasi-isomorphism is an actual complex map to the supplied complex. No strict lower bound is claimed for the replacement.