mathlib documentation

topology.sheaves.sheaf_of_functions

Sheaf conditions for presheaves of (continuous) functions. #

We show that

For

Future work #

Obviously there's more to do:

source
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.

source
theorem Top.presheaf.to_Type_is_sheaf (X : Top) (T : Type u) :
(X.presheaf_to_Type T).is_sheaf

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

source
def Top.sheaf_to_Types (X : Top) (T : ↥X → Type u) :
Top.sheaf (Type u) X

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

Equations
source
def Top.sheaf_to_Type (X : Top) (T : Type u) :
Top.sheaf (Type u) X

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

Equations