The degree-zero row of the Cech-injective spectral sequence

For an explicit injective resolution F ⟶ I⁰ ⟶ I¹ ⟶ ⋯, applying a fixed Cech cochain term gives an augmented complex that is exact at I⁰. Consequently, the zeroth vertical homology of the Cech-injective bicomplex is the corresponding term of the ordinary Cech complex of F.

The second half of the file tracks the initial-page differential through the adjacent-column mapping cones. It identifies the degree-zero row, including its horizontal differential, with the integer-extended Cech complex. The page-to-page homology isomorphism therefore identifies the following page with Cech cohomology.

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

Evaluation of the integer-extended Cech complex in a fixed cochain degree.

Equations

• CategoryTheory.Sheaf.cechTermFunctorInt U p = (CategoryTheory.Sheaf.cechCochainFunctorInt U).comp (HomologicalComplex.eval AddCommGrpCat (ComplexShape.up ℤ) p)

instance CategoryTheory.Sheaf.cechTermFunctorInt_additive {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) (p : ℤ) : (cechTermFunctorInt U p).Additive

noncomputable def CategoryTheory.Sheaf.cechCochainFunctorIntXIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) (G : Sheaf J AddCommGrpCat) (p : ℕ) : ((cechCochainFunctorInt U).obj G).X ↑p ≅ ∏ᶜ fun (x : Fin (p + 1) → index) => G.obj.obj (Opposite.op (∏ᶜ fun (k : Fin (p + 1)) => U (x k)))

A nonnegative term of the integer-extended Cech complex is the usual product of sections on the corresponding finite intersections.

Equations

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

theorem CategoryTheory.Sheaf.cechCochainFunctorIntXIso_naturality {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) {G H : Sheaf J AddCommGrpCat} (f : G ⟶ H) (p : ℕ) : CategoryStruct.comp (((cechCochainFunctorInt U).map f).f ↑p) (cechCochainFunctorIntXIso U H p).hom = CategoryStruct.comp (cechCochainFunctorIntXIso U G p).hom (Limits.Pi.map fun (x : Fin (p + 1) → index) => f.hom.app (Opposite.op (∏ᶜ fun (k : Fin (p + 1)) => U (x k))))

theorem CategoryTheory.Sheaf.cechCochainFunctorIntXIso_naturality_assoc {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] {index : Type a} (U : index → C) {G H : Sheaf J AddCommGrpCat} (f : G ⟶ H) (p : ℕ) {Z : AddCommGrpCat} (h : (∏ᶜ fun (x : Fin (p + 1) → index) => H.obj.obj (Opposite.op (∏ᶜ fun (k : Fin (p + 1)) => U (x k)))) ⟶ Z) : CategoryStruct.comp (((cechCochainFunctorInt U).map f).f ↑p) (CategoryStruct.comp (cechCochainFunctorIntXIso U H p).hom h) = CategoryStruct.comp (cechCochainFunctorIntXIso U G p).hom (CategoryStruct.comp (Limits.Pi.map fun (x : Fin (p + 1) → index) => f.hom.app (Opposite.op (∏ᶜ fun (k : Fin (p + 1)) => U (x k)))) h)

instance CategoryTheory.Sheaf.cechCochainFunctorInt_map_f_mono {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} (U : index → C) {G H : Sheaf J AddCommGrpCat} (f : G ⟶ H) [Mono f] (p : ℕ) : Mono (((cechCochainFunctorInt U).map f).f ↑p)

noncomputable def CategoryTheory.Sheaf.cechInjectiveColumnAugmentation {C : Type u} [Category.{a, 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 : ℤ) : (cechInjectiveBicomplexAugmentationSource U F).X p ⟶ (cechInjectiveBicomplex U I).X p

The augmentation on a fixed Cech column.

Equations

• CategoryTheory.Sheaf.cechInjectiveColumnAugmentation U I p = (CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentation U I).f p

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

The first two maps of an injective resolution after taking sections, in its original Nat-graded presentation.

Equations

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

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

The first two maps of an injective resolution after taking sections, in the integer-graded presentation used by the Cech bicomplex.

Equations

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

noncomputable def CategoryTheory.Sheaf.sectionsAugmentedShortComplexIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) : sectionsIntAugmentedShortComplex X I ≅ sectionsNatAugmentedShortComplex X I

The integer- and natural-graded augmented section short complexes agree.

Equations

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

