The Cech-to-total comparison

This file proves the first-quadrant comparison theorem for the Cech bicomplex of an explicit injective resolution. If the sheaf is acyclic on every nonempty finite intersection in the Cech nerve, the augmentation from its ordinary Cech complex to the total injective Cech complex is a quasi-isomorphism.

theorem CategoryTheory.Sheaf.cechInjectiveColumnAugmentation_quasiIso {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) [HasExt (Sheaf J AddCommGrpCat)] (hacyclic : IsCechAcyclicFor U F) (p : ℕ) : QuasiIso (cechInjectiveColumnAugmentation U I ↑p)

Under local Cech acyclicity, the augmentation of every nonnegative Cech column is a quasi-isomorphism.

theorem CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentationSource_verticallyConnective {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) : (cechInjectiveBicomplexAugmentationSource U F).IsVerticallyConnective

The augmentation source is supported in nonnegative vertical degrees.

theorem CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentationSource_horizontallyConnective {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) : (cechInjectiveBicomplexAugmentationSource U F).IsHorizontallyConnective

The augmentation source is supported in nonnegative Cech degrees.

theorem CategoryTheory.Sheaf.cechInjectiveBicomplex_verticallyConnective {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) : (cechInjectiveBicomplex U I).IsVerticallyConnective

The injective Cech bicomplex is supported in nonnegative resolution degrees.

theorem CategoryTheory.Sheaf.cechInjectiveBicomplex_horizontallyConnective {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) : (cechInjectiveBicomplex U I).IsHorizontallyConnective

The injective Cech bicomplex is supported in nonnegative Cech degrees.

theorem CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentation_total_quasiIso {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) [HasExt (Sheaf J AddCommGrpCat)] (hacyclic : IsCechAcyclicFor U F) : QuasiIso (HomologicalComplex₂.total.map (cechInjectiveBicomplexAugmentation U I) (ComplexShape.up ℤ))

Under local Cech acyclicity, the total augmentation is a quasi-isomorphism.

noncomputable def CategoryTheory.Sheaf.cechInjectiveBicomplexAugmentationSourceTotalIso {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) : (cechInjectiveBicomplexAugmentationSource U F).total (ComplexShape.up ℤ) ≅ (cechCochainFunctorInt U).obj F

The total of the Cech complex placed in vertical degree zero is canonically the ordinary integer-extended Cech complex.

Equations

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

noncomputable def CategoryTheory.Sheaf.cechToInjectiveTotalMap {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) : (cechCochainFunctorInt U).obj F ⟶ cechInjectiveTotalComplex U I

The comparison map from the ordinary Cech complex to the total Cech complex of an explicit injective resolution.

Equations

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

theorem CategoryTheory.Sheaf.cechToInjectiveTotalMap_quasiIso {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) [HasExt (Sheaf J AddCommGrpCat)] (hacyclic : IsCechAcyclicFor U F) : QuasiIso (cechToInjectiveTotalMap U I)

On a Cech-acyclic family, the comparison from the ordinary Cech complex to the injective Cech total complex is a quasi-isomorphism.

noncomputable def CategoryTheory.Sheaf.cechCohomologyIsoInjectiveTotalHomology {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) [HasExt (Sheaf J AddCommGrpCat)] (hacyclic : IsCechAcyclicFor U F) (n : ℤ) : HomologicalComplex.homology ((cechCochainFunctorInt U).obj F) n ≅ HomologicalComplex.homology (cechInjectiveTotalComplex U I) n

Degreewise homology comparison between the ordinary Cech complex and the injective Cech total complex on a Cech-acyclic family.

Equations

• CategoryTheory.Sheaf.cechCohomologyIsoInjectiveTotalHomology U I hacyclic n = isoOfQuasiIsoAt (CategoryTheory.Sheaf.cechToInjectiveTotalMap U I) n