Sheaf conditions for presheaves of (continuous) functions. #
We show that
Top.sheaf_condition.to_Type: not-necessarily-continuous functions into a type form a sheaf
Top.sheaf_condition.to_Types: in fact, these may be dependent functions into a type family
Top.sheaf_condition.to_Top: continuous functions into a topological space form a sheaf please see
topology/sheaves/local_predicate.lean, where we set up a general framework for constructing sub(pre)sheaves of the sheaf of dependent functions.
Future work #
Obviously there's more to do:
- sections of a fiber bundle
- various classes of smooth and structure preserving functions
- functions into spaces with algebraic structure, which the sections inherit
We show that the presheaf of functions to a type
(no continuity assumptions, just plain functions)
form a sheaf.
In fact, the proof is identical when we do this for dependent functions to a type family
so we do the more general case.