Documentation

Mathlib.Topology.Sheaves.PresheafOfFunctions

Presheaves of functions #

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

def TopCat.presheafToTypes (X : TopCat) (T : XType 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
  • One or more equations did not get rendered due to their size.
Instances For
    @[simp]
    theorem TopCat.presheafToTypes_obj (X : TopCat) {T : XType v} {U : (TopologicalSpace.Opens X)ᵒᵖ} :
    (X.presheafToTypes T).obj U = ((x : (Opposite.unop U)) → T x)
    @[simp]
    theorem TopCat.presheafToTypes_map (X : TopCat) {T : XType v} {U : (TopologicalSpace.Opens X)ᵒᵖ} {V : (TopologicalSpace.Opens X)ᵒᵖ} {i : U V} {f : (X.presheafToTypes T).obj U} :
    (X.presheafToTypes T).map i f = fun (x : (Opposite.unop V)) => f ((fun (x : (Opposite.unop V)) => x, ) 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.
    Instances For
      @[simp]
      theorem TopCat.presheafToType_obj (X : TopCat) {T : Type v} {U : (TopologicalSpace.Opens X)ᵒᵖ} :
      (X.presheafToType T).obj U = ((Opposite.unop U)T)
      @[simp]
      theorem TopCat.presheafToType_map (X : TopCat) {T : Type v} {U : (TopologicalSpace.Opens X)ᵒᵖ} {V : (TopologicalSpace.Opens X)ᵒᵖ} {i : U V} {f : (X.presheafToType T).obj U} :
      (X.presheafToType T).map i f = f fun (x : (Opposite.unop V)) => x,

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

      Equations
      Instances For
        @[simp]
        theorem TopCat.presheafToTop_obj (X : TopCat) (T : TopCat) (U : (TopologicalSpace.Opens X)ᵒᵖ) :
        (X.presheafToTop T).obj U = ((TopologicalSpace.Opens.toTopCat X).obj (Opposite.unop U) T)

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

        Equations
        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
                Instances For