Stokes theorem




Special and general types

Special notions


Extra structure



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)



Stokes theorem asserts that the integration of differential forms of the de Rham differential of a differential form over a domain equals the integral of the form itself over the boundary of the domain.


Traditional statement


Δ Diff:ΔDiff \Delta_{Diff} : \Delta \to Diff

be the cosimplicial object of standard kk-simplices in SmoothMfd: in degree kk this is the standard kk-simplex Δ Diff k k\Delta^k_{Diff} \subset \mathbb{R}^k regarded as a smooth manifold with boundary and corners. This may be parameterized as

Δ k={t 1,,t k 0| it i1} k. \Delta^k = \{ t^1, \cdots, t^k \in \mathbb{R}_{\geq 0} | \sum_i t^i \leq 1\} \subset \mathbb{R}^k \,.

In this parameterization the coface maps of Δ Diff\Delta_{Diff} are

i:(t 1,,t k1){(t 1,,t i1,t i+1,,t k1) |i>0 (1 i=1 k1t i,t 1,,t k1). \partial_i : (t^1, \cdots, t^{k-1}) \mapsto \left\{ \array{ (t^1, \cdots, t^{i-1}, t^{i+1} , \cdots, t^{k-1}) & | i \gt 0 \\ (1- \sum_{i=1}^{k-1} t^i, t^1, \cdots, t^{k-1}) } \right. \,.

For XX any smooth manifold a smooth kk-simplex in XX is a smooth function

σ:Δ kX. \sigma : \Delta^k \to X \,.

The boundary of this simplex in XX is the chain (formal linear combination of smooth (k1)(k-1)-simplices)

σ= i=0 k(1) iσ i. \partial \sigma = \sum_{i = 0}^k (-1)^i \sigma \circ \partial_i \,.

Let ωΩ k1(X)\omega \in \Omega^{k-1}(X) be a degree (k1)(k-1)-differential form on XX.


(Stokes theorem)

The integral of ω\omega over the boundary of the simplex equals the integral of its de Rham differential over the simplex itself

σω= σdω. \int_{\partial \sigma} \omega = \int_\sigma d \omega \,.

It follows that for CC any kk-chain in XX and C\partial C its boundary (k1)(k-1)-chain, we have

Cω= Cdω. \int_{\partial C} \omega = \int_{C} d \omega \,.

Abstract formulation in cohesive homotopy-type theory

We discuss here a general abstract formulation of differential forms, their integration and Stokes theorem in the axiomatics of cohesive homotopy type theory (following Bunke-Nikolaus-Völkl 13, theorem 3.2).

Let H\mathbf{H} be a cohesive (∞,1)-topos and write THT \mathbf{H} for its tangent cohesive (∞,1)-topos.

Assume that there is an interval object

**(i 0,i 1)Δ 1 \ast \cup \ast \stackrel{(i_0, i_1)}{\longrightarrow} \Delta^1

“exhibiting the cohesion” (see at continuum) in that there is a (chosen) equivalence between the shape modality Π\Pi and the localization L Δ 1L_{\Delta^1} at the the projection maps out of Cartesian products with this line Δ 1×()()\Delta^1\times (-) \to (-)

ΠL Δ 1. \Pi \simeq L_{\Delta^1} \,.

This is the case for instance for the “standard continuum”, the real line in H=\mathbf{H} = Smooth∞Grpd.

It follows in particular that there is a chosen equivalence of (∞,1)-categories

(H)L Δ 1H \flat(\mathbf{H})\simeq L_{\Delta^1}\mathbf{H}

between the flat modal homotopy-types and the Δ 1\Delta^1-homotopy invariant homotopy-types.

Given a stable homotopy type E^Stab(H)TH\hat E \in Stab(\mathbf{H})\hookrightarrow T \mathbf{H} cohesion provides two objects

Π dRΩE^, dRΣE^Stab(H) \Pi_{dR} \Omega \hat E \,,\;\; \flat_{dR}\Sigma \hat E \;\; \in Stab(\mathbf{H})

which may be interpreted as de Rham complexes with coefficients in Π( dRΣE^)\Pi(\flat_{dR} \Sigma \hat E), the first one restricted to negative degree, the second to non-negative degree. Moreover, there is a canonical map

Π dRΩE^ d dRΣE^ ι θ E^ E^ \array{ \Pi_{dR}\Omega \hat E && \stackrel{\mathbf{d}}{\longrightarrow} && \flat_{dR}\Sigma \hat E \\ & {}_{\mathllap{\iota}}\searrow && \nearrow_{\mathrlap{\theta_{\hat E}}} \\ && \hat E }

which interprets as the de Rham differential d\mathbf{d}. See at differential cohomology diagram for details.

Throughout in the following we leave the “inclusion” ι\iota of “differential forms regarded as E^\hat E-connections on trivial EE-bundles” implicit.


Integration of differential forms is the map

Δ 1:[Δ 1, dRΣE^]Π dRΩE^ \int_{\Delta^1} \;\colon\; [\Delta^1, \flat_{dR}\Sigma \hat E] \longrightarrow \Pi_{dR}\Omega \hat E

which is induced via the homotopy cofiber property of dRΩE^\flat_{dR}\Omega \hat E from the counit naturality square of the flat modality on [(**(i 0,i 1)Δ 1),][(\ast \coprod \ast \stackrel{(i_0, i_1)}{\to} \Delta ^1 ), -], using that this square exhibits a null homotopy due to the Δ 1\Delta^1-homotopy invariance of E^\flat \hat E.


Stokes’ theorem holds:

Δ 1di 1 *i 0 *. \int_{\Delta^1} \circ \mathbf{d} \;\simeq\; i_1^\ast - i_0^\ast \,.

(Bunke-Nikolaus-Völkl 13, theorem 3.2)


A standard account is for instance in

  • Reyer Sjamaar, Manifolds and differential forms, pdf

Discussion of Stokes theorem on manifolds with corners is in

Discussion for manifolds with more general singularities on the boundary is in

  • Friedrich Sauvigny, Partial Differential Equations: Vol. 1 Foundations and Integral Representations

Discussion in cohesive homotopy type theory is in

Revised on October 17, 2014 09:48:40 by Urs Schreiber (