Checking the sheaf condition on the underlying presheaf of types.

If G : C ⥤ D is a functor which reflects isomorphisms and preserves limits (we assume all limits exist in C), then checking the sheaf condition for a presheaf F : presheaf C X is equivalent to checking the sheaf condition for F ⋙ G.

The important special case is when C is a concrete category with a forgetful functor that preserves limits and reflects isomorphisms. Then to check the sheaf condition it suffices to check it on the underlying sheaf of types.

References

• https://stacks.math.columbia.edu/tag/0073

theorem TopCat.Presheaf.isSheaf_iff_isSheaf_comp' {C : Type u₁} [CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasLimitsOfSize.{v, v, v₁, u₁} C] [CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, v₁, v₂, u₁, u₂} G] {X : TopCat} (F : TopCat.Presheaf C X) : TopCat.Presheaf.IsSheaf F ↔ TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp F G)

If G : C ⥤ D is a functor which reflects isomorphisms and preserves limits (we assume all limits exist in C), then checking the sheaf condition for a presheaf F : presheaf C X is equivalent to checking the sheaf condition for F ⋙ G.

The important special case is when C is a concrete category with a forgetful functor that preserves limits and reflects isomorphisms. Then to check the sheaf condition it suffices to check it on the underlying sheaf of types.

Another useful example is the forgetful functor TopCommRing ⥤ Top.

See . In fact we prove a stronger version with arbitrary target category.

theorem TopCat.Presheaf.isSheaf_iff_isSheaf_comp {C : Type u₁} [CategoryTheory.Category.{v, u₁} C] {D : Type u₂} [CategoryTheory.Category.{v, u₂} D] (G : CategoryTheory.Functor C D) [CategoryTheory.ReflectsIsomorphisms G] [CategoryTheory.Limits.HasLimits C] [CategoryTheory.Limits.PreservesLimits G] {X : TopCat} (F : TopCat.Presheaf C X) : TopCat.Presheaf.IsSheaf F ↔ TopCat.Presheaf.IsSheaf (CategoryTheory.Functor.comp F G)

As an example, we now have everything we need to check the sheaf condition for a presheaf of commutative rings, merely by checking the sheaf condition for the underlying sheaf of types.

example (X : TopCat) (F : Presheaf CommRingCat X)
    (h : Presheaf.IsSheaf (F ⋙ (forget CommRingCat))) :
    F.IsSheaf :=
(isSheaf_iff_isSheaf_comp (forget CommRingCat) F).mpr h