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.

def TopCat.presheafToTypes (X : TopCat) (T : ↑X → Type v) : TopCat.Presheaf (Type v) 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.

@[simp]

theorem TopCat.presheafToTypes_obj (X : TopCat) {T : ↑X → Type v} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} : (TopCat.presheafToTypes X T).toPrefunctor.obj U = ((x : ↥U.unop) → T ↑x)

@[simp]

theorem TopCat.presheafToTypes_map (X : TopCat) {T : ↑X → Type v} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {V : (TopologicalSpace.Opens ↑X)ᵒᵖ} {i : U ⟶ V} {f : (TopCat.presheafToTypes X T).toPrefunctor.obj U} : (TopCat.presheafToTypes X T).toPrefunctor.map i f = fun (x : ↥V.unop) => f ((fun (x : ↥V.unop) => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }) x)

def TopCat.presheafToType (X : TopCat) (T : Type v) : TopCat.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

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

@[simp]

theorem TopCat.presheafToType_obj (X : TopCat) {T : Type v} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} : (TopCat.presheafToType X T).toPrefunctor.obj U = (↥U.unop → T)

@[simp]

theorem TopCat.presheafToType_map (X : TopCat) {T : Type v} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} {V : (TopologicalSpace.Opens ↑X)ᵒᵖ} {i : U ⟶ V} {f : (TopCat.presheafToType X T).toPrefunctor.obj U} : (TopCat.presheafToType X T).toPrefunctor.map i f = f ∘ fun (x : ↥V.unop) => { val := ↑x, property := (_ : ↑x ∈ ↑U.unop) }

def TopCat.presheafToTop (X : TopCat) (T : TopCat) : TopCat.Presheaf (Type v) X

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

Equations

• TopCat.presheafToTop X T = CategoryTheory.Functor.comp (TopologicalSpace.Opens.toTopCat X).op (CategoryTheory.yoneda.toPrefunctor.obj T)

@[simp]

theorem TopCat.presheafToTop_obj (X : TopCat) (T : TopCat) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) : (TopCat.presheafToTop X T).toPrefunctor.obj U = ((TopologicalSpace.Opens.toTopCat X).toPrefunctor.obj U.unop ⟶ T)

def TopCat.continuousFunctions (X : TopCatᵒᵖ) (R : TopCommRingCat) : CommRingCat

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).toPrefunctor.obj R)

def TopCat.continuousFunctions.pullback {X : TopCatᵒᵖ} {Y : TopCatᵒᵖ} (f : X ⟶ Y) (R : TopCommRingCat) : TopCat.continuousFunctions X R ⟶ TopCat.continuousFunctions Y R

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.

def TopCat.continuousFunctions.map (X : TopCatᵒᵖ) {R : TopCommRingCat} {S : TopCommRingCat} (φ : R ⟶ S) : TopCat.continuousFunctions X R ⟶ TopCat.continuousFunctions X 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

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

def TopCat.commRingYoneda : CategoryTheory.Functor TopCommRingCat (CategoryTheory.Functor TopCatᵒᵖ CommRingCat)

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.

def TopCat.presheafToTopCommRing (X : TopCat) (T : TopCommRingCat) : TopCat.Presheaf CommRingCat X

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

• TopCat.presheafToTopCommRing X T = CategoryTheory.Functor.comp (TopologicalSpace.Opens.toTopCat X).op (TopCat.commRingYoneda.toPrefunctor.obj T)