Differential forms and Stokes' theorem

Lens

MotivationH

Four theorems, or one?

A course in multivariable calculus ends with a list of theorems that look different:

the fundamental theorem of calculus: $\int_a^b f'(x)\,dx = f(b) - f(a)$ ;
Green's theorem: $\iint_D \big(\frac{\partial Q}{\partial x} - \frac{\partial P}{\partial y}\big)\,dx\,dy = \oint_{\partial D} P\,dx + Q\,dy$ ;
Stokes' theorem: $\iint_S (\nabla \times \mathbf F) \cdot d\mathbf S = \oint_{\partial S} \mathbf F \cdot d\mathbf r$ ;
the divergence theorem: $\iiint_V \nabla \cdot \mathbf F\, dV = \iint_{\partial V} \mathbf F \cdot d\mathbf S$ .

Each says that integrating some kind of derivative over a region equals integrating the original quantity over the region's boundary. With the right language — differential forms — they become literally one statement,

\int_M d\omega = \int_{\partial M} \omega ,

valid in every dimension. The same language turns Maxwell's four equations of electromagnetism into two, $dF = 0$ and $d{\star}F = J$ , valid in any coordinates and on curved spacetime.

There is a puzzle hiding here too. The vector field $\mathbf F = \big(-y/(x^2 + y^2),\ x/(x^2 + y^2)\big)$ has zero curl everywhere it is defined. Yet its circulation around the unit circle is $2\pi$ , not $0$ . Green's theorem has not failed: the field is undefined at the origin, which is inside the circle. The surprise is that calculus noticed the hole. Making that precise leads to de Rham cohomology, where calculus detects topology.

IntuitionH

Things you integrate

A differential form is something you integrate. A 1-form such as $P\,dx + Q\,dy$ is integrated along oriented curves: think of the work done by a force along a path. Reversing the path reverses the sign. A 2-form is integrated over oriented surfaces: think of the flux of a fluid through a membrane, which depends on which side counts as "out". A 0-form is a function, "integrated" over points by evaluating it, with signs for orientation.

Orientation is why forms are alternating. The 2-form $dx \wedge dy$ assigns to a pair of vectors the signed area of the parallelogram they span, so swapping the vectors changes the sign: $dy \wedge dx = -dx \wedge dy$ , and $dx \wedge dx = 0$ . That one rule replaces the right-hand rules, cross products and Jacobian determinants of vector calculus.

The exterior derivative $d$ measures "how much $\omega$ there is around the boundary of a tiny piece". For a 1-form in the plane, $d\omega$ at a point is the circulation of $\omega$ around a tiny square there, divided by its area. Stokes' theorem then follows from a picture: cut the region into tiny squares and add up their circulations. Each interior edge is traversed twice in opposite directions and cancels, leaving only the outer boundary.

Why Stokes' theorem holds. Cut a region into small squares and add up the circulation around each: interior edges are traversed once in each direction and cancel, so the total is the circulation around the outer boundary. And each small circulation is approximately dω times the area.

DefinitionsH

Forms, wedge, d and pullback

Throughout, $U \subseteq \R^n$ is open, with coordinates $x_1, \dots, x_n$ .

Definition— alternating forms and the wedge product

An alternating $k$ -form on $\R^n$ is a multilinear map $\alpha : (\R^n)^k \to \R$ that changes sign when two arguments are swapped (equivalently, vanishes when two arguments are equal). They form a vector space $\Lambda^k(\R^n)^*$ of dimension $\binom{n}{k}$ , with basis $dx_{i_1} \wedge \cdots \wedge dx_{i_k}$ for $i_1 \lt \cdots \lt i_k$ . Here $dx_i$ is the $i$ -th coordinate functional and

(dx_{i_1} \wedge \cdots \wedge dx_{i_k})(v_1, \dots, v_k) = \det\big( (v_j)_{i_l} \big)_{l, j = 1}^k .

The wedge product of a $k$ -form and an $l$ -form is the $(k + l)$ -form determined by bilinearity and $dx_I \wedge dx_J = dx_{I \cup J}$ written in order, with the sign of the permutation that sorts $(I, J)$ , or $0$ if $I$ and $J$ share an index. For two 1-forms, $(\alpha \wedge \beta)(u, v) = \alpha(u)\beta(v) - \alpha(v)\beta(u)$ .

