# Documentation

Mathlib.Topology.Sheaves.PresheafOfFunctions

# Presheaves of functions #

We construct some simple examples of presheaves of functions on a topological space.

• presheafToTypes X T, where T : X → Type, is the presheaf of dependently-typed (not-necessarily continuous) functions
• presheafToType X T, where T : Type, is the presheaf of (not-necessarily-continuous) functions to a fixed target type T
• presheafToTop X T, where T : TopCat, is the presheaf of continuous functions into a topological space T
• presheafToTopCommRing X R, where R : TopCommRingCat is the presheaf valued in CommRing of functions functions into a topological ring R
• as an example of the previous construction, presheafToTopCommRing X (TopCommRingCat.of ℂ) is the presheaf of rings of continuous complex-valued functions on X.
def TopCat.presheafToTypes (X : TopCat) (T : XType v) :

The presheaf of dependently typed functions on X, with fibres given by a type family T. There is no requirement that the functions are continuous, here.

Instances For
@[simp]
theorem TopCat.presheafToTypes_obj (X : TopCat) {T : XType v} {U : } :
().obj U = ((x : { x // x U.unop }) → T x)
@[simp]
theorem TopCat.presheafToTypes_map (X : TopCat) {T : XType v} {U : } {V : } {i : U V} {f : ().obj U} :
.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor U V i f = fun x => f ((fun x => { val := x, property := (_ : x U.unop) }) x)
def TopCat.presheafToType (X : TopCat) (T : Type v) :

The presheaf of functions on X with values in a type T. There is no requirement that the functions are continuous, here.

Instances For
@[simp]
theorem TopCat.presheafToType_obj (X : TopCat) {T : Type v} {U : } :
().obj U = ({ x // x U.unop }T)
@[simp]
theorem TopCat.presheafToType_map (X : TopCat) {T : Type v} {U : } {V : } {i : U V} {f : ().obj U} :
.map CategoryTheory.CategoryStruct.toQuiver (Type v) CategoryTheory.CategoryStruct.toQuiver ().toPrefunctor U V i f = f fun x => { val := x, property := (_ : x U.unop) }

The presheaf of continuous functions on X with values in fixed target topological space T.

Instances For
@[simp]
theorem TopCat.presheafToTop_obj (X : TopCat) (T : TopCat) (U : ) :
().obj U = (().obj U.unop T)

The (bundled) commutative ring of continuous functions from a topological space to a topological commutative ring, with pointwise multiplication.

Instances For
def TopCat.continuousFunctions.pullback {X : } {Y : } (f : X Y) (R : TopCommRingCat) :

Pulling back functions into a topological ring along a continuous map is a ring homomorphism.

Instances For

A homomorphism of topological rings can be postcomposed with functions from a source space X; this is a ring homomorphism (with respect to the pointwise ring operations on functions).

Instances For

An upgraded version of the Yoneda embedding, observing that the continuous maps from X : TopCat to R : TopCommRingCat form a commutative ring, functorial in both X and R.

Instances For

The presheaf (of commutative rings), consisting of functions on an open set U ⊆ X with values in some topological commutative ring T.

For example, we could construct the presheaf of continuous complex valued functions of X as

presheafToTopCommRing X (TopCommRing.of ℂ)


(this requires import Topology.Instances.Complex).

Instances For