Sheaf conditions for presheaves of (continuous) functions.

We show that

• Top.Presheaf.toType_isSheaf: not-necessarily-continuous functions into a type form a sheaf
• Top.Presheaf.toTypes_isSheaf: in fact, these may be dependent functions into a type family

For

• Top.sheafToTop: continuous functions into a topological space form a sheaf please see Topology/Sheaves/LocalPredicate.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 TopCat.Presheaf.toTypes_isSheaf (X : TopCat) (T : ↑X → Type u) : TopCat.Presheaf.IsSheaf (TopCat.presheafToTypes X T)

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.

theorem TopCat.Presheaf.toType_isSheaf (X : TopCat) (T : Type u) : TopCat.Presheaf.IsSheaf (TopCat.presheafToType X T)

The presheaf of not-necessarily-continuous functions to a target type T satsifies the sheaf condition.

def TopCat.sheafToTypes (X : TopCat) (T : ↑X → Type u) : TopCat.Sheaf (Type u) X

The sheaf of not-necessarily-continuous functions on X with values in type family T : X → Type u.

Equations

• TopCat.sheafToTypes X T = { val := TopCat.presheafToTypes X T, cond := (_ : TopCat.Presheaf.IsSheaf (TopCat.presheafToTypes X T)) }

def TopCat.sheafToType (X : TopCat) (T : Type u) : TopCat.Sheaf (Type u) X

The sheaf of not-necessarily-continuous functions on X with values in a type T.

Equations

• TopCat.sheafToType X T = { val := TopCat.presheafToType X T, cond := (_ : TopCat.Presheaf.IsSheaf (TopCat.presheafToType X T)) }