feat(topology/sheaves): checking the sheaf condition under a forgetful functor (#3609)

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 both C and D), 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