[proofplan] We define $d_M\omega$ locally in each coordinate chart by transporting $\omega$ to an open subset of Euclidean space, applying the Euclidean [exterior derivative](/theorems/1525), and transporting the result back. The main point is to prove that these local definitions agree on chart overlaps; this follows from the naturality of the Euclidean exterior derivative under smooth coordinate changes. Once the local forms glue to a global form, the identities $d^2=0$ and pullback compatibility are checked in charts, where they reduce to the corresponding Euclidean facts. Uniqueness follows because coordinate charts cover $M$. [/proofplan] [step:Define the local candidate in each coordinate chart] Fix an integer $k \geq 0$ and a form $\omega \in \Omega^k(M)$. Let $(U,\varphi)$ be a smooth chart on $M$, where \begin{align*} \varphi: U \to \varphi(U) \subseteq \mathbb{R}^n \end{align*} is a diffeomorphism onto the [open set](/page/Open%20Set) $\varphi(U)$. Define the local representative of $\omega$ in this chart to be \begin{align*} \omega_\varphi := (\varphi^{-1})^*(\omega|_U) \in \Omega^k(\varphi(U)). \end{align*} Using the Euclidean exterior derivative on the open set $\varphi(U)$, define a local $(k+1)$-form on $U$ by \begin{align*} \eta_U^\varphi := \varphi^*\left(d_{\varphi(U)}^k\omega_\varphi\right) = \varphi^*\left(d_{\varphi(U)}^k\left((\varphi^{-1})^*(\omega|_U)\right)\right) \in \Omega^{k+1}(U). \end{align*} This is the only possible definition compatible with the stated coordinate formula. [/step] [step:Prove that the chartwise definitions agree on overlaps] Let $(U,\varphi)$ and $(V,\psi)$ be smooth charts on $M$, and let $W := U \cap V$. If $W=\varnothing$, there is nothing to prove. Assume $W \neq \varnothing$. Define the open subsets \begin{align*} A &:= \varphi(W) \subseteq \mathbb{R}^n, & B &:= \psi(W) \subseteq \mathbb{R}^n, \end{align*} and define the smooth transition map \begin{align*} \tau: A &\to B \\ y &\mapsto \psi(\varphi^{-1}(y)). \end{align*} Then $\tau=\psi\circ\varphi^{-1}$ and $\varphi^{-1}|_A=\psi^{-1}\circ\tau$. Hence \begin{align*} (\varphi^{-1})^*(\omega|_W) = \tau^*\left((\psi^{-1})^*(\omega|_W)\right). \end{align*} We use the Euclidean naturality of exterior differentiation under smooth maps, namely \begin{align*} d_A^k(\tau^*\alpha)=\tau^*(d_B^k\alpha) \end{align*} for every $\alpha \in \Omega^k(B)$; this is the Euclidean exterior derivative theorem on open subsets of Euclidean space, citing a result not yet in the wiki: Euclidean naturality of the exterior derivative. Applying this with \begin{align*} \alpha := (\psi^{-1})^*(\omega|_W) \in \Omega^k(B), \end{align*} we obtain \begin{align*} d_A^k\left((\varphi^{-1})^*(\omega|_W)\right) &= d_A^k\left(\tau^*((\psi^{-1})^*(\omega|_W))\right) \\ &= \tau^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right). \end{align*} Pulling back by $\varphi|_W: W \to A$ gives \begin{align*} (\eta_U^\varphi)|_W &= (\varphi|_W)^*\left(d_A^k((\varphi^{-1})^*(\omega|_W))\right) \\ &= (\varphi|_W)^*\tau^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right) \\ &= (\tau\circ\varphi|_W)^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right) \\ &= (\psi|_W)^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right) \\ &= (\eta_V^\psi)|_W. \end{align*} Thus the local definitions agree on every chart overlap. [guided] We must check that defining $d\omega$ in coordinates does not depend on the coordinates. Take two charts $(U,\varphi)$ and $(V,\psi)$ and restrict attention to their overlap $W:=U\cap V$. If $W$ is empty, the compatibility condition is vacuous. Otherwise define \begin{align*} A &:= \varphi(W), & B &:= \psi(W), \end{align*} so $A$ and $B$ are open subsets of $\mathbb{R}^n$. The transition map is the smooth map \begin{align*} \tau: A &\to B \\ y &\mapsto \psi(\varphi^{-1}(y)). \end{align*} This map satisfies $\tau=\psi\circ\varphi^{-1}$, and therefore $\varphi^{-1}|_A=\psi^{-1}\circ\tau$. Now compare the two Euclidean representatives of $\omega|_W$. In the $\varphi$-chart the representative is \begin{align*} (\varphi^{-1})^*(\omega|_W), \end{align*} while in the $\psi$-chart it is \begin{align*} (\psi^{-1})^*(\omega|_W). \end{align*} Because $\varphi^{-1}|_A=\psi^{-1}\circ\tau$, functoriality of pullback gives \begin{align*} (\varphi^{-1})^*(\omega|_W) = \tau^*\left((\psi^{-1})^*(\omega|_W)\right). \end{align*} The key input is that the Euclidean exterior derivative is natural under smooth maps: \begin{align*} d_A^k(\tau^*\alpha)=\tau^*(d_B^k\alpha) \end{align*} for every $\alpha \in \Omega^k(B)$. This is the Euclidean exterior derivative theorem on open subsets of Euclidean space, citing a result not yet in the wiki: Euclidean naturality of the exterior derivative. Apply it to \begin{align*} \alpha := (\psi^{-1})^*(\omega|_W). \end{align*} Then \begin{align*} d_A^k\left((\varphi^{-1})^*(\omega|_W)\right) &= d_A^k\left(\tau^*((\psi^{-1})^*(\omega|_W))\right) \\ &= \tau^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right). \end{align*} Finally pull this identity back from $A$ to $W$ using $\varphi|_W$. Since $\tau\circ\varphi|_W=\psi|_W$, we get \begin{align*} (\eta_U^\varphi)|_W &= (\varphi|_W)^*\left(d_A^k((\varphi^{-1})^*(\omega|_W))\right) \\ &= (\varphi|_W)^*\tau^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right) \\ &= (\psi|_W)^*\left(d_B^k((\psi^{-1})^*(\omega|_W))\right) \\ &= (\eta_V^\psi)|_W. \end{align*} Therefore the two coordinate prescriptions define the same form on the overlap. [/guided] [/step] [step:Glue the compatible local forms to a global exterior derivative] The collection of chart domains covers $M$, and the forms $\eta_U^\varphi \in \Omega^{k+1}(U)$ agree on pairwise overlaps. Hence there is a unique smooth $(k+1)$-form \begin{align*} d_M^k\omega \in \Omega^{k+1}(M) \end{align*} such that \begin{align*} (d_M^k\omega)|_U=\eta_U^\varphi \end{align*} for every chart $(U,\varphi)$. Explicitly, for each $p\in M$, choose any chart $(U,\varphi)$ with $p\in U$ and set \begin{align*} (d_M^k\omega)_p := (\eta_U^\varphi)_p. \end{align*} The overlap compatibility proved above makes this definition independent of the chosen chart, and smoothness is local in charts because each $\eta_U^\varphi$ is smooth. Linearity follows from the linearity of restriction, pullback, and the Euclidean exterior derivative. Thus \begin{align*} d_M^k: \Omega^k(M) \to \Omega^{k+1}(M) \end{align*} is an $\mathbb{R}$-[linear map](/page/Linear%20Map) satisfying the stated coordinate formula. [/step] [step:Show that applying the exterior derivative twice gives zero] Let $\omega \in \Omega^k(M)$ and let $(U,\varphi)$ be a smooth chart. By the defining coordinate formula, \begin{align*} (d_M^{k+1}d_M^k\omega)|_U = \varphi^*\left( d_{\varphi(U)}^{k+1} \left( (\varphi^{-1})^*((d_M^k\omega)|_U) \right) \right). \end{align*} Using the defining formula for $(d_M^k\omega)|_U$, the Euclidean representative of $(d_M^k\omega)|_U$ is \begin{align*} (\varphi^{-1})^*((d_M^k\omega)|_U) = d_{\varphi(U)}^k\left((\varphi^{-1})^*(\omega|_U)\right). \end{align*} Therefore \begin{align*} (d_M^{k+1}d_M^k\omega)|_U &= \varphi^*\left( d_{\varphi(U)}^{k+1} d_{\varphi(U)}^k \left((\varphi^{-1})^*(\omega|_U)\right) \right) \\ &= \varphi^*(0) \\ &= 0. \end{align*} Here we used the Euclidean identity $d^{k+1}d^k=0$, citing a result not yet in the wiki: Euclidean exterior derivative squares to zero. Since the chart domains cover $M$, it follows that \begin{align*} d_M^{k+1}(d_M^k\omega)=0. \end{align*} [/step] [step:Verify compatibility with pullback by smooth maps] Let $F: N \to M$ be a smooth map between smooth manifolds, and let $\omega \in \Omega^k(M)$. It suffices to prove the identity locally on $N$. Let $(V,\eta)$ be a chart on $N$ and choose a chart $(U,\varphi)$ on $M$ such that, after replacing $V$ by a smaller chart domain if necessary, $F(V)\subseteq U$. Define the coordinate representative of $F$ by \begin{align*} f: \eta(V) &\to \varphi(U) \\ z &\mapsto \varphi(F(\eta^{-1}(z))). \end{align*} Also define the coordinate representative of $\omega|_U$ by \begin{align*} \alpha := (\varphi^{-1})^*(\omega|_U) \in \Omega^k(\varphi(U)). \end{align*} Then the coordinate representative of $(F^*\omega)|_V$ is \begin{align*} (\eta^{-1})^*((F^*\omega)|_V)=f^*\alpha. \end{align*} Using the definition of $d_N^k$ in the chart $(V,\eta)$ and Euclidean naturality of exterior differentiation, \begin{align*} (d_N^k(F^*\omega))|_V &= \eta^*\left(d_{\eta(V)}^k\left((\eta^{-1})^*((F^*\omega)|_V)\right)\right) \\ &= \eta^*\left(d_{\eta(V)}^k(f^*\alpha)\right) \\ &= \eta^*\left(f^*(d_{\varphi(U)}^k\alpha)\right). \end{align*} On the other hand, by the definition of $d_M^k$ in the chart $(U,\varphi)$, \begin{align*} (d_M^k\omega)|_U = \varphi^*(d_{\varphi(U)}^k\alpha). \end{align*} Pulling back by $F|_V: V\to U$ gives \begin{align*} (F^*(d_M^k\omega))|_V &= (F|_V)^*\varphi^*(d_{\varphi(U)}^k\alpha) \\ &= (\varphi\circ F|_V)^*(d_{\varphi(U)}^k\alpha) \\ &= (\,f\circ\eta\,)^*(d_{\varphi(U)}^k\alpha) \\ &= \eta^*\left(f^*(d_{\varphi(U)}^k\alpha)\right). \end{align*} Thus \begin{align*} (F^*(d_M^k\omega))|_V=(d_N^k(F^*\omega))|_V. \end{align*} Since the chart domains $V$ cover $N$, we conclude \begin{align*} F^*(d_M^k\omega)=d_N^k(F^*\omega). \end{align*} [guided] We prove pullback compatibility by reducing it to the Euclidean statement in coordinates. Let $F: N\to M$ be smooth and let $\omega\in\Omega^k(M)$. Because equality of differential forms is local, choose a chart $(V,\eta)$ on $N$. By shrinking $V$ if necessary, choose a chart $(U,\varphi)$ on $M$ such that $F(V)\subseteq U$. This shrinking is legitimate because smooth forms agree globally once they agree on an open cover. In these charts, the smooth map $F$ is represented by \begin{align*} f: \eta(V) &\to \varphi(U) \\ z &\mapsto \varphi(F(\eta^{-1}(z))). \end{align*} The form $\omega|_U$ is represented on $\varphi(U)$ by \begin{align*} \alpha := (\varphi^{-1})^*(\omega|_U). \end{align*} Now compute the coordinate representative of $F^*\omega$ on $V$. Since $\varphi\circ F|_V=f\circ\eta$, functoriality of pullback gives \begin{align*} (\eta^{-1})^*((F^*\omega)|_V)=f^*\alpha. \end{align*} Apply the definition of $d_N^k$ in the chart $(V,\eta)$. We get \begin{align*} (d_N^k(F^*\omega))|_V &= \eta^*\left(d_{\eta(V)}^k\left((\eta^{-1})^*((F^*\omega)|_V)\right)\right) \\ &= \eta^*\left(d_{\eta(V)}^k(f^*\alpha)\right). \end{align*} The Euclidean naturality of the exterior derivative says that \begin{align*} d_{\eta(V)}^k(f^*\alpha)=f^*(d_{\varphi(U)}^k\alpha), \end{align*} so \begin{align*} (d_N^k(F^*\omega))|_V = \eta^*\left(f^*(d_{\varphi(U)}^k\alpha)\right). \end{align*} Now compute the other side. By definition of $d_M^k$ in the chart $(U,\varphi)$, \begin{align*} (d_M^k\omega)|_U = \varphi^*(d_{\varphi(U)}^k\alpha). \end{align*} Pulling back along $F|_V$ gives \begin{align*} (F^*(d_M^k\omega))|_V &= (F|_V)^*\varphi^*(d_{\varphi(U)}^k\alpha) \\ &= (\varphi\circ F|_V)^*(d_{\varphi(U)}^k\alpha) \\ &= (f\circ\eta)^*(d_{\varphi(U)}^k\alpha) \\ &= \eta^*\left(f^*(d_{\varphi(U)}^k\alpha)\right). \end{align*} The two local expressions are identical. Therefore \begin{align*} (F^*(d_M^k\omega))|_V=(d_N^k(F^*\omega))|_V. \end{align*} Since such chart domains $V$ cover $N$, the global identity follows. [/guided] [/step] [step:Prove uniqueness from the coordinate formula] Suppose \begin{align*} D_M^k: \Omega^k(M)\to\Omega^{k+1}(M) \end{align*} is another $\mathbb{R}$-linear map satisfying the same coordinate formula. For every $\omega\in\Omega^k(M)$ and every chart $(U,\varphi)$, \begin{align*} (D_M^k\omega)|_U = \varphi^*\left(d_{\varphi(U)}^k((\varphi^{-1})^*(\omega|_U))\right) = (d_M^k\omega)|_U. \end{align*} Because chart domains cover $M$, equality on every chart domain implies \begin{align*} D_M^k\omega=d_M^k\omega. \end{align*} Since this holds for every $\omega\in\Omega^k(M)$, the map $d_M^k$ is unique. The construction, the identity $d^2=0$, and pullback compatibility together prove the theorem. [/step]