The augmented Čech complex of a presheaf

Let C be a category with finite products and a terminal object T, let U : ι → C be a family of objects and let P : Cᵒᵖ ⥤ A be a presheaf with values in a preadditive category with products. Mathlib's CategoryTheory.cechComplexFunctor U sends P to its Čech complex Č(U, P), whose degree n term is the product, over a : Fin (n + 1) → ι, of P(U (a 0) × ⋯ × U (a n)). This file constructs the augmentation P(T) ⟶ Č⁰(U, P), as a map of cochain complexes from P(T) placed in degree 0, and characterises when it is a quasi-isomorphism, that is, when the augmented Čech complex 0 ⟶ P(T) ⟶ Č⁰(U, P) ⟶ Č¹(U, P) ⟶ ⋯ is exact. The augmentation is Mathlib's AlgebraicTopology.AlternatingFaceMapComplex.ε for the augmented Čech object FormalCoproduct.cech.augmentOfIsTerminal evaluated at P, transported from Aᵒᵖ to A.

For an open cover U of a topological space X and a presheaf of abelian groups F on X, this is Wedhorn's notion of an F-acyclic cover: the augmentation identifies F(X) with the degree 0 cohomology of Č(U, F), and Č(U, F) has no cohomology in positive degrees. A cover of an open subset W fits this setting in the category Over W, which has finite products and the terminal object Over.mk (𝟙 W) (CategoryTheory.Over.mkIdTerminal).

Main definitions

• TauCeti.CategoryTheory.cechAugmentation U hT P: the augmentation of the Čech complex of P for U; its degree 0 component restricts a section over T along each map to T (TauCeti.CategoryTheory.cechAugmentation_f_zero_comp_π).

Main results

• TauCeti.CategoryTheory.quasiIsoAt_cechAugmentation_zero_iff: the augmentation induces an isomorphism in degree 0 exactly when P satisfies the sheaf condition for the family of maps U i ⟶ T, in Mathlib's form for presheaves with values in A: every P ⋙ coyoneda.obj E is a sheaf for Presieve.ofArrows U.
• TauCeti.CategoryTheory.quasiIso_cechAugmentation_iff: the augmentation is a quasi-isomorphism exactly when P satisfies that sheaf condition and the Čech complex is exact in every positive degree.
• TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_hom: if some U i₀ receives a map from T, for instance if U i₀ = T, then the augmentation is a quasi-isomorphism. This comes from Mathlib's extra degeneracy CategoryTheory.Limits.FormalCoproduct.extraDegeneracyCech of the Čech object, which makes ε a homotopy equivalence (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv).

References

• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Appendix A: Definition A.1 and the acyclicity of a cover having X as a member, stated after Remark A.2.

The Čech complex in degrees 0 and 1

Mathlib's cechComplexFunctor is a composite of several functors, so its terms agree only up to unfolding with the products that define them. The identity isomorphisms cechXIso₀ and cechXIso₁ record these identifications once, so that every later statement composes maps between syntactically equal objects. A 0-cochain is determined by its restrictions restrict to the members U i, and it is killed by the differential Č⁰(U, P) ⟶ Č¹(U, P) exactly when these restrictions agree on the products of pairs of members (comp_d_eq_zero_iff).

The augmented Čech object with values in Aᵒᵖ

Applying P to Mathlib's augmented Čech object FormalCoproduct.cech.augmentOfIsTerminal gives an augmented simplicial object in Aᵒᵖ, whose alternating face map complex is, after passing back to A, the Čech complex of P. Its augmentation AlternatingFaceMapComplex.ε, passed back to A in the same way (singleIso), is the augmentation of the Čech complex.

noncomputable def TauCeti.CategoryTheory.cechAugmentation {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {ι : Type w} (U : ι → C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasZeroObject A] : (CochainComplex.single₀ A).obj (P.obj (Opposite.op T)) ⟶ (CategoryTheory.cechComplexFunctor U).obj P

The augmentation of the Čech complex of P for the family U, as a map of cochain complexes from P(T) placed in degree 0. It is Mathlib's augmentation AlternatingFaceMapComplex.ε of the augmented Čech object evaluated at P, passed from Aᵒᵖ back to A. Its degree 0 component P(T) ⟶ Č⁰(U, P) restricts a section over T along the maps to T (cechAugmentation_f_zero_comp_π). As for CategoryTheory.InjectiveResolution.ι, exactness of the augmented Čech complex 0 ⟶ P(T) ⟶ Č⁰(U, P) ⟶ Č¹(U, P) ⟶ ⋯ is expressed as QuasiIso (cechAugmentation U hT P); quasiIso_cechAugmentation_iff unpacks it into the sheaf condition for the family U i ⟶ T and exactness of the Čech complex in positive degrees.

Equations

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

theorem TauCeti.CategoryTheory.cechAugmentation_f_zero_comp_π {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {ι : Type w} (U : ι → C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasZeroObject A] (a : Fin 1 → ι) : CategoryTheory.CategoryStruct.comp ((cechAugmentation U hT P).f 0) (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := 0 })).I) => P.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := 0 })).obj i))) a) = P.map (hT.from (∏ᶜ fun (j : Fin 1) => U (a j))).op

