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).
A morphism of families U ⟶ V, that is a morphism of formal coproducts, induces a map of Čech
complexes Č(V, P) ⟶ Č(U, P) compatible with the augmentations, and any two morphisms U ⟶ V
induce homotopic maps. For open covers this says that the map on Čech cohomology induced by a
refinement does not depend on the refinement map; in particular, acyclicity of a cover only depends
on the cover up to refinement in both directions, so that members contained in other members may
be added or removed.
Main definitions #
TauCeti.CategoryTheory.cechAugmentation U hT P: the augmentation of the Čech complex ofPforU; its degree0component restricts a section overTalong each map toT(TauCeti.CategoryTheory.cechAugmentation_f_zero_comp_π).TauCeti.CategoryTheory.cechComplexMap P φ: the map of Čech complexesČ(V, P) ⟶ Č(U, P)induced by a morphism of familiesφ : U ⟶ V.TauCeti.CategoryTheory.cechComplexHomologyMap A n φ: the map on degreenČech cohomology induced by a morphism of families, as a natural transformation of functors of the presheaf.
Main results #
TauCeti.CategoryTheory.quasiIsoAt_cechAugmentation_zero_iff: the augmentation induces an isomorphism in degree0exactly whenPsatisfies the sheaf condition for the family of mapsU i ⟶ T, in Mathlib's form for presheaves with values inA: everyP ⋙ coyoneda.obj Eis a sheaf forPresieve.ofArrows U.TauCeti.CategoryTheory.quasiIso_cechAugmentation_iff: the augmentation is a quasi-isomorphism exactly whenPsatisfies that sheaf condition and the Čech complex is exact in every positive degree.TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_hom: if someU i₀receives a map fromT, for instance ifU i₀ = T, then the augmentation is a quasi-isomorphism. This comes from Mathlib's extra degeneracyCategoryTheory.Limits.FormalCoproduct.extraDegeneracyCechof the Čech object, which makesεa homotopy equivalence (SimplicialObject.Augmented.ExtraDegeneracy.homotopyEquiv).TauCeti.CategoryTheory.cechComplexMapHomotopy: any two morphisms of familiesU ⟶ Vinduce homotopic maps of Čech complexes.TauCeti.CategoryTheory.cechComplexMapHomotopy_hom_π: this homotopy is the prism homotopy: its componentČⁿ⁺¹(V, P) ⟶ Čⁿ(U, P)is minus the alternating sum overkof the restrictions from the factors indexed by(φ (a 0), …, φ (a k), ψ (a k), …, ψ (a n)). It is natural in the presheaf (TauCeti.CategoryTheory.cechComplexMapHomotopy_hom_naturality) and compatible with further refinements of either family (TauCeti.CategoryTheory.cechComplexMapHomotopy_precomp_homandTauCeti.CategoryTheory.cechComplexMapHomotopy_postcomp_hom).TauCeti.CategoryTheory.cechComplexHomologyMap_eq: hence any two morphisms of families induce the same map on Čech cohomology.TauCeti.CategoryTheory.cechComplexHomotopyEquiv: families with morphismsU ⟶ VandV ⟶ Uhave homotopy equivalent Čech complexes.TauCeti.CategoryTheory.quasiIso_cechAugmentation_congr: for such families, the augmented Čech complex ofPforUis exact if and only if the one forVis.TauCeti.CategoryTheory.isIso_cechComplexMap: a morphism of families that is the identity on indices induces an isomorphism of Čech complexes whenPinverts the induced maps of products.TauCeti.CategoryTheory.cechAugmentation_naturality: the augmentation is natural inP.TauCeti.CategoryTheory.cechComplexMap_naturality: the map induced by a morphism of families is natural inP.TauCeti.CategoryTheory.quasiIso_cechAugmentation_iff_of_iso: acyclicity of a family is invariant under isomorphisms of presheaves.TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_retract: acyclicity of a family passes to retracts of presheaves.TauCeti.CategoryTheory.cechComplexFunctor_map_f: a morphism of presheaves acts on the Čech complexes factorwise; in particularCategoryTheory.cechComplexFunctor Uis additive.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Appendix A: Definition A.1 and
the acyclicity of a cover having
Xas a member, stated after Remark A.2. - R. Hartshorne, Algebraic Geometry, Graduate Texts in Mathematics 52, Springer, 1977, Exercise III.4.4, for the independence of the map induced by a refinement from the refinement map.
- The Stacks Project, Cohomology of Sheaves, §20.15 (tag 09UY) for refinement maps, and the computation following equation (20.25.0.2) in §20.25 for the prism homotopy and its sign.
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.
The differential #
The differential of the Čech complex is the alternating sum of the restrictions along the
coface maps: the factor of ((cechComplexFunctor U).obj P).d n (n + 1) indexed by
k : Fin (n + 2) → ι is the alternating sum over m of the factor indexed by k ∘ m.succAbove,
restricted along the projection U (k 0) × ⋯ × U (k (n + 1)) ⟶ ∏ⱼ U (k (m.succAbove j)).
The differential of the Čech complex is the alternating sum of the restrictions along the
coface maps: the factor of ((cechComplexFunctor U).obj P).d n (n + 1) indexed by
k : Fin (n + 2) → ι is the alternating sum over m of the factor indexed by k ∘ m.succAbove,
restricted along the projection U (k 0) × ⋯ × U (k (n + 1)) ⟶ ∏ⱼ U (k (m.succAbove j)).
Maps of presheaves #
A morphism of presheaves α : P ⟶ Q acts on the Čech complexes factorwise: the factor of
((cechComplexFunctor U).map α).f n indexed by a is the component of α at
U (a 0) × ⋯ × U (a n).
A morphism of presheaves α : P ⟶ Q acts on the Čech complexes factorwise: the factor of
((cechComplexFunctor U).map α).f n indexed by a is the component of α at
U (a 0) × ⋯ × U (a n).
The degree n component of (cechComplexFunctor U).map α is the product of the components of
α at the products U (a 0) × ⋯ × U (a n).
The Čech complex is additive in the presheaf, since a morphism of presheaves acts on it factorwise.
Maps of families #
A morphism φ from the family U to a family V : κ → C, as a morphism of formal coproducts,
consists of a map φ.f : ι → κ of indices and morphisms φ.φ i : U i ⟶ V (φ.f i); for open covers
it is a refinement map. It induces a map of Čech complexes Č(V, P) ⟶ Č(U, P)
(cechComplexMap). Any two morphisms U ⟶ V induce homotopic maps (cechComplexMapHomotopy),
because they induce simplicially homotopic maps of Čech nerves
(CategoryTheory.Arrow.mapCechNerveHomotopy).
The map of Čech complexes Č(V, P) ⟶ Č(U, P) induced by a morphism φ from the family U
to the family V. In degree n it sends the factor P(V (b 0) × ⋯ × V (b n)) indexed by
b = φ.f ∘ a to the factor P(U (a 0) × ⋯ × U (a n)) by restriction along the product of the
φ.φ (a j) (cechComplexMap_f_π).
Instances For
The factor of (cechComplexMap P φ).f n indexed by a is the factor of Č(V, P) indexed by
φ.f ∘ a, restricted along the product of the morphisms φ.φ (a j).
The identity morphism of a family induces the identity of its Čech complex.
cechComplexMap is contravariantly functorial in the morphism of families.
cechComplexMap is natural in the presheaf: for α : P ⟶ Q, applying α and then
restricting along a morphism of families is restricting and then applying α.
cechComplexMap is natural in the presheaf: for α : P ⟶ Q, applying α and then
restricting along a morphism of families is restricting and then applying α.
A morphism of families which is the identity on indices, given by morphisms
φ i : U i ⟶ W i, induces an isomorphism of Čech complexes Č(W, P) ⟶ Č(U, P) as soon as P
turns each induced morphism U (a 0) × ⋯ × U (a n) ⟶ W (a 0) × ⋯ × W (a n) into an
isomorphism.
Any two morphisms of families induce homotopic maps of Čech complexes. For morphisms
φ ψ from the family U to the family V, for instance two refinement maps between open covers,
the maps Č(V, P) ⟶ Č(U, P) they induce are homotopic.
Instances For
The prism homotopy #
The component Čⁿ⁺¹(V, P) ⟶ Čⁿ(U, P) of cechComplexMapHomotopy P φ ψ is the alternating sum
over k of the restrictions from the factors indexed by the prism tuples
(φ (a 0), …, φ (a k), ψ (a k), …, ψ (a n)), with an overall minus sign
(cechComplexMapHomotopy_hom_π). As a homotopy from cechComplexMap P φ to
cechComplexMap P ψ in Mathlib's convention f - g = d h + h d, it says that the alternating sum
h of these restrictions, listing φ before ψ, satisfies T_ψ - T_φ = δ h + h δ for the maps
T_φ and T_ψ induced by the two refinement maps. The homotopy is natural in the presheaf
(cechComplexMapHomotopy_hom_naturality) and compatible with further refinements on both sides
(cechComplexMapHomotopy_precomp_hom and cechComplexMapHomotopy_postcomp_hom).
The prism formula. The factor indexed by a : Fin (n + 1) → ι of the component
Čⁿ⁺¹(V, P) ⟶ Čⁿ(U, P) of the homotopy cechComplexMapHomotopy P φ ψ is minus the alternating
sum over k of the factor of Čⁿ⁺¹(V, P) indexed by the prism tuple
(φ.f (a 0), …, φ.f (a k), ψ.f (a k), …, ψ.f (a n)), restricted along the morphism of products
given by φ.φ on its first k + 1 factors and by ψ.φ on the others.
The prism formula. The factor indexed by a : Fin (n + 1) → ι of the component
Čⁿ⁺¹(V, P) ⟶ Čⁿ(U, P) of the homotopy cechComplexMapHomotopy P φ ψ is minus the alternating
sum over k of the factor of Čⁿ⁺¹(V, P) indexed by the prism tuple
(φ.f (a 0), …, φ.f (a k), ψ.f (a k), …, ψ.f (a n)), restricted along the morphism of products
given by φ.φ on its first k + 1 factors and by ψ.φ on the others.
The homotopy cechComplexMapHomotopy is natural in the presheaf: its components commute with
the maps of Čech complexes induced by a morphism of presheaves α : P ⟶ Q.
The homotopy cechComplexMapHomotopy is natural in the presheaf: its components commute with
the maps of Čech complexes induced by a morphism of presheaves α : P ⟶ Q.
Compatibility of the homotopy with a further refinement of the source. For a morphism of
families χ : W ⟶ U, the homotopy between the maps induced by χ ≫ φ and χ ≫ ψ is the homotopy
between the maps induced by φ and ψ, followed by the map induced by χ.
Compatibility of the homotopy with a further refinement of the target. For a morphism of
families ω : V ⟶ V', the homotopy between the maps induced by φ ≫ ω and ψ ≫ ω is the map
induced by ω followed by the homotopy between the maps induced by φ and ψ.
The map on degree n Čech cohomology induced by a morphism of families φ : U ⟶ V, for open
covers a refinement map, as a natural transformation of functors of the presheaf: its component
at P is the map Hⁿ(Č(V, P)) ⟶ Hⁿ(Č(U, P)) induced by cechComplexMap P φ.
Instances For
The component of cechComplexHomologyMap A n φ at P is the map on homology induced by
cechComplexMap P φ.
Any two morphisms of families induce the same map on Čech cohomology. For open covers: the map on Čech cohomology induced by a refinement does not depend on the refinement map.
The identity morphism of a family induces the identity on Čech cohomology.
cechComplexHomologyMap is contravariantly functorial in the morphism of families.
Families that map to each other have homotopy equivalent Čech complexes. Given morphisms
of families φ : U ⟶ V and ψ : V ⟶ U, for instance two open covers each refining the other, the
induced maps Č(V, P) ⟶ Č(U, P) and Č(U, P) ⟶ Č(V, P) are mutually inverse homotopy
equivalences.
Instances For
The forward map of cechComplexHomotopyEquiv P φ ψ is the map induced by φ.
The backward map of cechComplexHomotopyEquiv P φ ψ is the map induced by ψ.
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.
Instances For
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 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 augmentations of the Čech complexes are compatible with the maps induced by morphisms of
families: restricting a section over T to the members of V and then to the members of U
restricts it to the members of U.
The augmentations of the Čech complexes are compatible with the maps induced by morphisms of
families: restricting a section over T to the members of V and then to the members of U
restricts it to the members of U.
The augmentation is natural in the presheaf: for α : P ⟶ Q, restricting a section of P
over T to the members of the family and then applying α is applying α over T and then
restricting.
The augmentation is natural in the presheaf: for α : P ⟶ Q, restricting a section of P
over T to the members of the family and then applying α is applying α over T and then
restricting.
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).
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.
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.
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.
Acyclicity of the Čech complex depends only on the family up to maps both ways. If there
are morphisms of families U ⟶ V and V ⟶ U, for instance if U and V are open covers each
refining the other, then the augmented Čech complex of P for U is exact if and only if the one
for V is.
Acyclicity of a family is invariant under isomorphisms of presheaves. If P ≅ Q, then the
augmented Čech complex of P for U is exact if and only if the one for Q is.
Acyclicity passes to retracts of presheaves. If P is a retract of Q and the augmented
Čech complex of Q for U is exact, then so is the one of P: by naturality, the augmentation of
P is a retract of the augmentation of Q.