Choosing the injective resolution on a small site

DerivedAlgGeo.CategoryTheory.Sites.SheafCohomology.Cech.Bicomplex and DerivedAlgGeo.CategoryTheory.Sites.SheafCohomology.Cech.Comparison thread an explicit InjectiveResolution F through every construction, because no EnoughInjectives instance is available for abelian sheaves over an arbitrary site. That restriction is narrower than it looks. The pinned Mathlib derives enough injectives from CategoryTheory.IsGrothendieckAbelian, and its sheaf instance requires the site to be small in the universe of the sheaf values.

Concretely, Comparison carries C : Type u with Category.{a} C and sheaves valued in AddCommGrpCat.{a}; the missing hypothesis is exactly u = a, that is, SmallCategory C. Every site this library computes on has that form -- in particular Opens.grothendieckTopology X for a topological space X, where the opens form a Type a with Category.{a} structure.

So on a small site the resolution argument is redundant, and this file discharges it: canonicalInjectiveResolution chooses one, and the wrappers below restate the Cech spectral-sequence interface without an InjectiveResolution parameter.

Nothing here is an axiom, and no new instance enters the graph. enoughInjectives_of_small is inferInstance against Mathlib's existing chain

AddCommGrpCat.{a} Grothendieck abelian -> Sheaf J AddCommGrpCat.{a} Grothendieck abelian -> Sheaf J AddCommGrpCat.{a} has enough injectives (@[stacks 079H]).

The remaining Cech-to-derived boundaries recorded in Comparison are unaffected: identifying the degree-zero row of the initial page with the Cech complex, and proving abutment against the named total complex, are still open.

theorem CategoryTheory.Sheaf.enoughInjectives_of_small {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] : EnoughInjectives (Sheaf J AddCommGrpCat)

On a small site, abelian sheaves have enough injectives.

This is not a new instance; it names the conclusion of Mathlib's Grothendieck-abelian chain so that the axiom audit can see it, and so that the smallness hypothesis is stated once.

theorem CategoryTheory.Sheaf.hasInjectiveResolutions_of_small {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] : HasInjectiveResolutions (Sheaf J AddCommGrpCat)

On a small site, every abelian sheaf admits an injective resolution.

theorem CategoryTheory.Sheaf.enoughInjectives_opens (T : Type a) [TopologicalSpace T] : EnoughInjectives (Sheaf (Opens.grothendieckTopology T) AddCommGrpCat)

The site of opens of a topological space is small, so its abelian sheaves have enough injectives. This is the instantiation the coherent-sheaf cohomology layer actually uses.

noncomputable def CategoryTheory.Sheaf.canonicalInjectiveResolution {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] (F : Sheaf J AddCommGrpCat) : InjectiveResolution F

An injective resolution chosen on a small site, rather than supplied as a hypothesis.

Equations

• F.canonicalInjectiveResolution = CategoryTheory.injectiveResolution F

noncomputable def CategoryTheory.Sheaf.canonicalSectionsCohomologyAddEquivHPrime {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] (X : C) (F : Sheaf J AddCommGrpCat) (n : ℕ) : ↑(HomologicalComplex.homology (injectiveResolutionSectionsComplex X F.canonicalInjectiveResolution) ↑n) ≃+ ↑(F.H' n X)

The cohomology of the sections of the canonical injective resolution computes H'.

Resolution-free form of injectiveResolutionSectionsCohomologyAddEquivHPrime.

Equations

• CategoryTheory.Sheaf.canonicalSectionsCohomologyAddEquivHPrime X F n = CategoryTheory.Sheaf.injectiveResolutionSectionsCohomologyAddEquivHPrime X F.canonicalInjectiveResolution n

noncomputable def CategoryTheory.Sheaf.canonicalCechBicomplex {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [Limits.HasFiniteProducts C] {ι : Type a} (U : ι → C) (F : Sheaf J AddCommGrpCat) : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)

The Cech bicomplex of the canonical injective resolution.

Resolution-free form of cechInjectiveBicomplex.

Equations

• CategoryTheory.Sheaf.canonicalCechBicomplex U F = CategoryTheory.Sheaf.cechInjectiveBicomplex U F.canonicalInjectiveResolution

noncomputable def CategoryTheory.Sheaf.canonicalCechSpectralSequence {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [Limits.HasFiniteProducts C] {ι : Type a} (U : ι → C) (F : Sheaf J AddCommGrpCat) : SpectralSequence AddCommGrpCat (fun (r : ℤ) => ComplexShape.up' (r - 1, 2 - r)) 2

The column-filtration spectral sequence of the Cech bicomplex, with no resolution argument.

Resolution-free form of cechInjectiveSpectralSequence.

Equations

• CategoryTheory.Sheaf.canonicalCechSpectralSequence U F = CategoryTheory.Sheaf.cechInjectiveSpectralSequence U F.canonicalInjectiveResolution

noncomputable def CategoryTheory.Sheaf.canonicalCechInitialPageColumnHomologyIso {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [Limits.HasFiniteProducts C] {ι : Type a} (U : ι → C) (F : Sheaf J AddCommGrpCat) (p q : ℤ) : ((canonicalCechSpectralSequence U F).page 2 canonicalCechInitialPageColumnHomologyIso._proof_4).X (p, q) ≅ ((canonicalCechBicomplex U F).X p).homology q

The initial page of the canonical spectral sequence is vertical homology of the fixed Cech column: E₂^{p,q} ≅ H^q(C^{p,*}).

Resolution-free form of cechInjectiveInitialPageColumnHomologyIso.

Equations

• CategoryTheory.Sheaf.canonicalCechInitialPageColumnHomologyIso U F p q = CategoryTheory.Sheaf.cechInjectiveInitialPageColumnHomologyIso U F.canonicalInjectiveResolution p q

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

Under local acyclicity, every positive-resolution-degree entry on the initial page vanishes.

Resolution-free form of isZero_cechInjectiveInitialPage_of_isCechAcyclicFor; the acyclicity hypothesis is a statement about F alone, so no resolution appears anywhere in this signature.

theorem CategoryTheory.Sheaf.subsingleton_canonicalCechInitialPage_of_isCechAcyclicFor {C : Type a} [SmallCategory C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] [HasExt (Sheaf J AddCommGrpCat)] [Limits.HasFiniteProducts C] {ι : Type a} (U : ι → C) {F : Sheaf J AddCommGrpCat} (hacyclic : IsCechAcyclicFor U F) (p q : ℕ) (hq : 0 < q) : Subsingleton ↑(((canonicalCechSpectralSequence U F).page 2 canonicalCechInitialPageColumnHomologyIso._proof_4).X (↑p, ↑q))

Elementwise form of isZero_canonicalCechInitialPage_of_isCechAcyclicFor.