Exactness of sheaves of abelian groups on a basis

A sequence F₁ ⟶ F₂ ⟶ F₃ of sheaves of abelian groups on a topological space is exact as soon as the sequences of sections F₁(V) ⟶ F₂(V) ⟶ F₃(V) are exact for the members V of a basis of the topology (TopCat.Sheaf.exact_of_isBasis). Exactness of sheaves is exactness on stalks (TopCat.Sheaf.exact_iff_stalkFunctor_map_exact), and every stalk is a filtered colimit of sections over basic open neighbourhoods. The converse fails: exactness of sheaves only says that a section of F₂ killed by F₂ ⟶ F₃ comes from F₁ locally.

This is how a sheaf defined as the homology of a complex of sheaves is shown to vanish, for instance a higher direct image computed from an injective resolution: it suffices that the complexes of sections are exact over a basis, where they compute sheaf cohomology.

In the other direction, an epimorphism of sheaves is only locally surjective on sections: a section of the target lifts near every point, on a member of any set of opens which contains a basis inside each of its members (TopCat.Sheaf.exists_mem_lift_of_epi).

References

• R. Hartshorne, Algebraic Geometry, GTM 52, Springer, 1977, Exercise II.1.2.

theorem TopCat.Sheaf.exact_of_isBasis {X : TopCat} {S : CategoryTheory.ShortComplex (CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat)} {B : Set (TopologicalSpace.Opens ↑X)} (hB : TopologicalSpace.Opens.IsBasis B) (h : ∀ V ∈ B, ∀ (s : ↑(S.X₂.obj.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (S.g.hom.app (Opposite.op V))) s = 0 → ∃ (t : ↑(S.X₁.obj.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (S.f.hom.app (Opposite.op V))) t = s) : S.Exact

A sequence of sheaves of abelian groups is exact when the sequences of its sections over the members of a basis of the topology are exact: every section of F₂ over a basic open killed by F₂ ⟶ F₃ comes from a section of F₁.

theorem TopCat.Sheaf.exists_mem_lift_of_epi {X : TopCat} {B : Set (TopologicalSpace.Opens ↑X)} (hbasis : ∀ U ∈ B, ∀ V ≤ U, ∀ x ∈ V, ∃ W ∈ B, x ∈ W ∧ W ≤ V) {F G : CategoryTheory.Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat} (π : F ⟶ G) [CategoryTheory.Epi π] {Y : TopologicalSpace.Opens ↑X} (hY : Y ∈ B) (s : ↑(G.obj.obj (Opposite.op Y))) (x : ↑X) (hx : x ∈ Y) : ∃ V ∈ B, x ∈ V ∧ ∃ (h : V ≤ Y) (t : ↑(F.obj.obj (Opposite.op V))), (CategoryTheory.ConcreteCategory.hom (π.hom.app (Opposite.op V))) t = (CategoryTheory.ConcreteCategory.hom (G.obj.map (CategoryTheory.homOfLE h).op)) s

Let B be a set of opens containing, inside each of its members, a basis of the topology of that member. Along an epimorphism of sheaves π : F ⟶ G, a section of G over a member Y of B lifts, near every point of Y, on a member of B contained in Y.