Top.presheaf_to_Top

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

Top.continuous_functions

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

Top.continuous_functions.pullback

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

Top.continuous_functions.map

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

Top.CommRing_yoneda

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.

Top.presheaf_to_TopCommRing

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

Top.presheaf_ℝ

The presheaf (of commutative rings) of real valued functions.

Top.presheaf_ℂ

The presheaf (of commutative rings) of complex valued functions.