Flasque sheaves: acyclicity, and injective sheaves of modules

Flasque abelian sheaves are acyclic

For a flasque sheaf of abelian groups F on a topological space, Sheaf.H F n vanishes for every n ≥ 1. This is Hartshorne III.2.5, proved by dimension shifting: embed F in an injective sheaf I, which is flasque by Sheaf.isFlasque_of_injective; the quotient Q is flasque by IsFlasque.of_shortExact_of_isFlasque₁₂; global sections of I surject onto those of Q by IsFlasque.epi_of_shortExact, which kills H¹ F (Sheaf.H_one_subsingleton_of_sections_epi); and H^(n+2) F vanishes once H^(n+1) Q does (Sheaf.H_succ_subsingleton_of_shortExact), so the induction closes.

Nothing here is Čech-theoretic; compare Sites/SheafCohomology/Cech/Comparison.lean, which obtains vanishing from Čech exactness instead.

Injective sheaves of modules are flasque

For a sheaf of rings R on a space, an injective sheaf of R-modules I has flasque underlying abelian sheaf. The proof is the one for abelian sheaves (Sheaf.isFlasque_of_injective) with the free abelian sheaf on an open replaced by the free sheaf of modules on an open, SheafOfModules.freeYonedaSheaf: a section over V is a map freeYonedaSheaf R V ⟶ I, an inclusion V ⊆ U induces a monomorphism freeYonedaSheaf R V ⟶ freeYonedaSheaf R U, and injectivity of I extends the map. Together with the first half this makes I acyclic for Sheaf.H, which is the acyclicity input of extComparisonAddEquiv for the forgetful functor from module sheaves to abelian sheaves.

Main results

• TopCat.Sheaf.subsingleton_H_of_isFlasque.
• SheafOfModules.freeYonedaSheafHomEquiv, SheafOfModules.freeYonedaSheafHomEquiv_comp, SheafOfModules.freeYonedaSheafMap_mono.
• SheafOfModules.isFlasque_toSheaf_of_injective.

theorem TopCat.Sheaf.subsingleton_H_of_isFlasque {X : TopCat} [hExt : CategoryTheory.HasExt (Sheaf AddCommGrpCat X)] (F : Sheaf AddCommGrpCat X) [F.IsFlasque] (n : ℕ) : Subsingleton (CategoryTheory.Sheaf.derivedH hExt F (n + 1))

Flasque sheaves are acyclic. For a flasque sheaf of abelian groups F on a topological space, Sheaf.H F (n + 1) is trivial for every n.

noncomputable def SheafOfModules.freeYonedaSheafHomEquiv {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat) (U : TopologicalSpace.Opens ↑X) (M : SheafOfModules R) : (freeYonedaSheaf R U ⟶ M) ≃ ↑(M.val.obj (Opposite.op U))

Sections of a sheaf of modules over an open U are the maps out of the free sheaf of modules on U: the sheafification adjunction followed by PresheafOfModules.freeYonedaEquiv.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def SheafOfModules.freeYonedaSheafMap {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat) {V U : TopologicalSpace.Opens ↑X} (i : V ⟶ U) : freeYonedaSheaf R V ⟶ freeYonedaSheaf R U

The map of free sheaves of modules induced by an inclusion of opens.

Equations

• SheafOfModules.freeYonedaSheafMap R i = (PresheafOfModules.sheafification (CategoryTheory.CategoryStruct.id R.obj)).map ((PresheafOfModules.free R.obj).map (CategoryTheory.yoneda.map i))

theorem SheafOfModules.freeYonedaEquiv_free_map_yoneda_map_comp {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat) {V U : TopologicalSpace.Opens ↑X} (i : V ⟶ U) (N : PresheafOfModules R.obj) (f : (PresheafOfModules.free R.obj).obj (CategoryTheory.yoneda.obj U) ⟶ N) : PresheafOfModules.freeYonedaEquiv (CategoryTheory.CategoryStruct.comp ((PresheafOfModules.free R.obj).map (CategoryTheory.yoneda.map i)) f) = (CategoryTheory.ConcreteCategory.hom (N.map i.op)) (PresheafOfModules.freeYonedaEquiv f)

Precomposition with the free presheaf map induced by i is restriction of sections along i, for presheaves of modules.

theorem SheafOfModules.freeYonedaSheafHomEquiv_comp {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat) {V U : TopologicalSpace.Opens ↑X} (i : V ⟶ U) (M : SheafOfModules R) (e : freeYonedaSheaf R U ⟶ M) : (freeYonedaSheafHomEquiv R V M) (CategoryTheory.CategoryStruct.comp (freeYonedaSheafMap R i) e) = (CategoryTheory.ConcreteCategory.hom (M.val.map i.op)) ((freeYonedaSheafHomEquiv R U M) e)

Precomposition with freeYonedaSheafMap R i is restriction of sections along i.

instance SheafOfModules.freeYonedaSheafMap_mono {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat) {V U : TopologicalSpace.Opens ↑X} (i : V ⟶ U) : CategoryTheory.Mono (freeYonedaSheafMap R i)

The map of free sheaves of modules induced by an inclusion of opens is a monomorphism: on presheaves it is objectwise the free module map on an injection of (subsingleton) hom types, and sheafification preserves monomorphisms.

theorem SheafOfModules.isFlasque_toSheaf_of_injective {X : TopCat} (R : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) RingCat) (I : SheafOfModules R) [CategoryTheory.Injective I] : TopCat.Sheaf.IsFlasque ((toSheaf R).obj I)

Injective sheaves of modules are flasque.