theorem CategoryTheory.Sheaf.sectionsIntAugmentedShortComplex_exact {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [HasSheafify J AddCommGrpCat] {F : Sheaf J AddCommGrpCat} (X : C) (I : InjectiveResolution F) : (sectionsIntAugmentedShortComplex X I).Exact

Taking sections preserves exactness at the beginning of an injective resolution.

noncomputable def CategoryTheory.Sheaf.cechAugmentedColumnProductShortComplex {C : Type u} [Category.{a, 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 : ℕ) : ShortComplex AddCommGrpCat

Product, over all intersections in a fixed Cech degree, of the augmented section short complexes.

Equations

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

theorem CategoryTheory.Sheaf.cechAugmentedColumnProductShortComplex_exact {C : Type u} [Category.{a, 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 : ℕ) : (cechAugmentedColumnProductShortComplex U I p).Exact

noncomputable def CategoryTheory.Sheaf.cechColumnAugmentationShortComplex {C : Type u} [Category.{a, 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 : ℕ) : ShortComplex AddCommGrpCat

The augmented first two terms in a fixed nonnegative Cech column.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechColumnAugmentationShortComplexIso {C : Type u} [Category.{a, 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 : ℕ) : cechColumnAugmentationShortComplex U I p ≅ cechAugmentedColumnProductShortComplex U I p

The fixed-column augmented short complex is the product of the augmented section short complexes.

Equations

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

theorem CategoryTheory.Sheaf.cechColumnAugmentationShortComplex_exact {C : Type u} [Category.{a, 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 : ℕ) : (cechColumnAugmentationShortComplex U I p).Exact

theorem CategoryTheory.Sheaf.cechInjectiveColumnAugmentation_f_zero_mono {C : Type u} [Category.{a, 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 : ℕ) : Mono ((cechInjectiveColumnAugmentation U I ↑p).f 0)

theorem CategoryTheory.Sheaf.cechAugmentationSourceColumn_d_neg_one_zero {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (p : ℕ) : ((cechInjectiveBicomplexAugmentationSource U F).X ↑p).d (-1) 0 = 0

theorem CategoryTheory.Sheaf.cechInjectiveColumn_d_neg_one_zero {C : Type u} [Category.{a, 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).X ↑p).d (-1) 0 = 0

instance CategoryTheory.Sheaf.cechInjectiveColumnAugmentation_quasiIsoAt_zero {C : Type u} [Category.{a, 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 : ℕ) : QuasiIsoAt (cechInjectiveColumnAugmentation U I ↑p) 0

The augmentation is a quasi-isomorphism in vertical degree zero in every nonnegative Cech degree.

noncomputable def CategoryTheory.Sheaf.cechInjectiveColumnAugmentationHomologyIso {C : Type u} [Category.{a, 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 : ℕ) : ((cechInjectiveBicomplexAugmentationSource U F).X ↑p).homology 0 ≅ ((cechInjectiveBicomplex U I).X ↑p).homology 0

Zeroth vertical homology of the augmentation source and the injective bicomplex agree.

Equations

• CategoryTheory.Sheaf.cechInjectiveColumnAugmentationHomologyIso U I p = isoOfQuasiIsoAt (CategoryTheory.Sheaf.cechInjectiveColumnAugmentation U I ↑p) 0

noncomputable def CategoryTheory.Sheaf.cechAugmentationSourceColumnIsoSingle {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} (U : index → C) (F : Sheaf J AddCommGrpCat) (p : ℤ) : (cechInjectiveBicomplexAugmentationSource U F).X p ≅ (CochainComplex.singleFunctor AddCommGrpCat 0).obj (((cechCochainFunctorInt U).obj F).X p)

A column of the augmentation source is the single complex concentrated in vertical degree zero on the corresponding term of the integer-extended Cech complex.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechAugmentationSourceColumnHomologyIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} (U : index → C) (F : Sheaf J AddCommGrpCat) (p : ℤ) : ((cechInjectiveBicomplexAugmentationSource U F).X p).homology 0 ≅ ((cechCochainFunctorInt U).obj F).X p

Zeroth homology of an augmentation-source column is its ordinary Cech term.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowXIso {C : Type u} [Category.{a, 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 : ℕ) : ((cechInjectiveSpectralSequence U I).page 2 cechInjectiveInitialPageZeroRowXIso._proof_1).X (↑p, 0) ≅ ((cechCochainFunctorInt U).obj F).X ↑p

The degree-zero row of the initial Cech-injective page has the same objects as the ordinary Cech complex.

Equations

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

theorem CategoryTheory.Sheaf.cechAugmentationSourceColumn_d_square {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} (U : index → C) (F : Sheaf J AddCommGrpCat) (p : ℤ) : CategoryStruct.comp ((cechInjectiveBicomplexAugmentationSource U F).d p (p + 1)) (cechAugmentationSourceColumnIsoSingle U F (p + 1)).hom = CategoryStruct.comp (cechAugmentationSourceColumnIsoSingle U F p).hom ((CochainComplex.singleFunctor AddCommGrpCat 0).map (((cechCochainFunctorInt U).obj F).d p (p + 1)))

The horizontal differential on the augmentation source is the ordinary Cech differential under the single-complex identifications of its columns.

theorem CategoryTheory.Sheaf.cechAugmentationSourceColumnHomologyIso_naturality {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} (U : index → C) (F : Sheaf J AddCommGrpCat) (p : ℤ) : CategoryStruct.comp (HomologicalComplex.homologyMap ((cechInjectiveBicomplexAugmentationSource U F).d p (p + 1)) 0) (cechAugmentationSourceColumnHomologyIso U F (p + 1)).hom = CategoryStruct.comp (cechAugmentationSourceColumnHomologyIso U F p).hom (((cechCochainFunctorInt U).obj F).d p (p + 1))

On zeroth homology, the augmentation-source horizontal map is the ordinary Cech differential.

theorem CategoryTheory.Sheaf.cechInjectiveColumnAugmentationHomologyIso_horizontal {C : Type u} [Category.{a, 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 : ℕ) : CategoryStruct.comp (HomologicalComplex.homologyMap ((cechInjectiveBicomplex U I).d (↑p) (↑p + 1)) 0) (cechInjectiveColumnAugmentationHomologyIso U I (p + 1)).inv = CategoryStruct.comp (cechInjectiveColumnAugmentationHomologyIso U I p).inv (HomologicalComplex.homologyMap ((cechInjectiveBicomplexAugmentationSource U F).d (↑p) (↑p + 1)) 0)

The augmentation isomorphisms intertwine the horizontal maps on zeroth vertical homology.

theorem CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRow_d {C : Type u} [Category.{a, 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 : ℕ) : CategoryStruct.comp (((cechInjectiveSpectralSequence U I).page 2 cechInjectiveInitialPageZeroRowXIso._proof_1).d (↑p, 0) (↑(p + 1), 0)) (cechInjectiveInitialPageZeroRowXIso U I (p + 1)).hom = CategoryStruct.comp (cechInjectiveInitialPageZeroRowXIso U I p).hom (((cechCochainFunctorInt U).obj F).d (↑p) (↑p + 1))

The first differential on the degree-zero row of the Cech-injective spectral sequence is the ordinary Cech differential.

noncomputable def CategoryTheory.Sheaf.cechInitialPageZeroRowEmbedding : (ComplexShape.up ℤ).Embedding ((fun (r : ℤ) => ComplexShape.up' (r - 1, 2 - r)) 2)

The embedding of the integer-graded degree-zero row into the bidegrees of the initial spectral-sequence page.

Equations

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

instance CategoryTheory.Sheaf.instIsRelIffIntProdCechInitialPageZeroRowEmbedding : cechInitialPageZeroRowEmbedding.IsRelIff

noncomputable def CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRow {C : Type u} [Category.{a, 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 degree-zero row of the initial Cech-injective page, with its inherited horizontal differential.

Equations

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

theorem CategoryTheory.Sheaf.isZero_cechInjectiveInitialPage_of_negative_cech_degree {C : Type u} [Category.{a, 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 : ℤ) (hp : p < 0) : Limits.IsZero (((cechInjectiveSpectralSequence U I).page 2 cechInjectiveInitialPageZeroRowXIso._proof_1).X (p, q))

Initial-page entries in a negative Cech degree vanish.

noncomputable def CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowXIsoInt {C : Type u} [Category.{a, 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 : ℤ) : (cechInjectiveInitialPageZeroRow U I).X p ≅ ((cechCochainFunctorInt U).obj F).X p

Every object of the integer-graded degree-zero row is the corresponding object of the integer-extended ordinary Cech complex.

Equations

• CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowXIsoInt U I p = if hp : 0 ≤ p then ⋯.mpr (CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowXIso U I p.toNat) else ⋯.iso ⋯

noncomputable def CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowIso {C : Type u} [Category.{a, u} C] {J : GrothendieckTopology C} [Limits.HasFiniteProducts C] [HasSheafify J AddCommGrpCat] {index : Type a} {F : Sheaf J AddCommGrpCat} (U : index → C) (I : InjectiveResolution F) : cechInjectiveInitialPageZeroRow U I ≅ (cechCochainFunctorInt U).obj F

The degree-zero row of the initial page, including its differential, is the ordinary Cech complex extended by zero from natural to integer degrees.

Equations

• CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowIso U I = HomologicalComplex.Hom.isoOfComponents (CategoryTheory.Sheaf.cechInjectiveInitialPageZeroRowXIsoInt U I) ⋯

noncomputable def CategoryTheory.Sheaf.cechInjectiveFollowingPageCechCohomologyIso {C : Type u} [Category.{a, 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 : ℕ) : ((cechInjectiveSpectralSequence U I).page 3 cechInjectiveFollowingPageCechCohomologyIso._proof_1).X (↑p, 0) ≅ cechCohomology U F.obj p

The page following the initial Cech-injective page is ordinary Cech cohomology along the degree-zero row.

Equations

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