mathlib documentation

topology.sheaves.presheaf_of_functions

Presheaves of functions

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

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 : (topological_space.opens X)ᵒᵖ} :
(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 : (topological_space.opens X)ᵒᵖ} {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 : (topological_space.opens X)ᵒᵖ} :

@[simp]
theorem Top.presheaf_to_Type_map (X : Top) {T : Type v} {U V : (topological_space.opens X)ᵒᵖ} {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

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

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