Documentation

Mathlib.Topology.Sheaves.SheafOfFunctions

Sheaf conditions for presheaves of (continuous) functions. #

We show that

For

Future work #

Obviously there's more to do:

theorem TopCat.Presheaf.toTypes_isSheaf (X : TopCat) (T : XType u) :
(X.presheafToTypes T).IsSheaf

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) :
(X.presheafToType T).IsSheaf

The presheaf of not-necessarily-continuous functions to a target type T satisfies 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
  • X.sheafToTypes T = { val := X.presheafToTypes T, cond := }
Instances For

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

    Equations
    • X.sheafToType T = { val := X.presheafToType T, cond := }
    Instances For