Bounded derived inclusion of finitely generated modules

Over a noetherian commutative ring, the canonical inclusion of finitely generated modules into all modules is exact. Finite free modules cover every finitely generated module and are projective on both sides of this inclusion. The acyclic-generators criterion therefore compares all Ext groups, and bounded dévissage makes the induced functor bijective on morphisms between bounded derived objects.

This is a full-faithfulness statement for the bounded source inside the unbounded derived category of all modules. It does not identify derived Hom after localization, make the unbounded inclusion fully faithful, or assert anything about coherent sheaves or relative geometry.

noncomputable def FGModuleCat.derivedInclusion {R : Type u} [CommRing R] [IsNoetherianRing R] : CategoryTheory.Functor (DerivedCategory (FGModuleCat R)) (DerivedCategory (ModuleCat R))

The exact derived functor of the canonical inclusion of finite modules into all modules. The exactness instances are supplied locally, so importing this leaf does not install alternative global category-theoretic instances.

Equations

• FGModuleCat.derivedInclusion = (ModuleCat.isFG R).ι.mapDerivedCategory

theorem FGModuleCat.boundedDerivedInclusion_map_bijective {R : Type u} [CommRing R] [IsNoetherianRing R] (E E' : DerivedCategory.Bounded (FGModuleCat R)) : Function.Bijective (DerivedCategory.Bounded.ι.comp derivedInclusion).map

On bounded derived objects of finitely generated modules, the inclusion into the derived category of all modules is bijective on each morphism set.