Definition— differential form

A differential $k$ -form on $U$ is a smooth assignment of an alternating $k$ -form to each point:

\omega = \sum_{i_1 \lt \cdots \lt i_k} f_{i_1 \dots i_k}(x)\, dx_{i_1} \wedge \cdots \wedge dx_{i_k}, \qquad f_I \in C^\infty(U).

We write $\Omega^k(U)$ for the space of $k$ -forms. A 0-form is a smooth function.

Definition— exterior derivative

The exterior derivative $d : \Omega^k(U) \to \Omega^{k+1}(U)$ is defined on functions by $df = \sum_i \frac{\partial f}{\partial x_i}\, dx_i$ , and on $k$ -forms by

d\Big( \sum_I f_I\, dx_I \Big) = \sum_I df_I \wedge dx_I = \sum_I \sum_i \frac{\partial f_I}{\partial x_i}\, dx_i \wedge dx_I .

Definition— pullback

If $\varphi : V \to U$ is smooth ( $V \subseteq \R^m$ open), the pullback $\varphi^*\omega \in \Omega^k(V)$ is $(\varphi^*\omega)_p(v_1, \dots, v_k) = \omega_{\varphi(p)}(D\varphi_p v_1, \dots, D\varphi_p v_k)$ . On functions $\varphi^* f = f \circ \varphi$ , and $\varphi^*(dx_i) = d\varphi_i$ , $\varphi^*(\alpha \wedge \beta) = \varphi^*\alpha \wedge \varphi^*\beta$ .

Definition— integration over cubes and chains

For a $k$ -form $\omega = f\, dx_1 \wedge \cdots \wedge dx_k$ on $[0, 1]^k$ , set $\int_{[0,1]^k} \omega = \int_{[0,1]^k} f\, dx_1 \cdots dx_k$ . A singular $k$ -cube in $U$ is a smooth map $c : [0, 1]^k \to U$ , and $\int_c \omega = \int_{[0,1]^k} c^*\omega$ . A $k$ -chain is a formal sum $\sum a_j c_j$ with integer coefficients, integrated linearly. The boundary of the standard cube is the $(k-1)$ -chain

\partial [0, 1]^k = \sum_{i=1}^k \sum_{\alpha = 0, 1} (-1)^{i + \alpha}\, I_{(i, \alpha)}, \qquad I_{(i, \alpha)}(t_1, \dots, t_{k-1}) = (t_1, \dots, t_{i-1}, \alpha, t_i, \dots, t_{k-1}),

and $\partial c = \sum (-1)^{i+\alpha} c \circ I_{(i, \alpha)}$ . For $k = 1$ , $\partial c = c(1) - c(0)$ , and a 0-form is integrated over it as $f(c(1)) - f(c(0))$ .

Definition— closed, exact, de Rham cohomology

A form is closed if $d\omega = 0$ and exact if $\omega = d\eta$ for some form $\eta$ . Since $d \circ d = 0$ (Theorem 2), exact forms are closed, and the de Rham cohomology groups

H^k_{\mathrm{dR}}(U) = \frac{\{\text{closed } k\text{-forms}\}}{\{\text{exact } k\text{-forms}\}}

measure how far closed forms are from being exact.

Worked examplesH

Worked examples

Example— Vector calculus is exterior calculus in R³

On $\R^3$ , identify a vector field $\mathbf F = (P, Q, R)$ with the 1-form $P\,dx + Q\,dy + R\,dz$ and with the 2-form $P\, dy \wedge dz + Q\, dz \wedge dx + R\, dx \wedge dy$ . Then

df = f_x\, dx + f_y\, dy + f_z\, dz \ \ (\text{grad}), \qquad d(P\,dx + Q\,dy + R\,dz) = (R_y - Q_z)\, dy \wedge dz + (P_z - R_x)\, dz \wedge dx + (Q_x - P_y)\, dx \wedge dy \ \ (\text{curl}),

d(P\, dy \wedge dz + Q\, dz \wedge dx + R\, dx \wedge dy) = (P_x + Q_y + R_z)\, dx \wedge dy \wedge dz \ \ (\text{div}).

