Formal manifolds]Formal manifolds: foundations, function spaces, and Poincaré's lemma

F. Chen]Fulin Chen
School of Mathematical Sciences, Xiamen University,
Xiamen, 361005, China<EMAIL_ADDRESS>
B. Sun]Binyong Sun
Institute for Advanced Study in Mathematics & New Cornerstone Science Laboratory, Zhejiang University,  Hangzhou, 310058, China

C. Wang]Chuyun Wang
Institute for Theoretical
Sciences and School of Science, Westlake University,
Hangzhou,310030, China

[2020]58A05, 58A12, 46F25

This is the first paper in a series that studies
smooth relative Lie algebra homologies and cohomologies
based on the theory of formal manifolds and formal Lie groups.
In this paper, we lay the foundations for this study by introducing the notion of formal manifolds in the context of differential geometry, inspired by the notion of formal schemes in algebraic geometry.
We develop the basic theory for formal manifolds, including a generalization of the theory of vector-valued distributions and generalized functions on smooth manifolds to the setting of formal manifolds. Additionally, we establish Poincaré's lemma for de Rham complexes with coefficients in formal functions, formal generalized functions, compactly supported formal densities, or compactly supported formal distributions.

§ INTRODUCTION

In the setting of algebraic geometry,
formal schemes are intensively studied in the literature.
In this article, we study similar objects called formal manifolds in the setting of differential geometry, motivated by their applications to the representation theory of Lie groups.

§.§ The motivation

The theory of smooth cohomologies and smooth homologies for Lie group representations are respectively introduced in  [11] and [7].
On the other hand,

there is a vast literature for the
algebraic theory of relative Lie algebra (co)homologies, which is concerned with the (co)homologies of representations
of certain Lie pairs $(\q,L)$. Here $\q$ is a finite-dimensional complex Lie
algebra and $L$ is a compact  Lie group,  with additional structures that satisfy specific compatibility conditions (see <cit.> for more details).
Motivated by the recent study in representation theory and automorphic forms, there is a growing interest in establishing a smooth
(co)homology theory for representations of
general Lie pairs $(\q,L)$, with $L$ not necessarily compact. We refer to this theory as smooth relative Lie algebra (co)homology theory, which unifies the smooth (co)homology theory (as introduced in  [11] and [7]) and the algebraic theory of relative Lie algebra (co)homologies.

We expect that the theory of  smooth relative (co)homologies will be useful in the study of
representation theory of
real reductive groups.
For example, by generalizing the work of Wong (see [35, 36]), the theory should yield interesting smooth representations of real reductive groups through
cohomological induction.
This is the analytic analog of Zuckerman's functor that
produces interesting Harish-Chandra modules (see [15]).
However, in Zuckerman's construction, no topology is considered, whereas the topologies that we put on the representations should play an important role in some problems in representation theory.

Starting with this paper, we will develop a new theory of smooth relative (co)homologies in several papers.
In this paper, we introduce and study formal manifolds,
which are analogs of formal schemes in the setting of differential geometry.
The definition of formal manifolds naturally comes out of the two objects in Lie pairs.
Recall that the formal Lie theory theorem asserts an equivalence of categories between
the category of finite-dimensional complex Lie algebras and the category
of complex formal group laws (see <cit.> for example). Underlying a formal group law is a formal power series algebra.
On the other hand, a smooth manifold (and in particular a Lie group) is naturally a locally ringed space with the sheaf of
$\C$-valued smooth functions as its structure sheaf.
Roughly speaking,  formal manifolds are locally ringed spaces over $\Spec(\C)$ that unify the notions of  formal power series algebras and smooth manifolds
(see Definition <ref> for details).

This paper primarily focuses on exploring function spaces and Poincaré's lemma within the context of formal manifolds.

In another paper of this series, we will study formal Lie groups, which are defined as group objects in the category of formal manifolds.

We will prove a generalization of the formal Lie theory theorem, which asserts an equivalence of categories between the category of formal Lie groups
and that of  Lie pairs.
Using the language of formal manifolds and formal Lie groups, we will finally establish the smooth relative
(co)homology theory.

We will define formal manifolds and related notions in what follows, and provide an outline of the main results of this paper.

§.§ $\BC$-locally ringed spaces

As mentioned before, we will work in the framework of locally ringed spaces.

A $\BC$-locally ringed space is a topological space $M$, together with a sheaf  $\CO$ of commutative unital $\BC$-algebras on it such that all the stalks are local rings. Equivalently, a  $\BC$-locally ringed space is a locally ringed space over the locally ringed space $\Spec(\BC)$.

All $\BC$-locally ringed spaces form a category as usual. The morphisms in this category are morphisms of locally ringed spaces over $\Spec(\BC)$. More precisely, a morphism from a $\BC$-locally ringed space $(M,\CO)$ to another  $\BC$-locally ringed space $(M',\CO')$ is a pair $\varphi=({\overline\varphi}, \varphi^*)$, where ${\overline\varphi}: M\rightarrow M'$ is a continuous map and

φ^*: φ^-1'→is a $\BC$-algebra sheaf homomorphism that induces local homomorphisms on the stalks.
For  open subsets $U'$ of $M'$ and $U$ of $M$ such that $\overline\varphi(U)\subset U'$,
we write

