[proofplan] The proof is local in coordinate charts, where the map becomes a smooth map between open subsets of Euclidean spaces and the wave front condition becomes a Fourier decay condition in cones. The only analytic input is the Euclidean Hörmander pullback theorem, stated below with its continuity and wave front conclusions; the normal-set hypothesis is checked locally by a compact conic separation argument. Applying that Euclidean theorem to the coordinate representatives gives local pullbacks compatible with changes of chart. The local constructions then glue, and uniqueness follows from the uniqueness part of the Euclidean theorem together with locality of distributions. [/proofplan]

[step:Reduce the construction to compactly supported distributions in coordinate charts]Let $K \subset X$ be compact. Choose finitely many coordinate charts $(U_i,\varphi_i)$ on $X$ with $K \subset \bigcup_i U_i$ and finitely many coordinate charts $(V_i,\psi_i)$ on $Y$ such that $F(U_i) \subset V_i$. Let $\alpha_i \in C_c^\infty(U_i)$ be a [partition of unity](/page/Partition%20of%20Unity) on a neighbourhood of $K$, and let $\beta_i \in C_c^\infty(V_i)$ satisfy $\beta_i = 1$ on a neighbourhood of $F(\operatorname{supp}\alpha_i)$. It is enough to construct, for each $i$, the pullback of $\beta_i u$ by the coordinate representative \begin{align*} f_i := \psi_i \circ F \circ \varphi_i^{-1}: \varphi_i(U_i) \to \psi_i(V_i), \end{align*} where $\varphi_i(U_i) \subset \mathbb{R}^{m}$ and $\psi_i(V_i) \subset \mathbb{R}^{n}$ are open sets. Assuming the local Euclidean theorem has supplied the continuous pullback operator \begin{align*} P_i: \mathcal{D}'_{\Gamma_i}(\psi_i(V_i)) \to \mathcal{D}'_{f_i^*\Gamma_i}(\varphi_i(U_i)), \end{align*} where $\Gamma_i$ is the coordinate image of $\Gamma$ over $V_i$, the desired distribution is determined for a [test function](/page/Test%20Function) $\phi \in C_c^\infty(X)$ supported in $K$ by the finite sum \begin{align*} F^*u(\phi) := \sum_i P_i(\mathcal{C}_{\psi_i}(\beta_i u))(\mathcal{C}_{\varphi_i}(\alpha_i\phi)). \end{align*} Here $\mathcal{C}_{\psi_i}(\beta_i u) \in \mathcal{D}'(\psi_i(V_i))$ denotes the standard coordinate representation of the compactly supported distribution $\beta_i u$ under the diffeomorphism $\psi_i:V_i\to\psi_i(V_i)$, defined by its usual action on pushed-forward test functions; this is not the singular pullback operation being constructed. Similarly, $\mathcal{C}_{\varphi_i}(\alpha_i\phi) \in C_c^\infty(\varphi_i(U_i))$ denotes the coordinate representation of the test function $\alpha_i\phi$ under $\varphi_i$. The coordinate transformation law for wave front sets and the locality of distributions show that the construction is independent of the chosen charts once the Euclidean construction is unique on overlaps. Thus we prove the theorem in the following local form: $U \subset \mathbb{R}^{m}$ and $V \subset \mathbb{R}^{n}$ are open, $f: U \to V$ is smooth, $u \in \mathcal{D}'(V)$ has compact support after multiplication by a cutoff, and test functions on $U$ have compact support. In this local form, $\mathcal{L}^{m}$ and $\mathcal{L}^{n}$ denote [Lebesgue measure](/page/Lebesgue%20Measure) on $\mathbb{R}^{m}$ and $\mathbb{R}^{n}$, respectively, and the [Fourier transform](/page/Fourier%20Transform) of a compactly supported smooth function $h: \mathbb{R}^{k} \to \mathbb{C}$ is defined by \begin{align*} \hat{h}(\xi) := \int_{\mathbb{R}^{k}} e^{-iz\cdot \xi}h(z)\,d\mathcal{L}^{k}(z). \end{align*}[/step]

