Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2021-10-13 13:20 edf07cfb

View on Github →

feat(topology/sheaves/sheaf_condition/sites): Connect sheaves on sites to sheaves on spaces (#9609) Show that a sheaf on the site opens X is the same thing as a sheaf on the space X. This finally connects the theory of sheaves on sites to sheaves on spaces, which were previously independent of each other.

Estimated changes