The sheaf condition for one presieve, for presheaves of abelian groups

For a presheaf P with values in an arbitrary category, the sheaf condition for a presieve R is expressed through the presheaves of types P ⋙ coyoneda.obj E (as in Presheaf.IsSheaf, or in Presheaf.isLimit_iff_isSheafFor_presieve). For a presheaf of abelian groups this is the same as the sheaf condition for R on the underlying presheaf of sets: a compatible family of homomorphisms out of E glues pointwise, and the glued map is additive because restriction to the members of R is jointly injective. Mathlib's Presheaf.isSheaf_iff_isSheaf_forget is the analogous statement for all covering sieves of a Grothendieck topology at once.

Main results

• CategoryTheory.Presieve.isSheafFor_comp_forget_addCommGrpCat_iff: a presheaf of abelian groups satisfies the sheaf condition for a presieve R against every abelian group exactly when its underlying presheaf of sets satisfies the sheaf condition for R.

theorem CategoryTheory.Presieve.isSheafFor_comp_forget_addCommGrpCat_iff {C : Type u} [Category.{v, u} C] {X : C} (R : Presieve X) (P : Functor Cᵒᵖ AddCommGrpCat) : IsSheafFor (P.comp (forget AddCommGrpCat)) R ↔ ∀ (E : AddCommGrpCatᵒᵖ), IsSheafFor (P.comp (coyoneda.obj E)) R

The sheaf condition for a presheaf of abelian groups is checked on underlying sets. A presheaf P of abelian groups satisfies the sheaf condition for a presieve R on the underlying presheaf of sets exactly when, for every abelian group E, the presheaf of homomorphisms P ⋙ coyoneda.obj E satisfies it.