Proof. It is immediate from the definition of the filtrations that (i) gives a well-defined $R$-linear graded morphism $\mu _n$ satisfying (ii).

For (iii), note that $\pi ^{nj}F_jM+F_{j-1}M_n=F_jM_n$ for any $j\geq 0$, so that $\mu _n(\operatorname {gr}_j M)=\operatorname {gr}_jM_n$.

For (iv), let $m\in F_jM$ with the property that $\bar {m}\in \operatorname {gr}_j M$ is annihilated by $\mu _n$. This means that $\pi ^{nj}m\in F_{j-1}M_n=\sum _{i=0}^{j-1}\pi ^{in}F_iM\subseteq F_{j-1}M$. So $\pi ^{nj}\bar {m}=0$, that is, $\bar {m}\in (\operatorname {gr}_j M)[\pi ^{nj}]$. The reverse inclusion is clear.

Proof. Let $\bar {x}\in \operatorname {gr}_jM_n$ satisfy $\pi \bar {x}=0$. If $j\geq 1$, then surjectivity of $\mu _n$ (Lemma 3.1(iii)) implies that there exists $\bar {y}\in \operatorname {gr}_jM$ such that $\mu _n(\bar {y})=\bar {x}$, and hence

\[ \mu_n(\pi \bar{y})=\pi \bar{x}=0. \]

Therefore $\bar {y}\in \operatorname {gr} M$ is $\pi$-torsion by Lemma 3.1(iv), implying that $\pi ^{n} \bar {y}=0$ by assumption. As $j\geq 1$, it follows that $\bar {x}=\pi ^{nj}\bar {y}=0$ as well.

As $\operatorname {gr}_0 M_n=F_0 M$ is also $\pi$-torsionfree, we have $(\operatorname {gr} M_n)[\pi ]=\oplus _j (\operatorname {gr}_j M_n)[\pi ]=0$, as required.

Proof. Let $S_n=1+\pi U_n$. Equipping $U$ with its $\pi$-adic filtration, it follows from [Reference LiLi96, Corollary 2.2] that $S_n$ is an Ore set in $U$ and hence in $U_K$. In particular, the set of $S_n$-torsion elements in $N$ is a $U_K$-submodule of $N$, and by simplicity is either $0$ or $N$ itself. Assume therefore that $N$ and hence $M_n$ is $S_n$-torsion.

We now claim that $F_jM_n=\pi F_jM_n$ for any $j\geq 0$. Once we have proved the claim, finite generation of $F_jM_n$ over the Noetherian $\pi$-adically complete ring $F_0U$ forces $F_jM_n=0$ by [Reference Atiyah and MacdonaldAM69, Corollary 10.19], so $M_n=0$, which provides us with the desired contradiction, as $M_n\otimes _R K=N\neq 0$.

Let $m\in F_jM_n$. As $M_n$ is $S_n$-torsion, there exists $u\in U_n$ such that $(1-\pi u)m=0$, so $m=\pi um$.

Since $\operatorname {gr} M_n$ is $\pi$-torsionfree, the same is true for $F_iM_n/F_{i-1}M_n$ for each $i$, and thus $M_n/F_jM_n$ is also $\pi$-torsionfree. In particular, $\pi um\in F_jM_n$ implies $um\in F_jM_n$ and thus $m\in \pi F_jM_n$, as required.

Proof of Theorem 3.1 By the remark after Corollary 3.1 and by Lemma 3.2, there exists $t$ such that $N$ is $S_n$-torsionfree for any $n\geq t$. Then $\widehat {M_n}\neq 0$ by [Reference Atiyah and MacdonaldAM69, Theorem 10.17]. As $M_n$ is $\pi$-torsionfree, so is $\widehat {M_n}\cong \widehat {U_n}\otimes _{U_n}M_n$, and hence $\widehat {M_n}\otimes _R K\cong \widehat {{U}_{n,K}}\otimes _{U_K}N\neq 0$ for any $n\geq t$. Therefore $\widehat {{U}_K}\otimes _{U_K}N\neq 0$, as required.

Proof. Flatness was already proven in [Reference BodeBod19a, Lemma 4.14], so it suffices to show faithfulness.

If $L$ admits a smooth Lie lattice, this follows directly from Theorem 3.1. In the general case, note that there exists a finite affinoid covering $(\operatorname {Sp} A_i)$ of $\operatorname {Sp} A$ such that $A_i\otimes _A L$ is free (and in particular admits a smooth Lie lattice) for each $i$. We thus obtain the commutative diagram

where the left vertical arrow is faithfully flat due to the isomorphism $U(A_i\otimes _A L)\cong A_i\otimes _A U_A(L)$ (see [Reference Ardakov and WadsleyAW19, Proposition 2.3]). Theorem 3.1 thus implies that $\oplus \widehat {U(A_i\otimes _A L)}$ is faithfully flat over $U_A(L)$: if $N$ is a non-zero $U(L)$-module, then there exists some $i$ such that ${U(A_i\otimes L)\otimes _{U(L)} N\neq 0}$, and hence $\widehat {U(A_i\otimes L)}\otimes _{U(L)} N\neq 0$. Therefore, if $N$ is a $U(L)$-module such that $\widehat {U(L)}\otimes N=0$, it follows from $\oplus \widehat {U(A_i\otimes L)}\otimes _{U(L)}N=0$ that $N=0$.

