The Cech bicomplex of an injective resolution

Given a cover-shaped family U and an injective resolution I of an abelian sheaf F, this file constructs the classical cohomological bicomplex

C^{p,q} = Cech^p(U, I^q).

The Cech direction is the first direction and the resolution direction is the second. We also retain the augmentation induced by F ⟶ I⁰, and instantiate the column-filtered total-complex spectral sequence constructed in DerivedAlgGeo.Algebra.Homology.SpectralSequence.FilteredTotalComplex.

The site here is a general C : Type u with Category.{v} C, and at the pinned Mathlib revision abelian sheaves over such a site carry no EnoughInjectives instance. Accordingly, the construction takes an explicit InjectiveResolution F; it does not install its existence as an axiom or typeclass. The obstruction is smallness alone: over a small site Mathlib does derive enough injectives, and DerivedAlgGeo.CategoryTheory.Sites.SheafCohomology.Cech.SmallSiteResolution discharges the resolution argument there.

instance CategoryTheory.Limits.FormalCoproduct.evalOp_additive {C : Type u} [Category.{v, u} C] {A : Type uA} [Category.{vA, uA} A] [Preadditive A] [HasProducts A] : (evalOp C A).Additive

instance CategoryTheory.whiskeringLeft_obj_additive {B : Type u_1} {D : Type u_2} {A : Type u_3} [Category.{v_1, u_1} B] [Category.{v_2, u_2} D] [Category.{v_3, u_3} A] [Preadditive A] (F : Functor B D) : ((Functor.whiskeringLeft B D A).obj F).Additive

@[implicit_reducible]

instance AlgebraicTopology.cosimplicialObject_preadditive {A : Type a} [CategoryTheory.Category.{u_1, a} A] [CategoryTheory.Preadditive A] : CategoryTheory.Preadditive (CategoryTheory.CosimplicialObject A)

Equations

• AlgebraicTopology.cosimplicialObject_preadditive = id CategoryTheory.functorCategoryPreadditive

instance AlgebraicTopology.alternatingCofaceMapComplex_additive {A : Type a} [CategoryTheory.Category.{u_1, a} A] [CategoryTheory.Preadditive A] : (alternatingCofaceMapComplex A).Additive

instance CategoryTheory.Sheaf.cech_evalOp_additive {C : Type u} [Category.{v, u} C] : (Limits.FormalCoproduct.evalOp C AddCommGrpCat).Additive

instance CategoryTheory.Sheaf.cech_whiskeringLeft_additive {C : Type u} [Category.{v, u} C] (E : SimplicialObject (Limits.FormalCoproduct C)) : ((Functor.whiskeringLeft SimplexCategory (Limits.FormalCoproduct C)ᵒᵖ AddCommGrpCat).obj (Functor.rightOp E)).Additive

instance CategoryTheory.Sheaf.cech_cosimplicialObjectFunctor_additive {C : Type u} [Category.{v, u} C] (E : SimplicialObject (Limits.FormalCoproduct C)) : (Limits.FormalCoproduct.cosimplicialObjectFunctor E).Additive

instance CategoryTheory.Sheaf.cechComplexFunctor_additive {C : Type u} [Category.{v, u} C] [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) : (cechComplexFunctor U).Additive

noncomputable def CategoryTheory.Sheaf.cechCochainFunctorInt {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) : Functor (Sheaf J AddCommGrpCat) (CochainComplex AddCommGrpCat ℤ)

Apply the Cech complex to the underlying presheaf of an abelian sheaf and extend its ℕ-grading by zero to a ℤ-grading.

Equations

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

instance CategoryTheory.Sheaf.cechCochainFunctorInt_additive {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) : (cechCochainFunctorInt U).Additive

noncomputable def CategoryTheory.Sheaf.cechResolutionBicomplexUnflipped {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)

Before flipping the two directions, applying the Cech-complex functor to an injective resolution gives a complex in the resolution degree whose values are Cech complexes.

Equations

• CategoryTheory.Sheaf.cechResolutionBicomplexUnflipped U I = ((CategoryTheory.Sheaf.cechCochainFunctorInt U).mapHomologicalComplex (ComplexShape.up ℤ)).obj I.cochainComplex

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplex {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)

The Cech bicomplex C^{p,q} = Cech^p(U, I^q), with Cech degree first and resolution degree second.

Equations

• CategoryTheory.Sheaf.cechInjectiveBicomplex U I = (CategoryTheory.Sheaf.cechResolutionBicomplexUnflipped U I).flip

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplexXXIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) (p q : ℤ) : ((cechInjectiveBicomplex U I).X p).X q ≅ ((cechCochainFunctorInt U).obj (I.cochainComplex.X q)).X p

