Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-28 05:18 513f7407

View on Github →

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.


Estimated changes