mathlib

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

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 Co-authored-by: Scott Morrison <scott.morrison@gmail.com>