Injective module sheaves on a scheme are flasque #
SheafOfModules.isFlasque_toSheaf_of_injective transported across the wrapper X.Modules,
whose category instance is a copy of that of SheafOfModules X.ringCatSheaf, so that
Injective must be carried across by hand. The consequence for cohomology is that an
injective 𝒪_X-module is acyclic for Sheaf.H, by TopCat.Sheaf.subsingleton_H_of_isFlasque.
theorem
AlgebraicGeometry.Scheme.Modules.injective_sheafOfModules_of_injective
{X : Scheme}
(I : X.Modules)
[hI : CategoryTheory.Injective I]
:
CategoryTheory.Injective
(have this := I;
this)
Injective for the wrapper X.Modules is Injective for SheafOfModules: the
category structures agree on the nose.
theorem
AlgebraicGeometry.Scheme.Modules.isFlasque_toSheaf_of_injective
{X : Scheme}
(I : X.Modules)
[CategoryTheory.Injective I]
:
TopCat.Sheaf.IsFlasque ((toSheaf X).obj I)
Injective module sheaves on a scheme are flasque.