# mathlibdocumentation

topology.sheaves.presheaf_of_functions

# Presheaves of functions

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

• presheaf_to_Type X f, where f : X → Type, is the presheaf of dependently-typed (not-necessarily continuous) functions
• presheaf_to_Type X T, where T : Type, is the presheaf of (not-necessarily-continuous) functions to a fixed target type T
• presheaf_to_Top X T, where T : Top, is the presheaf of continuous functions into a topological space T
• presheaf_To_TopCommRing X R, where R : TopCommRing is the presheaf valued in CommRing of functions functions into a topological ring R
• as an example of the previous construction, presheaf_to_TopCommRing X (TopCommRing.of ℂ) is the presheaf of rings of continuous complex-valued functions on X.
def Top.presheaf_to_Types (X : Top) :
(X → Type v)Top.presheaf (Type v) X

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

Equations
@[simp]
theorem Top.presheaf_to_Types_obj (X : Top) {T : X → Type v} {U : ᵒᵖ} :
(X.presheaf_to_Types T).obj U = Π (x : (opposite.unop U)), T x

@[simp]
theorem Top.presheaf_to_Types_map (X : Top) {T : X → Type v} {U V : ᵒᵖ} {i : U V} {f : (X.presheaf_to_Types T).obj U} :
(X.presheaf_to_Types T).map i f = λ (x : (opposite.unop V)), f ((i.unop) x)

def Top.presheaf_to_Type (X : Top) :
Type vTop.presheaf (Type v) X

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

Equations
@[simp]
theorem Top.presheaf_to_Type_obj (X : Top) {T : Type v} {U : ᵒᵖ} :
(X.presheaf_to_Type T).obj U = ( → T)

@[simp]
theorem Top.presheaf_to_Type_map (X : Top) {T : Type v} {U V : ᵒᵖ} {i : U V} {f : (X.presheaf_to_Type T).obj U} :
(X.presheaf_to_Type T).map i f = f (i.unop)

def Top.presheaf_to_Top (X : Top) :
TopTop.presheaf (Type v) X

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

Equations
@[simp]
theorem Top.presheaf_to_Top_obj (X T : Top) (U : ᵒᵖ) :

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

Equations

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

Equations
def Top.continuous_functions.map (X : Topᵒᵖ) {R S : TopCommRing} :
(R S)

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

Equations

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

Equations

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

presheaf_to_TopCommRing X (TopCommRing.of ℂ)


(this requires import topology.instances.complex).

Equations