The componentwise identification expressing the defining formula C^{p,q} = Cech^p(U, I^q).

Equations

• CategoryTheory.Sheaf.cechInjectiveBicomplexXXIso U I p q = CategoryTheory.Iso.refl (((CategoryTheory.Sheaf.cechInjectiveBicomplex U I).X p).X q)

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentationSource {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} (U : index → C) (F : Sheaf J AddCommGrpCat) : HomologicalComplex₂ AddCommGrpCat (ComplexShape.up ℤ) (ComplexShape.up ℤ)

The bicomplex obtained from the Cech complex of F, placed in resolution degree zero. It is the source of cechInjectiveBicomplexAugmentation.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentation {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : cechInjectiveBicomplexAugmentationSource U F ⟶ cechInjectiveBicomplex U I

The augmentation of the Cech bicomplex induced by the injective-resolution map F ⟶ I⁰.

Equations

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

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

The total cochain complex of the Cech bicomplex. Its cohomology is the intended abutment of the column-filtration spectral sequence.

Equations

• CategoryTheory.Sheaf.cechInjectiveTotalComplex U I = (CategoryTheory.Sheaf.cechInjectiveBicomplex U I).total (ComplexShape.up ℤ)

noncomputable def CategoryTheory.Sheaf.cechInjectiveFilteredToTotal {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) (p : ℤ) : (cechInjectiveBicomplex U I).columnFilteredTotalComplex.obj p ⟶ cechInjectiveTotalComplex U I

The canonical map from filtration stage p into the total Cech complex.

Equations

• CategoryTheory.Sheaf.cechInjectiveFilteredToTotal U I p = (CategoryTheory.Sheaf.cechInjectiveBicomplex U I).columnFilteredTotalι p

noncomputable def CategoryTheory.Sheaf.cechInjectiveFilteredToTotalNat {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : (cechInjectiveBicomplex U I).columnFilteredTotalComplex ⟶ (Functor.const ℤ).obj (cechInjectiveTotalComplex U I)

The filtration-stage maps to the total Cech complex, packaged with their compatibility.

Equations

• CategoryTheory.Sheaf.cechInjectiveFilteredToTotalNat U I = (CategoryTheory.Sheaf.cechInjectiveBicomplex U I).columnFilteredTotalιNat

noncomputable def CategoryTheory.Sheaf.cechInjectiveSpectralObject {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : Abelian.SpectralObject AddCommGrpCat ℤ

The abelian spectral object associated to the column-filtered Cech total complex.

Equations

• CategoryTheory.Sheaf.cechInjectiveSpectralObject U I = (CategoryTheory.Sheaf.cechInjectiveBicomplex U I).columnFilteredTotalSpectralObject

noncomputable def CategoryTheory.Sheaf.cechInjectiveSpectralSequence {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : SpectralSequence AddCommGrpCat (fun (r : ℤ) => ComplexShape.up' (r - 1, 2 - r)) 2

The E₂ cohomological spectral sequence of the Cech bicomplex of an explicit injective resolution.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechInjectiveInitialPageXIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) (p q : ℤ) : ((cechInjectiveSpectralSequence U I).page 2 cechInjectiveInitialPageXIso._proof_1).X (p, q) ≅ ((cechInjectiveSpectralObject U I).H (p + q)).obj (ComposableArrows.mk₁ (homOfLE ⋯))

The formal initial-page computation: an object on page 2 is the homology of the adjacent filtration layer selected by the stages -p - 1 ≤ -p.

Equations

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

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

The adjacent filtered-total mapping cone contributing Cech column p to the initial page.

Equations

• CategoryTheory.Sheaf.cechInjectiveAdjacentLayerComplex U I p = (CategoryTheory.Sheaf.cechInjectiveBicomplex U I).columnFilteredAdjacentLayerComplex p

noncomputable def CategoryTheory.Sheaf.cechInjectiveAdjacentLayerHomologyIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) (p q : ℤ) : ((cechInjectiveSpectralObject U I).H (p + q)).obj (ComposableArrows.mk₁ (homOfLE ⋯)) ≅ HomologicalComplex.homology (cechInjectiveAdjacentLayerComplex U I p) (p + q)

The spectral object's adjacent-layer term is ordinary homology of the corresponding mapping cone.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechInjectiveInitialPageColumnHomologyIso {C : Type u} [Category.{v, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) (p q : ℤ) : ((cechInjectiveSpectralSequence U I).page 2 cechInjectiveInitialPageXIso._proof_1).X (p, q) ≅ ((cechInjectiveBicomplex U I).X p).homology q

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

Equations

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