Short exact coefficient sequences and Čech acyclicity

The Čech complex preserves short exact sequences of presheaves when the coefficient category has products and its products of the required sizes are exact. The exactness requirement is automatic for finite families in an abelian category, and for arbitrary families of abelian groups. Exactness is tested in the presheaf values before sheafification, only at the objects specified below. For finite families, the exact-product hypothesis is supplied by locally enabling Abelian.hasFiniteBiproducts.

Only the values at finite products of members matter: a sequence of presheaves that is short exact after evaluation at each such product has a short exact sequence of Čech complexes (shortExact_map_cechComplexFunctor). For an open cover, this asks for exactness only on the finite intersections of members.

For a coefficient sequence that is short exact at the terminal object and at the finite products of members, acyclicity of its middle and right terms implies acyclicity of its left term. This is the coefficient-sequence descent used when iterating Mayer-Vietoris sequences for Laurent covers: the middle term is the pair of restrictions and the right term is the restriction to the intersection.

The comparison uses HomologicalComplex.HomologySequence.quasiIso_τ₁ for the morphism of short exact sequences induced by the augmentations.

Shifting dimension along such sequences gives Čech acyclicity from a resolution. If 0 ⟶ P ⟶ K⁰ ⟶ K¹ ⟶ ⋯ is a sequence of presheaves which is exact at the terminal object and at the finite products of members, and every Kᵏ is acyclic, then P is acyclic (quasiIso_cechAugmentation_of_resolution). The resolution splits into sequences of presheaves of cycles, short exact at those objects, and in each of them the augmented Čech complexes of the left and right terms agree up to a shift of one degree, by the degreewise lemmas HomologicalComplex.HomologySequence.isIso_homologyMap_τ₁ and HomologicalComplex.HomologySequence.mono_homologyMap_τ₁.

Main results

• TauCeti.CategoryTheory.preservesLimitsOfShape_cechComplexFunctor: the Čech complex functor preserves every limit that exists in the coefficient category.
• TauCeti.CategoryTheory.shortExact_map_cechComplexFunctor: a sequence of presheaves short exact at the finite products of members has a short exact sequence of Čech complexes.
• TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_shortExact: for a coefficient sequence short exact at the terminal object and at finite products of members, acyclicity of the middle and right terms implies acyclicity of the left term.
• TauCeti.CategoryTheory.quasiIso_cechAugmentation_X₃_of_shortExact: for such a coefficient sequence, acyclicity of the left and middle terms implies acyclicity of the right term.
• TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_resolution: a presheaf with a resolution by acyclic presheaves, exact at the terminal object and at the finite products of members, is acyclic.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Appendix A and Lemma 8.34(i).

instance TauCeti.CategoryTheory.preservesLimitsOfShape_cechComplexFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) (J : Type u_1) [CategoryTheory.Category.{u_2, u_1} J] [CategoryTheory.Limits.HasLimitsOfShape J A] : CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.cechComplexFunctor U)

The Čech complex functor preserves every limit that exists in the coefficient category: in each degree it is a product of evaluations, and limits commute with products and evaluations.

instance TauCeti.CategoryTheory.preservesFiniteLimits_cechComplexFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) [CategoryTheory.Limits.HasFiniteLimits A] : CategoryTheory.Limits.PreservesFiniteLimits (CategoryTheory.cechComplexFunctor U)

The Čech complex functor preserves finite limits.

instance TauCeti.CategoryTheory.preservesFiniteColimits_cechComplexFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Preadditive A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) [CategoryTheory.Limits.HasFiniteColimits A] [∀ (n : ℕ), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) A] : CategoryTheory.Limits.PreservesFiniteColimits (CategoryTheory.cechComplexFunctor U)

With exact products, the Čech complex functor preserves finite colimits.

theorem TauCeti.CategoryTheory.shortExact_map_cechComplexFunctor {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Abelian A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) [∀ (n : ℕ), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) A] (S : CategoryTheory.ShortComplex (CategoryTheory.Functor Cᵒᵖ A)) (hS : ∀ (n : ℕ) (a : Fin (n + 1) → ι), (S.map ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op (∏ᶜ fun (j : Fin (n + 1)) => U (a j))))).ShortExact) : (S.map (CategoryTheory.cechComplexFunctor U)).ShortExact

