Sheaf conditions for presheaves of (continuous) functions. #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
We show that
Top.presheaf.to_Type_is_sheaf: not-necessarily-continuous functions into a type form a sheafTop.presheaf.to_Types_is_sheaf: in fact, these may be dependent functions into a type family
For
Top.sheaf_to_Top: continuous functions into a topological space form a sheaf please seetopology/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
theorem
Top.presheaf.to_Types_is_sheaf
(X : Top)
(T : ↥X → Type u) :
(X.presheaf_to_Types T).is_sheaf
We show that the presheaf of functions to a type T
(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 T,
so we do the more general case.
The presheaf of not-necessarily-continuous functions to
a target type T satsifies the sheaf condition.
The sheaf of not-necessarily-continuous functions on X with values in type family
T : X → Type u.
Equations
- X.sheaf_to_Types T = {val := X.presheaf_to_Types T, cond := _}
The sheaf of not-necessarily-continuous functions on X with values in a type T.
Equations
- X.sheaf_to_Type T = {val := X.presheaf_to_Type T, cond := _}