# 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`

.

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

- One or more equations did not get rendered due to their size.

## Instances For

The presheaf of functions on `X`

with values in a type `T`

.
There is no requirement that the functions are continuous, here.

## Equations

- One or more equations did not get rendered due to their size.

## Instances For

The presheaf of continuous functions on `X`

with values in fixed target topological space
`T`

.

## Equations

- X.presheafToTop T = (TopologicalSpace.Opens.toTopCat X).op.comp (CategoryTheory.yoneda.obj T)

## Instances For

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

## Equations

- TopCat.continuousFunctions X R = CommRingCat.of (X.unop ⟶ (CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)

## Instances For

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

## Equations

- One or more equations did not get rendered due to their size.

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

## Equations

- One or more equations did not get rendered due to their size.

## 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`

.

## Equations

- One or more equations did not get rendered due to their size.

## 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`

).

## Equations

- X.presheafToTopCommRing T = (TopologicalSpace.Opens.toTopCat X).op.comp (TopCat.commRingYoneda.obj T)