The identities $\nabla \times \nabla f = 0$ and $\nabla \cdot (\nabla \times \mathbf F) = 0$ are both $d \circ d = 0$ . For example, $d(x^2 y\, dz) = 2xy\, dx \wedge dz + x^2\, dy \wedge dz$ .

Example— Polar coordinates

Pull back along $\varphi(r, \theta) = (r\cos\theta, r\sin\theta)$ . Then $\varphi^* dx = \cos\theta\, dr - r\sin\theta\, d\theta$ and $\varphi^* dy = \sin\theta\, dr + r\cos\theta\, d\theta$ . So

\varphi^*(dx \wedge dy) = (\cos\theta\, dr - r\sin\theta\, d\theta) \wedge (\sin\theta\, dr + r\cos\theta\, d\theta) = r\cos^2\theta\, dr \wedge d\theta - r\sin^2\theta\, d\theta \wedge dr = r\, dr \wedge d\theta .

The factor $r$ in $dx\,dy = r\,dr\,d\theta$ is the Jacobian determinant, produced automatically by the alternating rule.

Example— The angle form

On $U = \R^2 \setminus \{0\}$ , let

d\theta = \frac{x\, dy - y\, dx}{x^2 + y^2} .

In polar coordinates $\varphi^*(d\theta)$ is literally $d\theta$ , as the computation above shows. But the notation is misleading: there is no smooth (or even continuous) function $\theta$ on all of $U$ — the polar angle jumps by $2\pi$ somewhere on every circle around the origin. $d\theta$ is closed (Theorem 5), and its integral over the unit circle $\gamma(t) = (\cos t, \sin t)$ is $\int_0^{2\pi} (\cos t \cdot \cos t - \sin t \cdot (-\sin t))\, dt = 2\pi$ .

Example— A form that measures area

$\omega = x\, dy - y\, dx$ has $d\omega = dx \wedge dy - dy \wedge dx = 2\, dx \wedge dy$ . So by Green's theorem $\frac12 \oint_{\partial D} (x\,dy - y\,dx)$ is the area of $D$ . This is the principle of the planimeter, an instrument that measures areas on maps and drawings by tracing their boundaries.

ProofH

The wedge product and the exterior derivative

Theorem— Proposition 1 (graded commutativity)

The wedge product is bilinear and associative, and for a $k$ -form $\alpha$ and an $l$ -form $\beta$ ,

\alpha \wedge \beta = (-1)^{kl}\, \beta \wedge \alpha .

In particular $\alpha \wedge \alpha = 0$ for every 1-form (indeed every form of odd degree).

Proof

Bilinearity and associativity hold on basis elements, where concatenating index lists is associative and signs of sorting permutations multiply. By bilinearity it suffices to check graded commutativity on $dx_I \wedge dx_J$ with $|I| = k$ , $|J| = l$ . To turn the list $(I, J)$ into $(J, I)$ , move each of the $l$ indices of $J$ to the front past the $k$ indices of $I$ : $kl$ transpositions in all, each changing the sign. For a 1-form, $\alpha \wedge \alpha = (-1)^1 \alpha \wedge \alpha$ forces $\alpha \wedge \alpha = 0$ .

∎

So 1-forms anticommute, but a 1-form and a 2-form commute: $\alpha \wedge \beta = \beta \wedge \alpha$ .

Theorem— Theorem 2 (properties of d)

(a) $d(\alpha \wedge \beta) = d\alpha \wedge \beta + (-1)^k \alpha \wedge d\beta$ for a $k$ -form $\alpha$ . (b) $d \circ d = 0$ . (c) $d$ commutes with pullback: $\varphi^*(d\omega) = d(\varphi^* \omega)$ .

Proof

(a) By linearity take $\alpha = f\, dx_I$ and $\beta = g\, dx_J$ . Then $\alpha \wedge \beta = fg\, dx_I \wedge dx_J$ , and by the product rule

d(\alpha \wedge \beta) = (g\, df + f\, dg) \wedge dx_I \wedge dx_J = df \wedge dx_I \wedge g\, dx_J + (-1)^k f\, dx_I \wedge dg \wedge dx_J ,

