nLab geometry of physics -- differentiation


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



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




infinitesimal cohesion

tangent cohesion

differential cohesion

graded differential cohesion

singular 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& \mathrm{R}\!\!\mathrm{h} & \stackrel{rheonomic}{} \\ && \vee && \vee \\ &\stackrel{reduced}{} & \Re &\dashv& \Im & \stackrel{infinitesimal}{} \\ && \bot && \bot \\ &\stackrel{infinitesimal}{}& \Im &\dashv& \& & \stackrel{\text{étale}}{} \\ && \vee && \vee \\ &\stackrel{cohesive}{}& \esh &\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)



So far we have dealt with cohesive structures for which there is a notion of smooth variation, say of the position of a particle along a trajectory in spacetime. The idea of differentiation is to measure the difference between the position of two points on a cohesive trajectory in space as the difference between their worldline coordinates “tends to 0” without actually becoming 0. One also says that differentiation is forming “infinitesimal differences” of a cohesive process – and we will make precise here what this means.

There are two stages to the theory of differentiation:

  1. We may think of differentiation as just a means to analyze more in detail the cohesive structure already given, without adding new structure, hence without a priori refining our notion of what a “cohesive trajectory” is. Indeed, given any line object \mathbb{R} in a cohesive ∞-topos, there is canonically a homomorphism of cohesive spaces

    d:Ω cl 1(,) \mathbf{d} \colon \mathbb{R} \to \Omega^1_{cl}(-,\mathbb{R})

    from the line to the cohesive moduli space of closed differential 1-forms, which is such that it sends a cohesive curve on the line to the differential form on this curve whose value at each point is the differential of the curve, its rate of infinitesimal change at that point.

    Below in Differentiation of smooth functions and differetial forms we discuss this construction in the standard model of smooth cohesion for smooth spaces, where it reproduces what traditionally is called the de Rham differential d\mathbf{d}.

    Further below in Maurer-Cartan forms – Cohesive differentiation we show how d\mathbf{d} comes out from just the abstract axioms of cohesionn.

  2. We may think of differentiation as reflecting a refinement of smooth cohesion such that infinitesimal cohesive trajectories actually exist. Here, on top of having a measure for how a cohesive trajectory changes infinitesimally at a given point, it makes sense to ask concretely if two points on a trajectory are infinitesimally close to each other. In this approach the very notion of cohesion is refined to include explicitly a way to speak not just about a “cohesive blob of points”, but to decide whether it is in fact just an “infinitesimal cohesive blob of points” – an infinitesimally thickened point.

    Differential geometry with such an explicit notion of infinitesimals is known as synthetic differential geometry: the axioms here allow one to synthesize an infinitesimally thickened point and not just to reason about it as if it existed.

    In such a synthetic differential context then the differential d\mathbf{d} from above not just exists as a whole, but we can “take it apart and re-synthesize it” by realizing its value at each point literally as the ordinary difference between two infinitesimally close points. Similarly, various other fundamental constructions in differential geometry, such as that of tangent bundles and jet bundles have a usefully transparent axiomatic characterization in the presence of synthetic infinitesimals. (Sophus Lie, one of the founding fathers of differential geometry famously said that he indeed found his theorems using such synthetic reasoning intuitively, and just did not publish them this way due to a lack of formalization of this language – at his time. ) This we discuss in the Mod Layer in D-geometry below.

In the Differentiation semantic layer below we formalize differentiation, and these two aspects of it, by adding to the notion of cohesive topos that of an infinitesimal cohesive neighbourhood.

Recalling that a cohesive topos is an abstract cohesive blob, an infinitesimal cohesive neighbourhood is accordingly an infinitesimally thicked cohesive blob (which is itself again a cohesive blob):

CohesiveBlob InfinitesimallyThickenedCohesiveBlob PointH H th DiscSpaces. \array{ CohesiveBlob &&\hookrightarrow&& InfinitesimallyThickenedCohesiveBlob \\ & \searrow && \swarrow \\ && Point } \;\;\;\;\;\;\;\; \array{ \mathbf{H} &&\stackrel{}{\hookrightarrow}&& \mathbf{H}_{th} \\ & \searrow && \swarrow \\ && DiscSpaces } \,.

Model Layer

We discuss

