Documentation

Mathlib.Topology.Sheaves.SheafOfFunctions

Sheaf conditions for presheaves of (continuous) functions. #

We show that

For

Future work #

Obviously there's more to do:

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.

def TopCat.sheafToTypes (X : TopCat) (T : XType u) :

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

Equations
Instances For

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

    Equations
    Instances For