Global sections and the injective Cech total complex

For a cover of the terminal object, the augmented Cech complex of a sheaf is exact in degree zero. Combined with positive Cech exactness for injective sheaves, this identifies the total Cech complex of an injective resolution with the ordinary global-sections complex.

The file closes with the Cech-to-derived comparison itself, in two forms. The general form carries an explicit InjectiveResolution and an explicit HasExt witness, because neither is available over an arbitrary site. On the small site Opens X both are supplied by Mathlib's Grothendieck-abelian instances, so the specialization at the end of the file states the theorem with no witness arguments at all.

Importing Mathlib.CategoryTheory.Abelian.GrothendieckCategory.HasExt is what makes the second form possible: without it HasExt is not in scope as an instance, and instance search falls back to unfolding the abbreviation and diverges. HasExt is a Prop, so bringing the instance into scope creates no diamond with the HasExt.standard witnesses used elsewhere.

noncomputable def CategoryTheory.Sheaf.globalSectionsToCechZero {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (G : Sheaf J AddCommGrpCat) : G.obj.obj (Opposite.op T) ⟶ ((cechComplexFunctor U).obj G.obj).X 0

Restriction of a global section to the degree-zero term of a Cech complex.

Equations

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

theorem CategoryTheory.Sheaf.globalSectionsToCechZero_comp_d {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (G : Sheaf J AddCommGrpCat) : CategoryStruct.comp (globalSectionsToCechZero hT U G) (((cechComplexFunctor U).obj G.obj).d 0 1) = 0

theorem CategoryTheory.Sheaf.globalSectionsToCechZero_naturality {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) {G H : Sheaf J AddCommGrpCat} (f : G ⟶ H) : CategoryStruct.comp (globalSectionsToCechZero hT U G) (((cechComplexFunctor U).map f.hom).f 0) = CategoryStruct.comp (f.hom.app (Opposite.op T)) (globalSectionsToCechZero hT U H)

Restriction to degree-zero Cech cochains is natural in the sheaf.

noncomputable def CategoryTheory.Sheaf.globalSectionsToCechZeroInt {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (G : Sheaf J AddCommGrpCat) : G.obj.obj (Opposite.op T) ⟶ ((cechCochainFunctorInt U).obj G).X 0

Restriction of global sections to degree zero of the integer-extended Cech complex.

Equations

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

theorem CategoryTheory.Sheaf.globalSectionsToCechZeroInt_comp_d {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (G : Sheaf J AddCommGrpCat) : CategoryStruct.comp (globalSectionsToCechZeroInt hT U G) (((cechCochainFunctorInt U).obj G).d 0 1) = 0

theorem CategoryTheory.Sheaf.globalSectionsToCechZeroInt_naturality {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) {G H : Sheaf J AddCommGrpCat} (f : G ⟶ H) : CategoryStruct.comp (globalSectionsToCechZeroInt hT U G) (((cechCochainFunctorInt U).map f).f 0) = CategoryStruct.comp (f.hom.app (Opposite.op T)) (globalSectionsToCechZeroInt hT U H)

theorem CategoryTheory.Sheaf.globalSectionsToCechZero_exact {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (hU : J.CoversTop U) (G : Sheaf J AddCommGrpCat) : { X₁ := G.obj.obj (Opposite.op T), X₂ := ((cechComplexFunctor U).obj G.obj).X 0, X₃ := ((cechComplexFunctor U).obj G.obj).X 1, f := globalSectionsToCechZero hT U G, g := ((cechComplexFunctor U).obj G.obj).d 0 1, zero := ⋯ }.Exact

The sheaf gluing axiom identifies global sections with degree-zero Cech cocycles.

theorem CategoryTheory.Sheaf.globalSectionsToCechZero_mono {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (hU : J.CoversTop U) (G : Sheaf J AddCommGrpCat) : Mono (globalSectionsToCechZero hT U G)

A covering family detects global sections.

theorem CategoryTheory.Sheaf.globalSectionsToCechZeroInt_mono {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (hU : J.CoversTop U) (G : Sheaf J AddCommGrpCat) : Mono (globalSectionsToCechZeroInt hT U G)

theorem CategoryTheory.Sheaf.globalSectionsToCechZeroInt_exact {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (hU : J.CoversTop U) (G : Sheaf J AddCommGrpCat) : { X₁ := G.obj.obj (Opposite.op T), X₂ := ((cechCochainFunctorInt U).obj G).X 0, X₃ := ((cechCochainFunctorInt U).obj G).X 1, f := globalSectionsToCechZeroInt hT U G, g := ((cechCochainFunctorInt U).obj G).d 0 1, zero := ⋯ }.Exact

The integer-extended augmented Cech complex is exact in degree zero.

noncomputable def CategoryTheory.Sheaf.globalSectionsToCechRowMap {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) (U : index → C) (G : Sheaf J AddCommGrpCat) : (CochainComplex.singleFunctor AddCommGrpCat 0).obj (G.obj.obj (Opposite.op T)) ⟶ (cechCochainFunctorInt U).obj G

The augmented Cech row of a sheaf, with global sections placed in degree zero.

Equations

• CategoryTheory.Sheaf.globalSectionsToCechRowMap hT U G = HomologicalComplex.mkHomFromSingle (CategoryTheory.Sheaf.globalSectionsToCechZeroInt hT U G) ⋯

theorem CategoryTheory.Sheaf.globalSectionsToCechRowMap_quasiIso {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) (hU : (Opens.grothendieckTopology ↑X).CoversTop U) (G : TopCat.Sheaf AddCommGrpCat X) [Injective G] : QuasiIso (globalSectionsToCechRowMap hT U G)

For a cover of a topological space, the augmented Cech row of an injective sheaf is a quasi-isomorphism.

noncomputable def CategoryTheory.Sheaf.injectiveResolutionSectionsToCechZeroColumn {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : injectiveResolutionSectionsComplexUnlifted T I ⟶ (cechInjectiveBicomplex U I).X 0

Global sections of an injective resolution map to its degree-zero Cech column.

Equations

• CategoryTheory.Sheaf.injectiveResolutionSectionsToCechZeroColumn hT U I = { f := fun (q : ℤ) => CategoryTheory.Sheaf.globalSectionsToCechZeroInt hT U (I.cochainComplex.X q), comm' := ⋯ }

noncomputable def CategoryTheory.Sheaf.globalSectionsToCechBicomplexMap {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : HomologicalComplex₂.singleZeroBicomplex (injectiveResolutionSectionsComplexUnlifted T I) ⟶ cechInjectiveBicomplex U I

The augmented row map from the global-sections resolution, placed in Cech degree zero, to the full injective Cech bicomplex.

Equations

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

noncomputable def CategoryTheory.Sheaf.globalSectionsToCechBicomplexMapFlipRowIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {T : C} {F : Sheaf J AddCommGrpCat} (I : InjectiveResolution F) (q : ℤ) : (HomologicalComplex₂.singleZeroBicomplex (injectiveResolutionSectionsComplexUnlifted T I)).flip.X q ≅ (CochainComplex.singleFunctor AddCommGrpCat 0).obj ((I.cochainComplex.X q).obj.obj (Opposite.op T))

After flipping the augmented bicomplex, each fixed resolution degree is the corresponding augmented Cech row, up to the canonical identification between evaluation and a single complex.

Equations

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

theorem CategoryTheory.Sheaf.globalSectionsToCechBicomplexMap_flip_row {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) (q : ℤ) : ((HomologicalComplex₂.flipFunctor AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)).map (globalSectionsToCechBicomplexMap hT U I)).f q = CategoryStruct.comp (globalSectionsToCechBicomplexMapFlipRowIso I q).hom (globalSectionsToCechRowMap hT U (I.cochainComplex.X q))

theorem CategoryTheory.Sheaf.globalSectionsToCechBicomplexMap_flip_row_quasiIso {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) (hU : (Opens.grothendieckTopology ↑X).CoversTop U) {F : TopCat.Sheaf AddCommGrpCat X} (I : InjectiveResolution F) (q : ℤ) : QuasiIso (((HomologicalComplex₂.flipFunctor AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)).map (globalSectionsToCechBicomplexMap hT U I)).f q)

Each resolution-degree row of the flipped global-sections comparison is a quasi-isomorphism.

noncomputable def CategoryTheory.Sheaf.injectiveResolutionSectionsToCechTotalMap {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {T : C} (hT : Limits.IsTerminal T) {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : injectiveResolutionSectionsComplexUnlifted T I ⟶ cechInjectiveTotalComplex U I

The global-sections resolution maps canonically to the total Cech complex through the rowwise augmented Cech comparison.

Equations

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

theorem CategoryTheory.Sheaf.injectiveResolutionSectionsToCechTotalMap_quasiIso {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) (hU : (Opens.grothendieckTopology ↑X).CoversTop U) {F : TopCat.Sheaf AddCommGrpCat X} (I : InjectiveResolution F) : QuasiIso (injectiveResolutionSectionsToCechTotalMap hT U I)

For an open cover, the complex of global sections of an injective resolution and the injective Cech total complex are quasi-isomorphic.

noncomputable def CategoryTheory.Sheaf.cechCochainFunctorIntHomologyIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (n : ℕ) : HomologicalComplex.homology ((cechCochainFunctorInt U).obj F) ↑n ≅ cechCohomology U F.obj n

Integer extension does not change the Cech cohomology in a nonnegative degree.

Equations

• CategoryTheory.Sheaf.cechCochainFunctorIntHomologyIso U n = id (HomologicalComplex.extendHomologyIso ((CategoryTheory.cechComplexFunctor U).obj F.obj) ComplexShape.embeddingUpNat ⋯)

noncomputable def CategoryTheory.Sheaf.injectiveResolutionSectionsComplexUnliftedIso {X : TopCat} {T : TopologicalSpace.Opens ↑X} {F : TopCat.Sheaf AddCommGrpCat X} (I : InjectiveResolution F) : injectiveResolutionSectionsComplexUnlifted T I ≅ injectiveResolutionSectionsComplex T I

In one universe, the unlifted sections complex is canonically isomorphic to the universe-lifted complex used by the existing H' comparison.

Equations

• CategoryTheory.Sheaf.injectiveResolutionSectionsComplexUnliftedIso I = HomologicalComplex.Hom.isoOfComponents (fun (x : ℤ) => AddEquiv.ulift.symm.toAddCommGrpIso) ⋯

noncomputable def CategoryTheory.Sheaf.cechToSectionsHomologyIso {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) {F : TopCat.Sheaf AddCommGrpCat X} (I : InjectiveResolution F) (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) (hcover : IsCechAcyclicCover U F) (n : ℕ) : cechCohomology U F.obj n ≅ HomologicalComplex.homology (injectiveResolutionSectionsComplex T I) ↑n

The Cech-to-sections half of the comparison, as a named isomorphism.

The four factors are each the homology of an explicit chain map, or its inverse; the acyclicity hypothesis enters only through the proofs that two of them are quasi-isomorphisms, never through the construction. That is what makes the comparison compatible with a morphism of sheaves -- see cechComparisonAddEquiv_naturality.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechComparisonAddEquiv {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) {F : TopCat.Sheaf AddCommGrpCat X} (I : InjectiveResolution F) (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) (hcover : IsCechAcyclicCover U F) (n : ℕ) : ↑(cechCohomology U F.obj n) ≃+ H F n

The Cech-to-derived comparison, as a named additive equivalence.

The existential form below records only that some isomorphism exists, which is enough for a vanishing statement and not enough for anything else: a scalar action on cohomology arrives as the map induced by an endomorphism of the sheaf, and an unnamed isomorphism cannot be asked to commute with it. This is the comparison itself.

Equations

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

theorem CategoryTheory.Sheaf.isCechAcyclicCover_cechComputesDerivedCohomology {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) {F : TopCat.Sheaf AddCommGrpCat X} (I : InjectiveResolution F) (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) (hcover : IsCechAcyclicCover U F) : CechComputesDerivedCohomology U F

A Cech-acyclic open cover computes derived sheaf cohomology, relative to an explicit injective resolution and an explicit HasExt witness.

Both stay explicit here because the statement is universe-general in the HasExt parameter h. For the small site Opens X at h = u, see isCechAcyclicCover_cechComputesDerivedCohomology_opens, which supplies both.

The isomorphism is cechComparisonAddEquiv; this states only that one exists, which is all a vanishing argument needs.

theorem CategoryTheory.Sheaf.isCechAcyclicCover_cechComputesDerivedCohomology_opens {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) {F : TopCat.Sheaf AddCommGrpCat X} (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) (hcover : IsCechAcyclicCover U F) : CechComputesDerivedCohomology U F

A Cech-acyclic open cover computes derived sheaf cohomology, with no injective resolution supplied. The site Opens X is small, so Mathlib's Grothendieck-abelian chain gives enough injectives and canonicalInjectiveResolution chooses one.

The HasExt witness stays explicit, with a free universe h, and deliberately so. Sheaf.H is abbrev H (n : ℕ) : Type w', so the cohomology groups live in the HasExt universe: HasExt.{u} and HasExt.{u + 1} name genuinely different groups, not two proofs of one statement. The small site does permit pinning h := u through IsGrothendieckAbelian.hasExt, but that would state the theorem about groups no other part of this library computes -- Cohomology/Derived/AffineVanishing and Cohomology/Finiteness/FiniteDimensional both work at HasExt.{u + 1} through HasExt.standard. Keeping the witness explicit also stops instance search from silently resolving it to u inside IsCechAcyclicCover, which is why the hypothesis and conclusion below name it positionally.

theorem CategoryTheory.Sheaf.isCechAcyclicCover_cechComputesDerivedCohomologyAt_opens {X : TopCat} {T : TopologicalSpace.Opens ↑X} (hT : Limits.IsTerminal T) {index : Type u} (U : index → TopologicalSpace.Opens ↑X) {F : TopCat.Sheaf AddCommGrpCat X} (hExt : HasExt (TopCat.Sheaf AddCommGrpCat X)) (hcover : IsCechAcyclicCover U F) (n : ℕ) : CechComputesDerivedCohomologyAt U F n

Degreewise form of isCechAcyclicCover_cechComputesDerivedCohomology_opens.