Green morphisms induce algebraic Weyl maps

First the displayed Weyl relations define an associative unital $\ast$-algebra on the finite formal sums. For $v,w,z\in V(M)$, the exponent in $(W(v)W(w))W(z)$ is $-\frac{i}{2}(\sigma (v,w)+\sigma (v+w,z))$, whereas the exponent in $W(v)(W(w)W(z))$ is $-\frac{i}{2}(\sigma (w,z)+\sigma (v,w+z))$; bilinearity makes these equal. Also $W(0)W(v)=W(v)=W(v)W(0)$ since $\sigma (0,v)=\sigma (v,0)=0$, and $W(v)W(-v)=W(0)$ since $\sigma (v,-v)=0$. The involution reverses products because alternation gives $\sigma (w,v)=-\sigma (v,w)$; hence the relations are consistent with the claimed unit and involution.

Put $S_{\iota }[f]:=[{\iota }_{\ast }f]$. It is well-defined because ${\iota }_{\ast }(P_{U}k)=P_M({\iota }_{\ast }k)$ by [F4], so changing $f$ by an element of $P_U{\mathcal{D}}_g(U)$ changes ${\iota }_{\ast }f$ by an element of $P_M{\mathcal{D}}_g(M)$. For $f\in {\mathcal{D}}_g(U)$, the restriction $u=(E_M^{\pm }{\iota }_{\ast }f){\mathrm{\mid }}_U$ solves $P_{U}u=f$. Its support lies in $J_M^{\pm }(\mathrm{supp}f)\cap U=J_U^{\pm }(\mathrm{supp}f)$: the inclusion from right to left is immediate, and the reverse follows because a causal curve in $M$ from a point of $\mathrm{supp}f\subset U$ to a point of $U$ remains in $U$ by causal convexity [F4]. Here is the uniqueness argument actually needed. If $w$ is the difference of $u$ and $E_U^{+}f$, then $P_{U}w=0$ and $\mathrm{supp}w\subseteq J_U^{+}(\mathrm{supp}f)$. For any compact smooth real $h$ on $U$, set $v=E_U^{-}h$. The closed overlap of their supports is compact by [F5]. A compact cutoff $\eta =1$ near that overlap from [F6] gives ${\int }_{U}wh{\mu }_g={\int }_{U}wPv{\mu }_g={\int }_U(Pw)v{\mu }_g=0$: apply formal self-adjointness first to $\eta w$ and $v$; every commutator term has a derivative of $\eta$ where both supports meet and hence vanishes. A smooth nonzero real $w$ has a small fixed-sign coordinate neighborhood and a nonnegative test bump there, contradicting this vanishing integral. Thus $w=0$. The advanced case interchanges the signs. Hence $u=E_U^{\pm }f$ without presupposing uniqueness in the definition. The isometry preserves ${\mu }_g$, so this compatibility gives ${\sigma }_M(S_{\iota }[f],S_{\iota }[h])={\int }_{U}f(E_{U}h){\mu }_{g_U}={\sigma }_U([f],[h])$; thus $S_{\iota }$ is symplectic.

Define ${\alpha }_{\iota }$ on each basis symbol by ${\alpha }_{\iota }(W_U(v))=W_M(S_{\iota }v)$ and extend complex-linearly to finite sums. Since $S_{\iota }$ is symplectic, applying ${\alpha }_{\iota }$ to the product in [F3] gives $e^{-i{\sigma }_U(v,w)\mathrm{/}2}{W}_M(S_{\iota }(v+w))=W_M(S_{\iota }v)W_M(S_{\iota }w)$; applying it to $W_U(v{)}^{\ast }$ gives $W_M(-S_{\iota }v)=W_M(S_{\iota }v{)}^{\ast }$. It also sends $W_U(0)$ to $W_M(0)$, so it is a unital $\ast$-homomorphism. If $f$ is supported in an open $O\subseteq U$, then ${\iota }_{\ast }f$ is supported in $\mathrm{im}(\iota {\mathrm{\mid }}_O)$; therefore the generator formula sends each local generator into ${\mathfrak{W}}_M(\mathrm{im}(\iota {\mathrm{\mid }}_O))$, and sums and products do too. Extension by zero respects identity and composition, hence the generator formula gives ${\alpha }_{\mathrm{i}\mathrm{d}}=\mathrm{i}\mathrm{d}$ and ${\alpha }_{\mathrm{ȷ}\circ \iota }={\alpha }_{\mathrm{ȷ}}\circ {\alpha }_{\iota }$.