The Čech complexes of a coefficient sequence that is short exact on the members. If a sequence of presheaves becomes short exact after evaluation at every finite product U (a 0) × ⋯ × U (a n) of members of the family U, then its sequence of Čech complexes for U is short exact. No exactness is required at other objects: for an open cover, only the intersections of members matter.

theorem TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Abelian A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) [∀ (n : ℕ), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) A] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (S : CategoryTheory.ShortComplex (CategoryTheory.Functor Cᵒᵖ A)) (hST : (S.map ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op T))).ShortExact) (hSU : ∀ (n : ℕ) (a : Fin (n + 1) → ι), (S.map ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op (∏ᶜ fun (j : Fin (n + 1)) => U (a j))))).ShortExact) (h₂ : QuasiIso (cechAugmentation U hT S.X₂)) (h₃ : QuasiIso (cechAugmentation U hT S.X₃)) : QuasiIso (cechAugmentation U hT S.X₁)

Čech acyclicity descends to the kernel of a locally short exact coefficient sequence. If a sequence of presheaves is short exact at the terminal object and at every finite product of members of U, and U is acyclic for the middle and right presheaves, then U is acyclic for the left presheaf as well. Exactness at other objects is not required.

theorem TauCeti.CategoryTheory.quasiIso_cechAugmentation_X₃_of_shortExact {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Abelian A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) [∀ (n : ℕ), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) A] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) (S : CategoryTheory.ShortComplex (CategoryTheory.Functor Cᵒᵖ A)) (hST : (S.map ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op T))).ShortExact) (hSU : ∀ (n : ℕ) (a : Fin (n + 1) → ι), (S.map ((CategoryTheory.evaluation Cᵒᵖ A).obj (Opposite.op (∏ᶜ fun (j : Fin (n + 1)) => U (a j))))).ShortExact) (h₁ : QuasiIso (cechAugmentation U hT S.X₁)) (h₂ : QuasiIso (cechAugmentation U hT S.X₂)) : QuasiIso (cechAugmentation U hT S.X₃)

Čech acyclicity passes to the cokernel of a locally short exact coefficient sequence. If a sequence of presheaves is short exact at the terminal object and at every finite product of members of U, and U is acyclic for the left and middle presheaves, then U is acyclic for the right presheaf as well. Exactness at other objects is not required.

Acyclic resolutions

For a sequence of presheaves 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0 that is short exact at T and at the finite products of members, with X₂ acyclic, the augmented Čech complexes of X₁ and X₃ agree up to a shift by one degree. Along the short exact sequences of cycles of a resolution by acyclic presheaves, this shows that the resolved presheaf is acyclic.

theorem TauCeti.CategoryTheory.quasiIso_cechAugmentation_of_resolution {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteProducts C] {A : Type u'} [CategoryTheory.Category.{v', u'} A] [CategoryTheory.Abelian A] [CategoryTheory.Limits.HasProducts A] {ι : Type w} (U : ι → C) [∀ (n : ℕ), CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete (Fin (n + 1) → ι)) A] {T : C} (hT : CategoryTheory.Limits.IsTerminal T) {P : CategoryTheory.Functor Cᵒᵖ A} {K : CategoryTheory.Functor Cᵒᵖ (CochainComplex A ℕ)} (ε : P.comp (CochainComplex.single₀ A) ⟶ K) (hεT : QuasiIso (ε.app (Opposite.op T))) (hεU : ∀ (n : ℕ) (a : Fin (n + 1) → ι), QuasiIso (ε.app (Opposite.op (∏ᶜ fun (j : Fin (n + 1)) => U (a j))))) (hK : ∀ (k : ℕ), QuasiIso (cechAugmentation U hT (K.comp (HomologicalComplex.eval A (ComplexShape.up ℕ) k)))) : QuasiIso (cechAugmentation U hT P)

Čech acyclicity from an acyclic resolution. Let ε : P ⋙ single₀ ⟶ K be a morphism from a presheaf P, placed in degree 0, to a presheaf of cochain complexes K, which is a quasi-isomorphism at T and at every finite product of members of the family U: for an open cover, the sequence 0 ⟶ P ⟶ K⁰ ⟶ K¹ ⟶ ⋯ is exact on the whole space and on every finite intersection of members. If every presheaf Kᵏ is acyclic for U, then so is P.