Cohomology from Cech exactness on a compact basis

This file formalizes the non-circular basis argument of Stacks Project, Tag 01EW. A compact collection is required to admit finite subordinate refinements and to be stable under nonempty finite intersections. If a sheaf has exact positive Cech complexes on every finite cover inside the collection, then its positive local cohomology vanishes on every member. The whole-space case recovers positive derived global-cohomology vanishing.

The proof is by dimension shifting. After embedding the sheaf into an injective sheaf, local surjectivity and compactness produce a finite basis cover on which a section of the quotient lifts. Degree-one Cech exactness corrects those local lifts so that they glue. Consequently the quotient inherits the same basis-Cech exactness, and the Ext long exact sequence completes the induction. In particular, no cover is assumed to be derived-acyclic in advance.

structure CategoryTheory.Sheaf.CompactOpenBasis (X : TopCat) : Type u

A compact collection of opens suited to the Cech-to-derived comparison. The finite_refinement field says directly that every cover of a member admits a finite subordinate refinement by members. This formulation includes both a global compact-open basis and the distinguished-open basis lying below one fixed affine open. Stability under nonempty finite intersections keeps every term of a Cech nerve inside the collection.

• carrier : Set (TopologicalSpace.Opens ↑X)
• isCompact (U : TopologicalSpace.Opens ↑X) : U ∈ self.carrier → IsCompact ↑U
• finite_refinement {V : TopologicalSpace.Opens ↑X} : V ∈ self.carrier → ∀ {I : Type u} (U : I → TopologicalSpace.Opens ↑X), V ≤ ⨆ (i : I), U i → ∃ (J : Type u) (x : Fintype J) (W : J → TopologicalSpace.Opens ↑X) (a : J → I), (∀ (j : J), W j ∈ self.carrier) ∧ (∀ (j : J), W j ≤ U (a j)) ∧ V = ⨆ (j : J), W j
• inf_mem (U V : TopologicalSpace.Opens ↑X) : U ∈ self.carrier → V ∈ self.carrier → U ⊓ V ∈ self.carrier

noncomputable def CategoryTheory.Sheaf.CompactOpenBasis.ofIsBasis {X : TopCat} (carrier : Set (TopologicalSpace.Opens ↑X)) (isBasis : TopologicalSpace.Opens.IsBasis carrier) (isCompact : ∀ U ∈ carrier, IsCompact ↑U) (inf_mem : ∀ (U V : TopologicalSpace.Opens ↑X), U ∈ carrier → V ∈ carrier → U ⊓ V ∈ carrier) : CompactOpenBasis X

Construct a CompactOpenBasis from an ordinary topological basis of compact opens which is stable under nonempty finite intersections.

Equations

• CategoryTheory.Sheaf.CompactOpenBasis.ofIsBasis carrier isBasis isCompact inf_mem = { carrier := carrier, isCompact := isCompact, finite_refinement := ⋯, inf_mem := inf_mem }

theorem CategoryTheory.Sheaf.CompactOpenBasis.exists_finite_refinement {X : TopCat} (B : CompactOpenBasis X) {V : TopologicalSpace.Opens ↑X} (hV : V ∈ B.carrier) {I : Type u} (U : I → TopologicalSpace.Opens ↑X) (hVU : V ≤ ⨆ (i : I), U i) : ∃ (J : Type u) (x : Fintype J) (W : J → TopologicalSpace.Opens ↑X) (a : J → I), (∀ (j : J), W j ∈ B.carrier) ∧ (∀ (j : J), W j ≤ U (a j)) ∧ V = ⨆ (j : J), W j

Every compact basis open has a finite cover by basis opens subordinate to a given open cover.

theorem CategoryTheory.Sheaf.CompactOpenBasis.fin_pi_mem {X : TopCat} (B : CompactOpenBasis X) {n : ℕ} (U : Fin (n + 1) → TopologicalSpace.Opens ↑X) (hU : ∀ (i : Fin (n + 1)), U i ∈ B.carrier) : ∏ᶜ U ∈ B.carrier

A nonempty finite product of members of a compact basis is again a member.

def CategoryTheory.Sheaf.IsCechAcyclicOnCompactBasis {X : TopCat} (B : CompactOpenBasis X) (F : TopCat.Sheaf AddCommGrpCat X) : Prop

