The Cech-to-derived comparison boundary

This file supplies the first reusable layer of the comparison between Cech cohomology and derived-functor sheaf cohomology.

Mathlib defines the Cech complex and Sheaf.H, but it does not define the cohomology of that complex, a comparison morphism, or a theorem identifying the two. We therefore:

• name the homology objects of the Cech complex;
• prove the natural isomorphism F.H' n T ≃+ F.H n for a terminal object T;
• record the standard acyclicity hypothesis on all finite intersections in a cover;
• package, as a proposition, the exact conclusion a Cech-to-derived comparison theorem must produce; and
• prove the positive-degree comparison for the singleton cover of a terminal object, as well as the general implication from Cech exactness to derived vanishing once comparison is available.

This file is a layer, not the whole comparison. The nontrivial-cover step -- that IsCechAcyclicCover U F implies CechComputesDerivedCohomologyAt U F n -- is proved, in DerivedAlgGeo.Topology.Sheaves.Cech.GlobalComparison, by the augmented Cech resolution and its column-filtration spectral sequence. The chain runs:

• Bicomplex builds C^{p,q} = Cech^p(U, I^q) from an injective resolution, totalizes its column filtration, constructs the spectral sequence, and computes the initial page as the homology of an adjacent filtration layer;
• InitialPage identifies the degree-zero row, including its horizontal differential, with the integer-extended Cech complex, so the following page is ordinary Cech cohomology along that row;
• TotalComparison proves that under local acyclicity the augmentation from the ordinary Cech complex to the total injective Cech complex is a quasi-isomorphism, which is the abutment statement Mathlib's SpectralSequence structure cannot record as a field;
• GlobalComparison assembles these into isCechAcyclicCover_cechComputesDerivedCohomology.

The declarations below take an explicit InjectiveResolution F because the site here is a general C : Type u with Category.{a} C, and the pinned Mathlib supplies EnoughInjectives for abelian sheaves only over a small site. That is the only obstruction: on a small site the resolution is chosen rather than assumed. DerivedAlgGeo.CategoryTheory.Sites.SheafCohomology.Cech.SmallSiteResolution restates this interface without the resolution argument, and GlobalComparison.isCechAcyclicCover_cechComputesDerivedCohomology_opens states the comparison itself with neither a resolution nor a HasExt argument.

@[reducible, inline]

noncomputable abbrev CategoryTheory.cechCohomology {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] {A : Type a} [Category.{u_1, a} A] [Abelian A] [Limits.HasProducts A] {ι : Type i} (U : ι → C) (P : Functor Cᵒᵖ A) (n : ℕ) : A

Degree-n Cech cohomology is the homology of Mathlib's explicit Cech cochain complex.

Equations

• CategoryTheory.cechCohomology U P n = HomologicalComplex.homology ((CategoryTheory.cechComplexFunctor U).obj P) n

theorem CategoryTheory.cechCohomology_isZero_of_exactAt {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] {A : Type a} [Category.{u_1, a} A] [Abelian A] [Limits.HasProducts A] {ι : Type i} (U : ι → C) (P : Functor Cᵒᵖ A) (n : ℕ) (h : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj P) n) : Limits.IsZero (cechCohomology U P n)

Exactness of the explicit Cech complex at n kills degree-n Cech cohomology.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.freeAbelianYonedaSheaf {C : Type u} [Category.{a, u} C] (J : GrothendieckTopology C) [HasSheafify J AddCommGrpCat] (X : C) : Sheaf J AddCommGrpCat

The free abelian sheaf represented by X; this is the first argument of F.H' n X.

Equations

• CategoryTheory.Sheaf.freeAbelianYonedaSheaf J X = (CategoryTheory.presheafToSheaf J AddCommGrpCat).obj ((CategoryTheory.yoneda.obj X).comp AddCommGrpCat.free)

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaPresheafHomAddEquiv {C : Type u} [Category.{a, u} C] (X : C) (G : Functor Cᵒᵖ AddCommGrpCat) : ((yoneda.obj X).comp AddCommGrpCat.free ⟶ G) ≃+ ↑(G.obj (Opposite.op X))

Maps from the free abelian representable presheaf are sections.