[guided]The pullback of a distribution is local on the source. To define $F^*u$ against a compactly supported test function $\phi \in C_c^\infty(X)$, only the values of $F$ near $\operatorname{supp}\phi$ and the values of $u$ near $F(\operatorname{supp}\phi)$ matter. Therefore we choose finitely many coordinate charts $(U_i,\varphi_i)$ on $X$ covering $\operatorname{supp}\phi$ and charts $(V_i,\psi_i)$ on $Y$ with $F(U_i) \subset V_i$. Let $\alpha_i \in C_c^\infty(U_i)$ be a partition of unity near $\operatorname{supp}\phi$. For each $i$, choose $\beta_i \in C_c^\infty(V_i)$ with $\beta_i = 1$ near $F(\operatorname{supp}\alpha_i)$. This cutoff is needed because the local Euclidean argument is easiest for compactly supported distributions. In coordinates the map is \begin{align*} f_i := \psi_i \circ F \circ \varphi_i^{-1}: \varphi_i(U_i) \to \psi_i(V_i). \end{align*} Once the Euclidean theorem has supplied the local pullback operator \begin{align*} P_i: \mathcal{D}'_{\Gamma_i}(\psi_i(V_i)) \to \mathcal{D}'_{f_i^*\Gamma_i}(\varphi_i(U_i)), \end{align*} where $\Gamma_i$ is the coordinate image of $\Gamma$ over $V_i$, the local piece of the desired pairing is \begin{align*} P_i(\mathcal{C}_{\psi_i}(\beta_i u))(\mathcal{C}_{\varphi_i}(\alpha_i\phi)). \end{align*} Here $\mathcal{C}_{\psi_i}(\beta_i u)$ is the ordinary coordinate representation of the distribution $\beta_i u$ under the chart diffeomorphism $\psi_i$, and $\mathcal{C}_{\varphi_i}(\alpha_i\phi)$ is the coordinate representation of the test function $\alpha_i\phi$ under $\varphi_i$. Summing over $i$ gives \begin{align*} F^*u(\phi) := \sum_i P_i(\mathcal{C}_{\psi_i}(\beta_i u))(\mathcal{C}_{\varphi_i}(\alpha_i\phi)). \end{align*} This formula is meaningful once the Euclidean pullback has been constructed. It is independent of the partition and charts because distributions are local and because wave front sets transform covariantly under diffeomorphisms. Thus the only real analytic work is the Euclidean statement: construct the pullback for a smooth map $f: U \to V$ between open subsets of Euclidean spaces, with compact supports fixed by cutoffs.[/guided]