where moving the 1-form $dg$ past the $k$ -form $dx_I$ costs $(-1)^k$ (Proposition 1). This is $d\alpha \wedge \beta + (-1)^k \alpha \wedge d\beta$ .

(b) For a function, $d(df) = \sum_{i, j} \frac{\partial^2 f}{\partial x_j \partial x_i}\, dx_j \wedge dx_i$ . The coefficients are symmetric in $i, j$ (mixed partials of smooth functions commute) while $dx_j \wedge dx_i$ is antisymmetric, so the terms cancel in pairs and the diagonal terms vanish. For $\omega = f\, dx_I$ , $d\omega = df \wedge dx_I$ , and by (a), $d(d\omega) = d(df) \wedge dx_I - df \wedge d(dx_I) = 0$ , since $d(dx_I) = d(1) \wedge dx_I = 0$ .

(c) For functions this is the chain rule: $\varphi^*(df) = \sum_i (\partial_i f \circ \varphi)\, d\varphi_i = d(f \circ \varphi)$ . In particular $\varphi^*(dx_i) = d\varphi_i = d(\varphi^* x_i)$ . For $\omega = f\, dx_{i_1} \wedge \cdots \wedge dx_{i_k}$ , $\varphi^*\omega = (f \circ \varphi)\, d\varphi_{i_1} \wedge \cdots \wedge d\varphi_{i_k}$ . By (a) and (b), $d(\varphi^*\omega) = d(f \circ \varphi) \wedge d\varphi_{i_1} \wedge \cdots \wedge d\varphi_{i_k} = \varphi^*(df) \wedge \varphi^*(dx_{i_1}) \wedge \cdots = \varphi^*(d\omega)$ .

∎

Property (c) means that $d$ does not depend on coordinates: the same operator works on any manifold, and it is why the definition of $d$ through a coordinate formula is legitimate.

ProofH

Stokes' theorem