Equations

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

theorem CategoryTheory.Sheaf.freeAbelianYonedaPresheafHomAddEquiv_comp {C : Type u} [Category.{a, u} C] (X : C) {G H : Functor Cᵒᵖ AddCommGrpCat} (f : (yoneda.obj X).comp AddCommGrpCat.free ⟶ G) (g : G ⟶ H) : (freeAbelianYonedaPresheafHomAddEquiv X H) (CategoryStruct.comp f g) = (ConcreteCategory.hom (g.app (Opposite.op X))) ((freeAbelianYonedaPresheafHomAddEquiv X G) f)

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaSheafHomAddEquiv {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] (X : C) (G : Sheaf J AddCommGrpCat) : (freeAbelianYonedaSheaf J X ⟶ G) ≃+ ↑(G.obj.obj (Opposite.op X))

Maps from the free abelian representable sheaf are sections.

Equations

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

theorem CategoryTheory.Sheaf.freeAbelianYonedaSheafHomAddEquiv_comp {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] (X : C) {G H : Sheaf J AddCommGrpCat} (f : freeAbelianYonedaSheaf J X ⟶ G) (g : G ⟶ H) : (freeAbelianYonedaSheafHomAddEquiv X H) (CategoryStruct.comp f g) = (ConcreteCategory.hom (g.hom.app (Opposite.op X))) ((freeAbelianYonedaSheafHomAddEquiv X G) f)

noncomputable def CategoryTheory.Sheaf.sectionsAtFunctorUnlifted {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} (X : C) : Functor (Sheaf J AddCommGrpCat) AddCommGrpCat

Sections over X, as an additive functor on abelian sheaves.

Equations

• CategoryTheory.Sheaf.sectionsAtFunctorUnlifted X = (CategoryTheory.sheafToPresheaf J AddCommGrpCat).comp ((CategoryTheory.evaluation Cᵒᵖ AddCommGrpCat).obj (Opposite.op X))

instance CategoryTheory.Sheaf.sectionsAtFunctorUnlifted_additive {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} (X : C) : (sectionsAtFunctorUnlifted X).Additive

noncomputable def CategoryTheory.Sheaf.sectionsAtFunctor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} (X : C) : Functor (Sheaf J AddCommGrpCat) AddCommGrpCat

Sections over X, lifted to the universe in which morphisms of sheaves live.

Equations

• CategoryTheory.Sheaf.sectionsAtFunctor X = (CategoryTheory.Sheaf.sectionsAtFunctorUnlifted X).comp AddCommGrpCat.uliftFunctor

instance CategoryTheory.Sheaf.sectionsAtFunctor_additive {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} (X : C) : (sectionsAtFunctor X).Additive

noncomputable def CategoryTheory.Sheaf.injectiveResolutionSectionsComplexUnlifted {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) : CochainComplex AddCommGrpCat ℤ

Apply ordinary, unlifted sections over X degreewise to an explicit injective resolution.

Equations

• CategoryTheory.Sheaf.injectiveResolutionSectionsComplexUnlifted X I = ((CategoryTheory.Sheaf.sectionsAtFunctorUnlifted X).mapHomologicalComplex (ComplexShape.up ℤ)).obj I.cochainComplex

noncomputable def CategoryTheory.Sheaf.injectiveResolutionSectionsComplex {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) : CochainComplex AddCommGrpCat ℤ

Apply sections over X degreewise to an explicit injective resolution.

Equations

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

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaHomComplexXIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) (n : ℤ) : (((CochainComplex.singleFunctor (Sheaf J AddCommGrpCat) 0).obj (freeAbelianYonedaSheaf J X)).HomComplex I.cochainComplex).X n ≅ (injectiveResolutionSectionsComplex X I).X n

In each degree, cochains from the free abelian representable sheaf are sections.

Equations

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

@[simp]

