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
theory (physics), model (physics)
experiment, measurement, computable physics
Axiomatizations
Tools
Structural phenomena
Types of quantum field thories
synthetic differential geometry
Introductions
from point-set topology to differentiable manifolds
geometry of physics: coordinate systems, smooth spaces, manifolds, smooth homotopy types, supergeometry
Differentials
Tangency
The magic algebraic facts
Theorems
Axiomatics
(shape modality $\dashv$ flat modality $\dashv$ sharp modality)
$(ʃ \dashv \flat \dashv \sharp )$
dR-shape modality $\dashv$ dR-flat modality
$ʃ_{dR} \dashv \flat_{dR}$
(reduction modality $\dashv$ infinitesimal shape modality $\dashv$ infinitesimal flat modality)
$(\Re \dashv \Im \dashv \&)$
fermionic modality $\dashv$ bosonic modality $\dashv$ rheonomy modality
$(\rightrightarrows \dashv \rightsquigarrow \dashv Rh)$
Models
Models for Smooth Infinitesimal Analysis
smooth algebra ($C^\infty$-ring)
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.
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.
In this Model Layer we discuss concretely the definition of smooth spaces and of homomorphisms between them, together with basic examples and properties.
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?(https://ncatlab.org/nlab/show/geometry+of+physics+–+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 $X$. Instead, we define smooth spaces $X$ entirely operationally as something about which we can ask “Which ways are there to lay out $\mathbb{R}^n$ inside $X$?” 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:
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;
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.
For brevity we will refer to “a way to lay out a coordinate system in $X$” as a plot of $X$.
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 $X$ is
a collection of sets: for each Cartesian space $\mathbb{R}^n$ (hence for each natural number $n$) a set
– to be thought of as the set of ways of laying out $\mathbb{R}^n$ inside $X$;
for each abstract coordinate transformation, hence for each smooth function $f : \mathbb{R}^{n_1} \to \mathbb{R}^{n_2}$ a function between the corresponding sets
– to be thought of as the function that sends a plot of $X$ by $\mathbb{R}^{n_2}$ to the correspondingly transformed plot by $\mathbb{R}^{n_1}$ induced by laying out $\mathbb{R}^{n_1}$ inside $\mathbb{R}^{n_2}$.
such that this is compatible with coordinate transformations:
the identity coordinate transformation does not change the plots:
changing plots along two consecutive coordinate transformations $f_1 \colon \mathbb{R}^{n_1} \to \mathbb{R}^{n_2}$ and $f_2 \colon \mathbb{R}^{n_2} \to \mathbb{R}^{n_3}$ is the same as changing them along the composite coordinate transformation $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 $X$ be a smooth pre-space, def. 2. For $\{U_i \to \mathbb{R}^n\}_{i \in I}$ a differentially good open cover, def. \ref{DifferentiallyGoodOpenCover}, let
be the set of $I$-tuples of $U_i$-plots of $X$ which coincide on all double intersections
(also called the matching families of $X$ over the given cover):
says in words:
The plot $p_i$ of $X$ by the coordinate system $U_i$ inside the bigger coordinate system $\mathbb{R}^n$ coincides with the plot $p_j$ of $X$ by the other coordinate system $U_j$ inside $X$ when both are restricted to the intersection $U_i \cap U_j$ of $U_i$ with $U_j$ inside $\mathbb{R}^n$.
For each differentially good open cover $\{U_i \to \mathbb{R}^n\}_{i \in I}$ and each smooth pre-space $X$, def. 2, there is a canonical function
from the set of $\mathbb{R}^n$-plots of $X$ to the set of tuples of glued plots, which sends a plot $p \in X(\mathbb{R}^n)$ to its restriction to all the $\phi_i \colon U_i \hookrightarrow \mathbb{R}^n$:
If $X$ 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 $\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 \to \mathbb{R}^n\}$ as above. Therefore:
A smooth pre-space $X$, def. 2 is a smooth space if for all differentially good open covers $\{U_i \to \mathbb{R}^n\}$, def. \ref{DifferentiallyGoodOpenCover}, the canonical function of remark 3 from plots to glued plots is a bijection
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 $\mathbb{R}^2 \simeq D^2$ along a common rim yields the smooth space version of the sphere $S^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 \in \mathbb{R}^n$, there is a smooth space, def. 4, whose set of plots over the abstract coordinate systems $\mathbb{R}^k$ is the set
of smooth functions from $\mathbb{R}^k$ to $\mathbb{R}^n$.
Clearly this is the rule for plots that characterize $\mathbb{R}^n$ itself as a smooth space, and so we will just denote this smooth space by the same symbols “$\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 $S \in$ Set a set, write
for the smooth space whose set of $U$-plots for every $U \in CartSp$ is always $S$.
and which sends every coordinate transformation $f \colon \mathbb{R}^{n_1} \to \mathbb{R}^{n_2}$ to the identity function on $S$.
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.
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 : X \to Y$ between two smooth spaces is, it has to take the plots of $X$ by $\mathbb{R}^n$ to a corresponding plot of $Y$, such that this respects coordinate transformations.
Let $X$ and $Y$ be two smooth spaces, def. 4. Then a homomorphism $f \colon X \to Y$ is
for each abstract coordinate system $\mathbb{R}^n$ (hence for each $n \in \mathbb{N}$) a function
$f_{\mathbb{R}^n} : X(\mathbb{R}^n) \to Y(\mathbb{R}^n)$
that sends $\mathbb{R}^n$-plots of $X$ to $\mathbb{R}^n$-plots of $Y$
such that
for each smooth function $\phi : \mathbb{R}^{n_1} \to \mathbb{R}^{n_2}$ we have
hence a commuting diagram
For $f_1 : X \to Y$ and $f_2 : X \to Y$ two homomorphisms of smooth spaces, their composition $f_2 \circ f_1 \colon X \to Y$ is defined to be the homomorphism whose component over $\mathbb{R}^n$ is the composite of functions of the components of $f_1$ and $f_2$:
Write $Smooth0Type$ 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 $X$: on the hand, $X$ comes by definition with a rule for what the set $X(\mathbb{R}^n)$ of its $\mathbb{R}^n$-plots is. On the other hand, we can now regard the abstract coordinate system $\mathbb{R}^n$ itself as a smooth space, by example 1, and then say that an $\mathbb{R}^n$-plot of $X$ should be a homomorphism of smooth spaces of the form $\mathbb{R}^n \to X$.
The following proposition says that these two superficially different notions actually naturally coincide.
Let $X$ be any smooth space, def. 4, and regard the abstract coordinate system $\mathbb{R}^n$ as a smooth space, by example 1. There is a natural bijection
between the postulated $\mathbb{R}^n$-plots of $X$ and the actual $\mathbb{R}^n$-plots given by homomorphism of smooth spaces $\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 : \mathbb{R}^n \to X$ is uniquely fixed by the image of the identity element in $\mathbb{R}^n(\mathbb{R}^n) \coloneqq CartSp(\mathbb{R}^n, \mathbb{R}^n)$ under the component function $f_{\mathbb{R}^n} : \mathbb{R}^n(\mathbb{R}^n) \to X(\mathbb{R}^n)$.
Let $\mathbb{R} \in Smooth0Type$ denote the real line, regarded as a smooth space by def. 1. Then for $X \in Smooth0Type$ any smooth space, a homomorphism of smooth spaces
is a smooth function on $X$. Prop. 1 says here that when $X$ 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 $\mathbb{R}^0$ we also call the point and regarded as a smooth space we will often write it as
For any $X \in Smooth0Type$, we say that a homomorphism
is a point of $X$.
By prop. 1 the points of a smooth space $X$ are naturally identified with its 0-dimensional plots, hence with the “ways of laying out a 0-dimensional coordinate system” in $X$:
Let $X, Y \in Smooth0Type$ by two smooth spaces. Their product is the smooth space $X \times Y \in Smooth0Type$ whose plots are pairs of plots of $X$ and $Y$:
The projection on the first factor is the homomorphism
which sends $\mathbb{R}^n$-plots of $X \times Y$ to those of $X$ by forming the projection of the cartesian product of sets:
Analogously for the projection to the second factor
Let $* = \mathbb{R}^0$ be the point, regarded as a smooth space, def. 8. Then for $X \in Smooth0Type$ any smooth space the canonical projection homomorphism
is an isomorphism.
Let $f \colon X \to Z$ and $g \colon Y \to Z$ be two homomorphisms of smooth spaces, def. 6. There is then a new smooth space to be denoted
(with $f$ and $g$ understood), called the fiber product of $X$ and $Y$ along $f$ and $g$, and defined as follows:
the set of $\mathbb{R}^n$-plots of $X \times_Z Y$ is the set of pairs of plots of $X$ and $Y$ which become the same plot of $Z$ under $f$ and $g$, respectively:
Let $\Sigma, X \in Smooth0Type$ be two smooth spaces, def. 4. Then the smooth mapping space
is the smooth space defined by saying that its set of $\mathbb{R}^n$-plots is
Here in $\Sigma \times \mathbb{R}^n$ we first regard the abstract coordinate system $\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 $\mathbb{R}^n$-plot of the mapping space $[\Sigma,X]$ is a smooth $\mathbb{R}^n$-parameterized family of homomorphisms $\Sigma \to X$.
There is a natural bijection
for every smooth space $K$.
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 $K$ into the mapping space $[\Sigma,X]$ is equivalently a smooth function from $K \times \Sigma$ to $X$. The latter we may regard as a $K$-parameterized smooth family of smooth functions $\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 $[\Sigma,X]$ is the smooth moduli space of smooth functions from $\Sigma \to X$, because it is such that smooth maps $K \to [\Sigma,X]$ into it modulate, as we move around on $K$, a family of smooth functions $\Sigma\to X$, depending on $K$.
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 $n$-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 $[\Sigma,X]$ is the bare set of homomorphism $\Sigma \to X$: there is a natural isomorphism
Given a smooth space $X \in Smooth0Type$, its smooth path space is the smooth mapping space
By prop. 4 the points of $P X$ are indeed precisely the smooth trajectories $\mathbb{R}^1 \to X$. But $P 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 $X$ is a model for spacetime, then $P X$ may notably be interpreted as the smooth space of worldlines in $X$, hence the smooth space of paths or trajectories of a particle in $X$.
If in the above example 3 the path is constraind to be a loop in $X$, one obtains the smooth loop space
In example 2 we saw that a smooth function on a general smooth space $X$ is a homomorphism of smooth spaces, def. 6
The collection of these forms the hom-set $Hom_{Smooth0Type}(X, \mathbb{R})$. But by the discussion in Smooth mapping spaces such hom-sets are naturally refined to smooth spaces themselves.
For $X \in Smooth0Type$ a smooth space, we say that the moduli space of smooth functions on $X$ is the smooth mapping space (def. 11), from $X$ into the standard real line $\mathbb{R}$
We will also denote this by
since in the special case that $X$ is a Cartesian space this is the smooth refinement of the set $C^\infty(X)$ of smooth functions, def. \ref{SmoothFunctions}, on $X$.
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 $X \to \mathbb{R}$.
By prop. 4 a point $* \to [X,\mathbb{R}^1]$ of the moduli space is equivalently a smooth function $X \to \mathbb{R}^1$.
Later we define/see the following:
A smooth manifold is a smooth space that is locally equivalent to a coordinate system;
A diffeological space is a smooth space such that every coordinate labels a point in the space. In other words, a diffeological space is a smooth space that has an underlying set $X_s \in Set$ of points such that the set of $\mathbb{R}^n$-plots is a subset of the set of all functions:
(This need not be the case in a general smooth space, important counterexamples are the universal smooth moduli spaces of differential forms in Smooth moduli space of differential forms).
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.
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
Here the left adjoint $\overline{(-)}$, which is equivalently
the inverse image of the geometric embedding geometric morphism
the sheafification functor
is precisely such that for every covering $\{U_i \to U\}_{i \in I}$ in the site $C$ the sieve inclusion
(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)$ is the free cocompletion of the category $C$, hence the category obtained from $C$ by freely forming colimits of its objects.
In contrast, the localization $Sh(C) \hookrightarrow PSh(C)$ enforces relations between these free colimits.
Therefore in total we may think of $Sh(C)$ as obtained by generators and relations from the site $C$:
the objects of $C$ are the generators;
the coverings of $C$ are the relations.
Def. 13 is the “external” characterization of sheaf toposes.
More intrinsically we have Giraud's theorem:
A sheaf topos is equivalently a presentable category with
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.
A smooth pre-space, def. 2 is equivalently a presheaf on CartSp, hence a functor $X : CartSp^{op} \to Set$;
a smooth space, def. 4, is equivalently a presheaf on CartSp which is a sheaf with respect to the differentially good open cover-coverage:
the set of “glued plots”, def. 3 is the descent object;
the canonical morphism of remark 3 is the descent morphism;
the condition that it be an isomorphism (for each differentially good open cover) is the descent- or sheaf condition.
The sheaf topos, def. 13, of smooth spaces enjoys a few crucial properties: it is
a cohesive topos. This we discuss in the remainder of this Semantic Layer.
The full sheaf topos $Sh(CartSp)$ on CartSp is a locally connected topos in that the terminal global section geometric morphism to Set is an essential geometric morphism:
The extra left adjoint $\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)$ on CartSp is a locally connected topos.
The following argument works for every site $C$ which is such that constant presheaves on $C$ are already sheaves.
Notice that this is the case for $C = CartSp$ because every Cartesian space is connected: for $S \in Set$ a compatible family of elements of $Const S$ on a cover $\{U_i \to \mathbb{R}^n\}$ of some $\mathbb{R}^n$ is an element of $S$ 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 $S$ itself, hence the presheaf $Const S$ is a sheaf.
So with $L : PSh(C) \to Sh(C)$ the sheafification functor we have that $L 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 $X \in Sh(C)$ and $S \in Set$ we have natural bijections
Write $\Pi_0 := \lim_\to : Sh(CartSp) \to Set$ for the left adjoint to $LConst : Set \stackrel{Const}{\to} PSh(C) \stackrel{L}{\to} Sh(C)$.
For $X \in Sh(C)$ a diffeological space, $\Pi_0(X)$ is the set of path-connected components of the topological space underlying $X$.
By the co-Yoneda lemma we may write
and since $\Pi_0$ commutes with colimits we have
But also by the co-Yoneda lemma we have that the colimit over any representable is the singleton set, hence our expression
is the colimit over the category of plots of $X$ 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/X$ are the path-connected (or “plot-connected”) components of the underlying topological space of $X$.
The sheaf topos $Sh(CartSp)$ on CartSp is actually a connected topos.
Since $CartSp$ is a connected category it is immediate that $Const \colon Set \to PSh(CartSp)$ is a full and faithful functor. By the above this equals $L Const$, which is hence also full and faithful.
By the discussion at connected topos we could equivalently convince ourselves that $\Pi_0$ preserves the terminal object. The terminal object of $Sh(CartSp)$ is $y(\mathbb{R}^0)$, hence representable. By the above, $\Pi_0$ sends all representable objects to the singleton set, which is the terminal object of $Set$.
The sheaf topos $Sh(CartSp)$ is also a local topos
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 $CoDisc$ takes a set $S$ to the presheaf given by the assigmnent
that takes a Cartesian space $U$ to the set of functions from its underlying set of points to $S$. This is clearly a sheaf (a function of sets from $U$ to $S$ is clearly fixed by all its restrictions to a collections of subsets of $U$ whose unition is $U$.)
Geometrically, the object $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)$ these are precisely the diffeological spaces.
The concrete sheaves for the local topos $Sh(CartSp)$ are by definition those objects $X$ for which the $(\Gamma \dashv CoDisc)$-unit
is a monomorphism. Monomorphisms of sheaves are tested objectwise, so that means equivalently that for every $U \in CartSp$ we have that
is a monomorphism. This is precisely the condition on a sheaf to be a diffeological space.
The sheaf topos $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)$ 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)$, but with hom-sets given by
where $[X,Y]_{Sh(CartSp)}$ is the internal hom in the cartesian closed category $Sh(CartSp)$.
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 | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
dependent product type | dependent product | |
type formation | $\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}$ | $\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 introduction | $\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 elimination | $\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 | $(y \mapsto a(y))(x) = a(x)$ |
In the special case that $A$ does not actually deopend on $X$:
type theory | category theory | |
---|---|---|
syntax | semantics | |
natural deduction | universal construction | |
function type | internal hom | |
type formation | $\frac{\vdash\: X \colon Type \;\;\;\;\; \vdash\; A\colon Type}{\vdash \; \left(X \to A\right) \colon Type}$ | |
term introduction | $\frac{x \colon X \;\vdash\; a(x) \colon A}{\vdash (x \mapsto a\left(x\right)) \colon \left(X \to A\right) }$ | |
term elimination | $\frac{\vdash\; f \colon \left(X \to A\right)\;\;\;\; \vdash \; x \colon X}{x \colon X\;\vdash\; f(x) \colon A}$ | |
computation rule | $(y \mapsto a(y))(x) = a(x)$ |
What is called logic is the syntax for (-1)-truncated objects in slice categories, hence of monomorphisms regarded as objects of slice categories.
(…)
Let $\mathbf{H}$ be a local topos
Write
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 $\sharp A$ as the sharp type of $A$. This may be thought of as referring to the fact that by adjunction a homomorphism $X \to \sharp A$ is equivalently a function $\Gamma X \to \Gamma A$ of the underlying sets. This means that smooth maps $X \to \sharp A$ are like maps into $A$ that do not have to respect the cohesive structure on $A$, but instead can be arbitrarily “kinky” (“sharp”).
This motivates the following terminology.
We write
For the unit of the $(\Gamma \vdash coDisc)$-adjunction.
(…)