Theorem— Theorem 3 (Stokes' theorem for chains)

For every $(k-1)$ -form $\omega$ on $U$ and every $k$ -chain $c$ in $U$ ,

\int_c d\omega = \int_{\partial c} \omega .

Proof

Step 1: the standard cube. By linearity it suffices to take $\omega = f\, dx_1 \wedge \cdots \wedge \widehat{dx_i} \wedge \cdots \wedge dx_k$ (with $dx_i$ omitted) on $[0, 1]^k$ . Only the term $\frac{\partial f}{\partial x_i} dx_i$ of $df$ survives in $df \wedge (\cdots)$ , and moving $dx_i$ into position $i$ costs $(-1)^{i-1}$ :

d\omega = (-1)^{i-1} \frac{\partial f}{\partial x_i}\, dx_1 \wedge \cdots \wedge dx_k .

By Fubini and the fundamental theorem of calculus in the variable $x_i$ ,

\int_{[0,1]^k} d\omega = (-1)^{i-1} \int_{[0,1]^{k-1}} \big( f(\dots, 1, \dots) - f(\dots, 0, \dots) \big)\, dx_1 \cdots \widehat{dx_i} \cdots dx_k ,

with $1$ and $0$ in the $i$ -th slot. On the other side, $I_{(j, \alpha)}^* \omega = 0$ for $j \ne i$ , because along that face $x_j$ is constant, so $dx_j$ pulls back to $0$ , and $\omega$ contains $dx_j$ . For $j = i$ , $I_{(i, \alpha)}^*\omega = f(\dots, \alpha, \dots)\, dt_1 \wedge \cdots \wedge dt_{k-1}$ . Hence

\int_{\partial [0,1]^k} \omega = (-1)^{i+1} \int f(\dots, 1, \dots) + (-1)^{i} \int f(\dots, 0, \dots),

which is the same.

Step 2: singular cubes and chains. For a singular cube $c$ , by the definition of the integral, Theorem 2(c) and Step 1,

\int_c d\omega = \int_{[0,1]^k} c^*(d\omega) = \int_{[0,1]^k} d(c^*\omega) = \int_{\partial [0,1]^k} c^*\omega = \int_{\partial c} \omega ,

where the last equality holds because $(c \circ I_{(i,\alpha)})^* = I_{(i,\alpha)}^* c^*$ . Chains follow by linearity.

∎

Theorem— Theorem 4 (Stokes' theorem for manifolds; stated, proof referenced)

Let $M$ be a compact oriented smooth $k$ -manifold with boundary in $\R^n$ (or abstractly), with $\partial M$ given the induced orientation, and let $\omega$ be a smooth $(k-1)$ -form on a neighbourhood of $M$ . Then $\int_M d\omega = \int_{\partial M} \omega$ .

The proof reduces to Theorem 3 with a partition of unity and orientation-preserving charts (Spivak 1965, chapter 5; Lee, Introduction to Smooth Manifolds, chapter 16). The classical theorems are its special cases:

$k$	$M$	$\omega$	$\int_M d\omega = \int_{\partial M}\omega$ is
1	interval $[a, b]$	function $f$	$\int_a^b f' = f(b) - f(a)$ (fundamental theorem of calculus)
1	curve $\gamma$ in $\R^n$	function $f$	$\int_\gamma \nabla f \cdot d\mathbf r = f(\text{end}) - f(\text{start})$
2	region $D \subseteq \R^2$	$P\,dx + Q\,dy$	Green's theorem
2	surface $S \subseteq \R^3$	$\mathbf F \cdot d\mathbf r$	Stokes' (Kelvin–Stokes) theorem
3	solid $V \subseteq \R^3$	$\mathbf F \cdot d\mathbf S$	divergence (Gauss–Ostrogradsky) theorem

ProofH

Closed versus exact: the Poincaré lemma and the angle form

Theorem— Theorem 5 (dθ is closed but not exact)

The form $d\theta = (x\,dy - y\,dx)/(x^2 + y^2)$ on $\R^2 \setminus \{0\}$ is closed, but it is not $df$ for any smooth function $f$ on $\R^2 \setminus \{0\}$ .

Proof

Closed. With $P = -y/(x^2 + y^2)$ and $Q = x/(x^2 + y^2)$ , $d(P\,dx + Q\,dy) = (Q_x - P_y)\, dx \wedge dy$ , and

Q_x = \frac{(x^2 + y^2) - 2x^2}{(x^2 + y^2)^2} = \frac{y^2 - x^2}{(x^2 + y^2)^2} = P_y .

Not exact. If $d\theta = df$ , Stokes' theorem for the 1-cube $\gamma(t) = (\cos 2\pi t, \sin 2\pi t)$ , whose boundary $\gamma(1) - \gamma(0)$ is zero, would give $\int_\gamma d\theta = f(\gamma(1)) - f(\gamma(0)) = 0$ . But the example above computed $\int_\gamma d\theta = 2\pi$ .

∎

The Lean proof of non-exactness is the same argument in calculus form. If $df = d\theta$ , then $g(t) = f(\cos t, \sin t)$ has $g'(t) = 1$ , so $g(t) - t$ is constant, while $g(2\pi) = g(0)$ . Whether closed forms are exact depends on the shape of the domain:

Theorem— Theorem 6 (Poincaré lemma)

Let $U \subseteq \R^n$ be open and star-shaped with respect to $0$ (for every $x \in U$ , the segment from $0$ to $x$ lies in $U$ ). Then every closed $k$ -form on $U$ with $k \ge 1$ is exact. We prove the case $k = 1$ .

Proof

Let $\omega = \sum_i \omega_i\, dx_i$ be closed, so $\partial_j \omega_i = \partial_i \omega_j$ for all $i, j$ . Define $f$ by integrating $\omega$ along the segment from $0$ to $x$ :

f(x) = \int_0^1 \sum_i \omega_i(tx)\, x_i\, dt .

The integrand is smooth in $(t, x)$ , so we may differentiate under the integral sign:

\frac{\partial f}{\partial x_j}(x) = \int_0^1 \Big( \omega_j(tx) + \sum_i t\, x_i\, (\partial_j \omega_i)(tx) \Big) dt = \int_0^1 \Big( \omega_j(tx) + t \sum_i x_i\, (\partial_i \omega_j)(tx) \Big) dt ,

using closedness. The integrand is exactly $\frac{d}{dt}\big( t\, \omega_j(tx) \big)$ , so the integral is $1 \cdot \omega_j(x) - 0 = \omega_j(x)$ . Hence $df = \omega$ .

∎

For general $k$ , the same idea gives a linear operator $K : \Omega^k(U) \to \Omega^{k-1}(U)$ with $dK + Kd = \mathrm{id}$ on forms of degree $\ge 1$ . If $d\omega = 0$ , then $\omega = d(K\omega)$ (Spivak 1965, Theorem 4-11). The punctured plane is not star-shaped, and Theorem 5 shows that the conclusion fails there.

Theorem— Corollary 7 (first de Rham cohomology of the punctured plane)

$H^1_{\mathrm{dR}}(\R^2 \setminus \{0\}) \cong \R$ , spanned by the class of $d\theta$ . A closed 1-form $\omega$ is exact if and only if $\oint_{|x| = 1} \omega = 0$ .

Proof

$[d\theta] \ne 0$ by Theorem 5. Let $\omega$ be closed and $c = \frac{1}{2\pi}\oint_{|x|=1} \omega$ . Then $\eta = \omega - c\, d\theta$ is closed with $\oint_{|x|=1} \eta = 0$ . We show $\eta$ is exact. On the slit plane $V_1 = \R^2$ minus the closed negative $x$ -axis, which is star-shaped (with respect to $(1, 0)$ ), the Poincaré lemma gives $\eta = df_1$ . On $V_2 = \R^2$ minus the closed positive $x$ -axis, it gives $\eta = df_2$ . On $V_1 \cap V_2$ , the union of the open upper and lower half-planes, $d(f_1 - f_2) = 0$ , so $f_1 - f_2$ is a constant on each half-plane: $a$ on the upper one and $b$ on the lower one. Split the unit circle at $(1, 0)$ , $p_+ = (0, 1)$ , $(-1, 0)$ and $p_- = (0, -1)$ . The two arcs touching $(1, 0)$ lie in $V_1$ and the two touching $(-1, 0)$ lie in $V_2$ , so integrating $\eta = df_1$ or $df_2$ arc by arc gives

0 = \oint \eta = \big(f_1(p_+) - f_1(1, 0)\big) + \big(f_2(-1, 0) - f_2(p_+)\big) + \big(f_2(p_-) - f_2(-1, 0)\big) + \big(f_1(1, 0) - f_1(p_-)\big) = a - b .

So $a = b$ , and $f = f_1$ on $V_1$ , $f = f_2 + a$ on $V_2$ is a well-defined smooth function on $\R^2 \setminus \{0\}$ with $df = \eta$ . Hence $[\omega] = c\,[d\theta]$ .

∎

De Rham's theorem (1931) generalises this. For any smooth manifold $M$ , $H^k_{\mathrm{dR}}(M)$ is isomorphic to the singular cohomology $H^k(M; \R)$ , a purely topological invariant. Calculus detects holes: $\dim H^1_{\mathrm{dR}}$ of the plane with $m$ points removed is $m$ , of the torus $2$ , of the sphere $0$ .

Formal mathematicsF

Differential forms in Lean and Mathlib

Mathlib represents a differential $n$ -form on a normed space $E$ as a map $E \to (E \mathbin{[\bigwedge^{\mathrm{Fin}\,n}]\!\!\to\!L[\R]} F)$ into continuous alternating maps, and defines the exterior derivative extDeriv. It proves $d \circ d = 0$ and that $d$ commutes with pullback, and it has the exterior algebra and the divergence theorem on boxes. It does not (yet) have integration of forms over manifolds or the general Stokes theorem.

First the wedge product of two 1-forms, its antisymmetry, and $dx \wedge dy$ as signed area, alongside Mathlib's exterior algebra:

wedgeLean 4Formally verified

/-- The **wedge product** of two 1-forms (linear functionals) `α, β` on a real vector space: the
alternating bilinear form `(α ∧ β)(u, v) = α(u) β(v) - α(v) β(u)`. -/
def wedge {E : Type*} [AddCommGroup E] [Module ℝ E] (α β : E →ₗ[ℝ] ℝ) (u v : E) : ℝ :=
  α u * β v - α v * β u