Positive Cech exactness on all finite covers by members of a compact basis.

Equations

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

theorem CategoryTheory.Sheaf.isCechAcyclicOnCompactBasis_of_injective {X : TopCat} (B : CompactOpenBasis X) (F : TopCat.Sheaf AddCommGrpCat X) [Injective F] : IsCechAcyclicOnCompactBasis B F

Injective sheaves are Cech-acyclic on every compact basis.

theorem CategoryTheory.Sheaf.epi_app_of_isCechAcyclicOnCompactBasis {X : TopCat} (B : CompactOpenBasis X) {S : ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) (hF : IsCechAcyclicOnCompactBasis B S.X₁) {V : TopologicalSpace.Opens ↑X} (hV : V ∈ B.carrier) : Epi (S.g.hom.app (Opposite.op V))

On a basis open, degree-one Cech exactness makes the quotient map in a short exact sequence surjective on sections. This is the key correction-and-gluing step in Tag 01EW.

theorem CategoryTheory.Sheaf.isCechAcyclicOnCompactBasis_quotient {X : TopCat} (B : CompactOpenBasis X) {S : ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) (hF : IsCechAcyclicOnCompactBasis B S.X₁) [Injective S.X₂] : IsCechAcyclicOnCompactBasis B S.X₃

The quotient in a short exact sequence inherits positive Cech exactness on the compact basis when the middle sheaf is injective.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.derivedH {X : TopCat} (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) (F : TopCat.Sheaf AddCommGrpCat X) (n : ℕ) : Type (u + 1)

Sheaf.H on a topological space with the HasExt instance passed explicitly, so that statements about it elaborate without re-synthesizing the abelian structure of the sheaf category (whose universe levels are max-expressions instance search cannot re-unify).

Equations

• CategoryTheory.Sheaf.derivedH hExt F n = CategoryTheory.Sheaf.H F n

theorem CategoryTheory.Sheaf.H_one_subsingleton_of_sections_epi {X : TopCat} {F : TopCat.Sheaf AddCommGrpCat X} (ip : InjectivePresentation F) [hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)] (hepi : Epi (ip.shortComplex.g.hom.app (Opposite.op ⊤))) : Subsingleton (derivedH hExt F 1)

If the global sections of an injective presentation F ↪ I ↠ Q surject onto those of Q, then H¹ F = 0: the connecting map from H⁰ Q is onto H¹ F and factors through H⁰ I.

theorem CategoryTheory.Sheaf.H_succ_subsingleton_of_shortExact {X : TopCat} {S : ShortComplex (TopCat.Sheaf AddCommGrpCat X)} (hS : S.ShortExact) [Injective S.X₂] [hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)] (n : ℕ) [Subsingleton (derivedH hExt S.X₃ n)] : Subsingleton (derivedH hExt S.X₁ (n + 1))

Dimension shifting: for a short exact sequence with injective middle term, H^(n+1) of the first term vanishes as soon as H^n of the third does.

theorem CategoryTheory.Sheaf.HPrime_subsingleton_of_isCechAcyclicOnCompactBasis {X : TopCat} (B : CompactOpenBasis X) (F : TopCat.Sheaf AddCommGrpCat X) (hF : IsCechAcyclicOnCompactBasis B F) [hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)] (V : TopologicalSpace.Opens ↑X) (hV : V ∈ B.carrier) (n : ℕ) (hn : 0 < n) : Subsingleton (CategoryTheory.Sheaf.derivedHPrime✝ hExt F V n)

Cech exactness on finite covers in a compact intersection-stable collection implies vanishing of positive local cohomology on every member of the collection.

theorem CategoryTheory.Sheaf.H_subsingleton_of_isCechAcyclicOnCompactBasis {X : TopCat} (B : CompactOpenBasis X) (F : TopCat.Sheaf AddCommGrpCat X) (hF : IsCechAcyclicOnCompactBasis B F) [hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)] (hTop : ⊤ ∈ B.carrier) (n : ℕ) (hn : 0 < n) : Subsingleton (H F n)

Cech exactness on finite covers in a compact intersection-stable basis implies vanishing of positive derived global-section cohomology (Stacks Project, Tag 01EW).