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 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 u_1) : Presheaf (Type (max u_1 u_2)) 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 u_1} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} : (X.presheafToTypes T).obj U = ((x : ↥(Opposite.unop U)) → T ↑x)

@[simp]

theorem TopCat.presheafToTypes_map (X : TopCat) {T : ↑X → Type u_1} {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} {i : U ⟶ V} {f : (fun (X : Type (max u_1 u_2)) => X) ((X.presheafToTypes T).obj U)} : (CategoryTheory.ConcreteCategory.hom ((X.presheafToTypes T).map i)) f = fun (x : ↥(Opposite.unop V)) => f (i.unop x)

def TopCat.presheafToType (X : TopCat) (T : Type u_1) : Presheaf (Type (max u_1 u_2)) 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 u_1} {U : (TopologicalSpace.Opens ↑X)ᵒᵖ} : (X.presheafToType T).obj U = (↥(Opposite.unop U) → T)

@[simp]

theorem TopCat.presheafToType_map (X : TopCat) {T : Type u_1} {U V : (TopologicalSpace.Opens ↑X)ᵒᵖ} {i : U ⟶ V} {f : (fun (X : Type (max u_1 u_2)) => X) ((X.presheafToType T).obj U)} : (CategoryTheory.ConcreteCategory.hom ((X.presheafToType T).map i)) f = f ∘ ⇑i.unop

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

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)

@[simp]

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