Flasque sheaf theory and cohomological vanishing

A sheaf of abelian groups is flasque when every restriction map is epi. Such sheaves have vanishing higher cohomology, which is one of the key inputs to Grothendieck vanishing.

Main definitions

• IsFlasqueSheaf — the flasque predicate.

Main results

• epi_app_of_shortExact_flasque, isFlasque_X₃_of_shortExact — flasqueness propagates through short exact sequences.
• isFlasque_of_injective — every injective sheaf is flasque.
• sheafH_subsingleton_H1_of_flasque, sheafH_subsingleton_of_flasque — flasque sheaves have vanishing Hⁿ for n ≥ 1.

The four sub-lemmas inside the epi_app_of_shortExact_of_epi_restrictions block are adapted from Brian Nugent's Mathlib PR #35790.

Generic Sheaf.H and Ext API lives in CohomologyAPI.lean.

Flasque sheaf sub-lemmas

The four sub-lemmas below are adapted from Brian Nugent's Mathlib PR #35790. Together they imply FlasqueVanishing. Each is a self-contained statement that can be attacked independently.

@[reducible, inline]

abbrev IsFlasqueSheaf {X : TopCat} (F : TopCat.Sheaf AddCommGrpCat X) : Prop

A sheaf of abelian groups is flasque if all restriction maps are epi. This is equivalent to surjectivity of restriction on sections.

Equations

• IsFlasqueSheaf F = ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V), CategoryTheory.Epi (F.obj.map i.op)

theorem sections_exact_of_shortExact {X : TopCat} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) (V : TopologicalSpace.Opens ↑X) (x : ↑(S.X₂.obj.obj (Opposite.op V))) (hx : (CategoryTheory.ConcreteCategory.hom (S.g.hom.app (Opposite.op V))) x = 0) : ∃ (a : ↑(S.X₁.obj.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (S.f.hom.app (Opposite.op V))) a = x

For a short exact sequence of sheaves, the sequence of sections at any open V is exact: if g_V x = 0, then x lies in the image of f_V.

Structured-arrow Zorn setup for partial lifts

theorem epi_app_of_shortExact_of_epi_restrictions {X : TopCat} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) (hX₁_epi : ∀ {U V : TopologicalSpace.Opens ↑X} (i : U ⟶ V), CategoryTheory.Epi (S.X₁.obj.map i.op)) (U : TopologicalSpace.Opens ↑X) : CategoryTheory.Epi (S.g.hom.app (Opposite.op U))

If 0 → X₁ → X₂ → X₃ → 0 is short exact and every restriction map of the underlying presheaf S.X₁.obj is epi, then g(U) : X₂(U) → X₃(U) is epi.

theorem epi_app_of_shortExact_flasque {X : TopCat} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) (hX₁ : IsFlasqueSheaf S.X₁) (U : TopologicalSpace.Opens ↑X) : CategoryTheory.Epi (S.g.hom.app (Opposite.op U))

If 0 → X₁ → X₂ → X₃ → 0 is short exact and X₁ is flasque, then g(U) : X₂(U) → X₃(U) is epi.

theorem isFlasque_X₃_of_shortExact {X : TopCat} {S : CategoryTheory.ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) (hX₁ : IsFlasqueSheaf S.X₁) (hX₂ : IsFlasqueSheaf S.X₂) : IsFlasqueSheaf S.X₃

Quotients of flasque sheaves are flasque along a short exact sequence.

theorem isFlasque_of_injective {X : TopCat} (I : TopCat.Sheaf AddCommGrpCat X) [CategoryTheory.Injective I] : IsFlasqueSheaf I

Injective sheaves are flasque.

Cohomological vanishing for flasque sheaves

theorem sheafH_subsingleton_H1_of_flasque {X : TopCat} (F : TopCat.Sheaf AddCommGrpCat X) (hF : IsFlasqueSheaf F) : Subsingleton (CategoryTheory.Sheaf.H F 1)

H¹ vanishes for flasque sheaves.

theorem sheafH_subsingleton_of_flasque (X : TopCat) (F : TopCat.Sheaf AddCommGrpCat X) (hF : IsFlasqueSheaf F) (n : ℕ) : Subsingleton (CategoryTheory.Sheaf.H F (n + 1))

Flasque sheaves have vanishing higher cohomology.