mathlib3 documentation

topology.sheaves.presheaf_of_functions

Presheaves of functions #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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

def Top.presheaf_to_Types (X : Top) (T : X Type 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.

Equations
@[simp]
@[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) (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.

Equations
@[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 T : Top) :

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