Mathlib v3 is deprecated. Go to Mathlib v4

Commit 2020-08-15 12:43 099f070f

View on Github →

feat(topology/sheaves): the sheaf condition (#3605) Johan and I have been working with this, and it's at least minimally viable. In follow-up PRs we have finished:

  • constructing the sheaf of dependent functions to a type family
  • constructing the sheaf of continuous functions to a fixed topological space
  • checking the sheaf condition under forgetful functors that reflect isos and preserve limits (https://stacks.math.columbia.edu/tag/0073) Obviously there's more we'd like to see before being confident that a design for sheaves is workable, but we'd like to get started!

Estimated changes