Proof. First we show that $S$ is left Noetherian. Suppose that $(I_n)$ is an ascending chain of left ideals in $S$. For each $n\in \mathbb {N}$ let $J_n$ be the image of $S'\otimes _S I_n\to S'$ so that $(J_n)$ is an ascending chain of left ideals in $S'$. Since $S'$ is left Noetherian the chain $J_n$ must terminate. Because $S\to S'$ is faithfully flat $J_n/J_{n-1}\cong S'\otimes _S I_n/I_{n-1}\neq 0$ whenever $I_n/I_{n-1}\neq 0$. Thus the chain $I_n$ must terminate.

By symmetry (or by considering the opposite rings) $S$ is also right Noetherian.

Next we show that $S$ satisfies the Auslander condition. Let $N$ be a right $S$-submodule of $\operatorname {Ext}^{i}_S(M, S)$ for some finitely generated left $S$-module $M$, and let $j< i$. Since $S\to S'$ is flat there is an isomorphism $S'\otimes _S \operatorname {Ext}_S^{j}(N,S)\cong \operatorname {Ext}_{S'}^{j}(N\otimes _S S',S')$. The latter is zero since $S'$ satisfies the Auslander condition and $N\otimes _S S'$ is isomorphic to a submodule of $\operatorname {Ext}_S^{i}(M,S)\otimes _S S'\cong \operatorname {Ext}_{S'}^{i}(S'\otimes _S M,S')$ by the flatness of $S\to S'$ again. Since $S\to S'$ is faithfully flat we may deduce that $\operatorname {Ext}_S^{j}(N,S)=0$ as required.

Finally, suppose that $d=\mathrm {injdim}_{S'} S'$. For each cyclic $S$-module $M$ we can compute $\operatorname {Ext}^{d+1}(M,S)\otimes _S S'\cong \operatorname {Ext}^{d+1}(S'\otimes _S M,S')=0$. Since $S\to S'$ is faithfully flat we can deduce $\operatorname {Ext}^{d+1}(M,S)=0$ and so, using [Reference JansJan64, p. 55], that $\mathrm {injdim}_S S\leq d$.

Proof. By [Reference HartlHar03, Theorem 1.4] there is a finite separable field extension $K'$ of $K$ with ring of integers $R'$, a quasi-compact strictly semi-stable formal $R'$-scheme $\mathcal {X}'$, and a composition of morphisms of quasi-compact admissible formal $R$-schemes $\mathcal {X}'\to \mathcal {X}^{{\dagger} }\to \mathcal {X}$ such that $\mathcal {X}^{{\dagger} } \to \mathcal {X}$ is an admissible formal blowing-up and $\mathcal {X}'\to \mathcal {X}^{{\dagger} }$ is flat and surjective. Since being Gorenstein is a local condition and $\mathcal {X}'\to \mathcal {X}^{{\dagger} }$ is faithfully flat it suffices by Lemma 4.1 to show that $\mathcal {X}'$ is Gorenstein. But $\mathcal {X}'$ is a regular scheme [Reference HartlHar03, Remark 1.1.1] and so Gorenstein.

Proof. By [Reference RinehartRin63, Theorem 3.1] there is a positive filtration on $U(L)$ such that $\operatorname {gr} U(L)\cong \operatorname {Sym}(L)$ is commutative. By [Reference LevasseurLev85, Théorème 4.4, Remarque 4.5] it thus suffices to show that $\operatorname {Sym}(L)$ is Auslander–Gorenstein of dimension at most $\dim A+r$.

Since $L$ is a finitely generated projective $(k,A)$-module there is a cover of $\operatorname {Spec}(A)$ by basic open subsets $D(f_1),\ldots ,D(f_m)$ such that $A_{f_i}\otimes _A L$ is a free $A_{f_i}$-module of rank $r$ for each $i=1,\ldots ,m$. Since $\operatorname {Sym}(L)\to \oplus _{i=1}^{m}\operatorname {Sym}(A_{f_i}\otimes _A L)$ is faithfully flat we can use Lemma 4.1 to reduce to the case that $L$ is free over $A$, that is, $\operatorname {Sym}(L)$ is isomorphic to a polynomial ring $A[t_1,\ldots ,t_r]$. Thus we are done by [Reference Watanabe, Ishikawa, Tachibana and OtsukaWITO69, Corollary 1].

Proof. First we establish the result when $\mathcal {A}$ is Gorenstein with $m=0$. In this case it follows from the lemma that $U(\mathcal {L})$ is Auslander–Gorenstein of dimension at most $\dim \mathcal {A}+r=\dim A+1+r$. Thus $U(\mathcal {L})/\pi U(\mathcal {L})$ is Auslander–Gorenstein of dimension at most $\dim A+r$ by [Reference Ajitabh, Smith and ZhangASZ99, Propositions 1.3 and 2.1].

Now $\widehat {U(\pi ^{n}\mathcal {L})_K}$ is a complete doubly filtered $K$-algebra and

\[ \operatorname{Gr}(\widehat{U(\pi^{n}\mathcal{L})_K})\cong U(\mathcal{L})/\pi U(\mathcal{L}) \]

by [Reference Ardakov and WadsleyAW13, Lemma 3.7]. Thus $\widehat {U(\pi ^{n}\mathcal {L})_K}$ is Auslander–Gorenstein of dimension at most $\dim A+r$ by [Reference BjorkBjo89, Theorem 3.9].

In the general case Proposition 4.2 shows that there is an admissible formal blowing-up $\mathcal {X}\to \operatorname {Spf}(\mathcal {A})$ over $R$ with $\mathcal {X}$ Gorenstein. Let $\{\operatorname {Spf}(\mathcal {A}_i)\}$ be an affine cover of $\mathcal {X}$. By [Reference Ardakov and WadsleyAW19, Proposition 7.6] and the proof of [Reference Ardakov and WadsleyAW19, Lemma 7.6(b)] there is a positive integer $m$ such that each $\mathcal {A}_i$ is $\mathcal {L}$-stable and each $(\operatorname {Spf} \mathcal {A}_i)_{\mathrm {rig}}$ is a $\pi ^{n}\mathcal {L}$-accessible subdomain of $X$ for each $n\geq m$. Thus each natural map

\[ \widehat{U(\pi^{n}\mathcal{L})_K}\to \bigoplus \widehat{U(\mathcal{A}_i\otimes_{\mathcal{A}}\pi^{n}\mathcal{L})_K} \]

with $n\geq m$ is faithfully flat by [Reference Ardakov and WadsleyAW19, Theorem 4.9(b)]. The result now follows from Lemma 4.1 and the case $\mathcal {A}$ is Gorenstein.

Proof. As $\Omega _L$ is a projective $A$-module, the left-hand side is the $j$th cohomology of $\mathrm {R}\operatorname {Hom}_{\widehat {U(L)}}(\Omega _L\otimes ^{\mathbb {L}}_AM, \widehat {U(L)})$, while the right-hand side is the $j$th cohomology of $\mathrm {R}\operatorname {Hom}_A(\Omega _L, \mathrm {R}\operatorname {Hom}_{\widehat {U(L)}}(M, \widehat {U(L)})$. The natural isomorphism thus follows directly from the derived tensor-Hom adjunction [Reference Kashiwara and SchapiraKS06, Theorem 18.6.4(vii)].

Because $\Omega _L$ is an invertible $A$-module,

\[ \operatorname{Ext}^{j}_{\widehat{U(L)}}(M,\widehat{U(L)})=0 \ \text{if and only if}\ \operatorname{Hom}_A(\Omega_L, \operatorname{Ext}^{j}_{\widehat{U(L)}}(M, \widehat{U(L)}))=0 \]

for each $j\geq 0$, and hence $d(M)=d(\Omega _L\otimes _A M)$.

Proof. Let $\mathcal {M}$ be a coadmissible $\widehat {\mathscr {U}(\mathscr {L})}$-module and suppose that $Z\subset Y$ are in $X_w(\mathscr {L})$. Let $\mathcal {A}$ be an affine formal model in $\mathcal {O}(Y)$ such that $\mathscr {L}(Y)$ admits a smooth Lie lattice $\mathcal {L}$. By replacing $\mathcal {L}$ by $\pi ^{m}\mathcal {L}$ for some positive integer $m$, we may assume that $Z$ is $\pi ^{n}\mathcal {L}$-accessible for all $n\geq 0$ (see [Reference Ardakov and WadsleyAW19, Proposition 7.6]).

Let $\mathcal {B}$ be an affine formal model in $\mathcal {O}(Z)$ such that $\mathcal {B}\otimes _{\mathcal {A}}\mathcal {L}$ is a $\mathcal {B}$-Lie lattice in $\mathscr {L}(Z)=B\otimes _A\mathscr {L}(Y)$.

For each $n\geq 0$, let $U_n$ and $V_n$ denote the $K$-Banach algebras $\widehat {U(\pi ^{n}\mathcal {L})_K}$ and $\widehat {U(\mathcal {B}\otimes \pi ^{n}\mathcal {L})_K}$ respectively and let $U:=\varprojlim U_n=\widehat {U(\mathscr {L}(Y))}$ and $V:=\varprojlim V_n=\widehat {U(\mathscr {L}(Z))}$. Now, using [Reference Ardakov and WadsleyAW19, Theorem 9.4], we see that $M_n(Y):=U_n\otimes _{U}\mathcal {M}(Y)$ is a finitely generated left $U_n$-module, $M_n(Z):=V_n\otimes _{V}\mathcal {M}(Z)$ is a finitely generated left $V_n$-module and $M_n(Z)\cong V_n\otimes _{U_n}M_n(Y)$. Moreover, by [Reference Ardakov and WadsleyAW19, Theorem 4.8], $U_n\to V_n$ is flat on both sides for all positive integers $n$. Thus $\operatorname {Ext}^{t}_{V_n}(M_n(Z),V_n)\cong \operatorname {Ext}^{t}_{U_n}(M_n(Y),U_n)\otimes _{U_n}V_n$ for each $t\geq 0$.

By Lemma 5.1, $\operatorname {Ext}^{t}_{U}(\mathcal {M}(Y),U)$ is a coadmissible right $U$-module such that

\[ \operatorname{Ext}^{t}_{U}(\mathcal{M}(Y),U)\otimes_{U}U_n\cong \operatorname{Ext}^{t}_{U_n}(M_n(Y),U_n) \]

and $\operatorname {Ext}^{t}_{V}(\mathcal {M}(Z),V)$ is a coadmissible $V$-module with $\operatorname {Ext}^{t}_{V}(\mathcal {M}(Z),V)\otimes _{V}V_n\cong \operatorname {Ext}^{t}_{V_n}(M_n(Z),V_n)$. Thus we can compute

\begin{align*} \operatorname{Ext}^{t}_V(\mathcal{M}(Z),V)\otimes V_n & \cong \operatorname{Ext}^{t}_{V_n}(M_n(Z),V_n)\\ & \cong \operatorname{Ext}^{t}_{U_n}(M_n(Y),U_n)\otimes_{U_n}V_n\\ & \cong \operatorname{Ext}^{t}_U(\mathcal{M}(Y),U)\otimes_U V_n. \end{align*}

Now we see that $\operatorname {Ext}^{t}_V(\mathcal {M}(Z),V)\cong \operatorname {Ext}^{t}_U(\mathcal {M}(Y),U) {\widehat{\otimes}}_U V$ by (the proof of) [Reference Ardakov and WadsleyAW19, Lemma 7.3]. It follows, using [Reference Ardakov and WadsleyAW19, Theorem 8.2, Theorem 8.4], that the presheaf on $Y_w$ that sends $Z\in Y_w$ to $\operatorname {Ext}^{t}_{\widehat {U(\mathscr {L}(Z))}}(\mathcal {M}(Z),\widehat {U(\mathscr {L}(Z))})$ is a coadmissible sheaf of $\widehat {\mathscr {U}(\mathscr {L})}$-modules on $Y_w$. Applying [Reference Ardakov and WadsleyAW19, Theorem 9.1, Theorem 9.4] completes the proof of the proposition.

Proof. Since $X$ is quasi-separated, for any pair $Y\in \mathcal {U}$ and $Z\in \mathcal {V}$ that does not intersect trivially we can cover $Y\cap Z$ by a finite set of affinoid subspaces in $X_{w}(\mathcal {L})$. Thus we may reduce to the case that $\mathcal {V}$ is a refinement of $\mathcal {U}$ and every element of $\mathcal {U}$ has an admissible cover by elements of $\mathcal {V}$.

Now suppose $Y\in \mathcal {U}$ is covered by $Z_1,\ldots ,Z_k\in \mathcal {V}$. Then by the proposition $\operatorname {\mathscr {E}\!\mathit {xt}}_{\widehat {\mathscr {U}(\mathscr {L}|_Y)}}^{j}(\mathcal {M}|_Y, \widehat {\mathscr {U}(\mathscr {L}|_Y)})$ is a coadmissible $\widehat {\mathscr {U}(\mathscr {L}|_Y)}$-module for each $j\geq 0$. Since $\widehat {U(\mathscr {L}(Y))} \to \oplus _{i=1}^{k} \widehat {U(\mathscr {L}(Z_i))}$ is c-faithfully flat by [Reference Ardakov and WadsleyAW19, Theorem 7.7(b)] it follows that $j(\mathcal {M}(Y))=\inf \{j(\mathcal {M}(Z_i))\mid \mathcal {M}(Z_i)\neq 0\}$.

As $\dim Y=\dim Z_i$ for each $i$ by equidimensionality, the result follows.

Proof. By assumption, there exists $x\in \mathcal {L}$ such that $x\cdot f=1$. Applying the anchor map, we also have $\partial \in \mathrm {Der}_K(A)$ such that $\partial \cdot f=1$, and by [Reference Ardakov and WadsleyAW18, Lemma 4.1],

\[ \mathrm{Der}_K(A)=A\partial\oplus C, \]

where $C=\{\xi \in \mathrm {Der}(A): \xi \cdot f=0\}$. In particular, it follows from smoothness that $C$ is a projective $A$-module.

By the second fundamental exact sequence [Reference Bosch, Lütkebohmert and RaynaudBLR95, Proposition 1.2], we have

\[ \mathrm{Der}_K(B)=C/(f), \]

which is projective, so $B$ is smooth. Moreover, $\mathcal {B}$ is easily seen to be an affine formal model.

In the same vein, applying [Reference Ardakov and WadsleyAW18, Lemma 4.1] to $\mathcal {L}$ yields

\[ \mathcal{L}=\mathcal{A} x\oplus \mathcal{C}, \]

so $\mathcal {C}$ is projective over $\mathcal {A}$, and the $(R, \mathcal {B})$-Lie algebra $\mathcal {C}/I$ is also a projective $\mathcal {B}$-module.

For (ii), note that $f$ is central in $\widehat {U(\mathcal {C})_K}$ by definition of $\mathcal {C}$. So it suffices to show that $f\cdot P\neq 0$ for any non-zero $P\in \widehat {U(\mathcal {C})_K}$. In particular, this only depends on the $A$-module structure of $\widehat {U(\mathcal {C})_K}$. But it follows from [Reference RinehartRin63, Theorem 3.1] that

\[ \widehat{U(\mathcal{C})_K}\cong \widehat{\operatorname{Sym}_{\mathcal{A}}(\mathcal{C})_K} \]

as $A$-modules. Since $\mathcal {C}$ is a projective finitely generated $\mathcal {A}$-module, it is a direct summand of a free $\mathcal {A}$-module of finite rank, $\mathcal {L}'$. By functoriality, $\widehat {\operatorname {Sym} \mathcal {C}_K}$ embeds into $\widehat {\operatorname {Sym} \mathcal {L}_K'}$, so we are done if we can show that $f$ is regular in $A$.

To show that $f$ is regular in $A$, consider the annihilators

\[ \operatorname{Ann}_A(f)\subseteq \operatorname{Ann}_A(f^{2})\subseteq \cdots. \]

By Noetherianity of $A$, this chain of ideals stabilizes, so that

\[ \operatorname{Ann}(f^{r})=\operatorname{Ann}(f^{r+1})=\cdots \]

for some integer $r$.

As $X=\operatorname {Sp} A$ is smooth, we can consider the Fréchet–Stein algebra $D=\widehat {\mathcal {D}}(X)$. We claim that $\operatorname {Ann}_A(f^{r})$ is a $D$-submodule of $A$, from which $\operatorname {Ann}(f)\subseteq \operatorname {Ann}(f^{r})=\{0\}$ follows because of [Reference Ardakov and WadsleyAW18, Proposition 7.4] (note that $\operatorname {Ann}(f^{r})\neq A$ as $f^{r}\neq 0$ by reducedness of $\operatorname {Sp} A$).

If $a\in \operatorname {Ann}(f^{r})$ and $\xi \in \mathrm {Der}(A)$, then

\[ \xi(a)\cdot f^{r+1}=\xi(af^{r+1})-af^{r}\xi(f)=0, \]

so that $\xi (a)\in \operatorname {Ann}(f^{r+1})=\operatorname {Ann}(f^{r})$. By [Reference Ardakov and WadsleyAW18, Theorem 7.3], it follows that $\operatorname {Ann}(f^{r})$ is a $D$-submodule of $A$, as required.

Proof. We first introduce some notation. For $i=0, \dots , r$, write $A_i=A/(f_1, \dots , f_i)$, $I_i=(\sum _{j=1}^{i} f_jA)\cap \mathcal {A}$ and $\mathcal {A}_i=\mathcal {A}/I_i$. Let $\mathcal {C}_i=C_{\mathcal {L}}(\{f_1, \dots , f_i\})$ and let $\mathcal {L}_i=\mathcal {C}_i/I_i$. By applying the preceding lemma repeatedly, each $A_i$ is smooth, with affine formal model $\mathcal {A}_i$, and $\mathcal {L}_i$ is a smooth $(R, \mathcal {A}_i)$-Lie algebra. Note also that $\mathcal {L}_0=\mathcal {L}$ and $\mathcal {L}_r=\mathcal {C}/(F)$.

In fact, [Reference Ardakov and WadsleyAW18, Lemma 4.1] gives an explicit description of $\mathcal {L}_i$: if $x_1, \dots , x_r\in \mathcal {L}$ such that $x_if_j=\delta _{ij}$, then

\[ \mathcal{L}_i=\mathop{\bigoplus}\limits_{j=i+1}^{r} \mathcal{A}_ix_j\oplus \mathcal{C}/I_i. \]

In particular, note that the natural map

\[ \mathcal{L}_{i}\to C_{\mathcal{L}_{i-1}}(f_{i})/I_i \]

is an isomorphism for $i=1, \dots , r$, and $\widehat {U(\mathcal {C})_K}/(F)\cong \widehat {U(\mathcal {L}_r)_K}\cong \widehat {U(C_{\mathcal {L}_{r-1}}(f_r))_K}/(f_r)$.

It thus suffices to prove the following claim. If $M$ is finitely generated $\widehat {U(\mathcal {L}_i)_K}$-module then

\[ j_{{\widehat{U(\mathcal{L}_{i-1})_K}}} \Big(\widehat{U(\mathcal{L}_{i-1})_K}\underset{\widehat{U(C_{\mathcal{L}_{i-1}}(f_i))_K}}{\otimes} M\Big)=j_{{\widehat{U(\mathcal{L}_i)_K}}}(M)+1. \]

Write $U=\widehat {U(C_{\mathcal {L}_{i-1}}(f_i))_K}$, $V=\widehat {U(\mathcal {L}_{i-1})_K}$. Since, by [Reference Ardakov and WadsleyAW18, Corollary 4.3], $U\to V$ is faithfully flat and $\operatorname {Ext}^{j}_{U}(M,U)\otimes _UV\cong \operatorname {Ext}^{j}_V(V\otimes _U M, V)$, we see that $j_U(M)=j_V(V\otimes _UM)$. Thus it suffices to show that $j_U(M)=j_{U/(f_i)}(M)+1$. By the preceding lemma, $f_i$ is a regular central element in $U$, so we can apply [Reference Ajitabh, Smith and ZhangASZ99, Lemma 1.1] to conclude the proof.

Proof. By Lemma 5.2, we can consider the case where $M$ is a right coadmissible module. Let $\{x_1, \dots , x_d\}$ be an $I$-standard basis and let $F=\{f_1, \dots , f_r\}\subset A$ be the corresponding generating set. Rescaling the $x_i$ and $f_j$ if necessary, we can assume that there exists an affine formal model $\mathcal {A}$ of $A$ such that $\mathcal {L}:=\sum \mathcal {A} x_i$ is a free Lie lattice in $L$.

Write $U_n=\widehat {U(\pi ^{n}\mathcal {L})_K}$. Recall that [Reference Ardakov and WadsleyAW18, Lemma 5.8] provides an isomorphism of Fréchet–Stein algebras

\[ \widehat{U(L_Y)}\cong \widehat{U(C_L(F))}/(F). \]

Denote $\widehat {U(C_{\pi ^{n}\mathcal {L}}(F))_K}$ by $V_n$, so $\widehat {U(L_Y)}\cong \varprojlim V_n/(F)$ exhibits $\widehat {U(L_Y)}$ as a Fréchet–Stein algebra.

Now

\[ j_{\widehat{U(L)}}(\iota_+M)=j_{U_n}\bigg(\iota_+M\underset{\widehat{U(L)}}{\otimes} U_n\bigg) \]

for sufficiently large $n$ by Lemma 5.1, and by definition of $\iota _+$,

\[ \iota_+M\underset{\widehat{U(L)}}{\bigotimes} U_n\cong M\underset{\widehat{U(L_Y)}}{\bigotimes} \frac{V_n}{(F)}\underset{V_n/(F)}{\bigotimes}\frac{U_n}{IU_n}. \]

Therefore Proposition 6.1 implies that

\[ j_{U_n}(\iota_+M\otimes U_n)=j_{V_n/(F)}\big(M\otimes_{\widehat{U(L_Y)}} V_n/(F)\big)+r. \]

Since $\dim A-\dim A/I=r$, it follows that for sufficiently large $n$,

\begin{align*} {d_{\widehat{U(L)}}}(\iota_+M)&=2\dim A-j_{U_n}\big(\iota_+M\otimes U_n\big)\\ & =2\dim A-j_{V_n/(F)}(M\otimes V_n/(F))-r\\ & = 2r +(2\dim A/I-{j_{\widehat{U(L_Y)}}}(M))-r\\ &={d_{\widehat{U(L_Y)}}}(M)+r \end{align*}

as required.

Proof. By [Reference Ardakov and WadsleyAW18, Theorem 6.2], there exists an affinoid covering $(X_i)$ of $X$, with $X_i=\operatorname {Sp} A_i$ connected such that the $(K, A_i)$-Lie algebra $L_i=\mathcal {T}(X_i)$ admits an $I_i$-standard basis, where $I_i\subset A_i$ is the vanishing ideal of $Y\cap X_i$ – the conditions in the reference are satisfied by smoothness of $Y$. Moreover, $\mathcal {T}_Y(Y\cap X_i)\cong N_{L_i}(I_i)/I_iL_i$ by dualizing [Reference Bosch, Lütkebohmert and RaynaudBLR95, Proposition 1.2]. Hence the claim follows from Corollary 6.1.

Proof. Let $\mathcal {L}$ be the $\mathcal {R}\langle x_1,\ldots , x_d\rangle$-submodule of $\operatorname {Der}_K(K\langle x_1,\ldots ,x_d\rangle )$ spanned by $\{\partial _1,\ldots ,\partial _d\}$. Then $\mathcal {L}$ is a smooth Lie lattice in $\mathcal {T}(X)$ and write $D_n=\widehat {U(\pi ^{n}\mathcal {L})_K}$ and $D=\widehat {\mathcal {D}}(X)$. Then $D=\varprojlim D_n$ is a presentation of $D$ as a Fréchet–Stein algebra.

Let $\mathcal {M}$ be a coadmissible $\widehat {\mathcal {D}}_X$-module and write $M:=\mathcal {M}(X)$, a coadmissible $D$-module, and $M_n=D_n\otimes _D M$. Since $X\in X_w(\mathcal {T}(X))$ it suffices to show that $j_D(M)\leq d$. Since $\operatorname {Ext}^{j}_{D}(M,D)\otimes _{D}D_n \cong \operatorname {Ext}^{j}_{D_n}(M_n,D_n)$ by Lemma 5.1 it suffices to show that $j_{D_n}(M_n)\leq d$ whenever $M_n\neq 0$. This follows from [Reference Ardakov and WadsleyAW13, Corollary 7.4, Theorem 3.3].

Proof. Let $\mathcal {M}$ be a non-zero coadmissible $\widehat {\mathcal {D}}_X$-module. Since $\dim \mathcal {M}$ is defined locally we may assume that $X$ is affinoid and $\mathcal {T}(X)$ admits a smooth Lie lattice. Now every $K$-affinoid can be viewed as a closed analytic subset of a polydisc $Y=\operatorname {Sp} K\langle x_1,\ldots ,x_N\rangle$ for $N$ sufficiently large. Let $\iota \colon X\to Y$ denote the closed embedding. By Theorem 6.1, $d(\iota _+\mathcal {M})= d(\mathcal {M})+ N -\dim X$. Thus it suffices to show that $d(\iota _+\mathcal {M})\geq N$, and the result follows from the proposition.

Proof. As the dimension can be calculated locally, we can assume that $X=\operatorname {Sp} A$ is a smooth, connected affinoid $K$-space with $\mathcal {T}(X)$ admitting a smooth Lie lattice. Choosing an affine formal model $\mathcal {A}$ and a smooth $(R, \mathcal {A})$-Lie lattice $\mathcal {L}$ in $\mathcal {T}(X)$, we can write $\widehat {\mathcal {D}}(X)=\varprojlim \widehat {U_{\mathcal {A}}(\pi ^{n}\mathcal {L})}_K$, where $\widehat {U_{\mathcal {A}}(\pi ^{n}\mathcal {L})}_K$ is Auslander–Gorenstein of dimension at most $2 \dim A$ for sufficiently large $n$ by Theorem 4.3. As before, we abbreviate $D=\widehat {\mathcal {D}}(X)$ and $D_n=\widehat {U(\pi ^{n}\mathcal {L})_K}$.

If $0\to M_1\to M_2\to M_3\to 0$ is a short exact sequence of coadmissible $D$-modules, there exists an integer $m$ such that

\[ j_{D}(M_i)=j_{D_n}(D_n\otimes_D M_i) \quad \text{for} \ i=1, 2, 3,\ n\geq m, \]

by Lemma 5.1, so the result follows from [Reference LevasseurLev92, Proposition 4.5(ii)] applied to

\[ 0\to D_n\otimes M_1\to D_n\otimes M_2\to D_n\otimes M_3\to 0, \]

which is exact by flatness of $D_n$ over $D$.

Proof. This is a direct consequence of Lemma 6.1.

Proof. Without loss of generality, $X=\operatorname {Sp} A$ is a smooth affinoid with free tangent sheaf. Write $D=\mathcal {D}(X)$ and $\widehat {D}=\widehat {\mathcal {D}}(X)$. If $M$ is a finitely generated $D$-module, then faithful flatness of $\widehat {D}$ over $D$ (Theorem 3.1) implies that for any $j$,

\[ \operatorname{Ext}^{j}_{\widehat{D}}(\widehat{D}\otimes_D M, \widehat{D})\cong \operatorname{Ext}^{j}_{D}(M, D)\otimes_D \widehat{D}=0 \ \text{if and only if} \ \operatorname{Ext}^{j}_D(M, D)=0. \]

In particular, $j_D(M)=j_{\widehat {D}}(\widehat {D}\otimes _D M)$, and the result follows.

Proof. Any integrable connection is a coherent $\mathcal {D}_X$-module of minimal dimension, so we are done by applying [Reference Ardakov and WadsleyAW18, Proposition 6.2].

Proof. As $X$ is equidimensional, we can assume that $X$ is affinoid, with $\mathcal {T}(X)$ admitting a smooth Lie lattice. Let $\mathcal {M}=\operatorname {Loc} M$ be a non-zero weakly holonomic $\widehat {\mathcal {D}}_X$-module, so that $j(M)=d$.

By Auslander's condition, $\operatorname {Ext}^{d}(M, \widehat {\mathcal {D}}(X))$ has grade $\geq d$ as a right $\widehat {\mathcal {D}}_X(X)$-module. Thus Proposition 5.3 implies that

\[ \operatorname{\mathscr{E}\!\mathit{xt}}^{d}_{\widehat{\mathcal{D}_X}}(\mathcal{M}, \widehat{\mathcal{D}_X})\cong \operatorname{Loc} \operatorname{Ext}^{d}(M, \widehat{\mathcal{D}}_X(X)) \]

is a coadmissible right $\widehat {\mathcal {D}}_X$-module of dimension $d$, and the result follows from Lemma 5.2.

Proof. Let $X$ be a smooth affinoid of dimension $d$ with $\mathcal {T}(X)$ admitting a smooth Lie lattice $\mathcal {L}$. Write $D=\widehat {\mathcal {D}}(X)$ and $D_n=\widehat {U(\pi ^{n}\mathcal {L})_K}$, so that $D=\varprojlim D_n$. By Theorem 4.3, we can assume that $D_n$ is Auslander–Gorenstein of dimension at most $2d$ for each $n\geq 0$.

Let $M$ be a coadmissible $D$-module of grade $d$. By Lemma 5.2 and [Reference Ardakov and WadsleyAW18, Theorem 3.4], we have

\[ \operatorname{Hom}_A(\Omega, \operatorname{Ext}^{d}_D(\operatorname{Hom}_A(\Omega, \operatorname{Ext}^{d}_D(M, D)), D))\cong \operatorname{Ext}^{d}_D(\operatorname{Ext}^{d}_D(M, D), D), \]

and now

\begin{align*} \operatorname{Ext}^{d}(\operatorname{Ext}^{d}(M, D), D)&\cong\varprojlim \big(D_n\otimes_D \operatorname{Ext}^{d}_D(\operatorname{Ext}^{d}_D(M, D), D)\big)\\ & \cong \varprojlim \operatorname{Ext}^{d}_{D_n}(\operatorname{Ext}^{d}_D(M, D)\otimes_D D_n, D_n)\\ & \cong \varprojlim \operatorname{Ext}^{d}_{D_n}(\operatorname{Ext}^{d}_{D_n}(D_n\otimes_D M, D_n), D_n) \end{align*}

by repeatedly applying Lemma 5.1.

Note that $\operatorname {Ext}^{i}_{D_n}(D_n\otimes _D M, D_n)=0$ for any $i\neq d$ by Lemma 5.1, so

\[ \operatorname{Ext}^{d}(\operatorname{Ext}^{d}(D_n\otimes M, D_n), D_n)\cong D_n\otimes M \]

by [Reference IwanagaIwa97, Theorem 4],Footnote ¹ and hence

\[ \operatorname{Ext}^{d}(\operatorname{Ext}^{d}(M, D), D)\cong \varprojlim (D_n\otimes_D M)\cong M \]

by coadmissibility of $M$.

Thus $\mathbb {D}^{2}(\operatorname {Loc} M)\cong \operatorname {Loc} M$ as required.

Proof. (i) is clear from the universal property, (ii) is [Reference SchoutensSch99, Example 1.3.2(1)]. (iii) is [Reference SchoutensSch99, Corollary 2.1.3]. Concerning (iv), it follows easily from the universal property that $\mathbf {Y}^{\mathrm {an}}\cong \eta ^{-1}(\mathbf {Y})$, which is an admissible open subspace of $\mathbf {X}^{\mathrm {an}}$ by continuity of $\eta$. By (iii), it is then even Zariski open. (v) is a consequence of (iv) and the fact that $\eta$ is a morphism of locally $G$-ringed spaces. (vi) follows again from the universal property.

Proof. Without loss of generality, we can assume that $X$ (and hence $\mathbf {X}$) is connected.

Let $x\in \mathbf {Z}$ be a closed point in $\operatorname {Spec} A$, and let $x_1, \dots , x_d\in \mathcal {O}_{\mathbf {X}, x}$ be a regular set of local parameters as in Definition 9.2. By definition, there exists some Zariski open affine subscheme $U_x=\operatorname {Spec} B(x)\subset \mathbf {X}$ containing $x$ such that $x_1, \dots , x_d$ are defined on $U_x$, and $\mathbf {Z}\cap U_x=\{\prod _{j=1}^{r} x_j=0\}$.

By smoothness, $\Omega ^{1}(X)$ is a finitely generated projective $A$-module, so there exists ${f_1, \dots , f_n\in A}$ such that

\[ A_{f_k}\otimes_A \Omega^{1}(X) \]

is a free $A_{f_k}$-module for each $k$, with free generating set $s_{k1}, \dots , s_{kd}$.

Fix $k$ such that $x\in \operatorname {Spec} A_{f_k}$. Then $B(x)_{f_k}\otimes _A \Omega ^{1}(X)$ is freely generated by $s_{k1}, \dots , s_{kd}$, so there exist $M=(m_{ij})\in \mathrm {Mat}_{d\times d}(B(x)_{f_k})$ such that

\[ {d} x_i=\sum_j m_{ij} s_{kj}. \]

As $x\in \mathbf {X}$ is closed, it corresponds to a unique point in $X=\operatorname {Sp} A$, which we also denote by $x$. As the $x_i$ form a regular system of local parameters in $\mathcal {O}_{\mathbf {X}, x}$, they also define a regular system of local parameters in the local ring $\mathcal {O}_{X, x}$ by [Reference BoschBos14, Propositions 4.1/1, 4.1/2], so that $\{{d} x_i\}$ form a free generating set in $\Omega ^{1}_{X, x}=\mathcal {O}_{X, x}\otimes _A \Omega ^{1}(X)$. Thus $M$ becomes invertible as a matrix over $\mathcal {O}_{X, x}$ and hence over $\mathcal {O}_{\mathbf {X}, x}$, as $\mathcal {O}_{\mathbf {X}, x}\to \mathcal {O}_{X, x}$ is injective by [Reference BoschBos14, Proposition 4.1/2]. Therefore $x$ is contained in a Zariski open affine subscheme $\operatorname {Spec} C(x)$ of $\mathbf {X}$ with the property that:

1. (i) $x_1, \dots , x_d\in C(x)$, and ${d} x_i$ form a free generating set of $C(x)\otimes _A \Omega ^{1}(X)$;

2. (ii) $\mathbf {Z}\cap \operatorname {Spec} C(x)=\{\prod _{j=1}^{r} x_j=0\}$ for some $1\leq r\leq d$.

As the $\operatorname {Spec} C(x)$ for varying $x\in \mathbf {Z}$ together with $\mathbf {X}\setminus \mathbf {Z}$ forms a Zariski covering of $\mathbf {X}$, it follows from Proposition 9.1(v) that their analytifications form an admissible covering of $X$, and any refinement of this covering by affinoid subdomains has the desired property.