By considering fiber products of smooth mapping spaces with discrete spaces of boundary configurations, we obtain from this the differentiation theory called

Differentiation of smooth functions and differential forms

Differentiation on coordinate patches

By definition to smooth function f:f \colon \mathbb{R} \to \mathbb{R} is associated its derivative, a smooth function f:f' \colon \mathbb{R} \to \mathbb{R}. And more generally to a smooth function f: nf \colon \mathbb{R}^n \to \mathbb{R} are associated its partial derivatives, smooth functions

fx i: n \frac{\partial f}{\partial x^i} \colon \mathbb{R}^n \to \mathbb{R}

for 1in1 \leq i \leq n .

The de Rham differential collects all partial derivatives of a function into a single differential 1-form


For nn \in \mathbb{N}, The de Rham differential on smooth functions in C ( n)C^\infty(\mathbb{R}^n) is the function

d:C ( n)Ω 1( n) \mathbf{d} \colon C^\infty(\mathbb{R}^n) \to \Omega^1(\mathbb{R}^n)

which takes fC ( n)f \in C^\infty(\mathbb{R}^n) to

df i=1 nfx idx i. \mathbf{d}f \coloneqq \sum_{i = 1}^n \frac{\partial f}{\partial x^i} \mathbf{d} x^i \,.

For x i: nx^i \colon \mathbb{R}^n \to \mathbb{R} one of the coordinate functions, the de Rham differential dx i\mathbf{d} x^i indeed coincides with the basis element of the same name according to def. , using that

