geometry of physics -- smooth sets

This entry contains one chapter of the material at geometry of physics.

previous chapter: coordinate systems

next chapters: differential forms, differentiation, smooth homotopy types



physics, mathematical physics, philosophy of physics

Surveys, textbooks and lecture notes

theory (physics), model (physics)

experiment, measurement, computable physics

Differential geometry

synthetic differential geometry


from point-set topology to differentiable manifolds

geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry



smooth space


The magic algebraic facts




tangent cohesion

differential cohesion

graded differential cohesion

id id fermionic bosonic bosonic Rh rheonomic reduced infinitesimal infinitesimal & étale cohesive ʃ discrete discrete continuous * \array{ && id &\dashv& id \\ && \vee && \vee \\ &\stackrel{fermionic}{}& \rightrightarrows &\dashv& \rightsquigarrow & \stackrel{bosonic}{} \\ && \bot && \bot \\ &\stackrel{bosonic}{} & \rightsquigarrow &\dashv& Rh & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& ʃ &\dashv& \flat & \stackrel{discrete}{} \\ && \bot && \bot \\ &\stackrel{discrete}{}& \flat &\dashv& \sharp & \stackrel{continuous}{} \\ && \vee && \vee \\ && \emptyset &\dashv& \ast }


Lie theory, ∞-Lie theory

differential equations, variational calculus

Chern-Weil theory, ∞-Chern-Weil theory

Cartan geometry (super, higher)



This chapter introduces a generalized kind of sets equipped with smooth structure, to be called smooth sets or smooth spaces or smooth 0-types.

The definition subsumes that of smooth manifolds, Fréchet manifolds and diffeological spaces but is both simpler and more powerful: smooth sets are simply sheaves on the gros site of Cartesian Spaces and as such form a nice category – a topos – and this contains as full subcategories the more “tame” objects such as smooth manifolds and diffeological spaces.

In fact smooth sets are an early stage in a long sequence of generalized smooth spaces used in higher differential geometry:

{\{coordinate systems}\} \hookrightarrow {\{smooth manifolds}\} \hookrightarrow {\{Hilbert manifolds}\} \hookrightarrow {\{Banach manifolds}\} \hookrightarrow {\{Fréchet manifolds}\} \hookrightarrow {\{diffeological spaces}\} \hookrightarrow {\{smooth spaces}\} \hookrightarrow {\{smooth orbifolds}\} \hookrightarrow {\{smooth groupoids}\} \hookrightarrow {\{smooth 2-groupoids}\} \hookrightarrow \cdots \hookrightarrow {\{smooth ∞-groupoids}\}


Note on terminology.

In view of the smooth homotopy types to be discussed in geometry of physics -- smooth homotopy types, the structures discussed now are properly called smooth 0-types or maybe smooth h-sets or just smooth sets. While this subsumes smooth manifolds which are indeed sets equipped with (particularly nice) smooth structure, it is common in practice to speak of manifolds as “spaces” (indeed as topological spaces equipped with smooth structure). Historically the Cartesian space and Euclidean space of Newtonian physics are the archetypical examples of smooth manifolds and modern differential geometry developed very much via motivation by the study of the spaces in general relativity, namely spacetimes. Unfortunately, in a parallel development the word “space” has evolved in homotopy theory to mean (just) the homotopy types represented by an actual topological space (their fundamental infinity-groupoids). Ironically, with this meaning of the word “space” the original Euclidean spaces become equivalent to the point, signifying that the modern meaning of “space” in homotopy theory is quite orthogonal to the original meaning, and that in homotopy theory therefore one should better stick to “homotopy types”.

Since historically grown terminology will never be fully logically consistent, and since often the less well motivated terminology is more widely understood, we will follow tradition here and take the liberty to use “smooth sets” and “smooth spaces” synonymously, the former when we feel more formalistic, the latter when we feel more relaxed.

Smooth sets

In the section Coordinate systems we have set up the archetypical spaces of differential geometry. Here we now define in terms of these the most general smooth spaces that differential geometry can deal with. We also discuss basic properties of these smooth spaces, all in the Mod Layer.

In the Sem Layer we discuss smooth spaces as a topos and in fact as a cohesive topos. This is essentially the stage on which all of the fellowing developments take place. Or rather, the refinement of this to a higher topos is, which we discuss further below in the chapter Smooth ∞-Groupoids.

Model Layer

In this Model Layer we discuss concretely the definition of smooth spaces and of homomorphisms between them, together with basic examples and properties.

Plots of smooth spaces and their gluing