theorem CategoryTheory.Sheaf.freeAbelianYonedaHomComplexXIso_hom_apply {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) (n : ℤ) (α : CochainComplex.HomComplex.Cochain ((CochainComplex.singleFunctor (Sheaf J AddCommGrpCat) 0).obj (freeAbelianYonedaSheaf J X)) I.cochainComplex n) : (ConcreteCategory.hom (freeAbelianYonedaHomComplexXIso X I n).hom) α = { down := (freeAbelianYonedaSheafHomAddEquiv X (I.cochainComplex.X n)) ((CochainComplex.HomComplex.Cochain.fromSingleEquiv ⋯) α) }

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaHomComplexIsoSections {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) : ((CochainComplex.singleFunctor (Sheaf J AddCommGrpCat) 0).obj (freeAbelianYonedaSheaf J X)).HomComplex I.cochainComplex ≅ injectiveResolutionSectionsComplex X I

The Hom complex from the free abelian representable sheaf is the sections complex.

Equations

• CategoryTheory.Sheaf.freeAbelianYonedaHomComplexIsoSections X I = HomologicalComplex.Hom.isoOfComponents (CategoryTheory.Sheaf.freeAbelianYonedaHomComplexXIso X I) ⋯

noncomputable def CategoryTheory.Sheaf.injectiveResolutionSectionsCohomologyAddEquivHPrime {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) (n : ℕ) : ↑(HomologicalComplex.homology (injectiveResolutionSectionsComplex X I) ↑n) ≃+ ↑(F.H' n X)

The cohomology of the sections of an explicit injective resolution computes H'.

Equations

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

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaPresheafIsoConstant {C : Type u} [Category.{a, u} C] {T : C} (hT : Limits.IsTerminal T) : (yoneda.obj T).comp AddCommGrpCat.free ≅ (Functor.const Cᵒᵖ).obj (AddCommGrpCat.of (ULift.{a, 0} ℤ))

At a terminal object, the free abelian representable presheaf is the constant presheaf ULift ℤ.

Equations

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

noncomputable def CategoryTheory.Sheaf.freeAbelianYonedaSheafIsoConstant {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {T : C} (hT : Limits.IsTerminal T) : freeAbelianYonedaSheaf J T ≅ (constantSheaf J AddCommGrpCat).obj (AddCommGrpCat.of (ULift.{a, 0} ℤ))

Sheafified form of freeAbelianYonedaPresheafIsoConstant.

Equations

• CategoryTheory.Sheaf.freeAbelianYonedaSheafIsoConstant hT = ⋯.mpr ((CategoryTheory.presheafToSheaf J AddCommGrpCat).mapIso (CategoryTheory.Sheaf.freeAbelianYonedaPresheafIsoConstant hT))

noncomputable def CategoryTheory.Sheaf.HPrimeNatIsoH {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {T : C} (hT : Limits.IsTerminal T) (n : ℕ) : (cohomologyPresheafFunctor J n).comp ((evaluation Cᵒᵖ AddCommGrpCat).obj (Opposite.op T)) ≅ functorH J n

The missing terminal-object natural isomorphism noted in Mathlib's sheaf-cohomology API: cohomology represented by a terminal object agrees with global sheaf cohomology.

Equations

• CategoryTheory.Sheaf.HPrimeNatIsoH hT n = id ((CategoryTheory.Abelian.extFunctor n).mapIso (CategoryTheory.Sheaf.freeAbelianYonedaSheafIsoConstant hT).symm.op)

noncomputable def CategoryTheory.Sheaf.HPrimeAddEquivH {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {T : C} (hT : Limits.IsTerminal T) (F : Sheaf J AddCommGrpCat) (n : ℕ) : ↑(F.H' n T) ≃+ F.H n

Pointwise additive equivalence supplied by HPrimeNatIsoH.

Equations

• CategoryTheory.Sheaf.HPrimeAddEquivH hT F n = ((CategoryTheory.Sheaf.HPrimeNatIsoH hT n).app F).addCommGroupIsoToAddEquiv

theorem CategoryTheory.Sheaf.subsingleton_HPrime_iff_H {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {T : C} (hT : Limits.IsTerminal T) (F : Sheaf J AddCommGrpCat) (n : ℕ) : Subsingleton ↑(F.H' n T) ↔ Subsingleton (F.H n)

Vanishing of terminal-object cohomology in the H' presentation is equivalent to vanishing of global sheaf cohomology.

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplexColumnXIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (p : ℕ) (q : ℤ) : ((cechInjectiveBicomplex U I).X ↑p).X q ≅ ∏ᶜ fun (x : Fin (p + 1) → ι) => (I.cochainComplex.X q).obj.obj (Opposite.op (∏ᶜ fun (k : Fin (p + 1)) => U (x k)))

In a nonnegative Čech degree, a column of the injective bicomplex is degreewise the product of sections over the corresponding finite intersections.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechColumnSectionsComplex {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (p : ℕ) : CochainComplex AddCommGrpCat ℤ

The explicit product complex of sections over the intersections in a fixed Cech degree.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplexColumnIsoSectionsComplex {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (p : ℕ) : (cechInjectiveBicomplex U I).X ↑p ≅ cechColumnSectionsComplex U I p

A fixed column of the Cech-injective bicomplex is the product of the corresponding intersection-wise section complexes, including its resolution differential.

Equations

• CategoryTheory.Sheaf.cechInjectiveBicomplexColumnIsoSectionsComplex U I p = HomologicalComplex.Hom.isoOfComponents (CategoryTheory.Sheaf.cechInjectiveBicomplexColumnXIso U I p) ⋯

theorem CategoryTheory.Sheaf.cechColumnSectionsComplex_exactAt {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (p : ℕ) (q : ℤ) (hlocal : ∀ (x : Fin (p + 1) → ι), HomologicalComplex.ExactAt (injectiveResolutionSectionsComplexUnlifted (∏ᶜ fun (k : Fin (p + 1)) => U (x k)) I) q) : HomologicalComplex.ExactAt (cechColumnSectionsComplex U I p) q

Exactness of all the intersection-wise section complexes is preserved by the product that forms a fixed Cech column.

def CategoryTheory.Sheaf.IsCechAcyclicFor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] (U : ι → C) (F : Sheaf J AddCommGrpCat) : Prop

A cover is Cech-acyclic for F when F has no positive cohomology on any nonempty finite intersection occurring in its Cech nerve.

Coverage itself is intentionally separate: U is just the family used to form the Cech complex. Use IsCechAcyclicCover for the complete Leray hypothesis.

Equations

• CategoryTheory.Sheaf.IsCechAcyclicFor U F = ∀ (q : ℕ), 0 < q → ∀ (n : ℕ) (x : Fin (n + 1) → ι), Subsingleton ↑(F.H' q (∏ᶜ fun (k : Fin (n + 1)) => U (x k)))

theorem CategoryTheory.Sheaf.subsingleton_injectiveResolutionSectionsHomology_of_isCechAcyclicFor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (hacyclic : IsCechAcyclicFor U F) (q : ℕ) (hq : 0 < q) (n : ℕ) (x : Fin (n + 1) → ι) : Subsingleton ↑(HomologicalComplex.homology (injectiveResolutionSectionsComplex (∏ᶜ fun (k : Fin (n + 1)) => U (x k)) I) ↑q)

Under the local acyclicity hypothesis, the positive-degree cohomology of the sections complex of the chosen injective resolution vanishes on every Čech intersection.

theorem CategoryTheory.Sheaf.exactAt_of_subsingleton_map_ulift_homology (K : CochainComplex AddCommGrpCat ℤ) (q : ℤ) (h : Subsingleton ↑(((AddCommGrpCat.uliftFunctor.mapHomologicalComplex (ComplexShape.up ℤ)).obj K).homology q)) : HomologicalComplex.ExactAt K q

If the homology of the universe-lifted complex vanishes, then the original complex is exact in the same degree.

theorem CategoryTheory.Sheaf.cechInjectiveBicomplexColumn_exactAt_of_isCechAcyclicFor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (hacyclic : IsCechAcyclicFor U F) (p q : ℕ) (hq : 0 < q) : ((cechInjectiveBicomplex U I).X ↑p).ExactAt ↑q

Local acyclicity makes every fixed Cech column exact in positive resolution degree.

theorem CategoryTheory.Sheaf.subsingleton_cechInjectiveBicomplexColumnHomology_of_isCechAcyclicFor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (hacyclic : IsCechAcyclicFor U F) (p q : ℕ) (hq : 0 < q) : Subsingleton ↑(((cechInjectiveBicomplex U I).X ↑p).homology ↑q)

Equivalently, every positive-resolution-degree homology object of a fixed Cech column vanishes under local acyclicity.

theorem CategoryTheory.Sheaf.isZero_cechInjectiveInitialPage_of_isCechAcyclicFor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (hacyclic : IsCechAcyclicFor U F) (p q : ℕ) (hq : 0 < q) : Limits.IsZero (((cechInjectiveSpectralSequence U I).page 2 isZero_cechInjectiveInitialPage_of_isCechAcyclicFor._proof_4).X (↑p, ↑q))

Under local acyclicity, every positive-resolution-degree entry on the initial page of the column-filtration spectral sequence is zero.

theorem CategoryTheory.Sheaf.subsingleton_cechInjectiveInitialPage_of_isCechAcyclicFor {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] {F : Sheaf J AddCommGrpCat} (U : ι → C) (I : InjectiveResolution F) (hacyclic : IsCechAcyclicFor U F) (p q : ℕ) (hq : 0 < q) : Subsingleton ↑(((cechInjectiveSpectralSequence U I).page 2 isZero_cechInjectiveInitialPage_of_isCechAcyclicFor._proof_4).X (↑p, ↑q))

Elementwise form of isZero_cechInjectiveInitialPage_of_isCechAcyclicFor.

def CategoryTheory.Sheaf.IsCechAcyclicCover {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] (U : ι → C) (F : Sheaf J AddCommGrpCat) : Prop

The standard Leray hypothesis for a Cech-to-derived comparison: U covers the terminal object and F is acyclic on every nonempty finite intersection in the Cech nerve.

Equations

• CategoryTheory.Sheaf.IsCechAcyclicCover U F = (J.CoversTop U ∧ CategoryTheory.Sheaf.IsCechAcyclicFor U F)

def CategoryTheory.Sheaf.CechComputesDerivedCohomologyAt {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] (U : ι → C) (F : Sheaf J AddCommGrpCat) (n : ℕ) : Prop

The conclusion of a degreewise Cech-to-derived comparison theorem.

This is a proposition so downstream vanishing results need not depend on a particular choice of isomorphism. It is not an assumption installed globally and it contains no unproved declaration.

Equations

• CategoryTheory.Sheaf.CechComputesDerivedCohomologyAt U F n = Nonempty (↑(CategoryTheory.cechCohomology U F.obj n) ≃+ F.H n)

def CategoryTheory.Sheaf.CechComputesDerivedCohomology {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] (U : ι → C) (F : Sheaf J AddCommGrpCat) : Prop

A cover computes derived sheaf cohomology when it does so in every degree.

Equations

• CategoryTheory.Sheaf.CechComputesDerivedCohomology U F = ∀ (n : ℕ), CategoryTheory.Sheaf.CechComputesDerivedCohomologyAt U F n

theorem CategoryTheory.Sheaf.cechComputesDerivedCohomologyAt_singleton_terminal_of_pos {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] [Limits.HasFiniteProducts C] {T : C} (hT : Limits.IsTerminal T) (F : Sheaf J AddCommGrpCat) (n : ℕ) (hn : 0 < n) (hacyclic : IsCechAcyclicFor (fun (x : PUnit.{a + 1}) => T) F) : CechComputesDerivedCohomologyAt (fun (x : PUnit.{a + 1}) => T) F n

The positive-degree comparison for the singleton cover by a terminal object. Here the Cech complex is contractible, while IsCechAcyclicFor says precisely that the derived group vanishes; HPrimeAddEquivH identifies its terminal-object and global presentations.

theorem CategoryTheory.Sheaf.subsingleton_H_of_cech_exactAt {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] {ι : Type a} [Limits.HasFiniteProducts C] (U : ι → C) (F : Sheaf J AddCommGrpCat) (n : ℕ) (hcomparison : CechComputesDerivedCohomologyAt U F n) (hexact : HomologicalComplex.ExactAt ((cechComplexFunctor U).obj F.obj) n) : Subsingleton (F.H n)

If Cech cohomology computes derived sheaf cohomology in degree n, exactness of the explicit Cech complex at n implies vanishing of derived sheaf cohomology there.