The degree 0 component of the augmentation, followed by the projection of Č⁰(U, P) onto its factor indexed by a : Fin 1 → ι, is P applied to the map from ∏ᶜ fun j ↦ U (a j) to the terminal object: the augmentation restricts a section over T to each member of the family, seen as a one-fold product.

theorem TauCeti.CategoryTheory.cechAugmentation_f_zero_comp_π_assoc {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {ι : Type w} (U : ι → C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasZeroObject A] (a : Fin 1 → ι) {Z : A} (h : P.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := 0 })).obj a)) ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp ((cechAugmentation U hT P).f 0) (CategoryTheory.Limits.Pi.π (fun (i : (Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := 0 })).I) => P.obj (Opposite.op ((Opposite.unop ((CategoryTheory.Functor.rightOp { I := ι, obj := U }.cech).obj { len := 0 })).obj i))) a)) h = CategoryTheory.CategoryStruct.comp (P.map (hT.from (∏ᶜ fun (j : Fin 1) => U (a j))).op) h

The degree 0 component of the augmentation, followed by the projection of Č⁰(U, P) onto its factor indexed by a : Fin 1 → ι, is P applied to the map from ∏ᶜ fun j ↦ U (a j) to the terminal object: the augmentation restricts a section over T to each member of the family, seen as a one-fold product.

The augmentation in degree 0

The degree 0 component augmentation₀ : P(T) ⟶ Č⁰(U, P) of the augmentation restricts along the maps to T. Since any family of sections over the U i defines a 0-cochain (lift₀), which is killed by the Čech differential exactly when the family is compatible, comp_d_eq_zero_iff shows that augmentation₀ is a kernel of the Čech differential exactly when P satisfies the sheaf condition for the family U i ⟶ T (isLimit_kernelFork_iff_isSheafFor).

theorem TauCeti.CategoryTheory.quasiIsoAt_cechAugmentation_zero_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {ι : Type w} (U : ι → C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.CategoryWithHomology A] : QuasiIsoAt (cechAugmentation U hT P) 0 ↔ ∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) (CategoryTheory.Presieve.ofArrows U fun (i : ι) => hT.from (U i))

The augmentation identifies P(T) with the degree 0 cohomology of the Čech complex (that is, 0 ⟶ P(T) ⟶ Č⁰(U, P) ⟶ Č¹(U, P) is exact) if and only if P satisfies the sheaf condition for the family of maps U i ⟶ T: for every E, the presheaf of types P ⋙ coyoneda.obj E is a sheaf for Presieve.ofArrows U. The condition holds when P is a sheaf (Presheaf.IsSheaf J P) for a topology J in which Sieve.ofArrows U _ covers T (use Presieve.isSheafFor_iff_generate), and Presheaf.isLimit_iff_isSheafFor_presieve expresses it as a limit condition.

theorem TauCeti.CategoryTheory.quasiIso_cechAugmentation_iff {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {ι : Type w} (U : ι → C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.CategoryWithHomology A] : QuasiIso (cechAugmentation U hT P) ↔ (∀ (E : Aᵒᵖ), CategoryTheory.Presieve.IsSheafFor (P.comp (CategoryTheory.coyoneda.obj E)) (CategoryTheory.Presieve.ofArrows U fun (i : ι) => hT.from (U i))) ∧ ∀ (n : ℕ), HomologicalComplex.ExactAt ((CategoryTheory.cechComplexFunctor U).obj P) (n + 1)

The augmentation is a quasi-isomorphism, that is, the augmented Čech complex 0 ⟶ P(T) ⟶ Č⁰(U, P) ⟶ Č¹(U, P) ⟶ ⋯ is exact, if and only if P satisfies the sheaf condition for the family of maps U i ⟶ T and the Čech complex is exact in every positive degree, that is, the Čech cohomology of P for U vanishes in every positive degree. This unpacks acyclicity in the sense of Wedhorn, Adic Spaces, Definition A.1, so that it can be proved or used degree by degree; the degree 0 part alone is quasiIsoAt_cechAugmentation_zero_iff.

theorem TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] {ι : Type w} (U : ι → C) {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (P : CategoryTheory.Functor Cᵒᵖ A) [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] [CategoryTheory.Limits.HasZeroObject A] [CategoryTheory.CategoryWithHomology A] {i₀ : ι} (f : T ⟶ U i₀) : QuasiIso (cechAugmentation U hT P)

If some member U i₀ of the family receives a map f : T ⟶ U i₀ from the terminal object, equivalently if U i₀ ⟶ T is a split epimorphism, then the augmentation of the Čech complex of every presheaf P for U is a quasi-isomorphism: the augmented Čech complex 0 ⟶ P(T) ⟶ Č⁰(U, P) ⟶ Č¹(U, P) ⟶ ⋯ is exact. For an open cover of W, viewed in Over W, such a map exists exactly when W is itself a member of the cover.