The image sequence of the embedding of a sheaf into an injective sheaf

Let F be a sheaf of abelian groups on a topological space X, embedded into the chosen injective sheaf I with cokernel sheaf Q. The cokernel sequence 0 ⟶ F ⟶ I ⟶ Q ⟶ 0 is exact as a sequence of sheaves, but not on sections: I(V) ⟶ Q(V) need not be onto. Replacing Q by the image presheaf G of I ⟶ Q gives a sequence 0 ⟶ F ⟶ I ⟶ G ⟶ 0 of presheaves which is exact on the sections over every open. Dimension-shifting arguments comparing Čech cohomology with sheaf cohomology apply the long exact Čech sequence to it.

Main definitions

• CategoryTheory.Sheaf.injectiveImageSequence F: the sequence 0 ⟶ F ⟶ I ⟶ G ⟶ 0 of presheaves.

Main results

• CategoryTheory.Sheaf.injectiveImageSequence_map_shortExact: this sequence is exact on the sections over every open.

@[reducible, inline]

noncomputable abbrev CategoryTheory.Sheaf.injectiveImageSequence {X : TopCat} (F : Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) : ShortComplex (Functor (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat)

The sequence of presheaves 0 ⟶ F ⟶ I ⟶ G ⟶ 0, where F ⟶ I is the chosen embedding into an injective sheaf and G is the image presheaf of I ⟶ Q, for Q its cokernel sheaf. Unlike the cokernel sequence of sheaves, it is exact on the sections over every open (CategoryTheory.Sheaf.injectiveImageSequence_map_shortExact).

theorem CategoryTheory.Sheaf.injectiveImageSequence_map_shortExact {X : TopCat} (F : Sheaf (Opens.grothendieckTopology ↑X) AddCommGrpCat) (V : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (F.injectiveImageSequence.map ((evaluation (TopologicalSpace.Opens ↑X)ᵒᵖ AddCommGrpCat).obj V)).ShortExact

The sequence 0 ⟶ F ⟶ I ⟶ G ⟶ 0 is exact on every open: the kernel of I(V) ⟶ Q(V) is F(V), and G(V) is the image of I(V) in Q(V).