[step:Extract uniform conic separation from the normal set condition] Work locally with $f: U \to V$, where $U \subset \mathbb{R}^{m}$ and $V \subset \mathbb{R}^{n}$ are open. Let $K \subset U$ be compact and let $L \subset V$ be compact with $f(K) \subset L$. Define the local normal set over $K$ by \begin{align*} N_{f,K} := \{(f(x),\eta) \in L \times (\mathbb{R}^{n}\setminus\{0\}) : x \in K \text{ and } (df_x)^*\eta = 0\}. \end{align*} Let $\Gamma_L := \Gamma \cap (L \times (\mathbb{R}^{n}\setminus\{0\}))$. Since $\Gamma \cap N_F = \varnothing$, the sets $\Gamma_L$ and $N_{f,K}$ are disjoint. [claim:There is a uniform lower bound for the pulled-back covectors] There exists a constant $c_K > 0$ such that \begin{align*} |(df_x)^*\eta| \geq c_K|\eta| \end{align*} for every $x \in K$ and every $\eta \in \mathbb{R}^{n}\setminus\{0\}$ with $(f(x),\eta) \in \Gamma_L$. [/claim] [proof] Suppose no such $c_K$ exists. Then there are sequences $x_j \in K$ and $\eta_j \in \mathbb{R}^{n}\setminus\{0\}$ such that $(f(x_j),\eta_j) \in \Gamma_L$ and \begin{align*} |(df_{x_j})^*\eta_j| < \frac{1}{j}|\eta_j|. \end{align*} Define $S^{n-1}:=\{\omega \in \mathbb{R}^{n}: |\omega|=1\}$ and set $\omega_j := \eta_j/|\eta_j| \in S^{n-1}$. Since $K$ and $S^{n-1}$ are compact, after passing to a subsequence there are $x \in K$ and $\omega \in S^{n-1}$ with $x_j \to x$ and $\omega_j \to \omega$. Because $\Gamma_L$ is closed in the local trivialization $L \times (\mathbb{R}^{n}\setminus\{0\})$ and conic, $(f(x),\omega) \in \Gamma_L$. By continuity of $x \mapsto df_x$, \begin{align*} |(df_x)^*\omega| = \lim_{j \to \infty}|(df_{x_j})^*\omega_j| = 0. \end{align*} Thus $(f(x),\omega) \in N_{f,K} \cap \Gamma_L$, contradicting $\Gamma \cap N_F = \varnothing$. Hence the constant $c_K$ exists. [/proof] This same compactness argument also proves that $F^*\Gamma$ is closed in $T^*X \setminus \{0\}$. Indeed, suppose $(x_j,(dF_{x_j})^*\eta_j) \in F^*\Gamma$ converges to $(x,\xi) \in T^*X \setminus \{0\}$ in a local trivialization. After restricting to a coordinate neighbourhood of $x$ and discarding finitely many terms, all $x_j$ lie in a compact set $K' \subset U$ and all $F(x_j)$ lie in a compact set $L' \subset V$. Since $(F(x_j),\eta_j) \in \Gamma \cap (L' \times (\mathbb{R}^{n}\setminus\{0\}))$, the lower bound applied on $K'$ gives \begin{align*} |\eta_j| \leq c_{K'}^{-1}|(dF_{x_j})^*\eta_j|. \end{align*} The convergent sequence $((dF_{x_j})^*\eta_j)_j$ is bounded, so $(\eta_j)_j$ is bounded. Passing to a subsequence, $\eta_j \to \eta$; closedness of $\Gamma$ gives $(F(x),\eta) \in \Gamma$, and continuity gives $\xi = (dF_x)^*\eta$. Thus $(x,\xi) \in F^*\Gamma$. Conicity follows directly from the linearity of $(dF_x)^*$ in the covector variable. [/step]

[step:Apply the Euclidean Hörmander pullback theorem to define the local pullback]We now use the following external Euclidean result, Hörmander's pullback theorem for distributions, in the form of The Analysis of Linear Partial Differential Operators I, Theorem 8.2.4 together with its standard uniqueness and regularization formulation. If $U \subset \mathbb{R}^{m}$ and $V \subset \mathbb{R}^{n}$ are open, $f:U\to V$ is smooth, $\Gamma \subset V \times (\mathbb{R}^{n}\setminus\{0\})$ is closed conic, and \begin{align*} \Gamma \cap \{(f(x),\eta):x\in U,\ \eta\in\mathbb{R}^{n}\setminus\{0\},\ (df_x)^*\eta=0\}=\varnothing, \end{align*} then ordinary composition on $C^\infty(V)$ extends to a continuous [linear map](/page/Linear%20Map) \begin{align*} f^*:\mathcal{D}'_\Gamma(V)\to \mathcal{D}'_{f^*\Gamma}(U), \end{align*} where \begin{align*} f^*\Gamma:=\{(x,(df_x)^*\eta):(f(x),\eta)\in\Gamma,\ (df_x)^*\eta\neq 0\}. \end{align*} The same Euclidean result gives the displayed wave front inclusion and the defining Fourier-seminorm continuity estimates. Its regularization formulation states that, after localizing to compact support, the extension is the distributional limit of $u*\rho_\varepsilon$ composed with $f$ for any [standard mollifier](/page/Standard%20Mollifier) $\rho$, and that this limit is independent of the chosen standard mollifier. Uniqueness is the uniqueness of a continuous extension agreeing with ordinary pullback on smooth functions in the Hörmander topology. The hypotheses of this external theorem match the local situation. The sets $U$ and $V$ are open subsets of Euclidean spaces, $f$ is smooth by construction, and the previous step proves the required separation from the local normal set on every compact set supporting a test function. Hence, for every $u\in\mathcal{D}'_\Gamma(V)$, the local pullback $f^*u\in\mathcal{D}'_{f^*\Gamma}(U)$ is defined by this theorem. If $\rho\in C_c^\infty(\mathbb{R}^{n})$ is a standard mollifier with \begin{align*} \int_{\mathbb{R}^{n}}\rho(y)\,d\mathcal{L}^{n}(y)=1, \end{align*} and if $\rho_\varepsilon:\mathbb{R}^{n}\to\mathbb{R}$ is given by \begin{align*} \rho_\varepsilon(y):=\varepsilon^{-n}\rho(y/\varepsilon), \end{align*} then, after extending compactly supported localized pieces of $u$ by zero to $\mathbb{R}^{n}$, the approximating functionals $T_\varepsilon:C_c^\infty(U)\to\mathbb{C}$ are \begin{align*} T_\varepsilon(\phi):=\int_U (u*\rho_\varepsilon)(f(x))\phi(x)\,d\mathcal{L}^{m}(x). \end{align*} Hörmander's theorem asserts that $T_\varepsilon(\phi)$ converges for every $\phi\in C_c^\infty(U)$ and that the resulting distribution is the unique continuous extension of ordinary pullback with the stated wave front control.[/step]

[guided]The analytic difficulty in the pullback theorem is not a formal manipulation with convolution. It is the Euclidean microlocal theorem of Hörmander: under the condition that no covector in $\Gamma$ annihilates the differential of $f$, composition with $f$ extends from smooth functions to distributions whose wave front sets lie in $\Gamma$. We use that theorem here as an external result, and we must check its hypotheses rather than reprove its nonstationary phase estimates. The local hypotheses have exactly the required form. We are working with open sets $U\subset\mathbb{R}^{m}$ and $V\subset\mathbb{R}^{n}$, and the coordinate representative $f:U\to V$ is smooth. The closed conic set is the coordinate version of $\Gamma$. The obstruction set in Hörmander's theorem is \begin{align*} \{(f(x),\eta):x\in U,\ \eta\in\mathbb{R}^{n}\setminus\{0\},\ (df_x)^*\eta=0\}. \end{align*} Let $K\subset U$ be a compact set containing the support of the test functions under consideration, and let $L\subset V$ be compact with $f(K)\subset L$. The normal-set hypothesis gives \begin{align*} \Gamma\cap\{(f(x),\eta):x\in K,\ \eta\in\mathbb{R}^{n}\setminus\{0\},\ (df_x)^*\eta=0\}=\varnothing. \end{align*} If no constant $c_K>0$ satisfied $|(df_x)^*\eta|\ge c_K|\eta|$ for $(f(x),\eta)\in\Gamma\cap(L\times(\mathbb{R}^{n}\setminus\{0\}))$, then normalized covectors $\omega_j=\eta_j/|\eta_j|$ and points $x_j\in K$ would have a convergent subsequence with limit $(x,\omega)\in K\times S^{n-1}$. Closedness and conicity of $\Gamma$ would give $(f(x),\omega)\in\Gamma$, while continuity of $df$ would give $(df_x)^*\omega=0$, contradicting the displayed disjointness. Therefore the required microlocal separation holds on every compact set supporting a test function, so the external theorem applies locally. The theorem gives a distribution $f^*u\in\mathcal{D}'(U)$ and also gives the topology needed later: the map \begin{align*} f^*:\mathcal{D}'_\Gamma(V)\to\mathcal{D}'_{f^*\Gamma}(U) \end{align*} is continuous for the Hörmander topologies. If $u$ is first smoothed by a standard mollifier $\rho_\varepsilon$, the temporary smooth pullback acts on $\phi\in C_c^\infty(U)$ by \begin{align*} T_\varepsilon(\phi):=\int_U (u*\rho_\varepsilon)(f(x))\phi(x)\,d\mathcal{L}^{m}(x). \end{align*} The Euclidean theorem asserts that these pairings converge to $f^*u(\phi)$ and that the limit is independent of the chosen standard mollifier. Thus no unjustified exchange of distributional pairing, Fourier inversion, and integration is needed in this proof; those estimates are exactly the content of the cited Euclidean theorem.[/guided]

[step:Record independence of regularization and agreement with smooth pullback] The independence of the mollifier is part of the Euclidean Hörmander pullback theorem just applied: any two standard mollifier families give the same distributional limit. Thus the local distribution $f^*u$ is intrinsic and is not tied to the auxiliary choice of $\rho$. If $u$ is represented by a smooth function $g:V\to\mathbb{C}$, the same theorem says that the extended pullback agrees with the ordinary smooth pullback. Equivalently, for every $\phi\in C_c^\infty(U)$ supported in $K$, \begin{align*} f^*u(\phi)=\int_U g(f(x))\phi(x)\,d\mathcal{L}^{m}(x). \end{align*} This verifies compatibility with ordinary composition in the local coordinates. [/step]

[step:Use the Euclidean theorem to obtain Hörmander-topology continuity]For clarity, recall the local seminorms involved. If $\beta\in C_c^\infty(V)$, $\Lambda\subset\mathbb{R}^{n}\setminus\{0\}$ is a closed cone with $\operatorname{supp}\beta\times\Lambda$ disjoint from $\Gamma$, and $N\in\mathbb{N}$, define the map $p_{\beta,\Lambda,N}:\mathcal{D}'_\Gamma(V)\to[0,\infty)$ by \begin{align*} p_{\beta,\Lambda,N}(u):=\sup_{\eta\in\Lambda}(1+|\eta|)^N|\widehat{\beta u}(\eta)|. \end{align*} Together with the ordinary distribution seminorms, these maps generate the local Hörmander topology. The Euclidean Hörmander pullback theorem applied in the previous step includes the following continuity assertion: for every $\alpha\in C_c^\infty(U)$, every closed cone $\Omega\subset\mathbb{R}^{m}\setminus\{0\}$ such that $\operatorname{supp}\alpha\times\Omega$ is disjoint from $f^*\Gamma$, and every $N\in\mathbb{N}$, the seminorm \begin{align*} u\mapsto \sup_{\xi\in\Omega}(1+|\xi|)^N|\widehat{\alpha f^*u}(\xi)| \end{align*} is bounded by a finite sum of ordinary distribution seminorms of $u$ and seminorms $p_{\beta_j,\Lambda_j,M_j}(u)$ whose cones satisfy $\operatorname{supp}\beta_j\times\Lambda_j\cap\Gamma=\varnothing$. Therefore \begin{align*} f^*: \mathcal{D}'_\Gamma(V) \to \mathcal{D}'_{f^*\Gamma}(U) \end{align*} is continuous for the Hörmander topologies. This continuity is not inferred from pointwise distributional convergence; it is one of the Fourier-seminorm estimates supplied by the Euclidean theorem.[/step]

[guided]The Hörmander topology has two kinds of controls: ordinary distribution seminorms and conic Fourier-decay seminorms. For a cutoff $\beta\in C_c^\infty(V)$ and a cone $\Lambda$ avoiding $\Gamma$ over $\operatorname{supp}\beta$, the Fourier-decay seminorm is the map \begin{align*} p_{\beta,\Lambda,N}:\mathcal{D}'_\Gamma(V)\to[0,\infty),\qquad p_{\beta,\Lambda,N}(u):=\sup_{\eta\in\Lambda}(1+|\eta|)^N|\widehat{\beta u}(\eta)|. \end{align*} Continuity of pullback means that every corresponding seminorm of $f^*u$ must be controlled by finitely many such seminorms of $u$. This is exactly part of Hörmander's Euclidean pullback theorem. We verify the hypotheses in the same local setting. The map $f$ is smooth, $\Gamma$ is closed conic, and for each compact $K\subset U$ meeting $\operatorname{supp}\alpha$ the compact conic argument gives a constant $c_K>0$ such that \begin{align*} |(df_x)^*\eta|\ge c_K|\eta| \end{align*} whenever $x\in K$ and $(f(x),\eta)\in\Gamma$. This is the local form of the condition that $\Gamma$ avoids the normal set. The theorem then states that whenever $\alpha\in C_c^\infty(U)$ and a closed cone $\Omega\subset\mathbb{R}^{m}\setminus\{0\}$ avoid $f^*\Gamma$ over $\operatorname{supp}\alpha$, the seminorm \begin{align*} u\mapsto \sup_{\xi\in\Omega}(1+|\xi|)^N|\widehat{\alpha f^*u}(\xi)| \end{align*} is bounded by finitely many defining seminorms of $\mathcal{D}'_\Gamma(V)$. Thus the proof does not rely on the false principle that distributional convergence implies weighted Fourier-seminorm convergence. The weighted Fourier estimates are supplied directly by the cited theorem after its support, cone, smoothness, and normal-set hypotheses have been checked.[/guided]

[step:Derive the wave front inclusion] Define the local normal set by \begin{align*} N_f := \{(f(x),\eta) \in V \times (\mathbb{R}^{n} \setminus \{0\}) : x \in U,\ (df_x)^*\eta = 0\}. \end{align*} Let $u \in \mathcal{D}'(V)$ satisfy $\operatorname{WF}(u) \cap N_f=\varnothing$, and define \begin{align*} \Gamma_u := \operatorname{WF}(u). \end{align*} The preceding construction applies with $\Gamma=\Gamma_u$. Let $(x_0,\xi_0) \in T^*U \setminus \{0\}$ be outside \begin{align*} \{(x,(df_x)^*\eta):(f(x),\eta)\in\operatorname{WF}(u) \text{ and } (df_x)^*\eta\neq 0\}. \end{align*} Choose a cutoff $\alpha \in C_c^\infty(U)$ with $\alpha(x_0)\neq 0$ and support sufficiently small, and choose a closed conic neighbourhood $\Omega$ of $\xi_0$ such that \begin{align*} \operatorname{supp}\alpha \times \Omega \end{align*} is disjoint from $f^*\Gamma_u$. The continuity estimate from the previous step gives, for every $N \in \mathbb{N}$, \begin{align*} \sup_{\xi \in \Omega}(1+|\xi|)^N|\widehat{\alpha f^*u}(\xi)| < \infty. \end{align*} By the local characterization of wave front sets by conic Fourier decay, $(x_0,\xi_0)\notin \operatorname{WF}(f^*u)$. Since $(x_0,\xi_0)$ was arbitrary outside the displayed set, we obtain \begin{align*} \operatorname{WF}(f^*u)\subset \{(x,(df_x)^*\eta):(f(x),\eta)\in\operatorname{WF}(u) \text{ and } (df_x)^*\eta\neq 0\}. \end{align*} This is the desired local wave front inclusion. [/step]

[step:Patch the local pullbacks and prove uniqueness] Return to the manifolds $X$ and $Y$. The local pullbacks constructed in coordinate charts agree on overlaps because both are limits of the same ordinary pullbacks of smooth regularizations and because the coordinate change formula for distributions is compatible with ordinary pullback by diffeomorphisms. Hence the local distributions glue to a unique global distribution $F^*u \in \mathcal{D}'(X)$. The local wave front estimate proved above is invariant under coordinate changes, so it gives \begin{align*} \operatorname{WF}(F^*u)\subset F^*\Gamma \end{align*} when $\operatorname{WF}(u)\subset\Gamma$, and gives the stated sharper inclusion when $\Gamma=\operatorname{WF}(u)$. Continuity of the global map follows from the local continuity estimates because the Hörmander topology on manifolds is defined by the corresponding finite families of coordinate cutoffs, distribution seminorms, and conic Fourier decay seminorms. Linearity follows from linearity of regularization, composition of smooth regularizations, and passage to the limit. Finally, uniqueness is local. On each coordinate patch, the Euclidean Hörmander pullback theorem gives the unique continuous extension of ordinary pullback from smooth functions to $\mathcal{D}'_\Gamma$ with the stated Hörmander topology. If two global continuous extensions existed, their restrictions to every coordinate patch would agree with this unique Euclidean extension. By locality of distributions, equality on all coordinate patches implies equality on $X$. This completes the proof. [/step]