\[\varphi^*_{U',U}:\CO'(U')\rightarrow \CO(U)\]
for the homomorphism of $\C$-algebras  induced by (<ref>).
If there is no confusion, we will denote   $\varphi^*_{U',U}$ by  $\varphi^*_{U'}$ or  $\varphi^*$ for simplicity.

For every $\BC$-locally ringed space $(M, \CO)$, define a subsheaf $\m_\CO$ of $\CO$ by

_(U):={f∈(U)|f_a∈_a   for all $a\in U$},
where $U$ is an open subset of $M$, $f_a$ is the germ of $f$ at $a$,  and  $\m_a$ is the maximal ideal of the stalk $\CO_a$.
Note that $\m_\CO$ is an ideal of $\CO$. Form the quotient sheaf

Then $(M, \underline \CO)$ is also a $\BC$-locally ringed space.

The $\BC$-locally ringed space $(M, \underline \CO)$ defined above is called the reduction of $(M, \CO)$.
The $\BC$-locally ringed space $(M, \CO)$ is said to be reduced if $\underline \CO=\CO$, or equivalently, $\m_\CO$ is the zero sheaf.

By abuse of notation,  we will often not distinguish a $\BC$-locally ringed space  $(M, \CO)$ with its underlying topological space $M$, and call $\CO$ the structure sheaf of $M$.
We write $\underline M:=M$ as a topological space, to be viewed as a reduced $\BC$-locally ringed space with the structure sheaf $\underline \CO$.

All reduced $\BC$-locally ringed spaces form a full subcategory of the category of
$\BC$-locally ringed spaces, and thus they also form a category.
By using (<ref>), we have an obvious morphism

of $\BC$-locally ringed spaces. For every morphism $\varphi:M_1\rightarrow M_2$ of $\BC$-locally ringed spaces, there is a unique morphism

φ: M_1→M_2such that the diagram

M_1 @>  φ>> M_2

@AAA          @AAA

M_1@> φ>>  M_2

commutes. We call $\underline \varphi$ the reduction of $\varphi$.
The reduction assignments  $M\mapsto \underline M$ and $\varphi\mapsto \underline \varphi$ form a functor from the category of  $\BC$-locally ringed spaces to the category of reduced  $\BC$-locally ringed spaces.

For a $\BC$-locally ringed space $M$ with structure sheaf $\CO$, the formal stalk at a point $a\in M$ is defined to be the local $\BC$-algebra

_a:=_k∈ _a/_a^k    (:={0,1,2,…}).

§.§ Formal manifolds

We consider a smooth manifold as a $\BC$-locally ringed space with the sheaf of complex-valued smooth functions as the structure sheaf.

Throughout this paper, we assume that all smooth manifolds are Hausdorff and paracompact. They may or may not be equi-dimensional,
and may or may not have countably many connected components. We also view the empty set as a smooth manifold. For a smooth manifold $N$, we use $\mathrm C^\infty(N)$ to denote the $\BC$-algebra of complex-valued smooth functions on $N$.

Let  $k\in \BN$, and let $N$ be a smooth manifold. For every open subset $U\subset N$, write

\[
\CO_N^{(k)}(U):=\RC^\infty(U)[[y_1, y_2, \dots, y_k]] \quad (\textrm{the algebra of formal power series}).
\]

With the obvious restriction maps, $(N, \CO_N^{(k)})$ is a $\BC$-locally ringed space. For simplicity, we also write $N^{(k)}$ for this $\BC$-locally ringed space.

The $\BC$-locally ringed space $N^{(k)}$ defined as above provides an example of formal manifolds. In general, we make the following definition.

A formal manifold  is a $\BC$-locally ringed space $(M, \CO)$ such that

* the topological space $M$ is paracompact and Hausdorff; and

* for every $a\in M$, there is an open  neighborhood $U$ of $a$ in $M$ and $n,k\in \BN$ such that $(U, \CO|_U)$ is isomorphic to $(\R^n)^{(k)}$ as a $\BC$-locally ringed space.

Let $(M, \CO)$ be a formal manifold.
For every $a\in M$, the  uniquely determined natural numbers $n$ and $k$ in Definition <ref> are respectively
called the dimension and the degree of $M$ at $a$, denoted by $\dim_a M$ and $\deg_a M$.
We say that $(M,\CO)$ has equi-dimension $n$ if $\dim_a M=n$ for all $a\in M$,
and has equi-degree $k$ if  $\deg_a M=k$ for all $a\in M$.
An element in $\CO(M)$ is called a formal function on $M$.

All formal manifolds form a full subcategory of the category of $\BC$-locally ringed spaces, and thus they also form a category.

A smooth manifold is naturally a formal manifold of equi-degree $0$.
On the other hand, the reduction of a formal manifold is naturally a smooth manifold.
Moreover, for every  formal manifold, the following conditions are  equivalent to each other:

* it has equi-degree $0$;

* it is reduced in the sense of Definition <ref>;

* it is a smooth manifold.

A formal manifold is said to be infinitesimal if its underlying topological space has precisely one element.

A formal power series algebra $A:=\C[[y_1, y_2, \dots, y_k]] $ ($k\in \BN$) induces naturally  an infinitesimal formal manifold $(M,\CO)$ such that  $\CO(M)= A$ as  $\C$-algebras.
Conversely, up to isomorphism, every infinitesimal formal manifold has such a form.

Let $(M,\CO)$ be a formal manifold.
In Section <ref>, we establish some basic properties of $(M,\CO)$.
In Section <ref>, we introduce the notion of differential operators between two sheaves of $\CO$-modules.
In Section <ref>, by using certain compactly supported differential operators, we define a canonical topology on the space $\CF(M)$ for every sheaf $\CF$ of $\CO$-modules.  We refer to this topology as the smooth topology.
With the smooth topology, $\CO(M)$ becomes a topological $\BC$-algebra. In other words, the addition map, the multiplication map, and the scalar multiplication map, are all jointly continuous.
As a topological vector space, it is a product of nuclear Fréchet spaces.
Specifically, the formal stalk $\widehat \CO_a$ is a topological $\BC$-algebra for every $a\in M$ (see Example <ref> and Proposition <ref>).

We prove the following theorem in Section <ref>.

For every morphism $\varphi=(\overline\varphi, \varphi^*): (M, \CO)\rightarrow (M', \CO')$ of formal manifolds, the homomorphism $\varphi^*: \CO'(M')\rightarrow \CO(M)$ between $\C$-algebras is continuous. Moreover,

(M, )↦(M),   (φ: (M, )→(M', '))↦(φ^*: '(M')→(M))
is a fully faithful contravariant functor from the category of formal manifolds to the category of topological $\BC$-algebras.

Throughout this paper,  by an LCS,
we mean a
locally convex topological vector
space over $\C$ which may or may not be Hausdorff.
However, a complete (or quasi-complete) LCS is always assumed to be Hausdorff.
As stated in [8], there are three useful topological tensor products on LCS,
the inductive tensor product $\otimes_{\mathrm{i}}$, the projective tensor product $\otimes_\pi$, and the epsilon tensor product $\otimes_\varepsilon$.
We denote the quasi-completions and completions of these topological tensor products by

\[\widetilde\otimes_{\mathrm{i}},\,\, \widetilde\otimes_\pi,\,\, \widetilde\otimes_{\varepsilon}, \quad \text{and}\quad
\widehat\otimes_{\mathrm{i}}, \,\,\widehat\otimes_\pi,\,\, \widehat\otimes_{\varepsilon},\]
Similar notations will be used for topological tensor products of
topological cochain complexes.
Some basics on these topological tensor products are reviewed in Appendixes <ref>, <ref>, and <ref>.

We know that finite products exist in the category of smooth manifolds.
In Section <ref>,
we extend this result to the category of formal manifolds.

Finite products exist in the category of formal manifolds. Moreover, for all formal manifolds $M_1$, $M_2$, $M_3$ such that

\[
M_3=M_1\times M_2,
\]

there are  identifications

\[
\CO_{3}(M_3)=\CO_{1}(M_1)\widetilde \otimes_\pi \CO_{2}(M_2)=\CO_{1}(M_1)\widehat \otimes_\pi \CO_{2}(M_2)\]

\[ \widehat \CO_{3,(a_1,a_2)}=\widehat \CO_{1,a_1}\widetilde \otimes_\pi \widehat \CO_{2,a_2}=\widehat \CO_{1,a_1}\widehat \otimes_\pi \widehat \CO_{2,a_2}
\]

of topological $\C$-algebras, and an identification
M_3=M_1 ×M_2
of smooth manifolds. Here $\CO_i$ is the structure sheaf of $M_i$ ($i=1,2,3$), and $(a_1,a_2)\in M_3=M_1\times M_2$.

§.§ Formal distributions  and formal generalized  functions

Smooth representations of Lie groups are often
realized as various function spaces.
For example,  the maximal globalization of a Harish-Chandra module for a real reductive group $G$
can be realized by using the space $\RC^{\infty}(G)$ or $\RC^{-\infty}(G)$,
and the minimal globalization can be realized by using the space $\RD^{\infty}_c(G)$ or $\RD^{-\infty}_c(G)$ (see [14, 24]). Here $\RC^{-\infty}(G)$ is the  space of complex-valued generalized functions on $G$, while
$\RD^{\infty}_c(G)$ and $\RD^{-\infty}_c(G)$ are respectively the spaces of compactly supported smooth densities and
compactly supported distributions on $G$.
On the other hand, in the  smooth (co)homology theory of Lie groups,  the standard (projective or injective) resolutions for a smooth representation $V$
can be constructed by using the spaces of suitable $V$-valued smooth functions, distributions or generalized functions (see [11, 7, 14]).
Thus, to establish the  smooth (co)homology theory for general Lie pairs (or equivalently, formal Lie groups), it is desirable
to generalize Schwartz's (vector-valued) distribution theory  (see [26, 27, 28]) to the formal manifold setting.

For two LCS $E_1$ and $E_2$, let $\CL(E_1,E_2)$ denote the space of all continuous linear maps from $E_1$ to $E_2$. When $E_2=\C$, we also set $E_1':=\CL(E_1,E_2)$.
Unless otherwise mentioned,  $\CL(E_1,E_2)$ is equipped with the strong topology (namely, the topology of uniform convergence on bounded sets).

Let $(M,\CO)$ be a formal manifold,
$\CF$  a sheaf of $\CO$-modules, and
$E$ a quasi-complete  LCS.
In Sections <ref> and
<ref>, for every open subset $U$
of $M$, we introduce a subspace $\RD_c^{\infty}(U;\CF)$ of $\CF(U)'$, and equip it with a certain inductive limit topology (in the category of LCS). Set $\RC^{-\infty}(U;\CF;E):=\CL(\RD_c^{\infty}(U;\CF),E)$.
Then we prove that the assignments

\[\RD_c^{\infty}(\CF): U\mapsto \RD_c^{\infty}(U;\CF)\quad \text{and}\quad
\RC^{-\infty}(\CF;E):U\mapsto \RC^{-\infty}(U;\CF;E)\]

respectively form a cosheaf and a sheaf of $\CO$-modules on $M$. As usual, by a cosheaf    of
$\CO$-modules on $M$, we mean a cosheaf $\mathcal{G}$ (see <cit.>) on $M$ together with  an $\CO(U)$-module structure on $\mathcal{G}(U)$  for every open
subset $U$ of $M$, with the following property: for all open subsets $V\subset U$ of $M$,
the extension map $\mathrm{ext}_{U,V}:\mathcal G(V)\rightarrow \mathcal G(U)$ is an $\CO(U)$-module homomorphism. Here the $\CO(U)$-module structure on $\CG(V)$ is
obtained from its $\CO(V)$-module structure through the homomorphism $\CO(U)\rightarrow \CO(V)$.

On the other hand, let $\CF_c(U)$ be the space of compactly supported  sections
of  $\CF(U)$, equipped with the usual inductive limit topology.  In Sections <ref> and <ref>,
we prove  that the assignments

\[\RD^{-\infty}(\CF;E): U\mapsto \RD^{-\infty}(U;\CF;E)\quad\text{and}\quad
\RD^{-\infty}_c(\CF;E): U\mapsto \RD^{-\infty}_c(U;\CF;E)
\]
respectively form  a sheaf and a cosheaf of  $\CO$-modules on $M$, where

\[\RD^{-\infty}(U;\CF;E):=\CL(\CF_c(U),E)\]
and $\RD^{-\infty}_c(U;\CF;E)$ is the subspace of  $\RD^{-\infty}(U;\CF;E)$ consisting of the compactly
supported sections.
Write $\RC^{-\infty}(\CF)=\RC^{-\infty}(\CF;\C)$ and  $\RC^{-\infty}(U;\CF)=\RC^{-\infty}(U;\CF;\C)$.
Similarly, we use the notations $\RD^{-\infty}(\CF), \RD^{-\infty}(U;\CF)$, $\RD_c^{-\infty}(\CF)$, and $\RD^{-\infty}_c(U;\CF)$.

Locally, when $M=(\R^n)^{(k)}$ with $n,k\in \BN$,  we have the LCS identifications

\begin{eqnarray*}
\RD_c^{\infty}(M;\CO)&=&\RD_c^\infty(\R^n)\widetilde\otimes_{\mathrm{i}}\C[y_1^*,y_2^*,\dots,y_k^*],\\
\RC^{-\infty}(M;\CO)&=&\RC^{-\infty}(\R^n)\widetilde\otimes_\pi \C[[y_1,y_2,\dots,y_k]],\\
%\CO_c(M)&=& \RC_c^\infty(N)\widehat\otimes_{\mathrm{i}}\C[[y_1,y_2,\dots,y_k]],\\
\RD^{-\infty}(M;\CO)&=& \RD^{-\infty}(\R^n)\widetilde\otimes_\pi \C[y_1^*,y_2^*,\dots,y_k^*],\\
\RD^{-\infty}_c(M;\CO)&=& \RD^{-\infty}_c(\R^n)\widetilde\otimes_{\mathrm{i}} \C[y_1^*,y_2^*,\dots,y_k^*]
\end{eqnarray*}

of LCS.
In view of these identifications, we refer to  an element in $\RD_c^\infty(M;\CO)$
(resp. $\RC^{-\infty}(M;\CO)$; $\RD^{-\infty}(M;\CO)$; $\RD^{-\infty}_c(M;\CO)$) as a compactly supported formal density (resp. a formal generalized function;
a formal distribution; a compactly supported formal distribution) on $M$.

More generally,  if $\CF$ is locally free of finite rank (namely, every point of $M$ has an open neighborhood $U$ such that $\CF|_U$ is free of finite rank), then we have the  following LCS identifications:

* $\RD_c^{-\infty}(M;\CF)=\CF(M)'$ ( <cit.>);

* $\RC^{-\infty}(M;\CF;E)=\RC^{-\infty}(M;\CF)\widetilde\otimes_\pi E$, and
$\RC^{-\infty}(M;\CF;E)=\RC^{-\infty}(M;\CF)\widehat\otimes_\pi E$ provided that $E$ is complete
( <cit.>);

* $\RD^{-\infty}(M;\CF;E)=\RD^{-\infty}(M;\CF)\widetilde\otimes_\pi E$, and
$\RD^{-\infty}(M;\CF;E)=\RD^{-\infty}(M;\CF)\widehat\otimes_\pi E$ provided that $E$ is complete
( <cit.>);

* $\RD^{-\infty}_c(M;\CF;E)=\RD^{-\infty}_c(M;\CF)\widetilde\otimes_\mathrm{i} E=\RD^{-\infty}_c(M;\CF)\widehat\otimes_\mathrm{i} E$ provided that $E$ is a barreled DF space ( <cit.>).

See Propositions <ref>, <ref>, <ref>,  and <ref> for details.

As a stone step towards the smooth
relative Lie algebra (co)homology theory, we  need to
construct standard resolutions for formal Lie groups
with coefficients in formal functions, formal generalized functions, compactly supported formal densities,
and compactly supported formal distributions.
To  achieve this goal, an important step is to define the de Rham complexes for formal manifolds with coefficients in these spaces and prove the corresponding Poincaré's lemma,
which we explain in the next subsection.

§.§ Poincaré's lemma

Let $(M,\CO)$ be a formal manifold. In Section <ref>, we  define the de Rham complex

Ω_^∙:  ⋯→0→0→Ω_^0→Ω_^1→Ω_^2→⋯for  $(M, \CO)$ with coefficients in formal functions, which is a  complex of sheaves of $\CO$-modules.
By taking the transpose of $\Omega_\CO^\bullet$, we obtain a complex

D^-∞_c(Ω_^-∙):  ⋯→D^-∞_c(Ω_^2)→D^-∞_c(Ω_^1)→D^-∞_c(Ω_^0)→0→⋯of cosheaves of $\CO$-modules.
We call $\mathrm{D}^{-\infty}_c(\Omega_\CO^{-\bullet})$ the de Rham complex
for $(M,\CO)$ with coefficients in compactly supported formal distributions.

As a subcomplex of $\mathrm{D}^{-\infty}_c(\Omega_\CO^{-\bullet})$, there is also a complex

D^∞_c(Ω_^-∙):  ⋯→D^∞_c(Ω_^2)→D^∞_c(Ω_^1)→D^∞_c(Ω_^0)→0→⋯of cosheaves of $\CO$-modules.
Similarly, by considering the  transpose of $\mathrm{D}^{\infty}_c(\Omega_\CO^{-\bullet})$, we have a complex

C^-∞(Ω_^∙):  ⋯→0→0→C^-∞(Ω_^0)→C^-∞(Ω_^1)→C^-∞(Ω_^2)→⋯of sheaves of $\CO$-modules.
We call $\mathrm{D}^{\infty}_c(\Omega_\CO^{-\bullet})$ and $\mathrm{C}^{-\infty}(\Omega_\CO^\bullet)$ the de Rham complexes for
$(M,\CO)$ with coefficients in compactly supported formal densities and formal generalized functions, respectively.

By taking the global sections in (<ref>)-(<ref>), these de Rham complexes
produce four topological cochain complexes
Ω^∙_(M),  D^-∞_c(M;Ω_^-∙),  D^∞_c(M;Ω_^-∙)  and  C^-∞(M;Ω_^∙)of reflexive complete LCS.
We prove in Section <ref> the following theorem, which is a generalization of
the usual Schwartz kernel theorems for smooth manifolds (see [26] or [8]).

Let $(M_1,\CO_1)$ and $(M_2,\CO_2)$ be two
formal manifolds and let
be the product of them. Then we have the following topological cochain complex identifications:

\begin{eqnarray*}
\Omega^\bullet_{\CO_3}(M_3)&=&\Omega^\bullet_{\CO_1}(M_1)\widetilde\otimes_{\pi} \Omega^\bullet_{\CO_2}(M_2)\\
&=&\Omega^\bullet_{\CO_1}(M_1)\widehat\otimes_{\pi} \Omega^\bullet_{\CO_2}(M_2),\\
\mathrm{D}^{-\infty}_c(M_3;\Omega_{\CO_3}^{-\bullet})&=&\mathrm{D}^{-\infty}_c(M_1;\Omega_{\CO_1}^{-\bullet})\wt\otimes_{\mathrm
&=& \mathrm{D}^{-\infty}_c(M_1;\Omega_{\CO_1}^{-\bullet})\widehat\otimes_{\mathrm{i}}  \mathrm{D}^{-\infty}_c(M_2;\Omega_{\CO_2}^{-\bullet}),\\
\mathrm{D}^{\infty}_c(M_3;\Omega_{\CO_3}^{-\bullet})&=&\mathrm{D}^{\infty}_c(M_1;\Omega_{\CO_1}^{-\bullet})
\widetilde\otimes_{\mathrm{i}} \mathrm{D}^{\infty}_c(M_2;\Omega_{\CO_2}^{-\bullet})\\
&=& \mathrm{D}^{\infty}_c(M_1;\Omega_{\CO_1}^{-\bullet})\widehat\otimes_{\mathrm{i}}  \mathrm{D}^{\infty}_c(M_2;\Omega_{\CO_2}^{-\bullet}),\\
\mathrm{C}^{-\infty}(M_3;\Omega_{\CO_3}^\bullet)&=&\mathrm{C}^{-\infty}(M_1;\Omega_{\CO_1}^\bullet)
\widetilde\otimes_\pi \mathrm{C}^{-\infty}(M_2;\Omega_{\CO_2}^\bullet)\\
&=& \mathrm{C}^{-\infty}(M_1;\Omega_{\CO_1}^\bullet)\widehat\otimes_\pi  \mathrm{C}^{-\infty}(M_2;\Omega_{\CO_2}^\bullet).
\end{eqnarray*}

Let $\C_M$ denote the sheaf of locally constant $\BC$-valued functions on $M$.
As slight modifications of those complexes in (<ref>), we have topological  cochain complexes

\begin{eqnarray}\label{extenddc1}
&&\cdots\rightarrow 0\rightarrow \BC_M(M)\rightarrow \Omega_\CO^0(M)\rightarrow \Omega_\CO^1(M)\rightarrow \cdots,\\
\label{extenddc2}&& \cdots \rightarrow \mathrm{D}^{-\infty}_c(M;\Omega_\CO^{1})\rightarrow \mathrm{D}^{-\infty}_c(M;\Omega_\CO^{0})\rightarrow
(\C_M(M))'\rightarrow 0\rightarrow \cdots,\\
\label{extenddc3}&& \cdots \rightarrow \mathrm{D}^{\infty}_c(M;\Omega_\CO^1)\rightarrow \mathrm{D}^{\infty}_c(M;\Omega_\CO^{0})\rightarrow
(\C_M(M))'\rightarrow 0\rightarrow \cdots,\\
\label{extenddc4}&& \cdots\rightarrow 0\rightarrow \BC_M(M)\rightarrow \mathrm{C}^{-\infty}(M;\Omega_{\CO}^0)\rightarrow  \mathrm{C}^{-\infty}(M;\Omega^1_{\CO})\rightarrow  \cdots
\end{eqnarray}

of reflexive complete   LCS.

Recall that a continuous linear map $\alpha: E_1\rightarrow E_2$ of complex topological vector spaces is said to be strong if there is a continuous linear map $\beta: E_2\rightarrow E_1$ such that $\alpha\circ\beta\circ \alpha=\alpha$.
Using Theorem <ref>, we prove in Section <ref> the following theorems, which generalize Poincaré's lemma for smooth manifolds.

Suppose that $M=N^{(k)}$ for some contractible smooth manifold $N$ and some $k\in \BN$. Then the complexes (<ref>)
and (<ref>) are strongly exact, namely, they are exact and all the arrows are strong continuous linear maps.

Suppose that $M=(\R^n)^{(k)}$ for some $n,k\in \BN$. Then the complexes (<ref>) and (<ref>) are strongly exact.

§ PRELIMINARIES ON FORMAL MANIFOLDS

In this section, we introduce some basic notions and establish some basic properties for formal manifolds.

§.§ Notations and conventions
Here we list some notations and conventions which will be used later.

In the rest of this paper, we let $(M,\CO)$ denote a formal manifold.
We say that the formal manifold $(M,\CO)$ is secondly countable if so is its underlying topological space.
We denote by $\pi_0(M)$ the set of all connected components in $M$.

We say that an open subset $U$ of $M$ is a chart if  there exist $n,k\in \BN$ and an open
submanifold $N$ of $\R^n$ such that $(U,\CO|_U)\cong (N,\CO_N^{(k)})$ as $\C$-locally ringed spaces.
An open cover of $M$ consisting of charts will be called an atlas of $M$.

Let $a\in M$.
Recall that $\dim_a M$ and $\deg_a M$ denote the dimension and degree of $M$ at $a$,  respectively.
For every sheaf  $\CF$ of $\CO$-modules, we let $\CF_a$ denote the stalk of $\CF$ at $a$.
We let $\m_a$ denote the maximal ideal of the stalk $\CO_a$, and define the Dirac
distribution supported at $a$ to be the
linear functional

δ_a: 𝒪_a⟶𝒪_a/_a=.

As in the Introduction, for every open subset $U$ of $M$,
we call an element of $\CO(U)$ a formal function on $U$.
For a formal function $f$ on $U$ and a point $a$ in $U$,
we define the value  $f(a)\in \BC$ of $f$ at $a$ to be
the image of $f$ under the following composition of natural maps:

\[\mathcal{O}(U)\longrightarrow \mathcal{O}_a\stackrel{\delta_a}{\longrightarrow} \C.\]

We also define the reduction

of $f$ to be the image of $f$ under the reduction map
$\CO(U)\longrightarrow \underline{\CO}(U)$ (see (<ref>)).
It is clear that $f(a)=\underline{f}(a)$ for all $a\in U$.

If $M=N^{(k)}$ for some smooth manifold $N$ and $k\in \BN$, then the reduction of

\[
f=\sum_{(j_1,j_2,\dots,j_k)\in \BN^k}f_{(j_1,j_2,\dots,j_k)}\, y_1^{j_1}y_2^{j_2}\cdots y_k^{j_k}\in \RC^\infty(U)[[y_1,y_2,\dots,y_k]]
\]

is $f_{(0,0,\dots,0)}$, and the value of $f$ at $a$ is $f_{(0,0,\dots,0)}(a)$.

Suppose now that $U$ is an open subset of $\R^n$.
We denote the standard coordinate functions on $U$ as $x_1, x_2, \dots, x_n$, and the first-order partial derivatives with respect to these variables as

\[\partial_{x_1},\partial_{x_2},\dots,\partial_{x_n}.\]

For every $n$-tuple $I=(i_1,i_2,\dots,i_n)\in \BN^n$, we use  the following usual multi-index notations:

I!=i_1!i_2! ⋯i_n!,      |I|=i_1+i_2+⋯+i_n,

x^I=x_1^i_1x_2^i_2⋯x_n^i_n,       ∂_x^I=∂_x_1^i_1∂_x_2^i_2⋯∂_x_n^i_n.

We also view the $|I|$-th order partial derivative $\partial_x^I$ as an operator on the formal power series algebra $\RC^\infty(U)[[y_1,y_2,\dots,y_k]]$ in
an obvious way.

\[\partial_{y_1},\partial_{y_2},\dots,\partial_{y_k}\]
denote the first-order  partial  derivatives on  $\RC^\infty(U)[[y_1,y_2,\dots,y_k]]$
with respect to the formal variables $y_1,y_2,\dots,y_k$.
For every $k$-tuple $J\in \BN^k$, the factorial $J!$, the length $|J|$, the monomial $y^J$, and the $|J|$-th order partial  derivative $\partial_y^J$, are defined as in (<ref>).

§.§ Partition of unity

In this subsection, we prove that partitions of unity exist for formal manifolds.

Let $f$ be a formal function on $M$. Then the following conditions are
equivalent to each other:

* $f$ is invertible;

* the reduction $\underline{f}$ of $f$ is invertible;

* the value of $f$ at $a$ is nonzero for every $a\in M$.

The assertion follows from  Example <ref> and the sheaf property of $\CO$ and $\underline {\CO}$.

Let $\mathcal{U}=\{U_\gamma\}_{\gamma\in \Gamma}$ be an open cover
of $M$. A family $\{f_\gamma\in \CO(M)\}_{\gamma\in \Gamma}$  of formal functions is said to be a
partition of unity on $M$  subordinate to $\mathcal{U}$ if the following  conditions hold:

* $\mathrm{supp}\,f_\gamma$ is contained in $U_\gamma$ for all $\gamma\in \Gamma$;

* the family $\{\mathrm{supp}\,f_\gamma\}_{\gamma\in \Gamma}$ is locally finite; and

* $\sum_{\gamma\in \Gamma } f_{\gamma}=1$, that is, for every relatively compact open subset $U$ of $M$,

\[
\sum_{\gamma\in \Gamma; (\mathrm{supp}\,f_\gamma)\cap U\neq \emptyset } (f_{\gamma})|_U=1.
\]

Here and henceforth, “$\mathrm{supp}$" indicates the support of a section of a sheaf.

When no confusion is possible,
we write $\overline U$ for the closure of a subset $U$ in a topological space.
Similar to the smooth manifold case, we have the following result.

For every open cover
of $M$, there is a  partition of unity on $M$ subordinate to it.

The proof is similar to that of the smooth manifold case (see <cit.> for example). We sketch a proof for
Let $\mathcal{U}=\{U_\gamma\}_{\gamma\in \Gamma}$ be an open cover
of $M$. Replacing $\mathcal{U}$ by a   refinement of it if necessary, we assume without loss of generality  that $\mathcal{U}$ is locally finite and
$U_\gamma$ is relatively compact for all $\gamma\in \Gamma$.

Take an open cover $\{V_\gamma\}_{\gamma\in \Gamma}$ of $M$ such that the closure  $ \overline {V_{\gamma}}$  of $V_\gamma$ is contained in $U_\gamma$ for all $\gamma\in \Gamma$.
Then  for each $\gamma\in \Gamma$, there is a formal function $f'_\gamma\in \CO(M)$ such that

* the support of $f'_\gamma$ is contained in $U_\gamma$; and

* $f'_\gamma(a)$ is a non-negative real number for all $a\in M$, and is a positive real number for all $a$ in the compact set $\overline {V_\gamma}$.

It is obvious that
\[f_\Gamma:=\sum_{\gamma\in \Gamma} f'_{\gamma}\]
is a well-defined formal function on $M$ such that
$f_\Gamma(a)>0$ for all $a\in M$.
Lemma   <ref> implies that the formal function $f_{\Gamma}$ is invertible.
The lemma then follows as  $\{f_\gamma\}_{\gamma\in \Gamma}$ is a partition of unity on $M$ subordinate to $\mathcal{U}$, where $f_\gamma:=f_\gamma'\cdot f_\Gamma^{-1}$.

For every sheaf $\CF$ of abelian groups on a topological space $X$, write ${\CF}|_S$ for its pull-back through the inclusion map $S\rightarrow X$, where $S$ is a subset of $X$. For every section $f\in \CF(X)$, write
\[f|_S\in  {\CF}|_S(S)\]
for the image of $f$ under the natural map $\CF(X)\rightarrow {\CF}|_S(S)$.
We will use the following result frequently without further explanation.

Let $V$, $U$ be two open subsets of $M$ such that $\overline{V}\subset U$. Then there are   formal functions $f,g\in \CO(M)$ such that

\begin{eqnarray*}f|_{\overline{V}}&=1,\quad\text{and}\quad f|_{M\setminus U}&=0 ,\\
g|_{\overline{V}}&=0,\quad\text{and}\quad g|_{M\setminus U}&=1.\end{eqnarray*}

The assertion follows by taking $\{f,g\}$ to be a partition of unity on $M$ subordinate to the open cover $\{U,M\setminus \overline{V}\}$.

§.§ Formal stalks

Let $a\in M$.
Recall from the Introduction that the formal stalk of $\CO$ at $a$ is

\[\wh{\CO}_a:=\varprojlim_{r\in \BN} \CO_a/\m_a^r.\]

For a formal function $f$ defined on an open neighborhood of $a$,
write $f_a$ for the germ of $f$ in $\CO_a$.
Assume that $M=(\R^n)^{(k)}$ for some $n,k\in \BN$. Then
for every $a\in M$ and $r\in \BN$, the set

{((x-a)^Iy^J)_a+_a^r|I∈^n, J∈^k with |I|+|J|<r}
forms a basis of $\CO_a/\m_a^r$, where for $I=(i_1,i_2,\dots,i_n)$ and $J=(j_1,j_2,\dots,j_k)$,

\[
(x-a)^Iy^J:=(x_1-x_1(a))^{i_1}(x_2-x_2(a))^{i_2}\cdots(x_n-x_n(a))^{i_n}y_1^{j_1}y_2^{j_2}\cdots y_k^{j_k}.
\]

Let $U$ be an open neighborhood of $a$ in $M$, and let

\[f=\sum_{J\in \BN^k} f_J y^J\in \RC^\infty(U)[[y_1,y_2,\dots,y_k]].\]

For every $J\in \BN^k$ with $|J|<r$, write

\[f_J=\sum_{I\in \BN^n; |I|< r-|J|}b_{I,J}\cdot (x-a)^I+ \sum_{I\in \BN^n; |I|=r-|J|}g_{I,J}\cdot (x-a)^I\]

for the $(r-|J|-1)$-th order Taylor expansion of $f_J$ around the point $a$, where  $b_{I,J}\in \C$ and $g_{I,J}\in \RC^\infty(U)$.
It is straightforward to check that

\[f_a=\sum_{I\in \BN^n, J\in \BN^k; |I|+|J|< r} b_{I,J} \cdot ((x-a)^Iy^J)_a \mod\ \m_a^r.\]

This implies that the set (<ref>) spans $\CO_a/\m_a^r$.
On the other hand,    by applying the

\[\partial_x^I\partial_y^J\quad (I\in \BN^n, J\in \BN^k\ \text{with}\ |I|+|J|<r)\]
to the elements in (<ref>), we see that these elements are  linearly   independent.
This completes the proof.

For every $a\in M$ and $r\in \BN$, Lemma <ref> implies that the quotient space $\CO_a/\m_a^r$ is  finite-dimensional. We equip the space $\CO_a/\m_a^r$ with the Euclidean topology, which is the unique topology that makes it a Hausdorff LCS.
Now, we endow the formal stalk
\[\wh{\CO}_a=\varprojlim_{r\in \BN} \CO_a/\m_a^r\]

with the projective limit topology. Then it becomes a topological
On the other hand, we view $\C[[x_1,x_2,\dots,x_n,y_1,y_2,\dots,y_k]]$ ($n,k\in \BN$) as a topological
$\C$-algebra with the usual term-wise convergence topology.

For every $a\in M$, we have that

_a ≅[[x_1,x_2,…,x_n,y_1,y_2,…,y_k]]
as topological $\C$-algebras, where $n:=\dim_a M$ and $k:=\deg_a M$. Furthermore, the natural map

is a $\BC$-algebra isomorphism.

Without loss of generality, we assume that $M=(\R^n)^{(k)}$ and  $a=0\in M$. Taylor expansion around the point $a$ yields  the following $\C$-algebra homomorphism

\begin{equation}\begin{split}\label{eq:Taylorexpansion}
\CO_a&\rightarrow \C[[{\mathbf{x},\mathbf{y}}]]:=\C[[x_1,x_2,\dots,x_n,y_1,y_2,\dots,y_k]],\\
f_a&\mapsto \sum_{J\in \BN^k}\left(\sum_{I\in \BN^n}\frac{1}{I!} \partial_x^{I}(f_{J})(a) \cdot x^I\right)y^J
\end{split}\end{equation}

where $f=\sum_{J\in \BN^k} f_J y^J$ is a formal function on an open neighborhood of $a$
\[\sum_{I\in \BN^n}\frac{1}{I!} \partial_x^{I}(f_{J})(a)\cdot x^I\]
is the Taylor series of $f_J$ at $a$.
Note that Borel's lemma implies that the map (<ref>) is surjective.

Write $\m$ for the maximal ideal of $ \C[[{\mathbf{x},\mathbf{y}}]]$. By  Lemma <ref>, we know that  the  algebra homomorphism

\[
\CO_a/\m_a^r \longrightarrow \C[[{\mathbf{x},\mathbf{y}}]]/\m^r\quad (r\in \BN)
\]

induced by (<ref>) is an isomorphism.
This produces a topological algebra isomorphism

_a=_r∈_a/_a^r ⟶[[𝐱,𝐲]]
= _r∈[[𝐱,𝐲]]/^r,
which proves the first assertion in this proposition.
For the second one, one only needs to note that
the surjective map (<ref>) is the composition of the maps

\[\CO_a\longrightarrow \wh\CO_a\xrightarrow{\eqref{eq:formalstalkisoring}} \C[[{\mathbf{x},\mathbf{y}}]].\]

We also record the following straightforward result as a lemma for later use.

The canonical map

(M)→∏_a∈M _a
is injective.

Let $\varphi=(\overline{\varphi}, \varphi^*): (M,\CO)\rightarrow (M', \CO')$ be a morphism of formal manifolds.
For every  $a\in M$,  we let

\[\varphi^*_a:\ \CO'_{\overline{\varphi}(a)}\rightarrow \CO_a\]
denote the induced local homomorphism of the stalks.
Then there is  a unique local homomorphism

φ^*_a: '_φ(a)→_a
between the formal stalks such that the diagram

'_φ(a) @>φ^*_a>>
@VVV @VVV

'_φ(a) @>φ^*_a>>

commutes. Furthermore,
we have the following result.

Under the projective limit topologies, the map (<ref>) is continuous.

This follows from the fact that every linear map between finite-dimensional Hausdorff LCS is automatically continuous.

\[
\varphi=(\overline\varphi, \varphi^*),\, \psi=(\overline\psi, \psi^*):\ (M,\CO)\rightarrow (M', \CO')
\]

be two morphisms of formal manifolds. If $\overline\varphi=\overline\psi$, and for all $a\in M$,
the maps

\[
\varphi^*_a,\, \psi^*_a:\ \widehat{\CO'}_b\rightarrow \widehat \CO_a\qquad (b:=\overline\varphi(a)=\overline\psi(a))
\]

are equal, then $\varphi=\psi$.

This follows from Lemma <ref>.

For every sheaf $\CF$ of $\CO$-modules  and $a\in M$, we define the formal stalk of $\CF$ at $a$ by

\[\widehat{\CF}_a:=\varprojlim_{r\in \BN} \CF_a/\m_a^r\CF_a.\]

Suppose that $N$ is a smooth manifold and $k,l\in \BN$. Then there is a homomorphism $\CO_N^{(k)}\rightarrow \CO_N^{(l)}$ of sheaves of algebras given by

\[
\begin{array}{rcl}
\CO_{N}^{(k)}(U)&\rightarrow &\CO_{N}^{(l)}(U), \smallskip \\
\sum\limits_{J\in \BN^k} f_J y^J&\mapsto&\left\{ \begin{array}{ll}
\sum\limits_{J\in \BN^k=\BN^k\times\{0\}^{l-k}\subset \BN^l}f_J y^{J},&\textrm{if $k\leq l$;} \smallskip \\
\sum\limits_{J\in \BN^l=\BN^l\times\{0\}^{k-l}\subset \BN^k}f_Jy^{J},&\textrm{if $k>l$},
\end{array}
\right.
\end{array}
\]

where $U$ is an open subset of $N$ and $f_J\in \RC^\infty(U)$. By using this homomorphism, every sheaf of
$\CO_N^{(l)}$-modules is also a sheaf of  $\CO_N^{(k)}$-modules.
Suppose that $\CF= \CO_{N}^{(l)}$, to be viewed as a sheaf of  $\CO_{N}^{(k)}$-modules as above. Then,
similar to (<ref>), for every $a\in N$, we have that

_a≅[[x_1, x_2, …, x_n, y_1, y_2, …, y_l]],  where   n:=_a N.

§.§ Softness

We discuss here the softness of structure sheaves of formal manifolds. Recall that a sheaf $\CF$  of abelian groups on a topological space $X$ is said to be soft if
for every closed subset $Z$ of $X$, the canonical map $\CF(X)\rightarrow (\CF|_Z)(Z)$ is surjective.

The sheaf  $\CO$  is soft.

By <cit.>, it suffices to show that every $a\in M$ admits
an open neighborhood $U$ such that the sheaf $\CO|_U$ is soft.
Thus it is enough to show that the sheaf $\CO_{\R^n}^{(k)}$ ($n,k\in \BN$) is soft.
We know that the  sheaf $\CO_{\R^n}^{(0)}$ of  smooth functions on $\R^n$ is soft (see <cit.>).
Recall from Example <ref> that $\CO_{\R^n}^{(k)}$ is a sheaf of  $\CO_{\R^n}^{(0)}$-modules.
Thus <cit.> implies that the sheaf  $\CO_{\R^n}^{(k)}$ is soft,
as required.

For every $a\in M$, the canonical maps

\[\CO(M)\rightarrow \CO_a\quad \text{and} \quad \CO(M)\rightarrow \wh{\CO}_a\]
are both surjective.

This  follows from Propositions <ref> and <ref>.

All sheaves of $\CO$-modules are soft.

This follows from Proposition <ref> and  <cit.>.

Recall the reduction $\underline \CO$ of $\CO$ from (<ref>).

The canonical map

is surjective.

Consider the exact sequence

\[
0\rightarrow \m_\CO\rightarrow \CO\rightarrow \underline \CO\rightarrow 0.
\]

By Corollary <ref>, the sheaf $\m_\CO$ is soft. Then the proposition follows from <cit.>.

§ DIFFERENTIAL OPERATORS ON FORMAL MANIFOLDS

In this section, we study differential operators between two sheaves of $\CO$-modules.

§.§ Differential operators on modules

We first review the notion of differential operators on modules of a commutative unital $\BC$-algebra.

Let $A$ be a commutative unital $\BC$-algebra, and let $F_1$, $F_2$ be two $A$-modules.
For  $D\in \Hom_{\BC}(F_1,F_2)$ and  $a\in A$, define an element $[D,a]\in \Hom_{\BC}(F_1,F_2)$ by

\[
[D,a](u)=D(au)-aD(u)\quad \textrm{ for all }  u\in F_1.
\]

Let $r\in \BN$  throughout this section.

A map $D\in  \Hom_{\BC}(F_1,F_2)$ is called a  differential
operator of order $\leq r$ if

\[
[\cdots[[D,a_0],a_1],\cdots, a_r] =0\ \  \textrm{  for all $a_0,a_1, \dots,a_r\in A$}.
\]

Write $\mathrm{Diff}_r(F_1,F_2)$ for the space of all differential operators of order $\leq r$ in  $\Hom_{\BC}(F_1,F_2)$.
Note that $\mathrm{Diff}_0(F_1,F_2)=\Hom_A(F_1,F_2)$, and

\[
\mathrm{Diff}_{r_1}(F_2,F_3)\circ \mathrm{Diff}_{r_2}(F_1,F_2)\subset \mathrm{Diff}_{r_1+r_2}(F_1,F_3)\quad \textrm{for all }r_1, r_2\in \BN,
\]

where $F_3$ is another $A$-module.

An element $D\in \Hom_{\BC}(A,F_2)$ is called a derivation  if

\[
D(a_1 a_2)=a_2 D(a_1)+a_1  D(a_2)\ \  \textrm{  for all $a_1,a_2\in A$}.\]

Write $\mathrm{Der}(A,F_2)$ for the space of all derivations in $\Hom_{\BC}(A,F_2)$. Obviously, $\mathrm{Der}(A,F_2)\subset \mathrm{Diff}_1(A,F_2)$.
We identify   $\mathrm{Diff}_0(A,F_2)=\Hom_{A}(A,F_2)$ with $F_2$  via the isomorphism

\[
\Hom_{A}(A,F_2)\rightarrow F_2, \quad D\mapsto D(1).
\]

One checks that $D-D(1)$ is a derivation for every $D\in \mathrm{Diff}_1(A, F_2)$, which implies

For every  $D\in \mathrm{Diff}_r(F_1,F_2)$ and every
ideal $I$ of $A$, we have that

D(I^i+rF_1)⊂I^iF_2    for all i∈.

We will prove the lemma by induction on $i+r$. The lemma is obvious if $i+r=0$.
Now assume that $i+r\geq 1$ and the lemma holds when $i+r$ is smaller.
If $i=0$ or $r=0$, then (<ref>) clearly holds. So we assume that $i>0$ and $r>0$. Let $f_1, f_2, \dots, f_{i+r}\in I$.
From the fact $[D, f_1]\in \mathrm{Diff}_{r-1}(F_1,F_2)$, it follows that

\begin{eqnarray*}
D(f_1 f_2 \cdots f_{i+r}F_1)&\subset& D (f_1I^{i+r-1}F_1)\\
&\subset& [D,f_1](I^{i+r-1}F_1)+ f_1D(I^{i+r-1}F_1)\\
&\subset& I^iF_2+f_1 I^{i-1}F_2=I^iF_2.
\end{eqnarray*}

This proves the lemma.

Assume now that $A=\BC[[y_1, y_2, \dots, y_k]]$ for some $k\in \BN$.
For every $J\in \BN^k$ with $|J|\le r$,  we have that

\[F_2\circ \partial_y^J\subset  \mathrm{Diff}_r(A,F_2),\]

where the identification $F_2=\mathrm{Diff}_0(A,F_2)$ is used. Conversely, we have the following result (<cit.>).

Assume that $A=\BC[[y_1, y_2, \dots, y_k]]$ for some $k\in \BN$, and $F_2$ is  an $A$-module such that
$\cap_{i\in \BN}\m^i F_2=0$, where $\m$ denotes the maximal ideal in $A$.

\[
\mathrm{Diff}_r(A,F_2)=\bigoplus_{J\in \BN^k; \abs{J}\leq r} F_2\circ \partial_y^J.
\]

Denote by $\C[\mathbf{y}]_{\le r}\subset \C[y_1,y_2,\dots,y_k]$ the subspace of polynomials of degree $\le r$ in $A$. We claim that

\begin{equation}\label{psirinj}
\text{the restriction map}\ \Psi_r:\ \mathrm{Diff}_r(A,F_2)\rightarrow \Hom_\BC(\C[\mathbf{y}]_{\le r}, F_2)\ \text{is injective}.\end{equation}

Note that the lemma is implied by this claim, as

\[\Psi_r\left(\bigoplus_{J\in \BN^k; \abs{J}\leq r} F_2\circ \partial_y^J\right)=\mathrm{Hom}_\C(\C[\mathbf{y}]_{\le r},F_2).\]

We now prove the claim (<ref>) by induction on $r$.
The claim obviously holds when $r=0$, and so we assume that $r>0$.
Pick an element $D\in \mathrm{Diff}_r(A,F_2)$ such that $D(f)=0$ for all $f\in \C[\mathbf{y}]_{\le r}$.
Then for every $i=1,2,\dots,k$, we have  that

\[[D,y_i]\in \mathrm{Diff}_{r-1}(A,F_2)\quad\text{and}\quad [D,y_i](g)=0\ \text{for all}\ g\in \C[\mathbf{y}]_{\le r-1}.\]

These together with the induction hypothesis imply that $[D,y_i]=0$ on $A$ for all $i$, and then one checks that

\begin{equation}\label{Dvanishpoly}
D(h)=0\quad \text{for all}\ h\in \BC[y_1, y_2,\dots, y_k].
\end{equation}

Let $f=\sum_{J\in \BN^k}c_J y^J$ be an arbitrary formal power series in $A$.
By  (<ref>) and Lemma <ref>,  for every $j\in \BN$, we have that

\[D(f)=D(f)-D\left(\sum_{|J|< j+r}c_J y^J\right)=D\left(\sum_{|J|\ge j+r}c_J y^J\right)\in D(\m^{j+r})\subset \m^j F_2.\]

Thus, the condition  $\cap_{j\in \BN}\m^j F_2=0$ in the lemma forces   that $D(f)=0$.
This proves  (<ref>) and hence the lemma.

§.§ Differential operators on formal manifolds

Let $\CF_1$ and $\CF_2$ be two sheaves of $\mathcal{O}$-modules. In this subsection, we introduce the
notion of differential operators between $\CF_1$ and $\CF_2$.

Recall that $\C_M$ denotes the sheaf  of  locally constant $\BC$-valued functions on $M$.
$\Hom_{\BC_M}(\CF_1,\CF_2)$ for the space of all $\BC_M$-homomorphisms between $\CF_1$ and $\CF_2$.
Then the assignment

\[U\mapsto\Hom_{\BC_U}(\CF_1|_U,\CF_2|_U)\quad (\text{$U$ is an open subset of $M$})\]

forms a sheaf of $\BC$-vector spaces over $M$, to be denoted by  $\CH\textrm{om}_{\BC_M}(\CF_1,\CF_2)$.

Recall that an element $D$ of $\Hom_{\BC_M}(\CF_1,\CF_2)$ is defined to be a family

\[
\{
(D_U: \CF_1(U)\rightarrow \CF_2(U))\}_{U\textrm{ is an open subset of }M}
\]

of linear maps that commute with the restriction maps.

An element $D\in\Hom_{\BC_M}(\CF_1,\CF_2) $ is called  a differential operator of order $\leq r$ if

\[
D_U\in \mathrm{Diff}_r(\CF_1(U),\CF_2(U))
\]

for all open subsets $U$ of $M$, where $\CF_1(U)$ and $\CF_2(U)$ are viewed as $\CO(U)$-modules, and $\CO(U)$ is viewed as a $\C$-algebra.

Write $\mathrm{Diff}_r(\CF_1,\CF_2)\subset \Hom_{\BC_M}(\CF_1,\CF_2)$ for the space of differential operators of order $\leq r$.
Then we have that

\[
\mathrm{Diff}_0(\CF_1,\CF_2)=\mathrm{Hom}_{\CO}(\CF_1,\CF_2),
\]

\[
\mathrm{Diff}_{r_1}(\CF_2,\CF_3)\circ \mathrm{Diff}_{r_2}(\CF_1,\CF_2)\subset \mathrm{Diff}_{r_1+r_2}(\CF_1,\CF_2)\qquad \textrm{for all }\, r_1,r_2\in \BN,
\]

where $\CF_3$ is another sheaf of $\CO$-modules.

An element $D\in \Hom_{\BC_M}(\CF_1,\CF_2)$ is called a finite order differential operator if it belongs to $\mathrm{Diff}_r(\CF_1,\CF_2)$ for some $r\geq 0$.
It is called a differential operator if for every $a\in M$, there is an open neighborhood $U$ of $a$ in $M$ such that $D|_U\in \Hom_{\BC_U}(\CF_1|_U,\CF_2|_U)$ is a finite order differential operator.

Respectively write $\mathrm{Diff}_{\mathrm{fin}}(\CF_1,\CF_2)$ and  $\mathrm{Diff}(\CF_1,\CF_2)$ for the space of finite order differential operators and the space of differential operators in $\Hom_{\BC_M}(\CF_1,\CF_2)$.

An element  $D\in \Hom_{\BC_M}(\CO,\CF_2)$ is called a derivation if

\[
(D_U: \CO(U)\rightarrow \CF_2(U))\in \mathrm{Der}(\CO(U),\CF_2(U))
\]

for every open subset $U$ of $M$.

The space of all derivations in $\Hom_{\BC_M}(\CO,\CF_2)$ is denoted by $\mathrm{Der}(\CO,\CF_2)$.

Write $\mathcal D\mathrm{iff}(\CF_1,\CF_2)$ for the subsheaf of $\CH\textrm{om}_{\BC_M}(\CF_1,\CF_2)$ given by

\[U\mapsto \mathrm{Diff}(\CF_1|_U,\CF_2|_U)\quad (U\ \text{is an open subset of}\ M).
\]

We also define  the subpresheaf $\mathcal D\mathrm{iff}_{\mathrm{fin}}(\CF_1,\CF_2)$ of $\CH\textrm{om}_{\BC_M}(\CF_1,\CF_2)$,
and the subsheaf $\mathcal D\textrm{er}(\CO,\CF_2)$ of $\CH\textrm{om}_{\BC_M}(\CO,\CF_2)$ similarly.

For every  $f\in \CO(M)$ and $D\in \mathrm{Diff}(\CF_1,\CF_2)$, we define two differential operators $f\circ D$ and $D\circ f$ in $\mathrm{Diff}(\CF_1,\CF_2)$  by setting
(f∘D)_U: u↦f|_U(D_U(u))  and  (D∘f)_U: u↦D_U (f|_Uu ),
where $u\in \CF_1(U)$ and $U$ is an open subset of $M$.
Then we have two natural  $\CO(M)$-module structures on $\mathrm{Diff}(\CF_1,\CF_2)$  with

\begin{eqnarray}
\label{eq:leftactiononD}  &&\CO(M)\times  \mathrm{Diff}(\CF_1,\CF_2)\rightarrow  \mathrm{Diff}(\CF_1,\CF_2),\quad (f,D)\mapsto f\circ D,\\
\label{eq:rightactiononD} &&\CO(M)\times  \mathrm{Diff}(\CF_1,\CF_2)\rightarrow  \mathrm{Diff}(\CF_1,\CF_2),\quad (f,D)\mapsto D\circ f.
\end{eqnarray}

Each of the  two actions mentioned above makes
$\mathcal D\mathrm{iff}(\CF_1,\CF_2)$ a sheaf of $\CO$-modules.
Unless otherwise mentioned,  $\mathcal D\mathrm{iff}(\CF_1,\CF_2)$ is
viewed as a sheaf of $\CO$-modules with the action (<ref>).
Under this action, $\mathcal D\textrm{er}(\CO,\CF_2)$ is a sheaf of  $\CO$-modules as well (as a subsheaf of $\mathcal D\mathrm{iff}(\CO,\CF_2)$).

Let $\CF$ be a sheaf of $\CO$-modules.
For every open subset $U$ of $M$, write $\CF_c(U)$ for the space of compactly supported sections in $\CF(U)$.
Obviously, $\CF_c(U)$ is an $\CO(U)$-submodule of $\CF(U)$.
The softness of $\CF$ (see Corollary <ref>) implies that
the assignment
U↦_c(U)  ($U$ is an open subset of $M$),together with the extension by zero maps
ext_U,V: _c(V)→_c(U)  (V⊂U are open subsets of $M$),forms  a cosheaf of $\CO$-modules on $M$ (see <cit.>). We denote the resulting cosheaf by $\CF_c$.
When $\CF=\mathcal{D}\mathrm{iff}(\CF_1,\CF_2)$, we also write

𝒟iff_c(_1,_2):=_c  and  Diff_c(_1,_2):=_c(M).

Let $U$ be an open subset of $M$.
For every formal function $f\in \CO(M)$  supported in $U$ and  every $u\in \CF(U)$, we define

f u∈(M)
by requiring that

\[
(fu)|_U=f|_U\, u \quad \textrm{and}\quad (fu)|_{M\setminus \mathrm{supp}\,f}=0.
\]

We have a canonical  map
Diff_r(_1,_2)→Diff_r(_1(M),_2(M)),   D↦D_M.  The following result shows that a differential operator $D$ of finite order is determined by its action on global sections.
Using this, we will often not distinguish between a finite order differential operator $D$  and the map $D_M$.

The linear map (<ref>) is bijective for every $r\in \BN$. In particular, the canonical map

\[\mathrm{Hom}_{\CO}(\CF_1,\CF_2)\rightarrow \mathrm{Hom}_{\CO(M)}(\CF_1(M),\CF_2(M))\]

is bijective.

Let  $U$ be an open subset of $M$.
We choose a family $\{(U_a,U'_a,f^a)\}_{a\in U}$ of triples, where

* $U_a$, $U'_a$ are open  neighborhoods  of $a$ such that $\overline{U_a}\subset U'_a$ and $\overline{U'_a}\subset{U}$;

* $f^a\in \CO(M)$ is a formal function   such that
$f^a|_{\overline{U_a}}=1$ and $f^a|_{M\setminus U'_a}=0$.

We first prove the injectivity of (<ref>).
Let $D\in \textrm{Diff}_r(\CF_1,\CF_2)$ and  $u\in\CF_1(U)$.

Since $D$ commutes with the restriction maps in $\CF_1$ and $\CF_2$,
we have that

\[D_U(u)|_{U_a}=D_{U_a}(u|_{U_a})=D_{U_a}((f^au)|_{U_a})=D_M(f^au)|_{U_a}.\]

This implies that $D=0$ provided that $D_M=0$, as desired.

Now we turn to prove that the map (<ref>) is surjective.  Fix a differential operator
$P\in \textrm{Diff}_r(\CF_1(M),\CF_2(M))$.
We claim that

\begin{equation}\label{claimind}
\text{for every $u'\in\CF_1(M)$ satisfying $u'|_U=0$, one has  that $P(u')|_{U}=0$.}
\end{equation}

Indeed, let $g\in\CO(M)$ be a formal  function such that

\[g|_{\overline{U_a}}=0\quad\text{and}\quad g|_{M\setminus U'_a}=1.\]

Then we have that $gu'=u'$ in $\CF_1(M)$.
Recall that $[P,g]=0$ if  $r=0$, and $[P,g]\in \mathrm{Diff}_{r-1}(\CF_1,\CF_2)$ otherwise. Since
\[P(u')|_{U_a}=P(gu')|_{U_a}=gP(u')|_{U_a}+[P,g](u')|_{U_a}=[P,g](u')|_{U_a},\]

it follows that $P(u')|_{U_a}=0$ by induction on $r$.
This proves the claim (<ref>) as $\{U_a\}_{a\in U}$ forms an open cover of $U$.

Let $u\in \CF_1(U)$. Define

\begin{eqnarray}\label{defPu}P_{U_a}(u|_{U_a}):=P(f^au)|_{U_a}\in \CF_2(U_a).\end{eqnarray}

For  all  $a,b\in U$, we have that

\[(f^au)|_{U_a\cap U_b}=u|_{U_a\cap U_b}=(f^bu)|_{U_a\cap U_b}.\]

Thus, by applying
the claim (<ref>)  (replace  $U$ by  $U_a\cap U_b$) , we have that

P_U_a(u|_U_a)|_U_a∩U_b=P(f^au)|_U_a∩U_b=P(f^bu)|_U_a∩U_b=P_U_b(u|_U_b)|_U_a∩U_b.This yields a map

\[P_U:\CF_1(U)\rightarrow \CF_2(U),\quad u\mapsto P_U(u),\]

where $P_U(u)$ is the section in $\CF_2(U)$ obtained by gluing the family $\{P_{U_a}(u|_{U_a})\}_{a\in U}$ together.

We remark that the definition of $P_U$ is independent of the choice of the family $\{(U_a,U_a',f^a)\}_{a\in U}$.
Indeed, let $\{(\tilde{U}_a,\tilde{U}_a',\tilde{f}^a)\}_{a\in U}$ be another such family, and as in (<ref>) we define a map $\tilde{P}_U$ associated to this
family. Then by a similar argument as  in (<ref>), we have that

\[P_U(u)|_{U_a\cap \tilde{U}_a}=\tilde{P}_U(u)|_{U_a\cap \tilde{U}_a},\]
as desired.
Using this independence, one concludes that the family
\[D=\{P_U\}_{U \text{ is an open subset of } M}\]
forms a homomorphism between the sheaves $\CF_1$ and $\CF_2$.

Let $i\in \BN$. We now prove by induction on $i$ that

\begin{eqnarray}\label{eq:P_U=Pf^a}
&&[\cdots[[P_U,h_1],h_2],\cdots,h_i](u)|_{U_a}=[\cdots[[P, f^ah_1],f^ah_2],\cdots,f^ah_i](f^au)|_{U_a}
\end{eqnarray}

for all $h_1,h_2,\dots,h_i\in \CO(U)$ and $u\in \CF_1(U)$.
When $i=0$, (<ref>) follows from the definition of $P_U$. Assume that $i>0$ and (<ref>) holds when $i$ is smaller.
\[
P_U':= [\cdots[[P_U,h_1],h_2],\cdots,h_{i-1}]\ \text{and}\  P':= [\cdots[[P,f^ah_1],f^ah_2],\cdots,f^ah_{i-1}].
\]

Then  we have that

\begin{eqnarray*}
&=&([P', f^ah_i](f^au))|_{U_a},
\end{eqnarray*}

where we have used the induction hypothesis in the second equality. This finishes the proof of (<ref>).
Since $P\in \textrm{Diff}_r(\CF_1(M),\CF_2(M))$,
it follows from  the equality (<ref>) (with $i=r+1$) that  $P_U\in \textrm{Diff}_r(\CF_1(U),\CF_2(U))$.
Then  $D\in \textrm{Diff}_r(\CF_1,\CF_2)$
and hence the map (<ref>) is surjective as  $D_M=P$.

In conclusion, we have proved the first assertion of the proposition. The second assertion follows by taking $r=0$ in the first assertion.

By Proposition <ref>, we have
an identification $\mathrm{Diff}_0(\CO,\CF_2)=\CF_2(M)$. Similar to (<ref>), we obtain that

Let $\CF$ be a sheaf of $\CO$-modules and let  $D\in\mathrm{Diff}_r(\CO,\CF)$.
For every $a\in M$,  write

D_a: _a→_a
for the linear map on the stalks induced by $D$.
It is clear that $D_a\in \mathrm{Diff}_r( \CO_a,\CF_a)$.
Furthermore, Lemma <ref> implies that
$D_a$ induces a linear map

D_a: _a→_a.

We have that   $\wh{D}_a\in \mathrm{Diff}_r(\widehat \CO_a,\widehat{\CF}_a)$.

Note that

\[
([\cdots[[\widehat{D}_a,f_0],f_1],\cdots, f_r])(f_{r+1}) =0
\]

for all $f_0,f_1, \dots,f_r, f_{r+1}$ in the image of the map $\CO_a\rightarrow \widehat \CO_a$. The second assertion then follows since the map
$\CO_a\rightarrow \widehat \CO_a$ is surjective (see  Proposition

Let $n,k\in \BN$, and let $N$ be   an open submanifold of $\R^n$.
Let $\CF$ be a sheaf of $\CO_N^{(k)}$-modules, and let $\{f_{I,J}\}_{I\in \BN^n, J\in \BN^k}$ be a locally finite family of elements of $\CF(N)$.
Identifying $\mathrm{Diff}_0(\CO_N^{(k)},\CF)$ with $\CF(N)$,
we see that

∑_I∈^n, J∈^k f_I,J∘∂_x^I∂_y^J
is an element of $\mathrm{Diff}(\CO_N^{(k)},\CF)$.
Conversely, we have the following result.

Assume that $M=N^{(k)}$ and the sheaf $\CF$ of $\CO$-modules satisfies the following  conditions:

* the canonical map $\CF(M)\rightarrow  \prod_{a\in M} \widehat \CF_a $ is injective; and

* $ \cap_{i\in\BN}\widehat{\m}_a^i\widehat{\CF}_a=0$ for every $a\in M$, where
$\widehat{\m}_a$ is the maximal ideal of $\widehat{\CO}_a$.
Then every element of $\mathrm{Diff}(\CO,\CF)$ is uniquely of the form (<ref>).

Without loss of generality, we assume that $M\neq\emptyset$.
\[\BC[\mathbf{x,y}]:=\BC[x_1, x_2, \dots, x_n, y_1, y_2, \dots, y_k]\]
for simplicity.
We view $\BC[\mathbf{x,y}]$ as a subspace of $\CO(M)$, as well as a subspace of $\widehat \CO_a$ for each $a\in M$
(see (<ref>)).
Then the uniqueness assertion follows by applying the differential operator  (<ref>) to the monomials in $\BC[\mathbf{x,y}]$.

$\BC[\mathbf{x,y}]_{\le r}\subset \BC[\mathbf{x,y}]$  for the subspace consisting of polynomials of degree $\leq r$.
We claim that the map

\[
\begin{array}{rcl}
\Psi_r: \mathrm{Diff}_r(\CO,\CF)&\rightarrow& \Hom_\BC(\BC[\mathbf{x,y}]_{\le r}, \CF(M)),\\
D&\mapsto&(f\mapsto D_M(f))
\end{array}
\]

is injective.
Indeed, take a differential operator $D\in  \mathrm{Diff}_r(\CO,\CF)$  such that $D_M(f)=0$ for all $f\in \BC[\mathbf{x,y}]_{\le r}$. For every $a\in M$,
Lemma <ref> implies that the map
\widehat{D}_a:  \widehat \CO_a\rightarrow \widehat \CF_a
belongs to $\mathrm{Diff}_r( \widehat \CO_a,\widehat{\CF}_a)$ and vanishes on $\BC[\mathbf{x,y}]_{\le r}$.
It then follows from Lemma <ref> and the second condition in the proposition that $\widehat{D}_a$ is the zero map. By

the commutative diagram

\[\xymatrix{
\CO(M) \ar[d] \ar[r]^{D_M} & \CF(M) \ar[d] \\
\wh{\CO}_a \ar[r]^{\widehat{D}_a} & \wh{\CF}_a,}\]

we conclude  that for every $g\in \CO(M)$, the image of $D_M(g)$ in $\wh{\CF}_a$ is zero for all $a\in M$.
Then the first condition in the proposition forces that $D_M=0$, which proves the claim by using Proposition <ref>.

Write $\mathrm{Diff}'_r(\CO,\CF)\subset \mathrm{Diff}_r(\CO,\CF)$ for the space of all differential operators of the form (<ref>) with $f_{I,J}=0$ whenever $\abs{I}+\abs{J}> r$.
It is easy to see that the map ${\Psi_r}|_{\mathrm{Diff}'_r(\CO,\CF)}$ is surjective. Hence $\mathrm{Diff}'_r(\CO,\CF)= \mathrm{Diff}_r(\CO,\CF)$. Together with the uniqueness assertion, this implies that every differential operator in $\mathrm{Diff}(\CO,\CF)$ has the form  (<ref>).

For every $l\in \BN$, it follows from Example <ref> (see (<ref>)) that the sheaf $\CO_N^{(l)}$ of $\CO_N^{(k)}$-modules
satisfies the conditions in Proposition <ref>.
Then every element of $\mathrm{Diff}(\CO_{N}^{(k)},\CO_{N}^{(l)})$ is uniquely of the form

\[ \sum_{I\in \BN^n, J\in \BN^k} f_{I,J}\circ \partial_x^I\partial_y^J,\]

where $\{f_{I,J}\}_{I\in \BN^n, J\in\BN^k}$ is a locally finite family of elements of $\CO_{N}^{(l)}(N)$.

As a by-product of Proposition <ref>, we have the following result.

The sheaf $\mathrm{Der}(\CO_N^{(k)},\CO_N^{(k)})$ of  $\CO_N^{(k)}(N)$-modules is free of rank $n+k$, with a set of free generators
given by

\[
\{\partial_{x_1}, \partial_{x_2}, \dots, \partial_{x_n},\, \partial_{y_1}, \partial_{y_2}, \dots, \partial_{y_k}\}.
\]

With the notations as in the proof of Proposition <ref>, we have shown  that

\[
\mathrm{Diff}'_1(\CO_N^{(k)},\CO_N^{(k)})=\mathrm{Diff}_1(\CO_N^{(k)},\CO_N^{(k)}).
\]

The assertion then follows by using (<ref>) and the fact that

\[
\mathrm{Der}(\CO_N^{(k)},\CO_N^{(k)})=\{D\in \mathrm{Diff}_1(\CO_N^{(k)},\CO_N^{(k)})\mid D(1)=0\}.
\]

§ THE TOPOLOGY ON THE SPACE OF FORMAL FUNCTIONS

In this section, we introduce a canonical topology on the space of formal functions on $M$.

§.§ Smooth topology on $\CF(M)$

Recall the reduction $\underline{\CO}$ of $\mathcal{O}$ defined in (<ref>), to be viewed as a sheaf of $\CO$-modules by using the reduction map.
Let $\CF$ be a sheaf of $\CO$-modules and let $D\in \mathrm{Diff}_c(\CF,\underline \CO)$. For every $u\in \CF(M)$, define

\[
\abs{u}_D:=\sup_{a\in M} \abs{(D(u))(a)}.
\]

Then $\abs{\,\cdot\,}_D$ is a seminorm on $\CF(M)$.

The locally convex  topology on $\CF(M)$ defined by the family

\[\{\abs{\,\cdot\,}_D\}_{D\in \mathrm{Diff}_c(\CF,\underline \CO)}\]
seminorms is called the smooth topology of $\CF(M)$.

Unless otherwise mentioned, $\CF(M)$ is equipped with the smooth topology.

Assume that $M=N^{(k)}$, where $N$ is a smooth manifold and $k\in \BN$.
Then it follows from  Example <ref> that  the smooth topology on $\CO(M)=\RC^{\infty}(N)[[y_1, y_2, \dots, y_k]]$
coincides with the term-wise  convergence topology, where $\RC^{\infty}(N)$ is equipped with the usual smooth topology.

For every $f\in \CO(M)$,
the linear map
\[\CF(M)\rightarrow \CF(M),\quad u\mapsto{fu}\]
is continuous.

For every $D\in \mathrm{Diff}_c(\CF,\underline{\CO})$, we have that
\[\abs{fu}_{D}=\abs{u}_{D\circ f}\]

for all $u\in \CF(M)$, where $D\circ f\in \mathrm{Diff}_c(\CF,\underline{\CO})$ is as in (<ref>). This implies the lemma.

The smooth topology on $\CF(M)$ is Hausdorff if and only if for every $0\ne u\in \CF(M)$, there exists some $D\in \mathrm{Diff}_c(\CF,\underline \CO)$
such that $D(u)\ne 0$.
Furthermore, if $\CF(M)$ is Hausdorff, then so is $\CF(U)$ for every open subset $U$  of $M$.

The first assertion is obvious. For the second one, let $0\ne u\in \CF(U)$.
Take  open subsets $V$ and $W$ of $U$ such that

\[
V\subset \overline{V}\subset W\subset\overline{W}\subset U\quad
\text{and}\quad u|_V\ne 0.
\]

And take a formal function $f$ on $M$
such that $\mathrm{supp}\,f\subset W$ and $f|_{\overline{V}}=1$.

\[(f u)|_V=u|_V\ne 0 \quad \text{and} \quad  \mathrm{supp}(fu)\subset W,\]
together with the condition that $\CF(M)$ is Hausdorff,  there is a differential operator  $D'\in \mathrm{Diff}_c(\CF,\underline \CO)$ such that
$D'(fu)|_W\ne 0$. Set
\[D:=(D'\circ f)|_U\in \mathrm{Diff}_c(\CF|_U,\underline \CO|_U).\]
Then $D(u)\ne 0$ as

\[D(u)|_W=((D'\circ f)|_U(u))|_W=D'(fu)|_W\ne 0.\]

This finishes the proof.

Let $U$  be an open subset of $M$. Then the restriction map

For every $D\in \mathrm{Diff}_c(\CF|_U,\underline{\CO}|_U)$, we have that

\[
\abs{u}_{\mathrm{ext}_{M,U}(D)}= \left|(u|_U)\right|_{D}\quad \textrm{for all $u\in \CF(M)$}.
\]

This implies that the restriction map (<ref>) is continuous.

Let $\{U_\gamma\}_{\gamma\in \Gamma}$ be an open cover of $M$.  Then the linear map

(M)→∏_γ∈Γ (U_γ),   u↦{u|_U_γ}_γ∈Γ
is a topological embedding of topological spaces.
Furthermore, if $\CF(M)$ is Hausdorff,
then the image of (<ref>) is closed.

The sheaf property of $\CF$ implies  that the map (<ref>) is injective.
Lemma <ref> implies that the map (<ref>) is continuous.
Let $D\in \mathrm{Diff}_c(\CF,\underline \CO)$. Choose  $\gamma_1, \gamma_2, \dots, \gamma_s\in \Gamma$ ($s\in\BN$) such that

\[\mathrm{supp}\,D\subset U_{\gamma_1}\cup U_{\gamma_2}\cup \cdots \cup U_{\gamma_s}.\]

Let $\{g, f_{\gamma_1}, f_{\gamma_2}, \dots, f_{\gamma_s}\}$ be a partition of unity on $M$ subordinate to the open cover
$\{V:=M\setminus \mathrm{supp}\,D, U_{\gamma_1},U_{\gamma_2},\dots, U_{\gamma_s}\}$.
Note that for each $i=1,2,\dots, s$, we have that

\[(f_{\gamma_i}\circ D)|_{U_{\gamma_i}}\in \mathrm{Diff}_c(\CF|_{U_{\gamma_i}},\underline{\CO}|_{U_{\gamma_i}}),\]

where $f_{\gamma_i}\circ D\in \mathrm{Diff}_c(\CF,\underline{\CO})$ is as in (<ref>).
For every $u\in \CF(M)$, we obtain that

\[
\abs{u}_D\leq \abs{u}_{g\circ D}+ \sum_{i=1}^s \abs{u}_{f_{\gamma_i}\circ D} =\sum_{i=1}^s \left|(u|_{U_{\gamma_i}})\right|_{(f_{\gamma_i}\circ D)|_{U_{\gamma_i}}}.
\]

Therefore the continuous linear map (<ref>) is a homeomorphism onto its image.

Furthermore, if $\CF(M)$ is Hausdorff, then by Lemma <ref>,  $\CF(U_\gamma\cap U_{\gamma'})$ is  also Hausdorff for all $\gamma, \gamma'\in \Gamma$.
One  concludes from this and the sheaf property of $\CF$  that the map (<ref>)
has closed image.

Assume that the sheaf $\CF$ of $\CO$-modules is locally free of finite rank. Then the space $\CF(M)$ is a product of nuclear Fréchet spaces.

First assume that $M$ is secondly countable. Take an atlas $\{U_i\}_{i\in\mathbb{N}}$ of $M$ such that each $\CF(U_i)$  is free of finite rank. Since each $\CO(U_i)$ is a nuclear  Fréchet space (by Example <ref>), so is $\CF(U_i)$.
Using  Lemma <ref>, one concludes that  $\CF(M)$ is Hausdorff and moreover, $\CF(M)$ is a nuclear Fréchet space.

For the general case, the assertion follows from the fact that

(M)=∏_Z∈π_0(M) (Z)
as LCS, which is again implied by Lemma <ref>.

By applying  Lemma
<ref>, Example <ref>
and Corollary <ref>, one immediately gets the following result.

The $\BC$-algebra  $\CO(M)$ is a topological $\BC$-algebra. As a topological vector space, it is a product of nuclear Fréchet spaces. Especially, the LCS $\CO(M)$ is complete and nuclear.

§.§ Morphisms to $\R^m$

Define an $\R$-subalgebra

\[
\CO(M;\R):=\{f\in \CO(M)\mid f(a)\in \R\textrm{ for all }a\in M\}
\]

of $\CO(M)$.
Let $m\in \BN$, and let

\[
\varphi=(\overline\varphi, \varphi^*): (M,\CO)\rightarrow (\R^m, \CO_{\R^m}^{(0)})
\]

be a morphism of formal manifolds. Recall that $x_1, x_2, \dots , x_m\in  \CO_{\R^m}^{(0)}(\R^m)$ are standard coordinate functions of $\R^m$.
Then $\varphi$ yields an $m$-tuple

\[
c_\varphi:=(\varphi^*(x_1), \varphi^*(x_2), \dots, \varphi^*(x_m))\in (\CO(M;\R))^m.
\]

The main goal of this subsection is to prove the following theorem.

The map

{morphism from $(M,\CO)$ to $(\R^m,\CO_{\R^m}^{(0)})$}→((M;))^m,   φ↦c_φis bijective.

We will prove the theorem through a sequence of lemmas.
Firstly, the continuous map $\overline\varphi: M\rightarrow \R^m$ is determined by $c_\varphi$ by the following lemma.

Let $a\in M$. Then

\[
\overline\varphi(a)=((\varphi^*(x_1))(a), (\varphi^*(x_2))(a), \dots, (\varphi^*(x_m))(a)).
\]

Write $b:=\overline\varphi(a)$. For every $i=1,2,\dots,m$, we have that

\[
\]

This implies that $b=((\varphi^*(x_1))(a), (\varphi^*(x_2))(a), \dots, (\varphi^*(x_m))(a))$.

The map (<ref>) is injective.

For simplicity, let us set $\CO':=\CO_{\R^m}^{(0)}$.

\[
\varphi=(\overline\varphi, \varphi^*), \psi=(\overline\psi, \psi^*) : (M, \CO)\rightarrow (\R^m, \CO')
\]

be two morphisms such that $c_\varphi=c_\psi$.
From Lemma <ref>, it follows that $\overline\varphi=\overline\psi$.
Let $a\in M$ and write $b:=\overline\varphi(a)=\overline\psi(a)$. Then the maps

\[
\varphi^*_a, \psi^*_a:\ \widehat{\CO'}_b\rightarrow \widehat \CO_a
\]

are equal, since they are both continuous (see Lemma <ref>) and agree on the dense subalgebra generated by the images of the coordinate functions $x_1, x_2, \dots, x_m$ under the canonical map
\[\CO'(\R^m)\rightarrow \widehat{\CO'}_b.\]

Then the lemma follows from Lemma <ref>.

If $M=N^{(k)}$ with $N$ an open submanifold of $\R^n$ and $n,k\in \BN$, then the map
(<ref>) is surjective.

Let $(f_1,f_2,\dots,f_m)$  be an $m$-tuple in $(\CO(M;\R))^m$.
It  yields a  smooth map

\[
\overline\varphi: N\rightarrow \R^m, \quad a\mapsto (f_1(a), f_2(a), \dots, f_m(a)).
\]

Let $U$ be an open subset of $\R^m$ and set  $V:=\overline\varphi^{-1}(U)\subset N$.
For every smooth function $g\in \RC^\infty(U)$,  define a formal function
φ_U^*(g):=∑_I∈^m (∂_x^I(g)/I!∘φ)·f^I|_V∈^∞(V)[[y_1,y_2,…,y_k]],where

\[f^I:=(f_1- \underline{f_1})^{i_1}(f_2-\underline{f_2})^{i_2}\cdots(f_m-\underline{f_m})^{i_m}\in \RC^\infty(N)[[y_1, y_2, \dots, y_k]],\]
for $I=(i_1,i_2,\dots,i_m)\in \BN^m$.
Here $\underline{f_j}\in \RC^\infty(N)\subset \RC^\infty(N)[[y_1, y_2, \dots, y_k]] $ ($j=1,2,\dots, m$) is the reduction of $f_j$ as defined in (<ref>).

By using Leibniz's rule, one easily checks   that the map

\[
\varphi^*_U: \RC^{\infty}(U)\rightarrow \RC^\infty(V)[[y_1, y_2, \dots, y_k]], \quad g\mapsto \varphi^*_U(g)
\]

is an algebra homomorphism.
Then we obtain a morphism

\[
\varphi:=(\overline \varphi, \{\varphi^*_U\}_{U\textrm{ is an open subset of $\R^m$}}): (N, \CO_{N}^{(k)})\rightarrow (\R^m, \CO_{\R^m}^{(0)})
\]

of formal manifolds. Note that for every $i=1,2,\dots,m$,

\[\varphi^*(x_i)= x_i\circ \overline{\varphi}+(f_i-\underline{f_{i}})=f_i.\]

This implies that $c_{\varphi}=(f_1, f_2, \dots, f_m)$, and  the proof is finished.

Lemma <ref>, we only need to show the following lemma to finish the proof of Theorem <ref>.

The map
(<ref>) is surjective.

Let $f_1, f_2,\dots, f_m\in \CO(M;\R)$, and take an atlas  $\{U_\gamma\}_{\gamma\in \Gamma}$ of $M$.
Then for each $\gamma\in \Gamma$, it follows from Lemma <ref>  that there is a morphism

\[\varphi_\gamma: (U_\gamma, \CO|_{U_\gamma})\rightarrow (\R^m, \CO_{\R^m}^{(0)})\]
such that

\[
c_{\varphi_\gamma}=((f_1)|_{U_\gamma}, (f_2)|_{U_\gamma}, \dots,(f_m)|_{U_\gamma}).
\]

Moreover, Lemma <ref> implies that $\varphi_\gamma$ and $\varphi_{\gamma'}$
agree on $(U_\gamma\cap U_{\gamma'}, \CO|_{U_\gamma\cap U_{\gamma'}})$ for all $\gamma, \gamma'\in \Gamma$.
Hence the family $\{\varphi_\gamma\}_{\gamma\in \Gamma}$ patches together to
a morphism
\[\varphi: (M, \CO)\rightarrow (\R^m, \CO_{\R^m}^{(0)}).\]

It is clear that $c_\varphi=(f_1, f_2,\dots, f_m)$. This proves the lemma.

§.§ Automatic continuity

In this subsection, we prove that for every  morphism  of formal manifolds, the induced homomorphism on the topological $\BC$-algebras  of formal functions
is continuous.
We start with  the following special case.

Let $n,k,m,l\in\BN$.
For every morphism
$\varphi=(\overline\varphi, \varphi^*): (\R^n, \CO_{\R^n}^{(k)})\rightarrow (\R^m, \CO_{\R^m}^{(l)})$, the homomorphism

\[
\varphi^*: \RC^\infty(\R^m)[[y_1,y_2, \dots, y_l]]\rightarrow \RC^\infty(\R^n)[[y_1,y_2, \dots, y_k]]
\]

is continuous.

When $l=0$, this follows from Theorem <ref> and the explicit expression of $\varphi^*$ given in  (<ref>). In general, we have an obvious morphism

\[
\psi=(\overline\psi, \psi^*): (\R^m, \CO_{\R^m}^{(l)})\rightarrow (\R^{m+l}, \CO_{\R^{m+l}}^{(0)})
\]

so that the map

ψ^*:  ^∞(^m+l)→^∞(^m)[[y_1,y_2, …, y_l]]
is given by the Taylor series expansion along $\R^l$.
It follows from Borel's lemma that the map $\psi^*$ is surjective.
Thus by the open mapping theorem,  it is also open.

Consider the maps

\[
\RC^\infty(\R^{m+l})\xrightarrow{\psi^*} \RC^\infty(\R^m)[[y_1,y_2, \dots, y_l]]\xrightarrow{\varphi^*} \RC^\infty(\R^n)[[y_1,y_2, \dots, y_k]].
\]

We have shown that the composition of these two arrows is continuous, and the first arrow is open and surjective. Thus the second arrow is also continuous.

Let $\varphi=(\overline\varphi, \varphi^*): (M,\CO)\rightarrow (M', \CO')$ be a morphism of formal manifolds. Then the $\BC$-algebra homomorphism

\[
\varphi^*: \CO'(M')\rightarrow \CO(M)
\]

is continuous.

Lemma <ref>, we only need to show that for every $a\in M$, there is an open neighborhood $U$ of it in  $M$ such that the homomorphism

φ^*_M',U: '(M')→(U)
is continuous.
Choose an open neighborhood  $U$ of $a$ in $M$, and an open neighborhood  $U'$ of $\overline{\varphi}(a)$ in $M'$ such that

* $(U, \CO|_U)\cong(\R^n, \CO_{\R^n}^{(k)})$ ($n:=\dim_a(M)$, $k:=\deg_a(M)$);

* $(U', \CO|_{U'})\cong(\R^m, \CO_{\R^m}^{(l)})$ ($m:=\dim_{\overline{\varphi}(a)}(M')$, $l:=\deg_{\overline{\varphi}(a)}(M')$); and

* $\overline\varphi(U)\subset U'$.

View $\varphi^*_{M',U}$ as the  composition of the following two maps:

\[
\CO'(M')\xrightarrow{\textrm{restriction}} \CO'(U')\xrightarrow{\varphi^*_{U',U}} \CO(U).
\]

Note that the first arrow is continuous by Lemma <ref>, and the second one is continuous by Lemma <ref>. Hence the  map
$\varphi^*_{M',U}$ is  also continuous and the theorem is proved.

Let $\varphi=(\overline\varphi, \varphi^*): (M,\CO)\rightarrow (M', \CO')$ be a morphism of formal manifolds. If the homomorphism
\varphi^*: \CO'(M')\rightarrow \CO(M)
is surjective, then it is open.

In view of (<ref>), it suffices to prove the case that $M'$ is connected.
Note that $\CO'(M')$ is a Fréchet space  and $\CO(M)$ is a barreled space (see Corollary <ref> and Lemma <ref>).
The assertion then follows from Theorem <ref> and the fact that every continuous surjective linear map from a Fréchet space to a barreled space is open (see <cit.>).

§ THE ALGEBRA OF FORMAL FUNCTIONS

In this section, we show that a formal manifold is determined by the topological $\BC$-algebra of formal functions.

§.§ Characters of $\CO(M)$

For every $\BC$-algebra $A$, we call a  $\BC$-algebra homomorphism $A\rightarrow \BC$ a character of $A$.
For every $a\in M$, the map

Ev_a: (M)→,   f↦f(a)
of evaluating at $a$ is a continuous character of $\CO(M)$.
The main goal of this subsection is to prove the following theorem, which is known as Milnor's exercise when $M$ is a smooth
manifold (see <cit.>).

Suppose that the cardinality of $\pi_0(M)$ does not exceed the cardinality of $\R$.
Then every character of $\CO(M)$ is of  the form $\mathrm{Ev}_a$ for some $a\in M$.

Before proving the theorem, we establish some technical lemmas.

If $\pi_0(M)$ is countable, then
there exists a formal function $f\in \CO(M;\R)$ such that  the set $\{a\in M \mid f(a)\leq C\}$ is compact for all $C\in \R$.

Recall that the reduction $\underline{M}$ of $M$ is a smooth manifold.
It is well-known that there is a bounded below proper smooth map $\underline{f}: \underline{M}\rightarrow \R$ (see the proof of <cit.> for example). Let $f\in \CO(M)$ be an element in the preimage of $\underline{f}$ under the surjective map (<ref>). Then $f$ fulfills the requirement of the lemma.

Let $\chi: \CO(M)\rightarrow \BC$ be a character, and let $a\in M$. If $\chi\neq \mathrm{Ev}_a$, then there is an element $f_{\chi}^a\in \CO(M)$ such that

* $f_{\chi}^a(b)$ is a non-negative real number for all  $b\in M$;

* $f_{\chi}^a(a)=1$; and

* $\chi(f_{\chi}^a)=0$.

The condition $\chi\neq \mathrm{Ev}_a$ implies that there is an element $f\in \CO(M)$ such that $f(a)\neq 0$ and $\chi(f)=0$.
Let $U$ be an open neighborhood of $a$ in $M$ such that $(U, \CO|_U)\cong (\R^n, \CO_{\R^n}^{(k)})$ for some $n,k\in \BN$.
Multiplying $f$ by a suitable formal function if necessary, we assume without loss of generality that $\mathrm{supp}\,f$ is contained in $U$. Then we have a decomposition $f=f_1+\sqrt{-1} f_2$ such that $f_1, f_2\in \CO(M;\R)$, and the lemma follows by defining

\[
f_{\chi}^a:=(f_1(a)^2+f_2(a)^2)^{-1}\cdot (f_1+\sqrt{-1} f_2)\cdot (f_1-\sqrt{-1} f_2).
\]

For every $Z\in \pi_0(M)$, write $1_Z$ for the identity element of $\CO(N)$.

Suppose that the cardinality of $\pi_0(M)$ does not exceed the cardinality of $\R$.
Then for every  character  $\chi$ of $\CO(M)$, there is a formal function
$f_\chi\in \CO(M)$ such that

* $f_\chi(a)$ is a non-negative real number for all $a\in M$;

* the set
Z_0:=\{b\in M\mid f_\chi(b)=0\}
is  a connected component of $M$; and

* $\chi(f_\chi)=0$.

Fix an injective map

\[
\tau:\ \pi_0(M)\rightarrow \R.
\]

Let $g$ be the formal function on $M$ defined by setting $g|_Z=\tau(Z)1_Z$ for all $Z\in \pi_0(M)$,
and set

\[
f_\chi:=(g-\chi(g))\cdot (g-\overline{\chi(g)})\qquad ( \ \overline{\phantom{a}}\ \textrm{ indicates the complex conjugation}).
\]

\[
\chi(f_\chi)=0\quad\textrm{and}\quad f_\chi(a)\geq 0\ \textrm{ for all }a\in M.
\]

\[
Z_0:=\{b\in M\mid f_\chi(b)=0\}
\]

is either the empty set or a connected component of $M$. If $Z_0$ is empty, then $f_\chi$ is invertible in $\CO(M)$ by   Lemma <ref>,
which contradicts $\chi(f_\chi)=0$. Thus $f_\chi$ is a desired formal function.

Proof of Theorem <ref>:
Let $\chi: \CO(M)\rightarrow \BC$ be a character of $\CO(M)$.
Let $f_\chi$ be as in Lemma <ref> so that the set
Z_0:=\{b\in M\mid f_\chi(b)=0\}
is a connected component of $M$.

Applying Lemma <ref> to the formal manifold $Z_0$, we have a formal function $f\in \CO(Z_0;\R)$
such that $\{b\in Z_0\mid f(b)\le C\}$ is compact for all $C\in \R$. By extension by zero, we also view $f$ as an element of $\CO(M)$. Put

\[
f':=(f-\chi(f))\cdot (f-\overline{\chi(f)}). %\in\CO(M).
\]

Then $f'\in \CO(M;\R)$,  $\chi(f')=0$, $f'(b)\geq 0$ for all $b\in M$, and  the set

\[
\{a\in Z_0\mid f'(a)=0\}
\]

is compact.

Assume by contradiction that $\chi\neq  \mathrm{Ev}_a$ for all $a\in M$. Then for every $a\in M$, there is an element $f_{\chi}^a\in \CO(M)$ that satisfies the three conditions in Lemma <ref>. Since $f_{\chi}^a(a)=1$ for all $a\in M$, there  exist finitely many elements $a_1, a_2, \dots, a_s\in Z_0$ such that

\[
\bigcup_{i=1}^s \{b\in Z_0\mid f_{\chi}^{a_i}(b)>0\} \supset   \{a\in Z_0\mid f'(a)=0\}.
\]

Now we define

\[
f'':=f_\chi+f'+\sum_{i=1}^s f_{\chi}^{a_i}.
\]

Then $\chi(f'')=0$ and $f''(b)>0$ for all $b\in M$.
Lemma <ref> implies that  $f''$ is invertible in $\CO(M)$, which contradicts  $\chi(f'')=0$.

§.§ Continuous characters of $\CO(M)$

For every connected component $Z$ of $M$, we view the identity element $1_Z\in \CO(Z)$ as an element of $\CO(M)$ via extension by zero. Then $1_Z\in \CO(M)$ is an indecomposable idempotent in $\CO(M)$. Namely, it is an idempotent in the sense that $1_Z^2=1_Z$, and it is indecomposable in the sense that it is nonzero, and is not the sum of two nonzero idempotents.  Moreover,
it is obvious that every indecomposable idempotent in $\CO(M)$ is of the form $1_Z$ for a unique connected component $Z$ of $M$.

By Theorem <ref>, we know that if the cardinality of $\pi_0(M)$ does not exceed the cardinality of $\R$, then every character of $\CO(M)$ is continuous. In general, we have the following characterization of the continuity of a character of $\CO(M)$.

Let $\chi: \CO(M)\rightarrow \BC$ be a character. Then the following three conditions are equivalent to each other.

The character $\chi$ is continuous.

The character $\chi$  vanishes on $(1-e)\cdot \CO(M)$ for some indecomposable idempotent $e$ in $\CO(M)$.

The equality $\chi=\mathrm{Ev}_a$ holds for some $a\in M$.

When these conditions are satisfied, the elements $e\in \CO(M)$ and $a\in M$ as above are unique.

We first prove that (a) implies (c).  Suppose that $\chi$ is continuous.

\[
\CO(M)=\prod_{Z\in \pi_0(M)} \CO(Z)
\]

as LCS,
the continuity of $\chi$ implies that  there is an open  closed subset $Z'$ of $M$, consisting of
finitely many connected components of $M$, such that $\chi$ factors through the restriction map

\[
\CO(M)\rightarrow \CO(Z').
\]

Write $\chi': \CO(Z')\rightarrow \BC$ for the induced character. By Theorem <ref>, $\chi'$ equals the evaluation map at some $a\in Z'$. Thus $\chi=\mathrm{Ev}_a$ and we have proved that (a) implies (c).

By using Theorem <ref>, it is easy to see that (b) implies (c). The  uniqueness assertion as well as the  implications (c)$\Rightarrow $(a) and (c)$\Rightarrow $(b) are obvious.

§.§ The formal spectra

In this subsection, we reconstruct the formal manifold $(M,\CO)$ from the topological $\C$-algebra $\CO(M)$.
We start with the following definition.

A formal $\BC$-algebra is a topological $\BC$-algebra that is topologically isomorphic to $\CO(M)$ for some formal manifold $(M, \CO)$.

All topological $\BC$-algebras together with all continuous homomorphisms between them form a category.
All formal $\BC$-algebras form a full subcategory of the category of topological $\BC$-algebras, and thus they also form a category.

Let $A$ be a formal $\BC$-algebra.
Define the formal spectrum of $A$ to be the set

Specf(A):={continuous character of $A$}.
Equip $\mathrm{Specf}(A)$ with the coarsest topology such that the map

\[
\mathrm{Specf}(A)\rightarrow \BC, \quad \chi\mapsto \chi(f)
\]

is continuous for all $f\in A$.   For every $\chi\in \mathrm{Specf}(A)$, write $A_\chi$ for the localization of the ring $A$ at the maximal ideal $\ker(\chi)$.

Let $U$ be an open subset of $\mathrm{Specf}(A)$. We  say that an element

\[f=\{f_\chi\}_{\chi\in U} \in \prod_{\chi\in U} A_\chi\]

is locally represented by $A$ if for every $\chi_0\in U$,
there is an open neighborhood $U_0$ of $\chi_0$ in $U$,
and an element $f_0\in A$ such that  $\{f_\chi\}_{\chi\in U_0}$ equals the image of $f_0$ under the canonical map

\[
A\rightarrow \prod_{\chi\in U_0}A_\chi.
\]

_A(U):={f∈∏_χ∈U A_χ|f is locally represented by $A$ }.
Together with the restriction maps, $\CO_A$ is a sheaf of $\BC$-algebras over $\mathrm{Specf}(A)$.

The rest of this subsection is devoted to a proof of the following theorem.

The pair $(\mathrm{Specf}(A), \CO_A)$ is a formal manifold.
Furthermore, if $A=\CO(M)$, then there is an identification $(\mathrm{Specf}(A), \CO_A)=(M, \CO)$ of formal manifolds.

We begin with the following lemma, which asserts that the topology on $M$ is determined by the space $\CO(M)$.

The  map

ι_M:  M→∏_f∈(M)  ,   a↦{f(a)}_f∈(M)
is a  topological embedding.

The map (<ref>) is clearly continuous and injective.
In what follows we prove that the inverse  map

\[
\iota_M^{-1}:\ \iota_M(M)\rightarrow M
\]

is also continuous, which implies the lemma.

Let $a\in M$ and let $U$ be an open neighborhood of $a$ in $M$. Take a formal function $f_0\in \CO(M)$ such that its support is contained in $U$ and $f_0(a)=1$.

\[
U':= \left\{\{c_f\}_{f\in \CO(M)}\in  \prod_{f\in \CO(M)}  \BC \mid (c_{f_0}-1)\cdot (\overline{c_{f_0}}-1)<1\right\}
\]

is an open neighborhood of $\iota_M(a)$ in $\prod_{f\in \CO(M)}  \BC$ such that $\iota_M^{-1}(U')\subset U$, as required.

Let $a\in M$. Then as a $\BC$-algebra, the stalk $\CO_a$ is canonically isomorphic to the localization of $\CO(M)$ at the maximal ideal

\[
\m_a':= \{f\in \CO(M)\mid f(a)=0\}.
\]

\[
\rho_a: \CO(M)\rightarrow \CO(M)_{\m_a'}
\]

for the localization map. For every $f\in \CO(M)$, we have that

\begin{eqnarray*}
&&f\in \ker(\rho_a)\\
&\Longleftrightarrow& f_0 f=0\textrm{ for some $f_0\in \CO(M)\setminus \m_a'$}\\
&\Longleftrightarrow& f|_U=0 \textrm{ for some open neighborhood $U$ of $a$ in $M$}.
\end{eqnarray*}

Moreover, for every $f_0\in \CO(M)\setminus \m_a'$, there is an element $f_1\in \CO(M)$ such that $\rho_a(f_0f_1-1)=0$. This implies that the map $\rho_a$ is surjective.

The lemma then follows by noting  that the canonical map

\[
\CO(M)\rightarrow \CO_a
\]

is also surjective (see Corollary <ref>) and its kernel equals that of $\rho_a$.

Proof of Theorem <ref>:
Assume that $A=\CO(M)$. By Proposition <ref>, we have a bijection

\[
\mathrm{Ev}:   M\rightarrow \mathrm{Specf}(A), \quad a\mapsto \mathrm{Ev}_a.
\]

This is in fact a homeomorphism by Lemma <ref>. In the notation of Lemma <ref>, we have that $\CO_a=\CO(M)_{\m_a'}$ for every $a\in M$.
Also, note that for every open subset $U$ of $M$,

\[
\CO(U)=\left\{f\in \prod_{a\in U} \CO_a\mid f\textrm{ is locally represented by $\CO(M)$ }\right\}.
\]

Thus with respect to the homeomorphism $\mathrm{Ev}$,  the sheaf $\CO$ on $M$ coincides with the sheaf $\CO_A$ on $\mathrm{Specf}(A)$. The proof of Theorem <ref> is now finished.

§.§ An equivalence of categories

In this subsection, we prove that the category of formal manifolds is equivalent to the opposite category of that of formal $\C$-algebras.

Let $\psi: A'\rightarrow A$ be a continuous homomorphism of formal $\BC$-algebras.
Then it induces a map

ψ:  Specf(A)→Specf(A'),   χ↦χ∘ψ.
It is easily seen that this map is continuous. For every $\chi\in \mathrm{Specf}(A)$, $\psi$ also induces a homomorphism

\[
\psi_{\chi}^*:\, A'_{\psi(\chi)}\rightarrow A_\chi.
\]

Let $U'\subset \mathrm{Specf}(A')$ be an open subset and put $U:=\overline\psi^{-1}(U')\subset \mathrm{Specf}(A)$. Then  there exists a unique $\BC$-algebra homomorphism

ψ^*_U': _A'(U')→_A(U)
such that the diagram

\[
\begin{CD}
\CO_{A'}(U') @> \psi^*_{U'}  >>  \CO_A(U)\\
@V  VV           @V V V\\
A'_{\psi(\chi)} @> \psi_{\chi}^*>>  A_{\chi} \\
\end{CD}
\]

commutes for all $\chi\in U$.

The uniqueness follows from the fact that the canonical map $\CO_A(U)\rightarrow \prod_{\chi\in U} A_\chi$ is injective. Note that if an element

\[
f'=\{f'_{\chi'}\}_{\chi'\in U'}\in \prod_{\chi'\in U'} A'_{\chi'}
\]

is locally represented by $A'$, then

\[
f:=\{\psi_{\chi}^*(f'_{\overline\psi(\chi)})\}_{\chi\in U}\in \prod_{\chi\in U} A_{\chi}
\]

is locally represented by $A$. Furthermore, the map

\[
\psi^*_{U'}: \CO_{A'}(U')\rightarrow \CO_A(U),\quad f'\mapsto f
\]

is a $\C$-algebra homomorphism. Thus the existence assertion of the lemma also holds.

The family
$$\{\psi^*_{U'}: \CO_{A'}(U')\rightarrow \CO_A(U)\}_{\, U'\textrm{ is an open subset of }M'}$$
as in (<ref>) is compatible with respect to the restrictions. Thus we get a sheaf homomorphism

\[
\psi^*: \overline \psi^{-1} \CO_{A'}\rightarrow \CO_A.
\]

This sheaf homomorphism induces local homomorphisms of the stalks. Then we obtain in this way
a morphism
Specf(ψ)=(ψ, ψ^*): (Specf(A),_A)→(Specf(A'), _A')of formal manifolds. The assignment
$\psi\mapsto \mathrm{Specf}(\psi)$ is compatible with the compositions, and if $\psi$ is an identity homomorphism,
then $\mathrm{Specf}(\psi)$ is also an identity morphism. In conclusion, we get a functor

from the opposite category of the category of formal $\BC$-algebras to the category of formal manifolds.

On the other hand, by Theorem <ref>, we have a functor

(M, )↦(M)
from  the category of formal manifolds to the opposite category of the category of formal $\BC$-algebras.
Then we have  the following result, which implies Theorem <ref>.

The functors (<ref>) and (<ref>)
are quasi-inverse of each other.

This is implied by
Theorem <ref>.

Assume that

the cardinality of $\pi_0(M)$ does not exceed the cardinality of $\R$.
By Theorem <ref>, it is  not difficult to show that the formal spectrum $\mathrm{Specf(\CO(M))}$
coincides with the usual spectrum

\[\mathrm{Spec}(\CO(M)):=\{\text{character of $\CO(M)$}\}\]
of the $\C$-algebra $\CO(M)$  (see <cit.>) as topological spaces.
Similar to the case of smooth manifolds (see <cit.> for example),  in such case, $(M,\CO)$ can be reconstructed from the spectrum $\mathrm{Spec}(\CO(M))$ by Theorem <ref>.
Furthermore, for any formal manifold $(M',\CO')$ (whether or not it satisfies the condition (<ref>)),
it is easy to verify that every $\C$-algebra homomorphism from  $O(M)$ to
$O'(M')$  is automatically continuous (see  <cit.>).

§ VECTOR-VALUED FORMAL FUNCTIONS AND PRODUCTS OF FORMAL MANIFOLDS

In this section, we introduce the notion of vector-valued formal functions.
Using this, we prove the existence of finite products in the category of formal manifolds.

§.§ Vector-valued formal functions

Throughout this subsection, let $E$ be a quasi-complete  LCS.
For every open subset $U$ of $M$,  write

\[
\CO_E(U):=\CO(U)\widetilde \otimes E.
\]

We refer to  Section <ref> for the usual  notations

\[
\otimes_{\pi},\quad\otimes_{\varepsilon},\quad\otimes_{\mathrm{i}}, \quad \widetilde\otimes_{\pi},\quad\widetilde\otimes_{\varepsilon},\quad\widetilde\otimes_{\mathrm{i}}, \quad\widetilde \otimes, \quad\widehat\otimes_{\pi},\quad\widehat\otimes_{\varepsilon},\quad\widehat\otimes_{\mathrm{i}},\quad\widehat \otimes,
\]

which are used to denote various topological tensor products, their quasi-completions, and their completions.

Motivated by Schwartz's characterization of $E$-valued smooth functions (see (<ref>)), we make the following definition.

An element in $\CO_E(M)$ is called an $E$-valued formal function on $M$.

With the obvious restriction maps, the assignment

\[
\CO_E:\ U\mapsto \CO_E(U)\quad (\text{$U$ is an open subset of $M$})
\]

forms a presheaf of complex vector spaces on $M$.
The main goal of this subsection is to prove the following theorem.

The presheaf $\CO_E$ is a sheaf. Moreover, if $E$ is complete, then for every open subset $U$ of $M$,

\[
\CO_E(U)=\CO(U)\widehat \otimes E
\]

as LCS.

We start with the following special case.

Theorem <ref> holds when $M=N^{(k)}$, where   $N$ is  a smooth manifold and $k\in \BN$.

Let $U$ be an open subset of $M$. By applying (<ref>) and Example <ref>, we obtain that

\begin{eqnarray*}
\CO_E(U)&=&\CO(U)\widetilde \otimes E\\
&=& \RC^\infty(U)\widetilde \otimes \BC[[y_1, y_2, \dots, y_k]]\widetilde \otimes E\\
&=&\RC^\infty(U;E[[y_1, y_2, \dots, y_k]]).
\end{eqnarray*}

Thus $\CO_E$ is a sheaf. Moreover, if $E$ is complete, then $\RC^\infty(U;E[[y_1, y_2, \dots, y_k]])$
is complete by (<ref>), and so $\CO_E(U)=\CO(U) \widehat \otimes E$.

Write $\widetilde{\CO}_E$ for the sheaf associated to the presheaf $\CO_E$. Lemma <ref> implies that $\widetilde{\CO}_E(U)=\CO_E(U)$ whenever the open set $U$ is a
chart. In general, the sheaf property implies that

\[
\widetilde{\CO}_E(U)=\varprojlim_{V} \CO_E(V),
\]

where $V$ runs over all charts of $U$. Using the above equality, we view $\widetilde{\CO}_E(U)$ as an LCS with the projective limit topology. It is quasi-complete by <cit.>.
If the open set $U$ is a chart, then

as LCS.

The following lemma generalizes Lemma <ref>.

Let $U$ be an open subset of $M$. Then the restriction map

is continuous.

It suffices to show that for every  chart $V$ of $U$, the canonical map

\[
\widetilde{\CO}_E(M)\rightarrow \CO_E(V)
\]

is continuous. But this is self-evidence since $V$ is also a chart of $M$.

Similar to Lemma <ref>, we have the following result.

Let $\{U_\gamma\}_{\gamma\in \Gamma}$ be an open cover of $M$. Then the linear map

_E(M)→∏_γ∈Γ _E(U_γ),   f↦{f|_U_γ}_γ∈Γ
is a closed topological embedding.

The sheaf property of $\widetilde{\CO}_E$ and Lemma <ref> imply that the map (<ref>) is continuous, injective and its image is closed in the codomain.

Let $\{f_i\}_{i\in I}$ be a net in  $ \widetilde{\CO}_E(M)$ whose image under the map (<ref>)  converges to zero. Then

lim_i∈I (f_i|_U_γ)=0  for all γ∈Γ.
To finish the proof, we only need to show that

lim_i∈I (f_i|_U)=0
for all charts $U$ of $M$.

By Lemma <ref>, the linear map

\[
\CO(U)\rightarrow \prod_{\gamma\in \Gamma} \CO(U\cap U_\gamma)
\]

is a topological embedding. Since the epsilon tensor product of two linear topological embeddings of  Hausdorff LCS is a linear topological embedding (see the proof of <cit.>), Lemma <ref> and (<ref>)   imply that
the linear map

_E(U) →∏_γ∈Γ _E(U∩U_γ)   is also a topological embedding.
Now, Lemma <ref> and (<ref>) imply that

lim_i∈I (f_i|_U∩U_γ)=0  for all γ∈Γ.
Hence  (<ref>) holds by (<ref>).

Note that $\widetilde{\CO}_E$ is naturally a sheaf of $\CO$-modules, and the module structure map

\[
\CO(M)\times \widetilde{\CO}_E(M)\rightarrow \widetilde{\CO}_E(M), \quad (g,f)\mapsto gf
\]

is continuous and bilinear.

Let  $U$ be an open subset of $M$, and let $g\in \CO(M)$ be a formal function whose support is contained in $U$. Then the linear map  (see (<ref>))

m_g:  _E(U)→_E(M),   f↦gf
is continuous.

The lemma follows by applying Lemma <ref> to the open cover $\{U, M\setminus \mathrm{supp}\,g\}$ of $M$.

For every open subset $U$ of $M$, the canonical linear map

\[
\CO(U)\otimes_\pi E\rightarrow \widetilde{\CO}_E(U)
\]

is a topological embedding.

Consider the commutative diagram

\[
\begin{CD}
\CO(U)\otimes_\pi E@>  >>  \widetilde{\CO}_E(U)=\varprojlim_{V} \CO(V)\widetilde \otimes E \\
@V  VV           @V V V\\
\left(\prod_{V} \CO(V)\right)\widetilde\otimes E @ >> > \prod_{V} \left(\CO(V)\widetilde \otimes E\right),\\
\end{CD}
\]

where $V$ runs over all charts of $M$ that are contained in $U$.
By Lemma <ref>, Proposition <ref> and the fact that the epsilon tensor product of two linear topological embeddings of Hausdorff LCS is a linear topological embedding (see the proof of <cit.>), we see that the linear  map

\[
\CO(U)\otimes_\pi E=
\CO(U)\otimes_\varepsilon E\rightarrow
\left(\prod_{V} \CO(V)\right)\otimes_\pi E
=\left(\prod_{V} \CO(V)\right)\otimes_\varepsilon E
\]

is a topological embedding.
This implies that
the left vertical arrow
is a linear topological embedding. By Lemma <ref>, the bottom horizontal arrow is a topological linear isomorphism.
the right vertical arrow is a linear topological embedding by Lemma <ref>, the top horizontal arrow is also
a linear topological embedding.

Lemma <ref>, we identify the LCS $\CO(U)\otimes_\pi E$ with a subspace of $\widetilde{\CO}_E(U)$.

The subspace $\CO(M)\otimes_\pi E$ is strictly dense (see Definition <ref>) in $\widetilde{\CO}_E(M)$.

Take an atlas  $\{U_\gamma\}_{\gamma\in \Gamma}$  of $M$, and  let  $\{g_\gamma\}_{\gamma\in \Gamma}$ be a partition of unity on $M$ subordinate to it.
Let $A$ be a quasi-closed subset (see Definition <ref>) of $\widetilde{\CO}_E(M)$ containing $\CO(M)\otimes E$.
Since the inverse image of a quasi-closed set under a continuous linear map is still quasi-closed  (see <cit.>),
it follows from Lemma <ref>  that  $m_{g_\gamma}^{-1}(A)$ (see (<ref>))
is quasi-closed.
This, together with (<ref>), shows that $m_{g_\gamma}^{-1}(A)=\widetilde{\CO}_E(U_\gamma)$ for all $\gamma\in \Gamma$.
In particular, for every $f\in \widetilde{\CO}_E(M)$, we have that $f_\gamma:= g_\gamma\cdot f|_{U_\gamma}\in A$.

By Lemma <ref>, the canonical linear  map

\[
\widetilde{\CO}_E(M)\rightarrow \prod_{U\textrm{ is a  relatively compact open subset of $M$}} \widetilde{\CO}_E(U)
\]

is a topological embedding.
This implies that

\[B:=\left\{\sum_{\gamma\in \Gamma_0}f_\gamma\mid \Gamma_0\ \text{is a finite subset of}\ \Gamma\right\}\]

is a bounded subset in $A$. Thus $A$ contains the closure of $B$. Then

\[
f=\sum_{\gamma\in \Gamma}g_\gamma\, f=\sum_{\gamma\in \Gamma} f_\gamma
\]

belongs to $A$ since it belongs to the closure of $B$.
This completes the proof.

Proof of Theorem <ref>:
Let $U$ be an open subset of $M$.
Applying Proposition <ref> to the formal manifold $(U, \CO|_U)$, we know that
$\CO(U)\otimes_\pi E$ is strictly dense in $\widetilde{\CO}_E(U)$. Therefore, by Lemma <ref>, we have that

\[
\widetilde{\CO}_E(U)=\CO(U)\widetilde \otimes E=\CO_E(U)
\]
as LCS.
This proves that $\CO_E$ is a sheaf.
When $E$ is complete, Lemmas <ref> and <ref> imply that $\CO_E(U)$ is complete.
This finishes the proof of Theorem <ref>.

§.§ Products of formal manifolds

In this subsection, let $(M_1, \CO_1)$ and $(M_2, \CO_2)$ be two formal manifolds.
For open subsets $V_1\subset U_1$ of $M_1$, and $V_2\subset U_2$ of $M_2$,  we have the restriction map

\[
\CO_1(U_1)\widetilde \otimes \CO_2(U_2)\rightarrow
\CO_1(V_1)\widetilde \otimes \CO_2(V_2).
\]

Using these restriction maps, for each open subset $U_3$ of

\[M_3:=M_1\times M_2 \quad \text{(as topological spaces),}\]
we define

\[
\CO_3(U_3):=\varprojlim_{(U_1,U_2)} \CO_1(U_1)\widetilde \otimes \CO_2(U_2),
\]

where $(U_1,U_2)$ runs over all pairs of open subsets $U_1$ of $M_1$ and $U_2$ of $M_2$ such that $U_1\times U_2\subset U_3$. Then $\CO_3$ is obviously a presheaf of $\C$-algebras on $M_3$.

This subsection is devoted  to a proof of the following theorem, which together with the fact
that (see Theorem  <ref>)

\[\CO(M_3)=\CO_1(M_1)\widetilde \otimes \CO_2(M_2)=\CO_1(M_1)\widehat \otimes \CO_2(M_2)\]

implies Theorem <ref>.

The presheaf $\CO_3$ on $M_3$ is a sheaf, and $(M_3, \CO_3)$ is a formal manifold which is a product of $(M_1, \CO_1)$ and $(M_2, \CO_2)$ in the category of  formal manifolds. Moreover,

\[
(M_3,\underline{\CO_{3}})=(M_1, \underline{\CO_{1}}) \times (M_2, \underline{\CO_{2}})
\]

as smooth manifolds, and for $a_1\in M_1, a_2\in M_2$,

\[
\wh{\CO}_{3,a_3}=\wh{\CO}_{1,a_1}\wh{\otimes}\,\wh{\CO}_{2,a_2}=\wh{\CO}_{1,a_1}\widetilde{\otimes}\,\wh{\CO}_{2,a_2}\qquad (a_3:=(a_1,a_2))
\]

as topological $\C$-algebras.

We will prove the theorem through a sequence of lemmas.

Assume that $M_1=N^{(k)}$ and $M_2=L^{(l)}$, where $N$ and $L$ are smooth manifolds and $k,l\in \BN$.
Then $\CO_3$ is a sheaf,  $(M_3, \CO_3)$ is a formal manifold, and $M_3\cong (N\times L)^{(k+l)}$ as formal manifolds.

Let $U_1$ and $U_2$ be open subsets of $M_1$ and $M_2$, respectively.
It  follows from  Example <ref> and (<ref>) that

\begin{eqnarray*}
\CO_3(U_1\times U_2)&=&  \CO_1(U_1)\widetilde \otimes \CO_2(U_2)\\
&=& \RC^\infty(U_1)[[y_1, y_2, \dots, y_k]]\widetilde \otimes \RC^\infty(U_2)[[y_1, y_2,\dots, y_l]]\\
&=& \RC^\infty(U_1)\widetilde \otimes \BC[[y_1, y_2, \dots, y_k]]\widetilde \otimes \RC^\infty(U_2)\widetilde \otimes \BC [[ y_1, y_2,\dots, y_l]]\\
&=& \RC^\infty(U_1\times U_2)\widetilde \otimes \BC[[y_1, y_2, \dots, y_k,  y_{k+1}, y_{k+2},\dots, y_{k+l}]]\\
&=& \RC^\infty(U_1\times U_2)[[y_1, y_2, \dots, y_k,  y_{k+1}, y_{k+2},\dots, y_{k+l}]]
\end{eqnarray*}

as topological $\BC$-algebras. Hence by the sheaf property, we conclude that $\CO_3=\CO_{N\times L}^{(k+l)}$. This proves the lemma.

Write $\widetilde{\CO}_3$ for the sheafication of $\CO_3$. We will show that  $\widetilde{\CO}_3=\CO_3$.

If $M_1=N^{(k)}$ with $N$ a smooth manifold and $k\in \BN$, then $\CO_3$ is a sheaf, and $(M_3, \CO_3)$ is a formal manifold.

Let $U_1$ be an open subset of $M_1$.
For every open subset $U_2$ of $M_2$, we have a natural homomorphism

This yields a sheaf homomorphism

_2, _1(U_1) →(p_2)_*(_3|_U_1×M_2)
over $M_2$,
where $ \CO_{2, \CO_1(U_1)} $ is the sheaf

\[U_2\mapsto \CO_1(U_1)\widetilde \otimes \CO_2(U_2)\]
on $M_2$  (see Theorem <ref>), and
$p_2: U_1\times M_2\rightarrow M_2$ is the projection map. By Lemma <ref>, the map
(<ref>) is an isomorphism when $U_2$ is a chart. This implies that  (<ref>) is a sheaf isomorphism. In other words,

\[
\widetilde{\CO}_3(U_1\times U_2)=\CO_3(U_1\times U_2)
\]

for all open subsets $U_2$ of $M_2$. Then the sheaf property implies that $\widetilde{\CO}_3=\CO_3$, and Lemma <ref> implies that $(M_3, \CO_3)$ is a formal manifold.

The presheaf $\CO_3$ is a sheaf, and $(M_3, \CO_3)$ is a formal manifold.

The proof is similar to that of Lemma <ref>. Let $U_2$ be an open subset of $M_2$.
For every open subset $U_1$ of $M_1$, we have a natural homomorphism

This yields a sheaf homomorphism

_1, _2(U_2) →(p_1)_*(_3|_M_1×U_2)
over $M_1$,
where $ \CO_{1, \CO_2(U_2)} $ is the sheaf
\[U_1\mapsto \CO_1(U_1)\widetilde \otimes \CO_2(U_2)\]
on $M_1$ (see Theorem <ref>), and
$p_1: M_1\times U_2\rightarrow M_1$ is the projection map. By Lemma <ref>, the map
(<ref>) is an isomorphism when $U_1$ is a chart. This implies that  (<ref>) is a sheaf isomorphism. In other words,

\[
\widetilde{\CO}_3(U_1\times U_2)=\CO_3(U_1\times U_2)
\]

for all open subsets $U_1$ of $M_1$. Thus $\widetilde{\CO}_3=\CO_3$, and   $(M_3, \CO_3)$ is a formal manifold by Lemma <ref>.

The formal manifold $(M_3, \CO_3)$ is a product of $(M_1, \CO_1)$ and $(M_2, \CO_2)$ in the category of formal manifolds.

Theorem <ref>,
for every formal manifold $(M, \CO)$ we have that

\begin{eqnarray*}
&& \mathrm{Mor}((M, \CO), (M_3, \CO_3))\\
&=& \Hom(\CO_3(M_3), \CO(M))\\
&=& \Hom(\CO_1(M_1)\widehat \otimes \CO_2(M_2), \CO(M))\\
&=& \Hom(\CO_1(M_1), \CO(M))\times \Hom(\CO_2(M_2), \CO(M)) \\
&=& \mathrm{Mor}((M, \CO), (M_1, \CO_1))\times \mathrm{Mor}((M, \CO), (M_2, \CO_2)).
\end{eqnarray*}

Here $\mathrm{Mor}$ indicates the set of morphisms between two formal manifolds, and $\Hom$ indicates the set of continuous $\BC$-algebra homomorphisms.
This proves the lemma.

In the category of smooth manifolds, we have that

\[
(M_3,\underline{\CO_{3}})=(M_1, \underline{\CO_{1}}) \times (M_2, \underline{\CO_{2}}).
\]

Let $U_1\subset M_1$ and $U_2\subset M_2$ be open subsets, and set $U_3:=U_1\times U_2$.
Recall from Example <ref> that  the reduction assignment

\[
(M, \CO)\mapsto (M, \underline \CO)
\]

is  a functor from the category of formal manifolds to the category of smooth manifolds.
Thus the projection morphisms
$(U_3,\CO_{3}|_{U_3})\rightarrow (U_1, \CO_{1}|_{U_1})$ and
$(U_3,\CO_{3}|_{U_3})\rightarrow (U_2, \CO_{2}|_{U_2})$ induce respectively the smooth maps

\[
(U_3,\underline{\CO_{3}|_{U_3}})=(U_3,\underline{\CO_3}|_{U_3})\rightarrow (U_1,\underline{\CO_{1}|_{U_1}})=(U_1,\underline{\CO_1}|_{U_1})\]

\[
(U_3,\underline{\CO_{3}|_{U_3}})=(U_3,\underline{\CO_3}|_{U_3})\rightarrow (U_2,\underline{\CO_{2}|_{U_2}})=(U_2,\underline{\CO_2}|_{U_2}).
\]

These two smooth maps produce a smooth map

(U_3,_3|_U_3)→(U_1, _1|_U_1) ×(U_2, _2|_U_2).
When $U_1$ and $U_2$ are charts, it follows from Lemma <ref> that the smooth map (<ref>) is a
This implies  that the   map (<ref>) is a
diffeomorphism when $U_1=M_1$ and $U_2=M_2$.

For every $a_1\in M_1$ and $a_2\in M_2$, we have topological algebra  identifications

\[
\wh{\CO}_{3,a_3}=\wh{\CO}_{1,a_1}\wh{\otimes}\,\wh{\CO}_{2,a_2}=\wh{\CO}_{1,a_1}\wt{\otimes}\,\wh{\CO}_{2,a_2}\qquad (a_3:=(a_1,a_2)).
\]

The projection morphisms $(M_3,\CO_{3})\rightarrow (M_1, \CO_{1})$ and $(M_3,\CO_{3})\rightarrow (M_2, \CO_{2})$ induce
respectively the continuous homomorphisms (see Lemma <ref>)

\[
\wh{\CO}_{1,a_1}\rightarrow \wh{\CO}_{3,a_3} \quad\textrm{and}\quad \wh{\CO}_{2,a_2}\rightarrow \wh{\CO}_{3,a_3}.
\]

Since $\wh{\CO}_{3,a_3}$ is complete, the above two maps yield a continuous homomorphism

_1,a_1⊗  _2,a_2→_3,a_3.

Note that we may (and do) assume that  $(M_1, \CO_{1})=(\R^{n_1},\CO_{\R^{n_1}}^{(k_1)})$ and  $(M_2, \CO_{2})=(\R^{n_2},\CO_{\R^{n_2}}^{(k_2)})$
for some $n_1,n_2,k_1,k_2\in \BN$.
Then by Lemma <ref> we see that

\[(M_3, \CO_{3})=(\R^{n_3},\CO_{\R^{n_3}}^{(k_3)})\quad (n_3:=n_1+n_2,\ k_3:=k_1+k_2).\]

For  $i=1,2,3$, Taylor expansion at $a_i$ yields a topological algebra isomorphism (see  Proposition <ref> and its proof)

\[\wh{\CO}_{i,a_i}\cong \C[[x_1,x_2,\dots,x_{n_i},y_1,y_2,\dots,y_{k_i}]].\]

This, together with Example <ref>,  implies that $\wh{\CO}_{1,a_1}\wh{\otimes}\,\wh{\CO}_{2,a_2}$ $=\wh{\CO}_{1,a_1}\wt{\otimes}\,\wh{\CO}_{2,a_2}$, and that
the map (<ref>) is a topological algebra isomorphism.

Theorem <ref> is now proved by combining Lemmas   <ref>, <ref>, <ref> and <ref>.

§ COMPACTLY SUPPORTED FORMAL DENSITIES

In this section, let $\CF$ be a sheaf of $\CO$-modules.
Associated to $\CF$, we introduce a cosheaf
$\mathrm{D}^\infty_c(\CF)$ of $\CO$-modules over $M$, which generalizes the concept of cosheaves of compactly supported smooth densities on smooth manifolds.

§.§ The cosheaf $\mathrm{D}^\infty_c(\CF)$

Recall that the reduction $\underline{M}$
of $M$ is a smooth manifold (see Example <ref>).
Write $\underline{\mathcal{D}}$ for the sheaf of all (complex-valued) smooth densities on $\underline{M}$ (<cit.>).
Via the reduction map $\underline{M}\rightarrow M$ (see (<ref>)), $\underline{\mathcal{D}}$ is naturally a sheaf of $\CO$-modules.

Then we have a linear  map

\begin{equation}\begin{split}\label{eq:defcomsuppden}
\rho_U:\ \mathrm{Diff}_{c}(\CF|_U,\underline{\mathcal{D}}|_U)&\rightarrow \mathrm{Hom}_\C(\CF(U),\C),\\
D&\mapsto \left(u\mapsto  \int_{U} D(u)\right)
\end{split}\end{equation}
for every open subset $U$ of $M$, where $\mathrm{Diff}_{c}(\CF|_U,\underline{\mathcal{D}}|_U)$ is the space of all compactly supported differential operators (see (<ref>)).

For every $D\in \mathrm{Diff}_c(\CF|_U,\underline{\mathcal{D}}|_U)$,
it is clear that the linear functional $\rho_U(D)$ on $\CF(U)$ is continuous, where $\CF(U)$ is equipped
with the smooth topology (see Definition <ref>).
D^∞_c(U;):=ρ_U(Diff_c(|_U,𝒟|_U))⊂((U))'.Here $(\CF(U))'$ is the space of all continuous linear maps from $\CF(U)$ to $\BC$.

As stated in the Introduction, we make the following definition.

An element in $\mathrm{D}^\infty_c(M;\CO)$
is called a compactly supported formal density on $M$.

When $M$ is a smooth manifold, we will show in  Proposition <ref> that $\mathrm{D}^\infty_c(M;\CO)$
is nothing but the space of compactly supported smooth densities on $M$.

Let $V\subset U$ be open subsets  of $M$. Then
the transpose
\[{}^t\mathrm{res}_{V,U}: (\CF(V))'\rightarrow (\CF(U))'\]
of the restriction map $\mathrm{res}_{V,U}:\CF(U)\rightarrow \CF(V)$
yields an injective linear map
ext_U,V:=^tres_V,U|_D^∞_c(V;):  D^∞_c(V;)→D^∞_c(U;).
Let $D\in \mathrm{Diff}_{c}(\CF|_V,\underline{\mathcal{D}}|_V)$. Recall from (<ref>) that we have the extension map
\[\mathrm{ext}_{U,V}: \mathrm{Diff}_{c}(\CF|_V,\underline{\mathcal{D}}|_V) \rightarrow \mathrm{Diff}_{c}(\CF|_U,\underline{\mathcal{D}}|_U).\]

\begin{eqnarray*}\la\rho_U(\mathrm{ext}_{U,V}(D)),u\ra
&=&\int_U \mathrm{ext}_{U,V}(D)(u)
=\int_V D(u|_V)\\
&=&\la \rho_V(D), u|_V\ra \\ &=& \la {}^t\mathrm{res}_{V,U}(\rho_V(D)),u \ra
\end{eqnarray*}
for every $u\in \CF(U)$. It follows that
the map (<ref>) is well-defined and  satisfies the relation

To see the injectivity of (<ref>),
assume  that $\mathrm{ext}_{U,V}(\rho_V(D))=0$.
Take an open neighborhood $W$  of $\mathrm{supp}\,D$ in $V$ such that
$\overline{W}\subset  V$, where $\overline{W}$ is the closure of $W$ in $U$.
Let $v$ be a section in $\CF(V)$, and let $f$ be a  formal  function on $U$ such that
\[f|_{\overline{W}}=1 \quad \text{and}\quad  \mathrm{supp}\,f\subset V.\]

Then we have a section $fv\in \CF(U)$ as in (<ref>).
By  (<ref>), we have that

\begin{eqnarray*}\la\rho_V(D),v\ra&=&\int_V D(v)=\int_W D(v)|_W \\&=&
\int_U(\mathrm{ext}_{U,V}(D))(fv)
&=&\la \mathrm{ext}_{U,V}(\rho_V(D)),fv\ra=0.
\end{eqnarray*}
This finishes the proof.

With (<ref>) as the extension maps,
the assignment
U↦D^∞_c(U; )  ($U$ is an open subset of $M$)forms a precosheaf of complex vector spaces on $M$ (see <cit.>), which we denote as $\mathrm{D}^\infty_c(\CF)$. Recall that a precosheaf $\CG$ over $M$ is called flabby if the extension map
\[\mathrm{ext}_{U,V}: \CG(V)\rightarrow \CG(U)\]
is injective for all open sets $V\subset U$ of $M$ (see <cit.>).
Then Lemma <ref> implies that the precosheaf  $\mathrm{D}^\infty_c(\CF)$ is flabby.

Recall from Section <ref> that $\mathcal{D}\mathrm{iff}_c(\CF,\underline{\mathcal{D}})$ is a cosheaf over $M$.
From (<ref>), one  concludes that the family

ρ={ρ_U}_$U$ is an open subset of $M$:  𝒟iff_c(,𝒟)
→D^∞_c()is a  homomorphism of precosheaves.
The following result shows that $\rho$ is in fact a homomorphism of cosheaves.

The precosheaf  $\mathrm{D}^\infty_c(\CF)$ is a  cosheaf.

The rest of this subsection is devoted to a proof of Proposition <ref>.
Let $U_1$ and $U_2$ be two open subsets of $M$, and set $U:=U_1\cup U_2$.
We consider the  map

\[\begin{array}{rcl}
\phi:\,\mathrm{D}^\infty_c(U_1;\CF)\oplus \mathrm{D}^\infty_c(U_2;\CF) &\rightarrow& \mathrm{D}^\infty_c(U;\CF),\\(\eta_1,\eta_2)
\mathrm{ext}_{U,U_2}(\eta_2).
\end{array}
\]

Fix an element
η=(η_1,η_2)∈ϕ,and  choose a differential operator $D_i\in \mathrm{Diff}_c(\CF|_{U_i},\underline{\mathcal{D}}|_{U_i})$ such
that $\eta_i=\rho_{U_i}(D_i)$ for each $i=1,2$.
Set $K:=\mathrm{supp}\, D_1\cap \mathrm{supp}\, D_2$.

Let $i\in\{1,2\}$. If $u_i\in \CF(U_i)$  satisfies that $\mathrm{supp}\,u_i\cap K=\emptyset$, then $\la \eta_i,u_i\ra=0$.

Without loss of generality, suppose that $i=1$. Set
\[K_1:=\mathrm{supp}\,u_1\cap \mathrm{supp}\,D_1\quad\text{and}\quad  K_2:=\mathrm{supp}\,u_1\cap \mathrm{supp}\,D_2.\]

Since $K_1$ is compact in $U_1$ and $K_1\cap K_2\subset \mathrm{supp}\,u_1\cap K=\emptyset$, there are
open neighborhoods $U'$ and $U''$ of $K_1$ in $U_1$ such that
\[\overline{U'}
\subset U''\quad \text{and} \quad U''\cap K_2=\emptyset.\]
Here $\overline{U'}$ is the closure of $U'$ in $U$.
Let $f$ be a
formal function  on $U$ such that
\[f|_{\overline{U'}}=1 \quad \text{and} \quad f|_{U\setminus U''}=0.\]

This yields an element $fu_1\in\CF(U)$ as in (<ref>).
Then we have that

\begin{eqnarray*}
&&\la \eta_1, u_1\ra=\la\rho_{U_1}(D_1),u_1\ra\\
&=& \int_{U_1} D_1(u_1)
=\int_{U'} (D_1(u_1))|_{U'}\,\,\,\quad \quad \quad  \quad \quad (\text{as $\mathrm{supp}\,D_1(u_1) \subset K_1\subset U'$})\\
\int_U (\mathrm{ext}_{U,U_1}(D_1))(fu_1)\, \,\,\, \quad\quad \quad \quad\quad\quad \quad\quad (\text{as  $(fu_1)|_{U'}=u_1|_{U'}$})\\
&=& \la\rho_{U}(\mathrm{ext}_{U,U_1}(D_1)),fu_1\ra\quad \\
\la \rho_{U}(\mathrm{ext}_{U,U_1}(D_1)+\mathrm{ext}_{U,U_2}(D_2)), fu_1\ra \quad \,\quad(\text{as $\mathrm{supp}\,(fu_1)\cap \mathrm{supp}\,D_2=\emptyset$})\\
&=& \la \phi((\rho_U(D_1),\rho_U(D_2))),fu_1\ra\quad\quad \quad \quad \quad \quad \,\,(\text{by \eqref{eq:cosheafhom}})\\
&=&\la \phi(\eta),fu_1\ra=0,
\end{eqnarray*}

which proves the lemma.

Set $V:=U_1\cap U_2$. For each $i=1,2$, take an
open subset $V_i$ of $U_i$ such that

\[
K\subset V_i\subset \overline{V_i}\subset V\subset U_i\quad (\overline{V_i}\ \text{is the closure of}\ V_i\ \text{in}\ U_i).\]

Let $\{g_i,g_i'\}$ be a partition of unity on $U_i$ subordinate to the open cover $\{V, U_i\setminus \overline{V_i}\}$.
It is clear that $D_i\circ g_i \in \mathrm{Diff}_c(\CF|_{U_i},\underline {\mathcal{D}}|_{U_i} )$, where $D_i\circ g_i$ is defined as in (<ref>).
\[D_i':=(D_i\circ g_i)|_V \in \mathrm{Diff}_c(\CF|_V,\underline{\mathcal{D}}|_V)\quad \text{and}\quad  \eta'_i:=\rho_{V}(D_i')\in \mathrm{D}^\infty_c(V;\CF).\]

We have   that $\eta'_1+\eta'_2=0$, and $\eta_i=\mathrm{ext}_{U_i,V}(\eta'_i)$ for $i=1,2$.

For every $u_i'\in \CF(U_i)$,
$$\mathrm{supp}\,(g_i'u_i')\cap K=\emptyset, $$
follows from Lemma <ref> that $\la \eta_i, g_i'u_i'\ra=0$.
Together with the fact that $\mathrm{supp}\,g_i\subset V$, we have that

\begin{eqnarray*}
\la \eta_i, u_i'\ra &=&\la \eta_i, (g_i+g_i')u_i'\ra=\la \eta_i,g_iu_i'\ra\\&=& \int_{U_i} D_i(g_iu_i')
= \int_V D_i'(u_i'|_V)
\\ &=&\la \eta'_i,u_i'|_V\ra=\la \mathrm{ext}_{U_i,V}(\eta'_i), u_i'\ra.
\end{eqnarray*}

This implies  that $\eta_i=\mathrm{ext}_{U_i,V}(\eta'_i)$. Moreover, we have the following equalities:

\begin{eqnarray*}
\mathrm{ext}_{U,V}(\eta'_1+\eta'_2)
\\ &=&\phi(\eta)=0.
\end{eqnarray*}

Then the flabby property of $\mathrm{D}^\infty_c(\CF)$ forces that $\eta'_1+\eta'_2=0$, as required.

Mayer-Vietoris sequence
⊕D^∞_c(U_2; ) D^∞_c(U;)→0
in $\mathrm{D}^\infty_c(\CF)$ is exact, where $\psi:=(\mathrm{ext}_{U_1,V},-\mathrm{ext}_{U_2,V})$.

As $\mathcal{D}\mathrm{iff}_c(\CF,\underline{\mathcal{D}})$ is a cosheaf, the Mayer-Vietoris sequence

\[
\mathrm{Diff}_c(\CF|_V,\underline{\mathcal{D}}|_V)\rightarrow\mathrm{Diff}_c(\CF|_{U_1},\underline{\mathcal{D}}|_{U_1})
\oplus \mathrm{Diff}_c(\CF|_{U_2},\underline{\mathcal{D}}|_{U_2})\rightarrow \mathrm{Diff}_c(\CF|_U,\underline{\mathcal{D}}|_U)\rightarrow 0
\]
in $\mathcal{D}\mathrm{iff}_c(\CF,\underline{\mathcal{D}})$ is exact (see <cit.>). Using
the homomorphism $\rho$, it follows
that $\phi$ is surjective and $\phi\circ \psi=0$. On the other hand, we have  that $\ker\phi\subset \mathrm{im}\, \psi$ by Lemma <ref>. This finishes the proof.

Let $\{U_\alpha\}_{\alpha\in \Gamma}$ be a family   of open subsets of $M$ directed upwards by inclusions. Then
the canonical map

_α∈Γ D^∞_c(U_α; )→D^∞_c(∪_α∈ΓU_α; )
is a linear isomorphism.

As $\mathcal{D}\mathrm{iff}_c(\CF,\underline{\mathcal{D}})$ is a cosheaf, the canonical map
\[\varinjlim_{\alpha\in \Gamma}\mathrm{Diff}_c(\CF|_{U_{\alpha}},\underline{\mathcal{D}}|_{U_{\alpha}})\rightarrow\mathrm{Diff}_c(\CF|_{\cup_{\alpha\in \Gamma}U_{\alpha}},\underline{\mathcal{D}}|_{\cup_{\alpha\in \Gamma}U_{\alpha}})\]
is a linear isomorphism (see <cit.>).
Using the homomorphism $\rho$, it then follows
that the map (<ref>) is surjective.
On the other hand, the injectivity of (<ref>) follows from the flabby property of $\mathrm{D}^\infty_c(\CF)$, as required.

Finally,  by <cit.>, Proposition <ref> is implied by Lemmas <ref> and <ref>.

§.§ The topology on $\mathrm{D}^\infty_c(M;\CF)$

In this subsection, we define an
inductive limit topology on   $\mathrm{D}^\infty_c(M; \CF)$.

We first endow a locally convex topology  on the space $\mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$ of finite order differential
operators (see Definition <ref>).
Let  $X\in \mathrm{Diff}_c(\underline{\mathcal{D}},\underline{\CO})$ and $u\in \CF(M)$.
For every $D\in \mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$, define

\[
\abs{D}_{X,u}:=\sup_{a\in M}|((X\circ D)(u))(a)|.
\]

Then $\abs{\,\cdot\,}_{X,u}$ is a seminorm on $\mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$, and
$\mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$ becomes an LCS with the topology defined by all such seminorms.

Equip $\underline{\mathcal{D}}(M)$ with the smooth topology (see Definition <ref>).
Then we have the following straightforward result.

A net $\{D_i\}_{i\in I}$  in $\mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$
converges to $0$ if and only if $\{D_i(u)\}_{i\in I}$ converges to $0$ in $\underline{\mathcal{D}}(M)$ for all $u\in \CF(M)$.
Moreover, the topology
on $\mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$ is Hausdorff.

There is a  directed set $(\mathcal{C}(M),\preceq)$, where
𝒞(M):={(K,r)|$K$ is a compact subset of $M$ and $r\in \BN$},and for two pairs $(K,r),(K',r')\in \mathcal{C}(M)$,

\[\text{$(K,r)\preceq(K',r')$ if and only if $K\subset K'$ and $r\le r'$.}\]

For  $(K,r)\in \mathcal{C}(M)$, define

\[\mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}}):=\mathrm{Diff}_K(\CF,\underline{\mathcal{D}})\cap
\mathrm{Diff}_r(\CF,\underline{\mathcal{D}}),\]

where $\mathrm{Diff}_K(\CF,\underline{\mathcal{D}})$ denotes the subspace of $\mathrm{Diff}_c(\CF,\underline{\mathcal{D}})$  consisting of all the
differential operators supported in $K$.
Equip $\mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}})$ with the subspace topology of $\mathrm{Diff}_{\mathrm{fin}}(\CF,\underline{\mathcal{D}})$.

\[\mathrm{D}^\infty_{K,r}(M;\CF):=\rho_M(\mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}}))\subset \mathrm{D}^\infty_{c}(M;\CF),\]

which is endowed with the quotient topology of $\mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}})$.
Then $\mathrm{D}^\infty_{K,r}(M;\CF)$ becomes an LCS.
We equip $\mathrm{D}^\infty_c(M;\CF)$ with the inductive limit topology  of  the  directed system

\[\{\mathrm{D}^\infty_{K,r}(M;\CF)\}_{(K,r)\in \mathcal{C}(M)}\]

of LCS.

For every $(K,r)\in \mathcal{C}(M)$, the LCS $\mathrm{D}^\infty_{K,r}(M;\CF)$ is Hausdorff, and the LCS $\mathrm{D}^\infty_{c}(M;\CF)$ is also Hausdorff provided that the inductive limit

\[
\varinjlim_{(K,r)\in \mathcal{C}(M)}
\mathrm{D}^\infty_{K,r}(M;\CF)
\]
is strict (see Definition <ref>).

By Lemma <ref>,  it is easy to see that the subspace $\ker \rho_M\cap \mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}})$
is closed in $\mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}})$ for every $(K,r)\in \mathcal{C}(M)$.
This implies that the LCS $\mathrm{D}^\infty_{K,r}(M;\CF)$ is Hausdorff.

By definition, we have that

as LCS.
Then by Lemma <ref> (b), the LCS $\mathrm{D}^\infty_c(M;\CF)$ is  Hausdorff.

Let $U$ be an open subset of $M$. Then the extension map
ext_M,U: D^∞_c(U;)→D^∞_c(M;)
is continuous.

Let $(K,r)\in \mathcal{C}(U)$. Note that the extension map $\mathrm{ext}_{M,U}$ on $\mathrm{Diff}_{c}(\CF|_U,\underline{\mathcal{D}}|_U)$ induces a linear map

Then by taking the restriction, (<ref>) yields a linear map D^∞_K,r(U;)→D^∞_K,r(M;).

Let $f$ be a formal function on $M$ such that $\mathrm{supp}\,f\subset U$ and $f|_K=1$.
Note that

\[
\abs{\mathrm{ext}_{M,U}(D)}_{X,u}
=\abs{D}_{(f\circ X)|_U,u|_U}\quad \text{for all $D\in  \mathrm{Diff}_{K,r}(\CF|_U,\underline{\mathcal{D}}|_U)$},
\]

where $X\in \mathrm{Diff}_c(\underline{\mathcal{D}},\underline{\mathcal{O}})$, $u\in \CF(M)$, and $f\circ X$ is as in (<ref>).
Thus the map (<ref>) is continuous, and so is the map (<ref>).
Therefore,  the composition of

\[\mathrm{D}^\infty_{K,r}(U;\CF)\rightarrow \mathrm{D}^\infty_{K,r}(M;\CF)\rightarrow \mathrm{D}^\infty_c(M;\CF)
\]

is continuous as well.
The lemma then follows.

Recall the definition of a cosheaf of $\mathcal{O}$-modules on $M$ from Section <ref>.
In what follows, we give a canonical $\CO$-module structure on the cosheaf $\mathrm{D}^\infty_{c}(\CF)$.
For every open subset $U$ of $M$, we have a natural $\CO(U)$-structure on the space $(\CF(U))'$ with

(U)×((U))' →((U))',  (f,η)↦η∘f,
where $\eta\circ f$ is the map
η∘f:   (U)→,   u↦η(fu).   Let $\eta\in \mathrm{D}^\infty_{c}(U;\CF)$ and $f\in \CO(U)$.
Then the linear functional $\eta\circ f$
lies in $\mathrm{D}^\infty_{c}(U;\CF)$.

Choose a differential operator $D\in \mathrm{Diff}_c(\CF|_U,\underline{\mathcal{D}}|_U)$ such that
The lemma follows from the fact that $\eta\circ f=\rho_U(D\circ f)$. Here $D\circ f\in \mathrm{Diff}_c(\CF|_U,\underline{\mathcal{D}}|_U)$ is defined as in (<ref>).

Lemma <ref> and (<ref>), there is an $\CO$-module structure on the cosheaf $\mathrm{D}^\infty_{c}(\CF)$
transferred from that on $\CF$.
On the other hand,  the  $\CO$-module structure  (<ref>) on $\mathcal{D}\mathrm{iff}(\CF,\underline{\mathcal{D}})$ induces
an  $\CO$-module structure on  $\mathcal{D}\mathrm{iff}_c(\CF,\underline{\mathcal{D}})$.
It is obvious that $\rho$ (see (<ref>))  is an $\CO$-module homomorphism of cosheaves.

Let $(K,r)\in \mathcal{C}(M)$, $U$ an open subset of $M$, and $f$ a formal function on $M$ supported in $U$.
Then for every $\eta\in\mathrm{D}^\infty_{K,r}(M;\CF)$, there is a unique element  (η∘f)|_U∈D^∞_suppf∩K,r(U;)such that
$\mathrm{ext}_{M,U}((\eta\circ f)|_U)=\eta\circ f$. Furthermore, the linear map
m_f: D^∞_c(M;)→D^∞_c(U;),  η↦(η∘f)|_U
is continuous.

The uniqueness follows from the flabby property of $\mathrm{D}^{\infty}_{c}(\CF)$ (see Lemma <ref>).
Choose  $D\in \mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}})$ such that $\eta=\rho_M(D)$.
Note that
\[
(D\circ  f)|_U\in  \mathrm{Diff}_{\mathrm{supp}f\cap K,r}(\CF|_U,\underline{\mathcal{D}}|_U),\]

where $D\circ f$ is defined as in (<ref>).
By using the fact that $\rho$ is an $\CO$-module homomorphism of cosheaves,
the first assertion then follows by setting (η∘f)|_U:=ρ_U((D∘f)|_U).

For the second one, we first prove that the map

m_f: Diff_K,r(,𝒟)→Diff_K∩supp f,r(|_U,𝒟|_U),  D↦(D ∘f)|_Uis continuous.
Let $X\in \mathrm{Diff}_c(\underline{\mathcal{D}}|_U,
\underline{\CO}|_U)$, $u\in \CF(U)$, and let $g$ be a formal function  on $M$ such that
\[\mathrm{supp}\,g\subset U \quad \text{and} \quad g|_{\mathrm{supp}\,f}=1.\]

Then we have an element
$u':=fgu\in \CF(M)$
as in (<ref>), as well as an element
\[X':= \mathrm{ext}_{M,U}(X)\in \mathrm{Diff}_c(\underline{\mathcal{D}},\underline{\CO}).\]

For every $D\in \mathrm{Diff}_{K,r}(\CF,\underline{\mathcal{D}})$, we have that

\begin{eqnarray*}
(X'\circ D)(u')&=&X'(D(fgu))=X'((D\circ f)(gu))\\
&=&(\mathrm{ext}_{M,U}(X))(\mathrm{ext}_{M,U}((D\circ f)|_U(u))\\
&=&\mathrm{ext}_{M,U} ((X\circ (D\circ f)|_U)(u)).
\end{eqnarray*}

Consequently, we obtain that

\begin{eqnarray*}
|D|_{X',u'}&=&\sup_{a\in K}|((X'\circ D)(u'))(a)|\\
&=&\sup_{a\in K\cap \mathrm{supp}f}|((X\circ (D\circ f)|_U)(u))(a)|\\
\end{eqnarray*}

This implies that (<ref>) is continuous.

From (<ref>) and the continuity of (<ref>), one concludes that the map
m_f: D^∞_K,r(M;)→D^∞_suppf∩K,r(U;),  η↦(η∘f)|_U
is continuous, and so is the composition of

\[
\mathrm{D}^\infty_{K,r}(M;\CF)\xrightarrow{m_f} \mathrm{D}^\infty_{\mathrm{supp}f\cap K,r}(U;\CF)\rightarrow
\mathrm{D}^\infty_{c}(U;\CF).
\]

This implies that
(<ref>) is continuous, and we complete the proof.

We refer to Sections <ref> and <ref> for the following usual notations:

\[
\CL_b(E,F),\quad\CL_c(E,F),\quad E_b',\quad E_c'\quad \text{($E$ and $F$ are LCS)},
\]

which are used to denote various LCS of continuous linear maps.
Let $f: E\rightarrow F$
be a continuous linear map. Note that the transposes
^tf:  _b(F,G)→_b(E,G) and ^tf:  _c(F,G)→_c(E,G)
are continuous,where $G$ is another LCS (<cit.>). Together with  Lemma <ref>,
the following result is clear.
Let $U$ be an open subset of $M$, and let $f$ be  a formal function on $M$ supported in $U$.
Then the linear map
T_f: _c(D^∞_c(U;),D^∞_c(U;))

ϕ   ↦ext_M,U∘ϕ∘m_f
is continuous. Here $m_f$ is defined as in (<ref>).

Let $(K,r)\in \mathcal{C}(M)$.  Take a finite family $\{U_i\}_{i=1}^s$ of open subsets   of $M$ that covers  $K$, and
take a family $\{f_i\}_{i=1}^s$ of formal functions on $M$ such that

\[\text{$\mathrm{supp}\,f_i\subset U_i$ for all $i=1,2,\dots,s$,\quad and\quad
$\sum_{i=1}^s f_i|_K=1$.}\]

Recall from the proof of Lemma <ref> that the linear map (<ref>) is continuous. Then there is a continuous linear map

⊕_i=1^s D^∞_K_i,r(U_i;)   →D^∞_K,r(M;),

(η_1,η_2,…,η_s)   ↦∑_i=1^s ext_M,U_i(η_i),
where $K_i:=\mathrm{supp}\,f_i\cap K$ for all $i=1,2,\dots,s$. On the other hand, recall also from the proof of Lemma <ref> that the linear map (<ref>) is continuous. Then there is  another continuous linear map

D^∞_K,r(M;)   →⊕_i=1^s D^∞_K_i,r(U_i;),

η   ↦((η∘f_1)|_U_1,(η∘f_2)|_U_2,…,(η∘f_s)|_U_s).

The following result is straightforward.

The continuous linear map (<ref>) is a right inverse of
In particular, the continuous linear map  (<ref>) is open and surjective, and (<ref>) is a topological embedding.

Furthermore, we have the following result.

For every  open cover  $\{U_\alpha\}_{\alpha\in \Gamma}$  of $M$,
the canonical map

→D^∞_c(M;),  {η_α}_α∈Γ↦∑_α∈Γ
has a continuous linear right inverse. In particular, the linear map
is continuous, open and surjective.

Take a  partition of unity $\{f_\alpha\}_{\alpha\in \Gamma}$ on $M$ subordinate to  the cover $\{U_\alpha\}_{\alpha\in \Gamma}$.
It is easy to see that the linear map
D^∞_c(M;) →⊕_α∈Γ
D^∞_c(U_α;),  η↦{(η∘f_α)|_U_α}_α∈Γ
is a  right inverse of (<ref>).
Thus, it suffices to prove that (<ref>) is continuous.

For every $(K,r)\in \mathcal{C}(M)$ and $\alpha\in \Gamma$, write

\[
K_{\alpha}:=\mathrm{supp}\,f_\alpha\cap K\quad\text{and}\quad \Gamma_K:=\{\alpha\in \Gamma\mid K_{\alpha}\ne \emptyset\}.
\]

As in (<ref>), there is a continuous linear map

\[
\mathrm{D}^\infty_{K,r}(M;\CF)\rightarrow \bigoplus_{\alpha\in \Gamma_K} \mathrm{D}^\infty_{K_{\alpha}, r}(U_{\alpha};\CF),\quad \eta\mapsto \{(\eta\circ f_\alpha)|_{U_\alpha}\}_{\alpha\in \Gamma_K}.\]

This implies that the restriction of (<ref>) on $\mathrm{D}^\infty_{K,r}(M;\CF)$ is continuous, and so is the map (<ref>), as required.

The following result is a by-product of Proposition <ref>.

There is an identification

as LCS.

§.§ Compactly supported formal densities

Let $N$ be a smooth manifold and $k\in \BN$.
In this subsection, we suppose that  $(M,\CO)=(N,\CO_N^{(k)})$, and we will give  a description of the LCS $\mathrm{D}^\infty_{c}(M;\CO)$ (see Propositions <ref>).
Particularly, if $k=0$, it follows  that  $\mathrm{D}^\infty_{c}(M;\CO)$ is exactly the space of  compactly supported (complex-valued) smooth densities on $N$.
This justifies  Definition  <ref>.

Write  $\mathrm{D}_c^\infty(N)$ for the space of all compactly supported (complex-valued) smooth densities on $N$.
With the obvious  extension maps, the assignment

\[\mathcal{D}^{(k)}_{N,c}:\ U\mapsto \mathrm{D}^\infty_c(U)[y_1^*,y_2^*,\dots,y_k^*]\quad (\text{$U$ is an open subset of $N$})\]

forms a cosheaf of complex vector spaces over $N$. For every open subset $U$ of $N$, there is a   non-degenerate pairing
_N^(k)(U)×𝒟_N,c^(k)(U)→given by
∑_J∈^k f_J y^J,
τ·(y^*)^L= L! ·∫_U f_Lτ,where $f_J\in \mathrm{C}^\infty(U)$, $\tau\in \mathrm{D}^\infty_c(U)$, and
\[(y^*)^L=(y_1^*)^{l_1}(y_2^*)^{l_2}\cdots(y_k^*)^{l_k}\]
for every $L=(l_1,l_2,\dots,l_k)\in\BN^k$.

For every open subset $U$ of $N$, we view $\mathcal{D}_{N,c}^{(k)}(U)$ as a subspace of $(\CO_N^{(k)}(U))'$ through the pairing (<ref>).
On the other hand, recall that
$\mathrm{D}_c^{\infty}(U;\CO)$ is also a subspace of $(\CO(U))'=(\CO_N^{(k)}(U))'$ (see (<ref>)).
We have the following result.

Suppose that $M=N^{(k)}$ as above. Then
$\mathrm{D}^\infty_{c}(\CO)=\mathcal{D}_{N,c}^{(k)}$ as cosheaves over $M$.

Note that  the extension maps   in the cosheaf $\mathcal{D}_{N,c}^{(k)}$
are compatible with the transposes of the restriction maps of the sheaf $\CO$.
Thus, it suffices to prove that for every open subset $U$ of $N$,
D^∞_c(U;)=𝒟_N,c^(k)(U)as linear subspaces of $(\CO(U))'$.

Due to the cosheaf property of $\mathrm{D}^\infty_{c}(\CO)$ and $\mathcal{D}_{N,c}^{(k)}$, it is enough to focus on the case that $N$ is an open submanifold of $\R^n$ for some  $n\in \BN$.
In this case, it is easy to check that the sheaf $\underline{\mathcal{D}}$ of $\CO$-modules  satisfies the two conditions in Proposition <ref>. It follows that

=⊕_I∈^n,J∈^k D^∞_c(U)∘∂_x^I∂_y^J.

For every $\tau\in \mathrm{D}^\infty_c(U)$,  $I\in \BN^n$, $L\in \BN^k$, and $f=\sum_{J\in \BN^k}f_J y^J\in \CO_{N}^{(k)}(U)$, we have that

ρ_U(τ∘∂_x^I∂_y^L), f   =
∫_U (τ∘∂_x^I∂_y^L)(f)

=L!·∫_U τ(∂_x^I(f_L))

=L!·τ∂_x^I, f_L
Here $\tau\partial_x^I$ denotes the element in $\RD^\infty_c(U)$ such that

\[\la \tau \partial_x^I, g\ra= \la \tau,  \partial_x^I g\ra\quad\]
for every $g\in\mathrm C^{\infty}(U)$.
Using  (<ref>), it follows  that
ρ_U(∑_I∈^n, L∈^k τ_I,L∘∂_x^I∂_y^L)=
∑_I∈^n, L∈^k (τ_I,L∂_x^I) (y^*)^L,where $\tau_{I,L}\in \mathrm{D}_c^{\infty}(U)$ for $I\in \BN^n, L\in \BN^k$.
This, together with (<ref>), shows that

\begin{eqnarray*}
\mathrm{D}^\infty_{c}(U;\CO)=\rho_U(\mathrm{Diff}_c(\CO|_U,\underline{\mathcal{D}}|_U))
=\mathrm{D}^\infty_c(U)[y^*_1,y^*_2,\dots,y^*_k]= \mathcal{D}_{N,c}^{(k)}(U)
\end{eqnarray*}

as linear subspaces of $(\CO(U))'$, as desired.

Similar to the space $\mathrm C^\infty(N)$,  the space $\mathrm{D}^\infty(N)$ of all smooth densities on $N$ is naturally an LCS under the smooth topology (see Definition <ref>).
For every compact subset $K$ of $N$, write $\mathrm{D}_K^\infty(N)$ for the space of all
smooth densities supported in $K$, which is equipped with the subspace topology of $\mathrm{D}^\infty(N)$. It is obvious that $\mathrm D_{K}^{\infty}(N)$ is a nuclear Fréchet space.

For every $(K,r)\in \mathcal{C}(N)$, equip $\mathrm{D}^\infty_K(N)[y^*_1,y^*_2,\dots,y^*_k]_{\le r}$  with the term-wise convergence topology (see Example
<ref>). Then $\mathrm{D}^\infty_K(N)[y^*_1,y^*_2,\dots,y^*_k]_{\le r}$  becomes a nuclear Fréchet space as well.

with the inductive limit topology. By Lemma <ref>, we have that

𝒟_N,c^(k)(N)=D^∞_c(N)⊗_i[y^*_1,y^*_2,…,y^*_k]=D^∞_c(N)⊗_i [y^*_1,y^*_2,…,y^*_k]as LCS.

The inductive limit of the directed system

\[\left\{\mathrm{D}^\infty_c(N)[y^*_1,y^*_2,\dots,y^*_k]_{\le r}\right\}_{r\in \BN}\]
defines another topology on $\mathcal{D}_{N,c}^{(k)}(N)$. By  Example  <ref> and (<ref>),
this topology coincides with the topology given by the inductive limit  (<ref>), and also agrees with  the inductive tensor product topology on
$\mathcal{D}_{N,c}^{(k)}(N)=\mathrm{D}^\infty_c(N)\otimes \C[y^*_1,y^*_2,\dots,y^*_k]$.

Assume that $M=N^{(k)}$ with $N$  a smooth manifold and $k\in \BN$.
Then for every $(K,r)\in \mathcal{C}(M)$, we have that

\begin{eqnarray}\label{eq:CONkUKr=}
\mathrm{D}^\infty_{K,r}(M;\CO)=\mathrm{D}^\infty_K(N)[y^*_1,y^*_2,\dots,y^*_k]_{\le r}
\end{eqnarray}

as LCS. Furthermore,
$\mathrm{D}^\infty_{c}(M;\CO)= \mathcal{D}_{N,c}^{(k)}(N)$ as LCS.

We only need to prove the LCS identification (<ref>).
Applying Lemma <ref>,  we may (and do) assume that  $N$ is an open submanifold of $\mathbb{R}^n$ ($n\in\BN$).
In such case,
the LCS identification (<ref>) is implied by (<ref>) and Lemma <ref>.

Suppose that  $\CF$ is locally free of finite rank. Then

* for every $(K,r)\in \mathcal{C}(M)$,
$\mathrm{D}^\infty_{K,r}(M;\CF)$ is a nuclear Fréchet space;

* when $M$ is secondly countable, $\mathrm{D}^\infty_{c}(M;\CF)$ is a nuclear LF space (see Definition <ref>); and

* in general, $\mathrm{D}^\infty_{c}(M;\CF)$ is a direct sum of nuclear LF spaces.

Take an atlas $\{U_\gamma\}_{\gamma\in \Gamma}$ of $M$ such that for every $\gamma\in \Gamma$,  $\CF|_{U_\gamma}$ is a free $\CO|_{U_\gamma}$-module of
finite rank $r_\gamma$.
For every $\gamma\in \Gamma$ and $(K',r')\in \mathcal{C}(U_{\gamma})$, we have that

=    ρ_U_γ(Diff_K',r'(|_U_γ,𝒟|_U_γ))≅ρ_U_γ(Diff_K',r'((|_U_γ)^r_γ,𝒟|_U_γ))

=    ρ_U_γ((Diff_K',r'(|_U_γ,𝒟|_U_γ))^ r_γ)
=(D^∞_K',r'(U_γ;))^ r_γ
as LCS. This together with (<ref>) implies that
D^∞_K',r'(U_γ;) is a nuclear Fréchet space.

Take a partition of unity $\{f_\gamma\}_{\gamma\in \Gamma}$ on $M$ subordinate to  $\{U_\gamma\}_{\gamma\in \Gamma}$.
For every $(K,r)\in \mathcal{C}(M)$, it follows from Lemma <ref> that there is a surjective, open and continuous linear map

⊕_γ∈Γ_K D^∞_K_γ,r(U_γ;)
as well as a linear topological embedding

\[
\iota_{K,r}:\ \mathrm{D}^\infty_{K,r}(M;\CF)\rightarrow
\bigoplus_{\gamma\in \Gamma_K} \mathrm{D}^\infty_{K_\gamma,r}(U_\gamma;\CF),\quad
\eta\mapsto  \{ (\eta\circ f_\gamma)|_{U_\gamma}\}_{\gamma\in \Gamma_K},
\]

$K_\gamma:=K\cap \mathrm{supp}\,f_\gamma$ and $ \Gamma_K:=\{\gamma\in \Gamma\mid K_\gamma\ne \emptyset\}$.

We claim that

the inductive limit _(K,r)∈𝒞(M) D^∞_K,r(M;) is strict.
let $(K_1,r_1)$ and $(K_2,r_2)$ be two pairs in $\mathcal{C}(M)$ such that $(K_1,r_1)\preceq (K_2,r_2)$.
Then we have the following commutative diagram:

\[
\begin{CD}
\bigoplus\limits_{\gamma\in \Gamma_{K_1}} \mathrm{D}^\infty_{K_{1,\gamma},r_1}(U_\gamma;\CF)@>  >>  \bigoplus\limits_{\gamma\in \Gamma_{K_2}} \mathrm{D}^\infty_{K_{2,\gamma},r_2}(U_\gamma;\CF)\\
@A \iota_{K_1,r_1}    AA
@AA  \iota_{K_2,r_2} A\\
\mathrm D^{\infty}_{K_1,r_1}(M;\CF) @ >> >
\mathrm D^{\infty}_{K_2,r_2}(M;\CF).
\end{CD}
\]

It follows from (<ref>) and (<ref>) that the top horizontal arrow is a  linear topological embedding.
This, together with the fact that both $\iota_{K_1,r_1}$ and $\iota_{K_2,r_2}$  are linear topological embeddings, implies that the bottom horizontal arrow is  also a linear topological embedding, as required.

By using (<ref>) and (<ref>),  we obtain  that $\mathrm{D}^\infty_{K,r}(M;\CF)$ is a nuclear Fréchet space for every $(K,r)\in \mathcal{C}(M)$.
Furthermore, in view of the claim (<ref>),
$\mathrm{D}^\infty_{c}(M;\CF)$ is  a nuclear LF space when $M$ is secondly countable, and in general,
$\mathrm{D}^\infty_{c}(M;\CF)$ is a direct sum of nuclear LF spaces by (<ref>).

Suppose that  $\CF$ is locally free of finite rank. Then the inductive limit
\[\varinjlim_{(K,r)\in \mathcal{C}(M)}\mathrm{D}^\infty_{K,r}(M;\CF)\]
is regular (see Definition <ref>).

The assertion follows from Proposition  <ref>  and Lemma <ref> (c).

Suppose  that  $\CF$  is  locally free of finite rank.
Then the LCS $\mathrm{D}^\infty_{c}(M;\CF)$ has the strict approximation property (see Definition <ref>).

Let $\{U_\gamma\}_{\gamma\in \Gamma}$ be an open cover of $M$ such that for every $\gamma\in \Gamma$,

* $(U_\gamma,\CO|_{U_\gamma})\cong (\R^{n_\gamma})^{(k_\gamma)}$ for some $n_\gamma,k_\gamma\in \BN$; and

* $\CF|_{U_\gamma}$ is a free $\CO|_{U_\gamma}$-module.

Then $\mathrm{D}^\infty_{c}(U_{\gamma};\CF)$ is a finite direct sum of some copies of $\RD^\infty_c(\R^{n_\gamma})[y_1^*,y_2^*,\dots,y_{k_\gamma}^*]$
(see Proposition <ref> and (<ref>)).
Thus, by Lemma <ref> and (<ref>),  $\mathrm{D}^\infty_{c}(U_{\gamma};\CF)$ has the strict approximation property for every $\gamma\in \Gamma$.

Take a partition of unity $\{f_\gamma\}_{\gamma\in \Gamma}$ on $M$ subordinate to the cover $\{U_\gamma\}_{\gamma\in \Gamma}$.
Let $A$ be the quasi-closure  (see Definition <ref>) of the subset $(\mathrm{D}^\infty_{c}(M;\CF))'\otimes \mathrm{D}^\infty_{c}(M;\CF)$ in $\CL_c(\mathrm{D}^\infty_c(M;\CF),\mathrm{D}^\infty_{c}(M;\CF))$.
Recall from (<ref>) the continuous linear map
\[T_{f_{\gamma}}:\ \CL_c(\mathrm{D}^\infty_{c}(U_{\gamma};\CF),\mathrm{D}^\infty_{c}(U_{\gamma};\CF))
\rightarrow \CL_c(\mathrm{D}^\infty_{c}(M;\CF),\mathrm{D}^\infty_{c}(M;\CF)). \]

Note that $T_{f_{\gamma}}$ maps $(\mathrm{D}^\infty_c(U_{\gamma};\CF))'\otimes \mathrm{D}^\infty_{c}(U_{\gamma};\CF)$
into $(\mathrm{D}^\infty_{c}(M;\CF))'\otimes \mathrm{D}^\infty_{c}(M;\CF)$.

As the inverse image of a quasi-closed set under a continuous linear map is still quasi-closed (see <cit.>), it follows that   $T_{f_\gamma}^{-1}(A)$ is a quasi-closed subset of $\CL_c(\mathrm{D}^\infty_{c}(U_{\gamma};\CF),\mathrm{D}^\infty_{c}(U_{\gamma};\CF))$ containing
$(\mathrm{D}^\infty_{c}(U_{\gamma};\CF))'\otimes \mathrm{D}^\infty_c(U_{\gamma};\CF)$, and hence equals to $\CL_c(\mathrm{D}^\infty_{c}(U_{\gamma};\CF),\mathrm{D}^\infty_{c}(U_{\gamma};\CF))$.  Note that
\[B:=\left\{\sum_{\gamma\in \Gamma_0}T_{f_\gamma}(\mathrm{id}_{\mathrm{D}^\infty_{c}(U_{\gamma};\CF)})\mid \Gamma_0\ \text{is a finite subset of}\ \Gamma\right\}\]
is a bounded subset of $A$.
The lemma then follows from the fact that

\[\mathrm{id}_{\mathrm{D}^\infty_{c}(M;\CF)}=\sum_{\gamma\in \Gamma} T_{f_\gamma}(\mathrm{id}_{\mathrm{D}^\infty_{c}(U_{\gamma};\CF)})\in\text{ the closure of }B\subset A.\]