The general kind of “smooth space” that we want to consider is a something that can be probed by laying out coordinate systems as in this definition?(–+coordinate+systems#CartesianSpaces) inside it, and that can be obtained by gluing all the possible coordinate systems in it together.

At this point we want to impose no further conditions on a “space” than this. In particular we do not assume that we know beforehand a set of points underlying XX. Instead, we define smooth spaces XX entirely operationally as something about which we can ask “Which ways are there to lay out n\mathbb{R}^n inside XX?” and such that there is a self-consistent answer to this question. The following definitions make precise what we mean by this. The reader wishing to see more motivational discussion first might look at conceptual exposition.

The idea of the following definitions may be summarized like this:

  1. a generalized smooth space is something that may be probed by laying out coordinate systems into it, in a way that respects transformation of coordinate patches and gluing of coordinate patches;

  2. the Yoneda lemma says that this is consistent in that coordinate systems themselves as well as smooth manifolds may naturally be regarded as generalized smooth spaces themselves and that under this identification “laying out a coordinate system” in a smooth space means having a map of smooth spaces from the coordinate system to the smooth space.

Definition (terminology)

For brevity we will refer to “a way to lay out a coordinate system in XX” as a plot of XX.

The first set of consistency conditions on plots of a space is that they respect coordinate transformations. This is what the following definition formalises.


A smooth pre-space XX is

  1. a collection of sets: for each Cartesian space n\mathbb{R}^n (hence for each natural number nn) a set

    X( n)Set X(\mathbb{R}^n) \in Set

    – to be thought of as the set of ways of laying out n\mathbb{R}^n inside XX;

  2. for each abstract coordinate transformation, hence for each smooth function f: n 1 n 2f : \mathbb{R}^{n_1} \to \mathbb{R}^{n_2} a function between the corresponding sets

    X(f):X( n 2)X( n 1) X(f) : X(\mathbb{R}^{n_2}) \to X(\mathbb{R}^{n_1})

    – to be thought of as the function that sends a plot of XX by n 2\mathbb{R}^{n_2} to the correspondingly transformed plot by n 1\mathbb{R}^{n_1} induced by laying out n 1\mathbb{R}^{n_1} inside n 2\mathbb{R}^{n_2}.

such that this is compatible with coordinate transformations:

  1. the identity coordinate transformation does not change the plots:

    X(id n)=id X( n), X(id_{\mathbb{R}^n}) = id_{X(\mathbb{R}^n)} \,,
  2. changing plots along two consecutive coordinate transformations f 1: n 1 n 2f_1 \colon \mathbb{R}^{n_1} \to \mathbb{R}^{n_2} and f 2: n 2 n 3f_2 \colon \mathbb{R}^{n_2} \to \mathbb{R}^{n_3} is the same as changing them along the composite coordinate transformation f 2f 1f_2 \circ f_1:

    X(f 1)X(f 2)=X(f 2f 1). X(f_1) \circ X(f_2) = X(f_2 \circ f_1) \,.

But there is one more consistency condition for a collection of plots to really be probes of some space: it must be true that if we glue small coordinate systems to larger ones, then the plots by the larger ones are the same as the plots by the collection of smaller ones that agree where they overlap. We first formalize this idea of “plots that agree where their coordinate systems overlap.”


Let XX be a smooth pre-space, def. 2. For {U i n} iI\{U_i \to \mathbb{R}^n\}_{i \in I} a differentially good open cover, def. \ref{DifferentiallyGoodOpenCover}, let

GluedPlots({U i n},X)Set GluedPlots(\{U_i \to \mathbb{R}^n\}, X) \in Set

be the set of II-tuples of U iU_i-plots of XX which coincide on all double intersections

U iU j ι i ι j U i U j n \array{ && U_i \cap U_j \\ & {}^{\mathllap{\iota_i}}\swarrow && \searrow^{\mathrlap{\iota_j}} \\ U_i &&&& U_j \\ & \searrow && \swarrow \\ && \mathbb{R}^n }

(also called the matching families of XX over the given cover):

GluedPlots({U i n},X){(p iX(U i)) iI| i,jI:X(ι i)(p i)=X(ι j)(p j)}. GluedPlots(\{U_i \to \mathbb{R}^n\}, X) \;\;\coloneqq\;\; \left\{ \; \left(p_i \in X(U_i)\right)_{i \in I} \;|\;\; \forall_{i,j \in I} \;:\; X(\iota_i)(p_i) = X(\iota_j)(p_j) \; \right\} \,.

In def. 3 the equation

X(ι i)(p i)=X(ι j)(p j) X(\iota_i)(p_i) = X(\iota_j)(p_j)

says in words:

The plot p ip_i of XX by the coordinate system U iU_i inside the bigger coordinate system n\mathbb{R}^n coincides with the plot p jp_j of XX by the other coordinate system U jU_j inside XX when both are restricted to the intersection U iU jU_i \cap U_j of U iU_i with U jU_j inside n\mathbb{R}^n.


For each differentially good open cover {U i n} iI\{U_i \to \mathbb{R}^n\}_{i \in I} and each smooth pre-space XX, def. 2, there is a canonical function

X( n)GluedPlots({U i n},X) X(\mathbb{R}^n) \to GluedPlots(\{U_i \to \mathbb{R}^n\}, X)

from the set of n\mathbb{R}^n-plots of XX to the set of tuples of glued plots, which sends a plot pX( n)p \in X(\mathbb{R}^n) to its restriction to all the ϕ i:U i n\phi_i \colon U_i \hookrightarrow \mathbb{R}^n:

p(X(ϕ i)(p)) iI. p \mapsto (X(\phi_i)(p))_{i \in I} \,.

If XX is supposed to be consistently probable by coordinate systems, then it must be true that the set of ways of laying out a coordinate system n\mathbb{R}^n inside it coincides with the set of ways of laying out tuples of glued coordinate systems inside it, for each good cover {U i n}\{U_i \to \mathbb{R}^n\} as above. Therefore:


A smooth pre-space XX, def. 2 is a smooth space if for all differentially good open covers {U i n}\{U_i \to \mathbb{R}^n\}, def. \ref{DifferentiallyGoodOpenCover}, the canonical function of remark 3 from plots to glued plots is a bijection

X( n)GluedPlots({U i n},X). X(\mathbb{R}^n) \stackrel{\simeq}{\to} GluedPlots(\{U_i \to \mathbb{R}^n\}, X) \,.

We may think of a smooth space as being a kind of space whose local models (in the general sense discussed at geometry) are Cartesian spaces:

while definition 4 explicitly says that a smooth space is something that is consistently probeable by such local models; by a general abstract fact – which we discuss in more detail below in Smooth Spaces - Semantic Layer – that is sometimes called the co-Yoneda lemma it follows in fact that smooth spaces are precisely the objects that are obtained by gluing coordinate systems together.

For instance we will see that two open 2-balls 2D 2\mathbb{R}^2 \simeq D^2 along a common rim yields the smooth space version of the sphere S 2S^2, a basic example of a smooth manifold. But before we examine such explicit constructions, we discuss here for the moment more general properties of smooth spaces. The reader instead wishing to see more of these concrete examples at this point should jump ahead to Smooth Spaces - Outlook.

But the following most basic example we consider right now:


For n nn \in \mathbb{R}^n, there is a smooth space, def. 4, whose set of plots over the abstract coordinate systems k\mathbb{R}^k is the set

CartSp( k, n)Set CartSp(\mathbb{R}^k, \mathbb{R}^n) \in Set

of smooth functions from k\mathbb{R}^k to n\mathbb{R}^n.

Clearly this is the rule for plots that characterize n\mathbb{R}^n itself as a smooth space, and so we will just denote this smooth space by the same symbols “ n\mathbb{R}^n”:

n: kCartSp( k, n). \mathbb{R}^n \colon \mathbb{R}^k \mapsto CartSp(\mathbb{R}^k, \mathbb{R}^n) \,.

In particular the real line \mathbb{R} is this way itself a smooth space.

In a moment we find a formal justification for this slight abuse of notation.

Another basic class of examples of smooth spaces are the discrete smooth spaces:


For SS \in Set a set, write

DiscSSmooth0Type Disc S \in Smooth0Type

for the smooth space whose set of UU-plots for every UCartSpU \in CartSp is always SS.

DiscS:US Disc S \colon U \mapsto S

and which sends every coordinate transformation f: n 1 n 2f \colon \mathbb{R}^{n_1} \to \mathbb{R}^{n_2} to the identity function on SS.

A smooth space of this form we call a discrete smooth space.

More examples of smooth spaces can be built notably by intersecting images of two smooth spaces inside a bigger one. In order to say this we first need a formalization of homomorphism of smooth spaces. This we turn to now.

Homomorphisms of smooth spaces

We discuss “functions” or “maps” between smooth spaces, def. 4, which preserve the smooth space structure in a suitable sense. As with any notion of function that preserves structure, we refer to them as homomorphisms.

The idea of the following definition is to say that whatever a homomorphism f:XYf : X \to Y between two smooth spaces is, it has to take the plots of XX by n\mathbb{R}^n to a corresponding plot of YY, such that this respects coordinate transformations.


Let XX and YY be two smooth spaces, def. 4. Then a homomorphism f:XYf \colon X \to Y is

  • for each abstract coordinate system n\mathbb{R}^n (hence for each nn \in \mathbb{N}) a function

    f n:X( n)Y( n)f_{\mathbb{R}^n} : X(\mathbb{R}^n) \to Y(\mathbb{R}^n)

    that sends n\mathbb{R}^n-plots of XX to n\mathbb{R}^n-plots of YY

such that

  • for each smooth function ϕ: n 1 n 2\phi : \mathbb{R}^{n_1} \to \mathbb{R}^{n_2} we have

    Y(ϕ)f n 1=f n 2X(ϕ) Y(\phi) \circ f_{\mathbb{R}^{n_1}} = f_{\mathbb{R}^{n_2}} \circ X(\phi)

    hence a commuting diagram

    X( n 1) f n 1 Y( n 1) X(ϕ) Y(ϕ) X( n 2) f n 2 Y( n 1). \array{ X(\mathbb{R}^{n_1}) &\stackrel{f_{\mathbb{R}^{n_1}}}{\to}& Y(\mathbb{R}^{n_1}) \\ \downarrow^{\mathrlap{X(\phi)}} && \downarrow^{\mathrlap{Y(\phi)}} \\ X(\mathbb{R}^{n_2}) &\stackrel{f_{\mathbb{R}^{n_2}}}{\to}& Y(\mathbb{R}^{n_1}) } \,.

For f 1:XYf_1 : X \to Y and f 2:XYf_2 : X \to Y two homomorphisms of smooth spaces, their composition f 2f 1:XYf_2 \circ f_1 \colon X \to Y is defined to be the homomorphism whose component over n\mathbb{R}^n is the composite of functions of the components of f 1f_1 and f 2f_2:

(f 2f 1) nf 2 nf 1 n. (f_2\circ f_1)_{\mathbb{R}^n} \coloneqq {f_2}_{\mathbb{R}^n} \circ {f_1}_{\mathbb{R}^n} \,.

Write Smooth0TypeSmooth0Type for the category whose objects are smooth spaces, def. 4, and whose morphisms are homomorphisms of smooth spaces, def. 6.

At this point it may seem that we have now two different notions for how to lay out a coordinate system in a smooth space XX: on the hand, XX comes by definition with a rule for what the set X( n)X(\mathbb{R}^n) of its n\mathbb{R}^n-plots is. On the other hand, we can now regard the abstract coordinate system n\mathbb{R}^n itself as a smooth space, by example 1, and then say that an n\mathbb{R}^n-plot of XX should be a homomorphism of smooth spaces of the form nX\mathbb{R}^n \to X.

The following proposition says that these two superficially different notions actually naturally coincide.


Let XX be any smooth space, def. 4, and regard the abstract coordinate system n\mathbb{R}^n as a smooth space, by example 1. There is a natural bijection

X( n)Hom Smooth0Type( n,X) X(\mathbb{R}^n) \simeq Hom_{Smooth0Type}(\mathbb{R}^n, X)

between the postulated n\mathbb{R}^n-plots of XX and the actual n\mathbb{R}^n-plots given by homomorphism of smooth spaces nX\mathbb{R}^n \to X.


This is a special case of the Yoneda lemma, as will be made more explicit below in The topos of smooth spaces. The reader unfamiliar with this should write out the simple proof explicitly: use the defining commuting diagrams in def. 6 to deduce that a homomorphism f: nXf : \mathbb{R}^n \to X is uniquely fixed by the image of the identity element in n( n)CartSp( n, n)\mathbb{R}^n(\mathbb{R}^n) \coloneqq CartSp(\mathbb{R}^n, \mathbb{R}^n) under the component function f n: n( n)X( n)f_{\mathbb{R}^n} : \mathbb{R}^n(\mathbb{R}^n) \to X(\mathbb{R}^n).


Let Smooth0Type\mathbb{R} \in Smooth0Type denote the real line, regarded as a smooth space by def. 1. Then for XSmooth0TypeX \in Smooth0Type any smooth space, a homomorphism of smooth spaces

f:X f \colon X \to \mathbb{R}

is a smooth function on XX. Prop. 1 says here that when XX happens to be an abstract coordinate system regarded as a smooth space by def. 1, then this general notion of smooth functions between smooth spaces reproduces the basic notion of def, \ref{CartesianSpaceAndHomomorphism}.


The 0-dimensional abstract coordinate system 0\mathbb{R}^0 we also call the point and regarded as a smooth space we will often write it as

*Smooth0Type. * \in Smooth0Type \,.

For any XSmooth0TypeX \in Smooth0Type, we say that a homomorphism

x:*X x \colon * \to X

is a point of XX.


By prop. 1 the points of a smooth space XX are naturally identified with its 0-dimensional plots, hence with the “ways of laying out a 0-dimensional coordinate system” in XX:

Hom(*,X)X( 0). Hom(*, X) \simeq X(\mathbb{R}^0) \,.

Products and fiber products of smooth spaces


Let X,YSmooth0TypeX, Y \in Smooth0Type by two smooth spaces. Their product is the smooth space X×YSmooth0TypeX \times Y \in Smooth0Type whose plots are pairs of plots of XX and YY:

X×Y( n)X( n)×Y( n)Set. X\times Y (\mathbb{R}^n) \coloneqq X(\mathbb{R}^n) \times Y(\mathbb{R}^n) \;\; \in Set \,.

The projection on the first factor is the homomorphism

p 1:X×YX p_1 \colon X \times Y \to X

which sends n\mathbb{R}^n-plots of X×YX \times Y to those of XX by forming the projection of the cartesian product of sets:

p 1 n:X( n)×Y( n)p 1X( n). {p_1}_{\mathbb{R}^n} \colon X(\mathbb{R}^n) \times Y(\mathbb{R}^n) \stackrel{p_1}{\to} X(\mathbb{R}^n) \,.

Analogously for the projection to the second factor

p 2:X×YY. p_2 \colon X \times Y \to Y \,.

Let *= 0* = \mathbb{R}^0 be the point, regarded as a smooth space, def. 8. Then for XSmooth0TypeX \in Smooth0Type any smooth space the canonical projection homomorphism

X×*X X \times * \to X

is an isomorphism.


Let f:XZf \colon X \to Z and g:YZg \colon Y \to Z be two homomorphisms of smooth spaces, def. 6. There is then a new smooth space to be denoted

X× ZYSmooth0Type X \times_Z Y \in Smooth0Type

(with ff and gg understood), called the fiber product of XX and YY along ff and gg, and defined as follows:

the set of n\mathbb{R}^n-plots of X× ZYX \times_Z Y is the set of pairs of plots of XX and YY which become the same plot of ZZ under ff and gg, respectively:

(X× ZY)( n)={(p XX( n),p YY( n))|f n(p X)=g n(p Y)}. (X \times_Z Y)(\mathbb{R}^n) = \left\{ (p_X \in X(\mathbb{R}^n), p_Y \in Y(\mathbb{R}^n)) \; |\; f_{\mathbb{R}^n}(p_X) = g_{\mathbb{R}^n}(p_Y) \right\} \,.

Smooth mapping spaces and smooth moduli spaces


Let Σ,XSmooth0Type\Sigma, X \in Smooth0Type be two smooth spaces, def. 4. Then the smooth mapping space

[Σ,X]Smooth0Type [\Sigma,X] \in Smooth0Type

is the smooth space defined by saying that its set of n\mathbb{R}^n-plots is

[Σ,X]( n)Hom(Σ× n,X). [\Sigma, X](\mathbb{R}^n) \coloneqq Hom(\Sigma \times \mathbb{R}^n, X) \,.

Here in Σ× n\Sigma \times \mathbb{R}^n we first regard the abstract coordinate system n\mathbb{R}^n as a smooth space by example 1 and then we form the product smooth space by def. 9.


This means in words that a n\mathbb{R}^n-plot of the mapping space [Σ,X][\Sigma,X] is a smooth n\mathbb{R}^n-parameterized family of homomorphisms ΣX\Sigma \to X.


There is a natural bijection

Hom(K,[Σ,X])Hom(K×Σ,X) Hom(K, [\Sigma, X]) \simeq Hom(K \times \Sigma, X)

for every smooth space KK.


With a bit of work this is straightforward to check explicitly by unwinding the definitions. It follows however from general abstract results once we realize that [,][-,-] is of course the internal hom of smooth spaces. This we come to below in Smooth spaces - Semantic Layer.


This says in words that a smooth function from any KK into the mapping space [Σ,X][\Sigma,X] is equivalently a smooth function from K×ΣK \times \Sigma to XX. The latter we may regard as a KK-parameterized smooth family of smooth functions ΣX\Sigma \to X. Therefore in view of the previous remark 6 this says that smooth mapping spaces have a universal property not just over abstract coordinate systems, but over all smooth spaces.

We will therefore also say that [Σ,X][\Sigma,X] is the smooth moduli space of smooth functions from ΣX\Sigma \to X, because it is such that smooth maps K[Σ,X]K \to [\Sigma,X] into it modulate, as we move around on KK, a family of smooth functions ΣX\Sigma\to X, depending on KK.

First interesting examples of such smooth moduli spaces are discussed in Differential forms – Model Layer below. Many more interesting examples follow once we pass from smooth 0-types to smooth nn-types below in Smooth n-groupoids.

We will see many more examples of smooth moduli spaces, starting below in Differential forms - Model Layer.


The set of points, def. 8, of a smooth mapping space [Σ,X][\Sigma,X] is the bare set of homomorphism ΣX\Sigma \to X: there is a natural isomorphism

Hom(*,[Σ,X])Hom(Σ,X). Hom(*, [\Sigma, X]) \simeq Hom(\Sigma, X) \,.

Combine prop. 3 with prop. 2.


Given a smooth space XSmooth0TypeX \in Smooth0Type, its smooth path space is the smooth mapping space

PX[ 1,X]. \mathbf{P}X \coloneqq [\mathbb{R}^1, X] \,.

By prop. 4 the points of PXP X are indeed precisely the smooth trajectories 1X\mathbb{R}^1 \to X. But PXP X also knows how to smoothly vary such smooth trajectories.

This is central for variational calculus which determines equations of motion in physics. This we turn to below in Variational calculus.


In physics, if XX is a model for spacetime, then PXP X may notably be interpreted as the smooth space of worldlines in XX, hence the smooth space of paths or trajectories of a particle in XX.


If in the above example 3 the path is constraind to be a loop in XX, one obtains the smooth loop space

LX[S 1,X]. \mathbf{L}X \coloneqq [S^1, X] \,.

The smooth moduli space of smooth functions

In example 2 we saw that a smooth function on a general smooth space XX is a homomorphism of smooth spaces, def. 6

f:X. f \colon X \to \mathbb{R} \,.

The collection of these forms the hom-set Hom Smooth0Type(X,)Hom_{Smooth0Type}(X, \mathbb{R}). But by the discussion in Smooth mapping spaces such hom-sets are naturally refined to smooth spaces themselves.


For XSmooth0TypeX \in Smooth0Type a smooth space, we say that the moduli space of smooth functions on XX is the smooth mapping space (def. 11), from XX into the standard real line \mathbb{R}

[X,]Smooth0Type. [X, \mathbb{R}] \in Smooth0Type \,.

We will also denote this by

C (X)[X,], \mathbf{C}^\infty(X) \coloneqq [X, \mathbb{R}] \,,

since in the special case that XX is a Cartesian space this is the smooth refinement of the set C (X)C^\infty(X) of smooth functions, def. \ref{SmoothFunctions}, on XX.


We call this a moduli space because by prop. 3 above and in the sense of remark 7 it is such that smooth functions into it modulate smooth functions XX \to \mathbb{R}.

By prop. 4 a point *[X, 1]* \to [X,\mathbb{R}^1] of the moduli space is equivalently a smooth function X 1X \to \mathbb{R}^1.



Later we define/see the following:


This ends the Model-layer discussion of smooth spaces. We now pass to a more advanced discussion of this topic in the Semantics layer below. The reader wishing to stick to more elementary discussion for the time being should skip ahead to the Model-layer discussion of Differential forms below.

Semantic Layer

In this [Semantic Layer] we mention some basic definitions of topos theory and discuss the topos formed by the smooth spaces defined in Smooth Spaces - Mayer Mod.



A sheaf topos is subtopos of presheaf topos

Sh(C)()¯PSh(C). Sh(C) \stackrel{\overset{\overline{(-)}}{\leftarrow}}{\hookrightarrow} PSh(C) \,.

Here the left adjoint ()¯\overline{(-)}, which is equivalently

is precisely such that for every covering {U iU} iI\{U_i \to U\}_{i \in I} in the site CC the sieve inclusion

S({U i})UPSh(C) S(\{U_i\}) \hookrightarrow U \;\;\;\; \in PSh(C)

(a dense monomorphism) is sent to an isomorphism.

Hence the sheaf topos is the left exact localization at the covering sieve inclusions.


The presheaf topos PSh(C)PSh(C) is the free cocompletion of the category CC, hence the category obtained from CC by freely forming colimits of its objects.

In contrast, the localization Sh(C)PSh(C)Sh(C) \hookrightarrow PSh(C) enforces relations between these free colimits.

Therefore in total we may think of Sh(C)Sh(C) as obtained by generators and relations from the site CC:

  • the objects of CC are the generators;

  • the coverings of CC are the relations.

Def. 13 is the “external” characterization of sheaf toposes.

More intrinsically we have Giraud's theorem:

This characterization, or rather its refinement to (infinity,1)-categories of (infinity,1)-sheaves, is crucial, below, for the discussion of principal bundles and their associated fiber bundles.

For other general considerations we need rather that every sheaf topos is in particular an elementary topos

The first of these says that the internal language is dependent type theory with dependent sum types and dependent product types, the second says that its has a type of propositions. This we turn to in Smooth Spaces - Syntactic Layer below.


Slice toposes

Local, connected and cohesive toposes

The topos of smooth spaces


The sheaf topos, def. 13, of smooth spaces enjoys a few crucial properties: it is


The full sheaf topos Sh(CartSp)Sh(CartSp) on CartSp is a locally connected topos in that the terminal global section geometric morphism to Set is an essential geometric morphism:

Sh(CartSp)ΓLConstΠ 0Set Sh(CartSp) \stackrel{\overset{\Pi_0}{\to}}{\stackrel{\overset{L Const}{\leftarrow}}{\underset{\Gamma}{\to}}} Set

The extra left adjoint Π 0:Sh(CartSp)Set\Pi_0 : Sh(CartSp) \to Set sends diffeological spaces to the set of path-connected components of their underlying topological spaces.


The sheaf topos Sh(CartSp)Sh(CartSp) on CartSp is a locally connected topos.


The following argument works for every site CC which is such that constant presheaves on CC are already sheaves.

Notice that this is the case for C=CartSpC = CartSp because every Cartesian space is connected: for SSetS \in Set a compatible family of elements of ConstSConst S on a cover {U i n}\{U_i \to \mathbb{R}^n\} of some n\mathbb{R}^n is an element of SS on each patch, such that their restriction maps to intersections of patches coincide. But the restriction maps are all identities, so this says that all these elements coincide. Therefore the set of compatible families is just the set SS itself, hence the presheaf ConstSConst S is a sheaf.

So with L:PSh(C)Sh(C)L : PSh(C) \to Sh(C) the sheafification functor we have that LConstSConstSL Const S \simeq Const S.

Whenever this is the case the left adjoint to the constant presheaf functor, which always exists for presheaves and is given by the colimit functor, is also left adjoint on the level of sheaves, because for each XSh(C)X \in Sh(C) and SSetS \in Set we have natural bijections

Hom Sh(C)(X,LConstS) =Hom PSh(C)(X,LConstS) Hom PSh(C)(X,ConstS) Hom Set(lim X,S). \begin{aligned} Hom_{Sh(C)}(X, L Const S) & = Hom_{PSh(C)}(X, L Const S) \\ & \simeq Hom_{PSh(C)}(X, Const S) \\ & \simeq Hom_{Set}(\lim_\to X, S) \end{aligned} \,.

Write Π 0:=lim :Sh(CartSp)Set\Pi_0 := \lim_\to : Sh(CartSp) \to Set for the left adjoint to LConst:SetConstPSh(C)LSh(C)LConst : Set \stackrel{Const}{\to} PSh(C) \stackrel{L}{\to} Sh(C).


For XSh(C)X \in Sh(C) a diffeological space, Π 0(X)\Pi_0(X) is the set of path-connected components of the topological space underlying XX.


By the co-Yoneda lemma we may write

X=lim (UX)y/XU X = {\lim_\to}_{(U \to X) \in y/X} U

and since Π 0\Pi_0 commutes with colimits we have

Π 0(X)Π 0lim (UX)Ulim (UX)Π 0(U). \Pi_0(X) \simeq \Pi_0 {\lim_\to}_{(U \to X)} U \simeq {\lim_\to}_{(U \to X)} \Pi_0(U) \,.

But also by the co-Yoneda lemma we have that the colimit over any representable is the singleton set, hence our expression

lim (UX)* \cdots \simeq {\lim_\to}_{(U \to X)} *

is the colimit over the category of plots of XX of the functor that is constant on the point. This colimit is the coproduct of points over the connected components of the diagram category.

The connected components of the category of plots y/Xy/X are the path-connected (or “plot-connected”) components of the underlying topological space of XX.


The sheaf topos Sh(CartSp)Sh(CartSp) on CartSp is actually a connected topos.


Since CartSpCartSp is a connected category it is immediate that Const:SetPSh(CartSp)Const \colon Set \to PSh(CartSp) is a full and faithful functor. By the above this equals LConstL Const, which is hence also full and faithful.

By the discussion at connected topos we could equivalently convince ourselves that Π 0\Pi_0 preserves the terminal object. The terminal object of Sh(CartSp)Sh(CartSp) is y( 0)y(\mathbb{R}^0), hence representable. By the above, Π 0\Pi_0 sends all representable objects to the singleton set, which is the terminal object of SetSet.


The sheaf topos Sh(CartSp)Sh(CartSp) is also a local topos

(LConstΓCoDisc):Sh(CartSp)CoDiscΓLConstSet (L Const \dashv \Gamma \dashv CoDisc) \colon Sh(CartSp) \stackrel{\overset{L Const}{\longleftarrow}}{\stackrel{\overset{\Gamma}{\longrightarrow}}{\underset{CoDisc}{\longleftarrow}}} Set

The site CartSp is a local site: it has a terminal object and the only covering sieve of this object is the trivial one. This implies the claim, by the discussion at local site.

Concretely, the extra right adjoint CoDiscCoDisc takes a set SS to the presheaf given by the assigmnent

CoDisc(S):UHom Set(CartSp(*,U),S), CoDisc(S) : U \mapsto Hom_{Set}(CartSp(*,U), S) \,,

that takes a Cartesian space UU to the set of functions from its underlying set of points to SS. This is clearly a sheaf (a function of sets from UU to SS is clearly fixed by all its restrictions to a collections of subsets of UU whose unition is UU.)

Geometrically, the object CoDiscSSh(CartSp)CoDisc S \in Sh(CartSp) is the diffeological space codiscrete (indiscrte) smooth structure.


Every local topos comes with its notion of concrete sheaves that form a sub-quasitopos. For the local topos Sh(CartSp)Sh(CartSp) these are precisely the diffeological spaces.

SetCoDiscDiffologicalSpSh(CartSp) Set \stackrel{\leftarrow}{\underset{CoDisc}{\hookrightarrow}} DiffologicalSp \stackrel{\leftarrow}{\hookrightarrow} Sh(CartSp)

The concrete sheaves for the local topos Sh(CartSp)Sh(CartSp) are by definition those objects XX for which the (ΓCoDisc)(\Gamma \dashv CoDisc)-unit

XCoDiscΓX X \to CoDisc \Gamma X

is a monomorphism. Monomorphisms of sheaves are tested objectwise, so that means equivalently that for every UCartSpU \in CartSp we have that

X(U)Hom Sh(U,X)Hom Sh(U,CodiscΓX)Hom Set(ΓU,ΓX) X(U) \simeq Hom_{Sh}(U,X) \to Hom_{Sh}(U, Codisc \Gamma X) \simeq Hom_{Set}(\Gamma U, \Gamma X)

is a monomorphism. This is precisely the condition on a sheaf to be a diffeological space.


The sheaf topos Sh(CartSp)Sh(CartSp) is even a cohesive topos in which the axiom pieces have points holds.


The site CartSp is a cohesive site (see there for detail). This implies the statement.

This implies that Sh(CartSp)Sh(CartSp) is a locally connected topos, connected topos, local topos. It means in addition that it is also a strongly connected topos.

This means that there is a homotopy category or concordance category of smooth spaces, with the same objects as Sh(CartSp)Sh(CartSp), but with hom-sets given by

Conc(X,Y):=Π 0[X,Y] Sh(CartSp), Conc(X,Y) := \Pi_0 [X,Y]_{Sh(CartSp)} \,,

where [X,Y] Sh(CartSp)[X,Y]_{Sh(CartSp)} is the internal hom in the cartesian closed category Sh(CartSp)Sh(CartSp).

Syntactic Layer

In this Syntactic Layer we discuss the two further aspects that the internal language of a topos adds to the internal language of a just a category with finite products (which is the dependent type theory with unit type and product type discussed in Coordinate systems - Syntactic Layer): dependent product types and a type of propositions.

dependent type theory \leftrightarrow locally cartesian closed category

type of propositions \leftrightarrow subobject classifier


Type theory of a topos

Natural deduction rules for dependent product types
type theorycategory theory
natural deductionuniversal construction
dependent product typedependent product
type formationX:Typex:XA(x):Type( x:XA(x)):Type\displaystyle\frac{\vdash\: X \colon Type \;\;\;\;\; x \colon X \;\vdash\; A(x)\colon Type}{\vdash \; \left(\prod_{x \colon X} A\left(x\right)\right) \colon Type}(A p 1 p 1 X p 1𝒞)( x:XA(x)𝒞)\left( \array{ A^{\phantom{p_1}} \\ \downarrow^{p_1} \\ X_{\phantom{p_1}}} \in \mathcal{C}\right) \Rightarrow \left( \prod_{x\colon X} A\left(x\right) \in \mathcal{C}\right)
term introductionx:Xa(x):A(x)(xa(x)): x:XA(x)\displaystyle\frac{x \colon X \;\vdash\; a\left(x\right) \colon A\left(x\right)}{\vdash (x \mapsto a\left(x\right)) \colon \prod_{x' \colon X} A\left(x'\right) }
term eliminationf:( x:XA(x))x:Xx:Xf(x):A(x)\displaystyle\frac{\vdash\; f \colon \left(\prod_{x \colon X} A\left(x\right)\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A(x)}
computation rule(ya(y))(x)=a(x)(y \mapsto a(y))(x) = a(x)

In the special case that AA does not actually deopend on XX:

type theorycategory theory
natural deductionuniversal construction
function typeinternal hom
type formationX:TypeA:Type(XA):Type\frac{\vdash\: X \colon Type \;\;\;\;\; \vdash\; A\colon Type}{\vdash \; \left(X \to A\right) \colon Type}
term introductionx:Xa(x):A(xa(x)):(XA)\frac{x \colon X \;\vdash\; a(x) \colon A}{\vdash (x \mapsto a\left(x\right)) \colon \left(X \to A\right) }
term eliminationf:(XA)x:Xx:Xf(x):A\frac{\vdash\; f \colon \left(X \to A\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A}
computation rule(ya(y))(x)=a(x)(y \mapsto a(y))(x) = a(x)
Internal logic of a topos

What is called logic is the syntax for (-1)-truncated objects in slice categories, hence of monomorphisms regarded as objects of slice categories.


Sharp modality and Codiscrete types

Let H\mathbf{H} be a local topos

HCoDiscΓDisc. \mathbf{H} \stackrel{\stackrel{Disc}{\leftarrow}}{\stackrel{\overset{\Gamma}{\to}}{\underset{CoDisc}{\leftarrow}}} \,.


():HΓDisc.coDiscΓ. (\flat \dashv \sharp) \; \colon \; \mathbf{H} \stackrel{\overset{Disc}{\leftarrow}}{\underset{\Gamma}{\to}} \, . \stackrel{\overset{\Gamma}{\leftarrow}}{\underset{coDisc}{\to}} \, .

for the induced adjoint monad \sharp and comonad \flat. We

  • call \sharp the sharp modality;

  • call \flat the flat modality.

The term modality refers to modal logic. (…)


We refer to A\sharp A as the sharp type of AA. This may be thought of as referring to the fact that by adjunction a homomorphism XAX \to \sharp A is equivalently a function ΓXΓA\Gamma X \to \Gamma A of the underlying sets. This means that smooth maps XAX \to \sharp A are like maps into AA that do not have to respect the cohesive structure on AA, but instead can be arbitrarily “kinky” (“sharp”).

This motivates the following terminology.


We write

DeCoh X:XX DeCoh_X \colon X \to \sharp X

For the unit of the (ΓcoDisc)(\Gamma \vdash coDisc)-adjunction.


Revised on June 6, 2016 11:59:50 by Cliff Harvey? (