x ix j={1 |i=j 0 |otherwise. \frac{\partial x^i}{\partial x^{j}} = \left\{ \array{ 1 & | i = j \\ 0 & | otherwise } \right. \,.

The de Rham differentials d:C ( n)Ω 1( n)\mathbf{d} \colon C^\infty(\mathbb{R}^n) \to \Omega^1(\mathbb{R}^n) for all nn \in \mathbb{N} are compatible with pullback of differential 1-forms, def. , in that for each coordinate transformation ϕ: k˜ k\phi \colon \mathbb{R}^{\tilde k} \to \mathbb{R}^{k} the diagram

C ( k) d Ω 1( k) ϕ * ϕ * C ( k˜) d Ω 1( k˜) \array{ C^\infty(\mathbb{R}^k) &\stackrel{\mathbf{d}}{\to}& \Omega^1(\mathbb{R}^k) \\ \downarrow^{\mathrlap{\phi^\ast}} && \downarrow^{\mathrlap{\phi^\ast}} \\ C^\infty(\mathbb{R}^{\tilde k}) &\stackrel{\mathbf{d}}{\to}& \Omega^1(\mathbb{R}^{\tilde k}) }



This is equivalently the statement of the chain rule of differentiation: For any fC ( k)f \in C^\infty(\mathbb{R}^k) we have on the one hand, by def. and def.

dϕ *f =d(fϕ) = j=1 k˜(fϕ)x jdx j \begin{aligned} \mathbf{d} \phi^\ast f & = \mathbf{d} (f \circ \phi) \\ & = \sum_{j = 1}^{\tilde k} \frac{\partial (f \circ \phi)}{\partial x^j}\mathbf{d} x^j \end{aligned}

and on the other hand, applying the definition in the other order,

ϕ *df =ϕ * i=1 kfx idx i = i=1 k j=1 k˜(fx iϕ)(ϕ ix j)dx j. \begin{aligned} \phi^* \mathbf{d}f & = \phi^* \sum_{i = 1}^k \frac{\partial f}{\partial x^i} \mathbf{d}x^i \\ & = \sum_{i = 1}^k \sum_{j = 1}^{\tilde k} \left(\frac{\partial f}{\partial x^i}\circ \phi \right) \cdot \left(\frac{\partial \phi^i}{\partial x^j}\right) \mathbf{d}x^j \end{aligned} \,.

Both expressions agree precisely if for all jj we have

(fϕ)x j= i=1 k(fx iϕ)(ϕ ix j)C ( k˜). \frac{\partial (f \circ \phi)}{\partial x^j} = \sum_{i = 1}^k \left(\frac{\partial f}{\partial x^i}\circ \phi\right) \cdot \left(\frac{\partial \phi^i}{\partial x^j}\right) \;\;\; \in C^\infty(\mathbb{R}^{\tilde k}) \,.

This is precisely the statement of the chain rule for differentiation.

Notice that as smooth spaces =Ω 0=C ()\mathbb{R} = \Omega^0 = C^\infty(-), by prop. . Therefore the above says that


The de Rham differential, def. , constitutes a homomorphism of smooth spaces, def.

d:Ω 1 \mathbf{d} \colon \mathbb{R} \to \Omega^1

from the real line to the universal smooth moduli space of differential 1-forms, def. .


Below in Maurer-Cartan form on a Lie group we discuss a more general abstract origin of d:Ω cl 1\mathbf{d} \colon \mathbb{R} \to \Omega^1_{cl}.

We now extend the de Rham differential to differential forms of higher degree.


For all nn \in \mathbb{N} let

d:Ω ( n)Ω ( n) \mathbf{d} \colon \Omega^\bullet(\mathbb{R}^n) \to \Omega^\bullet(\mathbb{R}^n)

be the unique extension of d:C ()Ω 1()\mathbf{d} \colon C^\infty(-) \to \Omega^1(-) to a degree-1 derivation with

ddx i=0. \mathbf{d}\mathbf{d}x^i = 0 \,.



For each nn \in \mathbb{N} the de Rham differential of def. constitutes a homomorphism of smooth spaces

d:Ω nΩ n+1 \mathbf{d} \colon \Omega^n \to \Omega^{n+1}

form the universal smooth moduli space of differental nn-forms to that of differential n+1n+1-forms.

Differentiation on smooth spaces

We now extend the notion of derivatives and de Rham differentials from smooth functions on Cartesian spaces to smooth functions on general smooth spaces.

Recall from def. that the set of differential nn-forms on a smooth space XX is Ω n(X)Hom(X,Ω n)\Omega^n(X) \coloneqq Hom(X, \Omega^n).


For XSmooth0TypeX \in Smooth0Type a smooth space and nn \in \mathbb{N}, the de Rham differential on nn-forms over XX is the function

d:Ω n(X)Ω n+1(X) \mathbf{d} \colon \Omega^n(X) \to \Omega^{n+1}(X)

which is the postcomposition with the homomorphism of smooth spaces of prop. :

Hom(X,d):Hom(X,Ω n)Hom(X,Ω n+1). Hom(X,\mathbf{d}) \colon Hom(X,\Omega^n) \to Hom(X,\Omega^{n+1}) \,.

In particular the derivative of a smooth function f:Xf \colon X \to \mathbb{R} is the composite

df:XfdΩ cl 1Ω 1. \mathbf{d}f \colon X \stackrel{f}{\to} \mathbb{R} \stackrel{\mathbf{d}}{\to} \Omega^1_{cl} \hookrightarrow \Omega^1 \,.

Below in Variation is differentiation on smooth spaces we find that this notion of differentiation of smooth functions on smooth spaces subsumes what traditionally is called variational calculus of functionals on mapping spaces.

Example: The electromagnetic field strength

for instance electromagnetic potential

A=ϕdt+A 1dx 1+A 2dx 2+A 3dx 3 A = \phi \mathbf{d}t + A_1 \mathbf{d}x^1 + A_2 \mathbf{d}x^2 + A_3 \mathbf{d}x^3

then the electromagnetic field strength is

FdA=E 1dx 1dt+E 2dx 2dt+E 3dx 3dt+B 1dx 2dx 3+B 2dx 3dx 1+B 3dx 1dx 2 F \coloneqq \mathbf{d}A = E_1 \mathbf{d}x^1 \wedge \mathbf{d}t + E_2 \mathbf{d}x^2 \wedge \mathbf{d}t + E_3 \mathbf{d}x^3 \wedge \mathbf{d}t + B_1 \mathbf{d}x^2 \wedge \mathbf{d}x^3 + B_2 \mathbf{d}x^3 \wedge \mathbf{d}x^1 + B_3 \mathbf{d}x^1 \wedge \mathbf{d}x^2


E i=ϕx iA it E_i = \frac{\partial \phi}{\partial x^i} - \frac{\partial A_i}{\partial t}


B 1=A 2x 3A 3x 2 B_1 = \frac{\partial A_2}{\partial x^3} - \frac{\partial A_3}{\partial x^2}


This are the first 2 of 4 Maxwell equations: dF=0\mathbf{d} F = 0

(the other 2 are discussed below in Riemannian geometry)


A,A:XΩ 1() A,A' : X \to \Omega^1(-)

a gauge transformation AAA \to A' is λ:X\lambda : X \to \mathbb{R} with

A=A+dλ A' = A + \mathbf{d} \lambda

Variational calculus

Traditionally a functional is a function which is sufficiently like a smooth function, but defined not on a manifold, but on a mapping space between manifolds. Also traditionally, a variational derivative of such a functional is something aking to a derivative, generalized to this context, and subject to the condition that all variations preserve some boundary conditions.

We formulate this classical theory in the context of smooth spaces. Here a functional is simply a homomorphism of smooth spaces out of a smooth mapping space, as in def. . We may impose respect for boundary conditions by forming the fiber product of this mapping space with a discrete smooth space inclusion, given in def. below. Then the variational derivative is simply the ordinary derivative of def. .

Discrete points of a smooth space

For XSmooth0TypeX \in Smooth0Type a smooth space, write

ΓXHom(*,X)Set \Gamma X \coloneqq Hom(*,X) \in Set

for its set of points, the set of homomorphisms, def. , from the point to XX.


XDisc(Γ(X)) \flat X \coloneqq Disc (\Gamma(X))

for the discrete smooth space, def. , on this set of points.


For every smooth space XX there is a canonical homomorphism of smooth spaces

XX. \flat X \to X \,.

This sends a plot UXU \to \flat X, which by definition of Disc()Disc(-) is a point in ΓX\Gamma X, hence a homomorphism x:*Xx \colon * \to X, to the plot U*xXU \to * \stackrel{x}{\to} X of XX.

Smooth functionals

Let XX be a smooth manifold. Let Σ\Sigma be a smooth manifold with boundary ΣΣ\partial \Sigma \hookrightarrow \Sigma.


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

for the smooth space (a diffeological space) which is the mapping space from Σ\Sigma to XX, hence such that for each UU \in CartSp we have

[Σ,X](U)=C (U×Σ,X). [\Sigma, X](U) = C^\infty(U \times \Sigma, X) \,.


[Σ,X] Σ[Σ,X]× [Σ,X][Σ,X] [\Sigma, X]_{\partial \Sigma} \coloneqq [\Sigma, X] \times_{[\partial \Sigma,X]} \flat [\partial \Sigma,X]

for the pullback in smooth spaces

[Σ,X] Σ [Σ,X] [Σ,X] ()| Σ [Σ,X], \array{ [\Sigma,X]_{\partial \Sigma} &\to& \flat [\partial \Sigma, X] \\ \downarrow && \downarrow \\ [\Sigma,X] &\stackrel{(-)|_{\partial \Sigma}}{\to}& [\partial \Sigma,X] } \,,


  • the bottom morphism is the restriction [ΣΣ,X][\partial \Sigma \hookrightarrow \Sigma, X] of configurations to the boundary;

  • the right vertical morphism is the homomorphism from def. .


The smooth space [Σ,X] Σ[\Sigma, X]_{\partial \Sigma} is a diffeological space whose underlying set is C (Σ,X)C^\infty(\Sigma,X) and whose UU-plots for UU \in CartSp are smooth functions ϕ:U×ΣX\phi \colon U \times \Sigma \to X such that ϕ(,s):UX\phi(-,s) \colon U \to X is the constant function for all sΣΣs \in \partial \Sigma \hookrightarrow \Sigma.


A functional on the mapping space [Σ,X][\Sigma, X] is a homomorphism of smooth spaces

S:[Σ,X] Σ. S \colon [\Sigma, X]_{\partial \Sigma} \to \mathbb{R} \,.
Functional derivative / variational derivative


d:Ω 1 \mathbf{d} \colon \mathbb{R} \to \Omega^1

for the de Rham differential incarnated as a homomorphism of smooth spaces from the real line to the smooth moduli space of differential 1-forms.


The functional derivative

dSΩ 1([Σ,X] Σ) \mathbf{d}S \in \Omega^1([\Sigma,X]_{\partial \Sigma})

of a functional SS, def. , is simply its de Rham differential as a homomorphism of smooth spaces, hence the composite

dS:[Σ,X] ΣSdΩ 1. \mathbf{d} S \colon [ \Sigma, X]_{\partial \Sigma} \stackrel{S}{\to} \mathbb{R} \stackrel{\mathbf{d}}{\to} \Omega^1 \,.

This means that for each smooth parameter space UU \in CartSp and for each smooth UU-parameterized collection

ϕ:U×ΣX \phi \colon U \times \Sigma \to X

of smooth functions ΣX\Sigma \to X, constant in the parameter UU in some neighbourhood of the boundary of Σ\Sigma,

S ϕ:[Σ,X] Σ(U)C (U,) S_\phi \colon [\Sigma,X]_{\partial \Sigma}(U) \to C^\infty(U,\mathbb{R})

is the function that sends each such UU-collection of configurations to the UU-collection of their values under SS. Then

(dS) ϕΩ 1(U) (\mathbf{d}S)_\phi \in \Omega^1(U)

is the smooth differential 1-form

(dS) ϕ=d(S(ϕ)). (\mathbf{d}S)_\phi = \mathbf{d}(S(\phi)) \,.

Let Σ=[0,1]\Sigma = [0,1] \hookrightarrow \mathbb{R} be the standard interval. Let

L(,)dtΩ 1([0,1],C ( 2)) L(-,-) \mathbf{d}t \in \Omega^1([0,1], C^\infty(\mathbb{R}^2))

and consider the functional

S:([0,1]γX) 0 1L(γ(t),γ˙(t))dt. S \colon ([0,1] \stackrel{\gamma}{\to} X) \mapsto \int_{0}^1 L(\gamma(t), \dot \gamma(t)) d t \,.

Then for U=U = \mathbb{R} and any smooth UU-parameterized collection {γ u:ΣX} uU\{\gamma_{u} \colon \Sigma \to X\}_{u \in U} the functional derivative takes the value

dS γ () =(ddu 0 1L(γ u(t),γ˙ u(t))dt)du = 0 1(Lγ(γ u(t),γ˙ u(t))dγ u(t)du+Lγ˙(γ u(t),γ˙ u(t))γ˙ u(t)u)dtdu = 0 1(Lγ(γ u(t),γ˙ u(t))dγ u(t)du+Lγ˙(γ u(t),γ˙ u(t))tγ u(t)u)dtdu = 0 1(Lγ(γ u(t),γ˙ u(t))tLγ˙(γ u(t),γ˙ u(t)))γ u(t)udtdu. \begin{aligned} \mathbf{d}S_{\gamma_{(-)}} & = \left( \frac{d}{d u} \int_0^1 L(\gamma_u(t), \dot \gamma_u(t)) dt \right) \mathbf{d}u \\ & = \int_{0}^1 \left( \frac{\partial L}{\partial \gamma}(\gamma_u(t), \dot \gamma_u(t)) \frac{d \gamma_u(t)}{d u} + \frac{\partial L}{\partial \dot \gamma}(\gamma_u(t), \dot \gamma_u(t)) \frac{\partial \dot \gamma_u(t)}{\partial u} \right) dt \mathbf{d} u \\ & = \int_{0}^1 \left( \frac{\partial L}{\partial \gamma}(\gamma_u(t), \dot \gamma_u(t)) \frac{d \gamma_u(t)}{d u} + \frac{\partial L}{\partial \dot \gamma}(\gamma_u(t), \dot \gamma_u(t)) \frac{\partial }{\partial t}\frac{\partial \gamma_u(t)}{\partial u} \right) dt \mathbf{d} u \\ & = \int_{0}^1 \left( \frac{\partial L}{\partial \gamma}(\gamma_u(t), \dot \gamma_u(t)) - \frac{\partial}{\partial t}\frac{\partial L}{\partial \dot \gamma}(\gamma_u(t), \dot \gamma_u(t)) \right) \frac{\partial \gamma_u(t)}{\partial u} dt \mathbf{d}u \end{aligned} \,.

Here we used integration by parts and used that the boundary term vanishes

0 1t(γ˙L(γ u(s),γ˙ u(s))γ u(s)u)ds =(γ˙L(γ u(1),γ˙ u(1))γ u(1)u)(γ˙L(γ u(0),γ˙ u(0))γ u(0)u) =0 \begin{aligned} \int_{0}^1 \frac{\partial}{\partial t} \left( \frac{\partial}{\partial \dot\gamma} L(\gamma_u(s), \dot \gamma_u(s)) \frac{\partial \gamma_u(s)}{\partial u} \right) d s & = \left( \frac{\partial}{\partial \dot\gamma} L(\gamma_u(1), \dot \gamma_u(1)) \frac{\partial \gamma_u(1)}{\partial u} \right) - \left( \frac{\partial}{\partial \dot\gamma} L(\gamma_u(0), \dot \gamma_u(0)) \frac{\partial \gamma_u(0)}{\partial u} \right) \\ & = 0 \end{aligned}

since by prop. γ ()(1)\gamma_{(-)}(1) and γ ()(0)\gamma_{(-)}(0) are constant.

Euler-Lagrange equations


Infinitesimal smooth loci


SmoothLociSmoothAlgebras opFunc ×(CartSp,Set) SmoothLoci \coloneqq SmoothAlgebras^{op} \coloneqq Func^\times(CartSp,Set)

for the category of spaces which are formally dual to smooth algebras: the opposite category of that of smooth algebras. This is called the category of smooth loci.


A smooth Artin algebra (also called a “Weil algebra” in the synthetic differential geometry-literature) is a smooth algebra AA whose underlying \mathbb{R}-vector space is a direct sum of the form

A=V, A = \mathbb{R} \oplus V \,,

where VV is of finite dimension and such that every element vVAv \in V \subset A is nilpotent, in that there is nn \in \mathbb{N} such that the nn-fold product of vv with itself in AA vanishes: v n=0v^n = 0.


The smallest smooth Artin algebra is the ring of dual numbers, def. , for which V=V = \mathbb{R}.



InfPointSmoothLoci InfPoint \hookrightarrow SmoothLoci

for the full subcategory of SmoothLociSmoothLoci, def. , of those that are duals of Artin algebras, def. .

We call this the category of infinitesimally thickened points.

de Rham space
Jet bundles

Semantic Layer

Synthetic differential geometry

We have two full and faithful functors

CartSpSmoothLoci CartSp \hookrightarrow SmoothLoci
InfPointSmoothLoci. InfPoint \hookrightarrow SmoothLoci \,.

Write CartSp thSmoothLocus{}_{th} \hookrightarrow SmoothLocus for the full subcategory of that of smooth loci, def. , on those of the form

U=U×D \mathbf{U} = U \times D

with UCartSpSmoothLociU \in CartSp \hookrightarrow SmoothLoci and DInfPointSmoothLociD \in InfPoint \hookrightarrow SmoothLoci.

We may call this the category of infinitesimally thickened Cartesian spaces or or formal smooth Cartesian spaces.

The category CartSp thCartSp_{th} carries several coverages of interest. One is this:


For U=U×DCartSp th\mathbf{U} = U \times D \in CartSp_{th} say that a covering family is a set of morphisms in CartSp thCartSp_{th} of the form {U i×D(ϕ i,id D)U×D} i\{ U_i \times D \stackrel{(\phi_i, id_D)}{\to} U \times D\}_i such that {U iϕ iU} i\{ U_i \stackrel{\phi_i}{\to} U\}_i is a covering family in CartSp.

The corresponding sheaf topos Sh(CartSp th)Sh(CartSp_{th}) is known as the Cahiers topos.


The Cahiers topos Sh(CartSp th)Sh(CartSp_{th}), def. ,
is a cohesive topos.


We write

SynthDiff0TypeSh(CartSp th). SynthDiff0Type \coloneqq Sh(CartSp_{th}) \,.
Tangent bundle

Write DSh(CartSp th)D \in Sh(CartSp_{th}) for the smooth locus formally dual to the ring of dual numbers, def. . Write

i:*D i \colon * \to D

for the unique point inclusion.


For XSynthDiff0TypeX \in SynthDiff0Type, the internal hom

TX[D,X]SynthDiff0Type T X \coloneqq [D,X] \in SynthDiff0Type

equipped with the morphism

[i,X]:[D,X][*,X]X [i,X] \colon [D,X] \to [*,X] \simeq X

is the tangent bundle of XX.


For XSynthDiff0TypeX \in SynthDiff0Type, a vector field vv on XX is a section

X v TX id [i,D] X. \array{ X &&\stackrel{v}{\to}&& T X \\ & {}_{\mathllap{id}}\searrow && \swarrow_{\mathrlap{[i,D]}} \\ && X } \,.

The smooth space of vector fields is the internal hom in the slice topos over XX

Γ X(TX)[X,TX] X. \mathbf{\Gamma}_X(T X ) \coloneqq [X,T X]_X \,.
Differential equations

Differential cohesion of the topos of smooth spaces

Recall the sites


Define functors

CartSppiCartSp thιInfPoint CartSp \stackrel{\overset{i}{\hookrightarrow}}{\underset{p}{\leftarrow}} CartSp_{th} \stackrel{\iota}{\leftarrow} InfPoint


  • i:UU×*i \colon U \mapsto U \times *;

  • p:U×DUp \colon U \times D \mapsto U

  • ι:D*×D\iota \colon D \mapsto * \times D


All three functors in def. are morphisms of sites. The induced geometric morphism of sheaf toposes is of the form

Sh(CartSp)Ran p()p()iLan iSh(CartSp th)()ιLan ιSh(InfPoint) Sh(CartSp) \stackrel{}{\stackrel{\overset{Lan_i}{\hookrightarrow}}{\stackrel{\overset{(-)\circ i}{\leftarrow}}{\stackrel{\overset{(-)\circ p}{\hookrightarrow}}{\underset{Ran_p}{\leftarrow}}}}} Sh(CartSp_{th}) \stackrel{\overset{Lan_\iota}{\leftarrow}}{\underset{(-)\circ \iota}{\to}} Sh(InfPoint)

where hence the morphism on the left is in particular an essential geometric embedding.


The sequence of geometric morphisms

Sh(CartSp)p *Sh(CartSp th)ι *Sh(InfPoint) Sh(CartSp) \stackrel{p^*}{\to} Sh(CartSp_{th}) \stackrel{\iota^*}{\to} Sh(InfPoint)

exhibit a homotopy cofiber sequence in the (2,1)-category Topos.


By the discussion at (∞,1)Topos – Existence of limits and colimits the statement is equivalently that the inverse image functors

Sh(CartSp)Lan pSh(CartSp th)Lan ιSh(InfPoint) Sh(CartSp) \stackrel{Lan_p}{\leftarrow} Sh(CartSp_{th}) \stackrel{Lan_\iota}{\leftarrow} Sh(InfPoint)

form a homotopy fiber sequence in (∞,1)Cat. Computing this in the model structure for quasi-categories after passing to nerves, the morphism N(Lan p)N(Lan_p) is clearly an inner Kan fibration because of the subcategory inclusion Sh(CartSp)Sh(CartSp th)Sh(CartSp) \hookrightarrow Sh(CartSp_{th}). So by the general discussion at homotopy pullback the homotopy fiber is given by the 1-categorical fiber of N(Lan p)N(Lan_p) in sSet. By the discussion at Left Kan extension - on representables Lan pLan_p acts as pp on representables. The 1-categorical fiber of N(p):N(CartSp th)N(CartSp)N(p) \colon N(CartSp_{th}) \to N(CartSp) is evidently N(InfPoint)N(InfPoint). Since Lan ιLan_\iota is a left adjoint it preserves colimits and since ever sheaf is a colimit of representables, this is sufficient to imply the claim.

Differential cohesion

We axiomatize the existence of infinitesimals by further modalities on a cohesive topos.


Given a cohesive topos H=Cohesive0Type\mathbf{H} = Cohesive0Type over a base topos Discrete0Type, a structure of differential cohesion on H\mathbf{H} is an geometric embedding into a cohesive topos H th=InfThickenedCohesive0Type\mathbf{H}_{th} = InfThickenedCohesive0Type with an extra left eadjoint? that preserves the terminal object:

Cohesive0Type i *i *i ! InfThickenedCohesive0Type Γ Disc Γ th Disc th Discrete0Type \array{ Cohesive0Type &&\stackrel{\overset{i_!}{\hookrightarrow}}{\stackrel{\overset{i^*}{\leftarrow}}{\underset{i_*}{\hookrightarrow}}}&& InfThickenedCohesive0Type \\ & {}_{\mathllap{\Gamma}}\searrow \nwarrow^{\mathrlap{Disc}} && {}^{\mathllap{\Gamma_{th}}}\swarrow \nearrow_{\mathrlap{Disc_{th}}} \\ && Discrete0Type }

Given differential cohesion, def. , define the monad/comonad adjunction

(RedΠ inf):H thi *i *Hi *i !H. (Red \dashv \Pi_{inf}) \colon \mathbf{H}_{th} \stackrel{\overset{i_*}{\leftarrow}}{\underset{i^*}{\to}} \mathbf{H} \stackrel{\overset{i_!}{\leftarrow}}{\underset{i_*}{\to}} \mathbf{H} \,.

We call Red(X)Red(X) the reduced type of XX and Π inf(X)\Pi_{inf}(X) the infinitesimal path ∞-groupoid of XX.

For the (i *i *)(i_* \dashv i^*)-unit we write

InfinitesimalPathInclusion X:XΠ inf(X) InfinitesimalPathInclusion_X \colon X \to \Pi_{inf}(X)

and call it the constant infinitesimal path inclusion on XX.

The (i *i *)(i_* \dashv i^*)-counit

RedXX Red X \to X

we call the inclusion of the reduced part of XX.


Given a geometric embedding of ∞-toposes

CohesiveTypeiInfThickenedCohesiveType CohesiveType \stackrel{i}{\hookrightarrow} InfThickenedCohesiveType

exhibiting differential cohesion, write

CohesiveTypeiInfThickenedCohesiveTypeInfinitesimalType CohesiveType \stackrel{i}{\hookrightarrow} InfThickenedCohesiveType \to InfinitesimalType

for the corresponding homotopy cofiber sequence in (∞,1)-topos. The full sub-(∞,1)-category that is the kernel of the global section geometric morphism of InfininitesimalTypeInfininitesimalType we call the (∞,1)-category of synthetic ∞-Lie algebras

L Algebraker(Γ)InfinitesimalTypestackrerlΓDiscreteType. L_\infty Algebra \coloneqq ker(\Gamma) \hookrightarrow InfinitesimalType \stackrerl{\Gamma}{\to} DiscreteType \,.


  • H thSh(CartSp th)\mathbf{H}_{th} \coloneqq Sh(CartSp_{th})

  • HSh(CartSp)\mathbf{H} \coloneqq Sh(CartSp)

  • H infSh(InfPoint)\mathbf{H}_{inf} \coloneqq Sh(InfPoint)

makes prop. exhibit differential cohesive structure.

de Rham space

For XH thX \in \mathbf{H}_{th} we call Π inf(X)H\Pi_{inf}(X) \in \mathbf{H} the de Rham space object of XX.

Jet bundle

For XHX \in \mathbf{H}

Jet X(InfinitesimalPathInclusion X) *:H th/XH th/Π inf(X). Jet_X \coloneqq (InfinitesimalPathInclusion_X)_* \colon \mathbf{H}_{th}/X \to \mathbf{H}_{th}/\Pi_{inf}(X) \,.

For (EX)H th/X(E \to X) \in \mathbf{H}_{th}/X, Jet X(E)Jet_X(E) is the jet bundle of EE.

Formally étale / formally unramified / formally smooth

A morphism f:XYf \;\colon\; X \to Y in H\mathbf{H} is called a formally étale morphism if the naturality square of the Π inf\mathbf{\Pi}_{inf}-unit

X Π inf(X) f Π inf(f) Y Π inf(Y) \array{ X &\stackrel{}{\to}& \mathbf{\Pi}_{inf}(X) \\ \downarrow^{\mathrlap{f}} && \downarrow^{\mathrlap{\mathbf{\Pi}_{inf}(f)}} \\ Y &\to& \mathbf{\Pi}_{inf}(Y) }

is an (∞,1)-pullback.


If X,YX, Y \in SmoothMfd \hookrightarrow Hi !H th\mathbf{H} \stackrel{i_!}{\to} \mathbf{H}_{th} then for f:XYf \colon X \to Y any morphism

  1. ff is formally étale morphism precisely if ff is a submersion of smooth manifolds;

  2. ff is a formally unramified morphism precisely if it is an immersion of smooth manifolds;

  3. ff is a formally smooth morphism precisely if it is a diffeomorphism.

Syntactic Layer

Differential homotopy type theory


Last revised on September 20, 2018 at 21:08:20. See the history of this page for a list of all contributions to it.