Uniform sheafy Tate rings that are not stably uniform

Christopher Birkbeck

Alex Torzewski

Abstract

Buzzard–Verberkmoes and Mihara show that a stably uniform Tate Huber ring is sheafy. We construct examples of uniform and strongly sheafy Tate rings which are not stably uniform, answering Question 7 of Kedlaya’s Nonarchimedean Scottish Book. In the first example a rational localisation is non-reduced, whilst in the second the rational localisation is an integral domain but is not uniform. The two main results are due to ChatGPT 5.6 Sol. Both constructions, the rational localisations witnessing failure of stable uniformity, and their strong sheafiness have been formalised in Lean 4.

Section 1 Introduction

Work of Buzzard–Verberkmoes and, separately, Mihara shows that every stably uniform Tate Huber ring is sheafy, but leaves open whether every uniform sheafy Tate Huber ring is stably uniform [bib-BV], [bib-Mihara]. Hansen and Kedlaya ask this explicitly [bib-HK, Remark 3.16]; it is also Question 7 of Kedlaya’s Nonarchimedean Scottish Book [bib-Scottish]. We answer this question in the negative, by constructing uniform and sheafy Tate rings that are not stably uniform. In fact, we prove the stronger statement that both examples are strongly sheafy. Both are non-noetherian, so neither Huber’s theorem for strongly noetherian Tate rings nor the stably uniform criterion applies.

The examples and proofs described here were found with the help of AI agents, specifically ChatGPT 5.6 Sol. In Section 9 we describe how we used ChatGPT in the search for these examples. Every result discussed here has also been fully formalised in Lean by Claude Code, and Appendix A records the formal definitions and theorem statements. This article was prepared with the help of AI from an initial human-written skeleton. We have kept many of the names given to our objects by the AI systems. This is a conscious choice intended to make it easier to trace sources that may have influenced their work; see Remark 1.3.

We start with the “finite-jet pullback” example. This is a non-noetherian uniform integral domain for which a certain rational localisation is non-reduced, and hence is no longer uniform. Let \(k\) be a complete discretely valued nonarchimedean field, with valuation ring \(k^\circ\text{,}\) uniformizer \(\varpi\text{,}\) and residue field \(\widetilde{k}\text{.}\) Put

\begin{equation*} L_0=k^\circ\langle W,W^{-1}\rangle, \qquad B_0=k^\circ\langle W,Q\rangle/(Q^2), \end{equation*}

\begin{equation*} C_0=L_0\langle Q\rangle, \qquad D_0=L_0\langle Q\rangle/(Q^2), \end{equation*}

where \(k^\circ\langle W,W^{-1}\rangle\) means \(k^\circ\langle W,V\rangle/(WV-1)\text{.}\) There are natural maps \(B_0\to D_0\) and \(C_0\onto D_0\text{.}\) Define

\begin{equation*} A_0=B_0\times_{D_0}C_0, \qquad A=A_0[1/\varpi], \end{equation*}

and endow \(A\) with the topology defined by the ring of definition \(A_0\text{.}\)

The main result is the following.

Theorem 1.1.

The ring \(A\) is a complete uniform non-noetherian Tate \(k\)-algebra and an integral domain, with \(A^\circ=A_0\text{.}\) It is strongly sheafy; in particular, the Huber pair \((A,A^\circ)\) is sheafy. However,

\begin{equation*} A\left\langle \frac{W}{\varpi}\right\rangle \cong k\langle X,Q\rangle/(Q^2), \qquad X=\frac{W}{\varpi}, \end{equation*}

so \(A\) is not stably uniform.

Lean (finiteJet_isUniform)Lean (finiteJet_isDomain)Lean (finiteJet_not_noetherian)Lean (finiteJet_not_stablyUniform)Lean (chartEquiv)Lean (finite-jet ring A)Lean (coefficient condition defining A)Lean (isClosed_jetSupport)Lean (isTateRing_JetA)Lean (finiteJet_isUniform_of_dvr)Lean (isPowerBounded_JetA_iff)Lean (finiteJet_isDomain)Lean (finiteJet_not_noetherian)Lean (finiteJet_not_stablyUniform_of_dvr)Lean (finiteJet_isSheafyFor_of_dvr)Lean (finiteJet_tateExt_isSheafyComplete_of_dvr)Lean

This construction also gives a new example solving Problems 24 and 28 of the Nonarchimedean Scottish Book. We recall the two problems and give the argument in Section 7.

The key element in this example is that after the rational localisation \(A\to A\langle W/\varpi\rangle\text{,}\) \(Q^2\) vanishes whereas \(Q\) does not. The proof uses Milnor squares of complete Tate rings. Recall that a cartesian square of rings with a surjective leg is called a Milnor square [bib-Milnor, Section 2]; the complete Tate setting is used by Kerz–Saito–Tamme in their work on analytic \(K\)-theory [bib-KST, Section 3].

Definition 1.2.

A commutative square of complete Tate \(k\)-algebras

\begin{equation*} \begin{matrix} A&\longrightarrow&C\\ \downarrow&&\downarrow\\ B&\longrightarrow&D \end{matrix} \end{equation*}

is a strict Milnor square if it is cartesian, the sequence of underlying topological \(k\)-vector spaces

\begin{equation*} 0\longrightarrow A\longrightarrow B\oplus C \xrightarrow{\ (b,c)\mapsto \bar b-\bar c\ }D\longrightarrow 0 \end{equation*}

is strict exact, and \(C\to D\) is a strict surjection.

The maps \(C\to D\) and \(B\oplus C\to D\) are continuous surjections between complete normed \(k\)-vector spaces, and \(A\) has the subspace topology as the kernel of the second. The nonarchimedean open mapping theorem [bib-KST, Lemma 3.1] therefore shows that the square defining \(A\) is strict. Our main input is that, for this finite-jet square, the strict exact row persists after completed rational localisation and is compatible with refinement. This transfers sheafiness from \(B,C,D\) to \(A\text{,}\) giving new ways for proving that these rings are sheafy. The second example shows that the failure of stable uniformity need not come from a non-reduced localisation.

Remark 1.3. Relation with earlier work.

It is difficult to understand exactly what sources an AI agent such as ChatGPT may have used in doing this work. In the interest of giving appropriate credit, we have listed here closely related work that may have been used in the development of the results here.

Buzzard–Verberkmoes construct a uniform affinoid ring with a rational localisation which is not uniform and, separately, a uniform affinoid ring whose structure presheaf is not a sheaf [bib-BV, Propositions 17 and 18]. Mihara gives further examples of both phenomena [bib-Mihara]. These examples do not give a uniform sheafy ring which is not stably uniform.

Ben-Bassat–Kremnizer prove strict two-term resolutions for Weierstrass and Laurent localisations, and reduce a general rational localisation to these cases [bib-BBK, Lemmas 5.13--5.14]. Bambozzi–Kremnizer formulate rational localisation in terms of Koszul complexes and prove strict Koszul regularity [bib-BK, Notation 4.3, Definitions 4.5--4.6, Proposition 4.9, Lemma 4.11, and Corollary 4.13]. The bounded-denominator estimates in Lemma 5.1 are the form needed to show that rational localisation preserves the finite-jet Milnor square. The resulting uniform sheafy domain which is not stably uniform appears to be new.

The weighted-parity construction of Section 8 is closer to the infinite monomial-support examples of Buzzard–Verberkmoes and Mihara. Its additional feature is that rational localisation can be calculated in a noetherian finite-variable subring.

Section 2 Conventions and notation

We follow Huber for Huber pairs, adic spectra, rational subsets, and rational localisation [bib-Huber94], and use Wedhorn’s account for strong noetherianity and sheafiness [bib-Wedhorn, Proposition and Definition 6.36, Section 8.1]; the bounded-denominator language for strictness follows Buzzard–Verberkmoes [bib-BV], and the quotient presentation of a rational localisation is also discussed by Hansen–Kedlaya [bib-HK].

Tate topology. Throughout, \(E\) denotes a complete Tate \(k\)-algebra. In the discretely valued setting of this paper, this means that \(E\) contains a topologically nilpotent unit and admits an open bounded \(k^\circ\)-subalgebra \(E_0\) such that

\begin{equation*} E=E_0[1/\varpi], \qquad \{\varpi^nE_0\}_{n\geq0} \end{equation*}

is a basis of neighbourhoods of zero. Such an \(E_0\) is called a ring of definition. We always choose it closed, hence \(\varpi\)-adically complete. A subset of \(E\) is bounded if it is contained in \(\varpi^{-r}E_0\) for some \(r\geq0\text{.}\)
Uniformity and noetherianity. We write \(E^\circ\) for the ring of power-bounded elements. The ring \(E\) is uniform if \(E^\circ\) is bounded, and strongly noetherian if \(E\langle Z_1,\ldots,Z_s\rangle\) is noetherian for every \(s\geq0\text{.}\) A Tate ring is stably uniform if every rational localisation is uniform.
Huber pairs and sheafiness. A ring of integral elements is an open subring \(E^+\subseteq E^\circ\) which is integrally closed in \(E\text{.}\) We call the Huber pair \((E,E^+)\) sheafy when its structure presheaf, valued in complete topological rings, satisfies the sheaf condition. Thus, for a finite rational cover \(U=\bigcup_iU_i\text{,}\) restriction identifies \(\mathcal O(U)\) homeomorphically with the subspace of \(\prod_i\mathcal O(U_i)\) consisting of tuples whose restrictions to every \(U_i\cap U_j\) agree.
Strictness. We use the following bounded-denominator form of strictness. Let \(u:M\to N\) be a continuous \(k\)-linear map, and let \(M_0\subset M\) and \(N_0\subset N\) be open bounded \(k^\circ\)-submodules. Then \(u\) is strict if and only if there exists \(a\geq0\) such that

\begin{equation*} \varpi^a\bigl(u(M)\cap N_0\bigr)\subset u(M_0). \end{equation*}

For a surjection this becomes \(\varpi^aN_0\subset u(M_0)\text{.}\) For an injection it says that the inverse image of \(N_0\) is bounded in \(M\text{.}\) This is the criterion used by Buzzard–Verberkmoes [bib-BV, Lemma 2]. We use the term strict Milnor square in the sense of Definition 1.2; the underlying algebraic terminology is standard [bib-Milnor], [bib-KST].
Rational localisation. We take every rational datum to have at least one numerator; an empty list may be padded by \(f_1=0\text{.}\) Let \(\alpha=(f_1,\dots,f_m;g)\) be a rational datum in \(E\text{,}\) so the ideal generated by \(g,f_1,\dots,f_m\) is open. Since \(E\) is a Tate \(k\)-algebra, this ideal is the unit ideal. After multiplying the entire datum by a common power of \(\varpi\text{,}\) we may assume that all entries lie in \(E_0\text{.}\)

The rational localisation \(E_\alpha\) is the \(\varpi\)-adic completion of \(E[1/g]\) for the ring of definition generated by

\begin{equation*} E_0\left[\frac{f_1}{g},\dots,\frac{f_m}{g}\right]. \end{equation*}

For such a ring of definition \(R\text{,}\) we use the notation

\begin{equation*} \widehat R=\varprojlim_{n\geq1}R/\varpi^nR, \qquad \ker(R\longrightarrow\widehat R)=\bigcap_{n\geq1}\varpi^nR. \end{equation*}

\(E_\alpha\) is independent of the ring of definition and of the presentation of the rational domain, and it is transitive under rational refinement. Put

\begin{equation*} T_E=E\langle T_1,\dots,T_m\rangle =E_0\langle T_1,\dots,T_m\rangle[1/\varpi], \qquad r_i=gT_i-f_i, \end{equation*}

and

\begin{equation*} I_{E,\alpha}:=(r_1,\dots,r_m) =\operatorname{im}\left( T_E^m\xrightarrow{\ d_{1,E}\ }T_E \right)\subset T_E, \end{equation*}

where \(d_{1,E}(u_1,\dots,u_m)=\sum_i u_i(gT_i-f_i).\) Then we have

\begin{equation} E_\alpha\cong T_E/\overline{I_{E,\alpha}}.\tag{2.1} \end{equation}

Here the bar is necessary until the ideal has been shown to be closed. This is the standard quotient presentation of rational localisation; see [bib-Huber94, Notations, (1.2), Proposition 1.3, Lemma 1.5] and [bib-HK, Definition 3.6].

Section 3 The finite-jet ring

In this section we identify the finite-jet algebra with a concrete subring of \(C\) and prove that it is a complete uniform domain. Recall that

\begin{equation*} L_0=k^\circ\langle W,W^{-1}\rangle, \qquad B_0=k^\circ\langle W,Q\rangle/(Q^2), \end{equation*}

\begin{equation*} C_0=L_0\langle Q\rangle, \qquad D_0=L_0\langle Q\rangle/(Q^2), \end{equation*}

where \(k^\circ\langle W,W^{-1}\rangle\) denotes \(k^\circ\langle W,V\rangle/(WV-1)\text{.}\) The natural maps \(B_0\to D_0\) and \(C_0\onto D_0\) allow us to define

\begin{equation*} A_0=B_0\times_{D_0}C_0. \end{equation*}

We write

\begin{equation*} A=A_0[1/\varpi],\quad L=L_0[1/\varpi],\quad B=B_0[1/\varpi],\quad C=C_0[1/\varpi],\quad D=D_0[1/\varpi]. \end{equation*}

Each of these Tate rings carries the topology defined by the corresponding subscript-zero ring.

The results in this section and the next do not require the valuation on \(k\) to be discrete. They hold for any complete ultrametric normed field \(k\) and any chosen \(\varpi\in k^\times\) with \(0<|\varpi|<1\text{,}\) with the same definitions using the norm unit ball \(k^\circ\text{.}\) We return to the discretely valued hypothesis in Section 5.

The quotient map \(C_0\to D_0\) has a continuous \(k^\circ\)-linear section

\begin{equation*} \sigma:D_0\longrightarrow C_0,\qquad \sigma(f_0+Qf_1)=f_0+Qf_1, \end{equation*}

obtained by viewing the unique representative of \(Q\)-degree at most one as an element of \(C_0\text{.}\) Consequently

\begin{equation*} 0\longrightarrow A_0\longrightarrow B_0\oplus C_0 \longrightarrow D_0\longrightarrow 0 \end{equation*}

is exact, and \(A_0\) is \(\varpi\)-adically complete. After inverting \(\varpi\) we obtain a strict Milnor square

\begin{equation*} \begin{matrix} A&\longrightarrow&C\\ \downarrow&&\downarrow\\ B&\longrightarrow&D. \end{matrix} \end{equation*}

The map \(B_0\to D_0\) is injective. Projection to \(C_0\) therefore identifies \(A_0\) with the subring

\begin{equation} A_0= \left\{ f_0(W)+Qf_1(W)+Q^2h(W,W^{-1},Q): f_0,f_1\in k^\circ\langle W\rangle, \ h\in C_0 \right\}.\tag{3.1} \end{equation}

Equivalently, \(A_0\) consists of the restricted series

\begin{equation*} \sum_{(a,b)\in S}c_{a,b}W^aQ^b, \qquad S=\{(a,b)\in\mathbb Z\times\mathbb N: b\leq 1\Rightarrow a\geq 0\}, \end{equation*}

with \(c_{a,b}\in k^\circ\text{.}\) Here restricted means that, for every \(n\text{,}\) only finitely many coefficients are nonzero modulo \(\varpi^n\text{.}\) The set \(S\) is closed under addition, so this is a subring of \(C_0\text{.}\) The same description with coefficients in \(k\) gives \(A\subset C\text{.}\)

Equip \(A,B,C,D\) with the coefficientwise Gauss norms whose unit balls are \(A_0,B_0,C_0,D_0\text{,}\) respectively. Write

\begin{equation*} \iota_B:A\to B,\qquad \iota_C:A\to C,\qquad \rho_B:B\to D,\qquad \rho_C:C\to D \end{equation*}

for the structural maps, and give \(A\) the restricted Gauss norm from \(C\text{.}\) For \(a=f_0+Qf_1+Q^2h\text{,}\) the coefficient formulas give

\begin{equation} \lVert\iota_C(a)\rVert_C=\lVert a\rVert_A, \qquad \lVert\iota_B(a)\rVert_B\leq \lVert a\rVert_A, \qquad \lVert\rho_B(b)\rVert_D\leq\lVert b\rVert_B, \qquad \lVert\rho_C(c)\rVert_D\leq\lVert c\rVert_C.\tag{3.2} \end{equation}

Thus every structural map is norm-nonincreasing.

Proposition 3.1.

The ring \(A\) is a complete uniform non-noetherian Tate \(k\)-algebra and an integral domain. Moreover,

\begin{equation*} A^\circ=A_0. \end{equation*}

Lean (finiteJet_isUniform)Lean (finiteJet_isDomain)Lean (finiteJet_not_noetherian)Lean (isClosed_jetSupport)Lean (isTateRing_JetA)Lean (finiteJet_isUniform_of_dvr)Lean (isPowerBounded_JetA_iff)Lean (finiteJet_isDomain)Lean (finiteJet_not_noetherian)

Proof.

The Gauss norm on \(L=k\langle W,W^{-1}\rangle\) is multiplicative, and the restricted Gauss norm on \(C=L\langle Q\rangle\) is therefore multiplicative as well. In particular, \(C\) is a domain, and hence so is its subring \(A\text{.}\) The constant- and linear-coefficient maps \(C\to L\) are continuous, and \(k\langle W\rangle\) is closed in \(L=k\langle W,W^{-1}\rangle\) for the Gauss norm. Hence the condition that these two coefficients lie in \(k\langle W\rangle\) defines a closed subring of \(C\text{,}\) so \(A\) is complete. The image of \(\varpi\) in \(A\) is a topologically nilpotent unit, and therefore \(A\) is a Tate ring.

The coefficient description of \(A_0\) shows that it is exactly the unit ball for the restricted Gauss norm on \(A\text{.}\) Since this norm is multiplicative,

\begin{equation*} \lVert a^n\rVert=\lVert a\rVert^n. \end{equation*}

It follows that \(a\) is power-bounded if and only if \(\lVert a\rVert\leq1\text{.}\) Thus \(A^\circ=A_0\text{,}\) and the unit ball is bounded, so \(A\) is uniform.

To see that \(A\) is not noetherian, let \(J=\ker(\iota_B)=Q^2C\subset A\text{.}\) If \(J\) were generated by \(a_1,\ldots,a_r\text{,}\) write \(b_i\in L\) for the coefficient of \(Q^2\) in \(a_i\text{.}\) Now, for every \(\ell\in L\text{,}\) we can write

\begin{equation*} Q^2\ell=\sum_i x_i a_i,\qquad x_i\in A, \end{equation*}

and write \(c_i\) for the constant coefficient of \(x_i\) as a series in \(Q\text{.}\) By (3.1), we have \(c_i\in k\langle W\rangle\text{.}\) Since \(a_i\in Q^2C\text{,}\) its coefficients in degrees \(0\) and \(1\) vanish. The coefficient of \(Q^2\) in \(x_i a_i\) is therefore exactly \(c_i b_i\text{.}\) Comparing the coefficients of \(Q^2\) on both sides gives

\begin{equation*} \ell=\sum_i c_i b_i,\qquad c_i\in k\langle W\rangle. \end{equation*}

Thus \(b_1,\ldots,b_r\) would generate \(L\) as a \(k\langle W\rangle\)-module. This is impossible. Indeed, it would make \(W^{-1}\) integral over \(k\langle W\rangle\text{.}\) Multiplying a monic relation for \(W^{-1}\) of degree \(n\) by \(W^n\) would put \(1\) in the proper ideal \((W)\subset k\langle W\rangle\text{.}\) Thus \(J\) is not finitely generated, and \(A\) is not noetherian.

Section 4 A rational localisation which is not uniform

We next compute the rational chart which witnesses the failure of stable uniformity.

Consider the datum

\begin{equation*} \alpha=(W;\varpi). \end{equation*}

The ideal \((\varpi,W)\) is open, since \(\varpi\) is a unit in \(A\text{.}\) Let

\begin{equation*} A_\alpha=A\left\langle\frac{W}{\varpi}\right\rangle \end{equation*}

be the corresponding rational localisation on which \(|W|\leq |\varpi|\text{,}\) and write \(X=W/\varpi\text{.}\) Since \(\varpi\) is already invertible in \(A\text{,}\) the algebraic localisation does not change the ring. More explicitly, \(A_\alpha\) is obtained by taking the \(\varpi\)-adic completion of \(A_0[X]\subset A\) and then inverting \(\varpi\text{.}\)

Proposition 4.1.

There is a canonical isomorphism of complete topological rings

\begin{equation*} A_\alpha\cong k\langle X,Q\rangle/(Q^2), \qquad W\longmapsto\varpi X,\quad Q\longmapsto Q. \end{equation*}

Lean (chartEquiv)Lean (chartEquiv_continuous)Lean (chartEquiv_symm_continuous)Lean (chartEquiv_canonicalMap_W)Lean (chartDatum_isRational)Lean (chartEquiv)Lean (chartEquiv_continuous)Lean (chartEquiv_symm_continuous)Lean (chartEquiv_canonicalMap_W)

Proof.

Put

\begin{equation*} T_0=k^\circ\langle X,Q\rangle/(Q^2), \qquad T=T_0[1/\varpi]. \end{equation*}

Let \(\rho:A\to A_\alpha\) be the canonical map. We first show that

\begin{equation} Q^2C\subseteq\ker(\rho).\tag{4.1} \end{equation}

Take \(y\in Q^2C\text{,}\) and choose \(r\geq0\) such that \(\varpi^r y\in Q^2C_0\text{.}\) For every \(n\geq0\text{,}\) the coefficient description of \(A_0\) gives

\begin{equation*} W^{-n}\varpi^r y\in A_0. \end{equation*}

Multiplication by \(W^{-n}\) only introduces negative powers of \(W\) in terms of \(Q\)-degree at least two. In \(A_0[X]\text{,}\) where \(W=\varpi X\text{,}\) we therefore have

\begin{equation*} \varpi^r y =W^n(W^{-n}\varpi^r y) =\varpi^nX^n(W^{-n}\varpi^r y)\in\varpi^nA_0[X] \end{equation*}

for every \(n\text{.}\) Hence \(\varpi^r y\) maps to zero in \(\widehat{A_0[X]}\text{.}\) Since \(\varpi\) is invertible in \(A_\alpha\text{,}\) this proves (4.1).

We now construct the isomorphism. Recall that the map \(\iota_B:A\to B\) from the defining pullback is given by

\begin{equation*} f_0(W)+Qf_1(W)+Q^2h\longmapsto f_0(W)+Qf_1(W); \end{equation*}

it simply discards the terms divisible by \(Q^2\text{.}\) The substitution \(W\mapsto\varpi X\text{,}\) \(Q\mapsto Q\) defines a continuous homomorphism \(B\to T\text{.}\) Their composite is

\begin{equation*} \theta:A\longrightarrow T,\qquad f_0(W)+Qf_1(W)+Q^2h\longmapsto f_0(\varpi X)+Qf_1(\varpi X). \end{equation*}

It sends \(A_0\) into \(T_0\) and sends \(W/\varpi\) to \(X\text{.}\) It therefore sends \(A_0[X]\) into \(T_0\) and extends, first to the completions and then after inverting \(\varpi\text{,}\) to a continuous homomorphism

\begin{equation*} \Phi:A_\alpha\longrightarrow T. \end{equation*}

Set

\begin{equation*} \overline X=\rho(W)/\varpi,\qquad \overline Q=\rho(Q). \end{equation*}

Both elements are power-bounded: they belong to the completed ring of definition coming from \(A_0[X]\text{.}\) Moreover, \(\overline Q^{\,2}=0\) by (4.1). Evaluation at \(\overline X\) therefore gives a continuous homomorphism

\begin{equation*} \Psi:T\longrightarrow A_\alpha,\qquad f+Qg\longmapsto f(\overline X)+g(\overline X)\overline Q. \end{equation*}

It remains to check the two composites. Write \(a=f_0(W)+Qf_1(W)+y\in A\text{,}\) with \(y\in Q^2C\text{.}\) Then

\begin{equation*} (\Psi \circ \Phi)(\rho(a)) =f_0(\varpi\overline X)+\overline Qf_1(\varpi\overline X) =\rho\bigl(f_0(W)+Qf_1(W)\bigr) =\rho(a), \end{equation*}

where the last equality uses (4.1). The image of \(A\) is dense in \(A_\alpha\text{,}\) so continuity gives \(\Psi \circ \Phi=1\text{.}\) Conversely, \(\Phi \circ \Psi\) fixes \(k\text{,}\) \(X\) and \(Q\text{,}\) and hence is the identity on the dense subring \(k[X,Q]/(Q^2)\) of \(T\text{.}\) It follows by continuity that \(\Phi\circ \Psi=1\text{.}\) Thus \(\Phi\) and \(\Psi\) are inverse continuous homomorphisms.

Proposition 4.2.

The ring \(A\) is not stably uniform.

Lean (not_isUniform_chart)Lean (finiteJet_not_stablyUniform)Lean (not_isUniform_chart)Lean (finiteJet_not_stablyUniform_of_dvr)

Proof.

In \(T=k\langle X,Q\rangle/(Q^2)\text{,}\) every element of the line \(kQ\) is nilpotent and hence power-bounded. This line is not bounded with respect to the ring of definition \(T_0\text{:}\) for every \(r\geq 0\text{,}\)

\begin{equation*} \varpi^r\bigl(\varpi^{-(r+1)}Q\bigr)=\varpi^{-1}Q\notin T_0. \end{equation*}

Thus \(T\) is not uniform. By Proposition 4.1, \(A_\alpha\) is not uniform.

Section 5 Localisation of the Milnor square

In this section we prove that rational localisation preserves the defining pullback. For the application to the finite-jet ring we again assume that \(k\) is complete and discretely valued. We first record the strict Koszul estimate needed for the proof in the greater generality in which it was formalised.

Subsection 5.1 Koszul complexes for rational localisations

Let \(E\) be a complete ultrametric normed commutative ring with \(\lVert1\rVert=1\text{,}\) and let \(t\in E^\times\) satisfy

\begin{equation*} 0<\lVert t\rVert<1, \qquad \lVert tx\rVert=\lVert t\rVert\lVert x\rVert \quad(x\in E). \end{equation*}

Write \(E_0=\{x\in E:\lVert x\rVert\leq1\}\) for its norm unit ball. Assume that \(E_0\text{,}\) \(E\langle T_1,\ldots,T_m\rangle\text{,}\) and the norm unit ball of this Tate algebra are noetherian. Let \(f_1,\dots,f_m,g\in E\) generate the unit ideal in \(E\text{.}\) Put

\begin{equation*} T_E=E\langle T_1,\dots,T_m\rangle, \qquad T_{E,0}=E_0\langle T_1,\dots,T_m\rangle, \end{equation*}

and set \(r_i=gT_i-f_i\text{.}\)

We give \(T_E\) the topology for which \(\{t^nT_{E,0}\}_{n\geq0}\) is a basis of neighbourhoods of zero. In the standard exterior basis, \(\bigwedge^qT_E^m\) has the finite product topology, and each image has the subspace topology. Thus a differential is strict precisely when it is open onto its image.

The strict Koszul regularity theorem of Bambozzi–Kremnizer [bib-BK, Notation 4.3, Definitions 4.5--4.6, Proposition 4.9, Lemma 4.11, and Corollary 4.13] gives the exactness, strictness, and closed-image assertions below. We include the direct proof followed in the formalisation because the two bounds (5.1) and (5.2) are not stated there and are needed below.

Lemma 5.1.

The Koszul complex

\begin{equation*} 0\longrightarrow \bigwedge^mT_E^m\longrightarrow\cdots \longrightarrow\bigwedge^2T_E^m\xrightarrow{d_{2,E}} T_E^m\xrightarrow{d_{1,E}}T_E \end{equation*}

is exact in positive degrees. Every differential is continuous and strict onto its image, and every image is closed. In particular, if

\begin{equation*} I_E=(r_1,\ldots,r_m)=\im(d_{1,E})\subset T_E, \qquad d_{1,E}(u_1,\ldots,u_m)=\sum_i u_ir_i, \end{equation*}

then \(I_E\) is closed. Moreover, there exists \(h_E\in\mathbb Z_{\geq0}\) such that

\begin{equation} t^{h_E}(I_E\cap T_{E,0}) \subset d_{1,E}(T_{E,0}^m).\tag{5.1} \end{equation}

There also exists \(z_E\in\mathbb Z_{\geq0}\) such that

\begin{equation} t^{z_E}\bigl(\ker(d_{1,E})\cap T_{E,0}^m\bigr) \subset d_{2,E}\bigl(\textstyle\bigwedge^2 T_{E,0}^m\bigr).\tag{5.2} \end{equation}

Lean (koszulGraph_exact_strict_closed)Lean (koszulGraph_restricted_exact)Lean (koszulDifferential_continuous)Lean (koszulDifferential_isStrict)Lean (isClosed_range_koszulDifferential)Lean (pow_smul_graphIdeal_inter_unitBall_subset)Lean (pow_smul_ker_d1_inter_subset)

Proof.

Over the polynomial ring \(E[T_1,\ldots,T_m]\text{,}\) the sequence \(gT_i-f_i\) has Koszul complex exact in positive degrees. Indeed, this may be checked after localising at a prime. If one of the \(gT_i-f_i\) is not in the prime, it is a unit after localisation and the Koszul complex is contractible. If all of them lie in the prime, then \(g\) does not: otherwise all the \(f_i\) would also lie in the prime, contrary to \((g,f_1,\ldots,f_m)=E\text{.}\) Thus \(g\) is invertible there and

\begin{equation*} gT_i-f_i=g(T_i-f_i/g). \end{equation*}

The elements \(T_i-f_i/g\) form a regular sequence, since they are monic linear polynomials in distinct variables. This proves the assertion over the polynomial ring.

The map

\begin{equation*} E[T_1,\ldots,T_m]\longrightarrow T_E \end{equation*}

is flat. Indeed, \(E_0\) is noetherian by assumption, so \(E_0[T_1,\ldots,T_m]\) is noetherian and its \(t\)-adic completion is flat over it [bib-Stacks, Tag 00MB]. After inverting \(t\text{,}\) the resulting map \(E[T_1,\ldots,T_m]\to T_E\) is flat. Tensoring the polynomial Koszul complex with \(T_E\text{,}\) and using the standard base-change identification of its finite free terms, proves positive-degree exactness. Notice that this does not assert exactness in degree zero.

Each differential is continuous because its coordinates are finite sums of multiplication maps. The image of \(d_{1,E}\) is closed by the noetherian closed-ideal theorem. In higher degree, exactness identifies an image with the kernel of the next continuous differential, and hence that image is closed. The nonarchimedean open mapping theorem therefore shows that, for each differential \(d_{q,E}\text{,}\) there is a constant \(C_{q,E}\geq1\) such that every \(y\in\im(d_{q,E})\) has a preimage \(x\) satisfying

\begin{equation*} d_{q,E}(x)=y, \qquad \lVert x\rVert\leq C_{q,E}\lVert y\rVert. \end{equation*}

This also proves that each differential is strict onto its image.

Choose \(h_E\geq0\) such that \(\lVert t\rVert^{h_E}C_{1,E}\leq1\text{.}\) If \(x\in I_E\cap T_{E,0}\text{,}\) choose \(u\in T_E^m\) with

\begin{equation*} d_{1,E}(u)=x, \qquad \lVert u\rVert\leq C_{1,E}\lVert x\rVert\leq C_{1,E}. \end{equation*}

Then \(t^{h_E}u\in T_{E,0}^m\) and \(d_{1,E}(t^{h_E}u)=t^{h_E}x\text{,}\) which proves (5.1). Similarly, choose \(z_E\geq0\) such that \(\lVert t\rVert^{z_E}C_{2,E}\leq1\text{.}\) If \(u\in\ker(d_{1,E})\cap T_{E,0}^m\text{,}\) choose \(v\) with \(d_{2,E}(v)=u\) and \(\lVert v\rVert\leq C_{2,E}\lVert u\rVert\text{.}\) Then \(t^{z_E}v\in\bigwedge^2T_{E,0}^m\text{,}\) proving (5.2).

Subsection 5.2 The defining ideals under pullback

The formal result used here is not specific to the finite-jet rings. Let

\begin{equation*} \begin{matrix} A&\xrightarrow{\phi_C}&C\\ \scriptstyle\phi_B\downarrow&&\downarrow\scriptstyle\psi_C\\ B&\xrightarrow{\psi_B}&D \end{matrix} \end{equation*}

be a cartesian square of complete ultrametric normed commutative rings. We assume that \(\phi_C\) and \(\psi_B\) preserve the norm, that \(\phi_B\) and \(\psi_C\) do not increase it, and that

\begin{equation*} \lVert a\rVert=\max\{\lVert\phi_B(a)\rVert, \lVert\phi_C(a)\rVert\}. \end{equation*}

We also assume that \(\psi_C\) has a norm-preserving section as a map of sets, that \(B,C,D\) have norm-scaling topologically nilpotent units as in Lemma 5.1. For the present number of variables, assume that the three Tate algebras \(T_B,T_C,T_D\) and their norm unit balls are noetherian, and that the norm unit ball of \(D\) is noetherian. These are precisely the noetherian inputs used in the formalisation; no noetherianity of the norm unit balls of \(B\) and \(C\) is required here. The finite-jet square satisfies them, with the coefficientwise section described in Section 3 and with \(t=\varpi\) at each vertex.

Fix elements

\begin{equation*} \alpha=(f_1,\dots,f_m;g) \end{equation*}

in \(A\) which generate the unit ideal. In the Tate setting this is a rational datum. Put

\begin{equation*} r_i=gT_i-f_i\in T_A, \end{equation*}

and use the same notation for its image in \(T_B,T_C\text{,}\) and \(T_D\text{.}\) For \(E\in\{A,B,C,D\}\) put

\begin{equation*} I_E=(r_1,\ldots,r_m)=\im(d_{1,E})\subset T_E. \end{equation*}

Write \(E_\alpha=T_E/I_E\) for the graph quotient. When the vertices are Tate rings, this is the completed rational localisation by (2.1).

The cartesian property and the section of \(C\to D\text{,}\) applied coefficientwise, give an exact sequence

\begin{equation} 0\longrightarrow T_{A,0}\longrightarrow T_{B,0}\oplus T_{C,0}\longrightarrow T_{D,0}\longrightarrow 0.\tag{5.3} \end{equation}

The map \(T_{C,0}\to T_{D,0}\) is surjective, as are the induced maps on finite free modules and their exterior powers. Exactness is coefficientwise: a compatible restricted coefficient pair lifts to \(A_0\text{,}\) and the max-norm identity ensures that the lifted coefficients still tend to zero.

Lemma 5.2.

The ideal \(I_A\) is closed in \(T_A\text{,}\) and the canonical map

\begin{equation*} I_A\longrightarrow I_B\times_{I_D}I_C \end{equation*}

is an isomorphism. Give each \(I_E\) the subspace topology inherited from \(T_E\text{,}\) and give \(I_B\oplus I_C\) the max norm. Then the sequence of topological abelian groups

\begin{equation} 0\longrightarrow I_A\longrightarrow I_B\oplus I_C \longrightarrow I_D\longrightarrow0\tag{5.4} \end{equation}

is strict exact. Here the maps are

\begin{equation*} x\longmapsto(x_B,x_C), \qquad (x_B,x_C)\longmapsto (x_B)_D-(x_C)_D. \end{equation*}

Lean (ext_pair_injective)Lean (ideal_row_surjective)Lean (ideal_pullback_controlled)Lean (isClosed_IA)Lean (ext_pair_injective)Lean (ideal_row_surjective)Lean (ideal_pullback_controlled)Lean (isClosed_IA)

Proof.

For \(E=B,C,D\text{,}\) let \(C_{1,E}\) be as in the proof of Lemma 5.1, and let \(C_{2,D}\) be the corresponding constant for \(d_{2,D}\text{.}\) Take \((x_B,x_C)\in I_B\times_{I_D}I_C\text{,}\) and choose \(u_B\in T_B^m\) and \(u_C\in T_C^m\) such that

\begin{equation*} d_{1,B}(u_B)=x_B,\qquad \lVert u_B\rVert\leq C_{1,B}\lVert x_B\rVert, \end{equation*}

\begin{equation*} d_{1,C}(u_C)=x_C,\qquad \lVert u_C\rVert\leq C_{1,C}\lVert x_C\rVert. \end{equation*}

In \(T_D^m\) the difference

\begin{equation*} w=(u_B)_D-(u_C)_D \end{equation*}

belongs to \(\ker(d_{1,D})\text{.}\) Choose \(v_D\in\bigwedge^2T_D^m\) such that

\begin{equation*} d_{2,D}(v_D)=w,\qquad \lVert v_D\rVert\leq C_{2,D}\lVert w\rVert. \end{equation*}

The norm-preserving coefficientwise section \(T_D\to T_C\) induces a norm-preserving section on second exterior powers; use it to obtain \(v_C\in\bigwedge^2T_C^m\) mapping to \(v_D\text{.}\) Replacing \(u_C\) by

\begin{equation*} u_C'=u_C+d_{2,C}(v_C) \end{equation*}

does not change \(d_{1,C}(u_C)\text{,}\) and the images of \(u_B\) and \(u_C'\) in \(T_D^m\) now agree. Exactness of (5.3), applied coefficientwise, gives \(u_A\in T_A^m\) mapping to this pair. Then \(d_{1,A}(u_A)\) maps to \((x_B,x_C)\text{.}\)

These bounds, continuity of \(d_{2,C}\text{,}\) and the norm-preserving coefficientwise section give a constant \(C\text{,}\) independent of \((x_B,x_C)\text{,}\) for which \(x_A=d_{1,A}(u_A)\) satisfies

\begin{equation*} \lVert x_A\rVert\leq C\max\{\lVert x_B\rVert,\lVert x_C\rVert\}. \end{equation*}

The map \(T_A\to T_B\oplus T_C\) is injective, so this proves both the algebraic pullback assertion and the boundedness of its inverse.

It remains to see that \(I_A\) is closed. The ideals \(I_B\) and \(I_C\) are closed by Lemma 5.1. If \(x\) lies in the closure of \(I_A\text{,}\) its images lie in \(I_B\) and \(I_C\text{.}\) The pullback isomorphism just proved gives \(x_A\in I_A\) with the same two images as \(x\text{.}\) Injectivity of \(T_A\to T_B\oplus T_C\) gives \(x=x_A\text{,}\) as required.

Finally, for \(y\in I_D\) choose \(u_D\in T_D^m\) such that

\begin{equation*} d_{1,D}(u_D)=y,\qquad \lVert u_D\rVert\leq C_{1,D}\lVert y\rVert. \end{equation*}

Apply the norm-preserving section \(T_D^m\to T_C^m\) and then \(d_{1,C}\text{.}\) This gives \(x_C\in I_C\) mapping to \(y\text{,}\) with \(\lVert x_C\rVert\) bounded by a fixed multiple of \(\lVert y\rVert\text{.}\) Thus \(I_B\oplus I_C\to I_D\) is a strict surjection. Its kernel is \(I_A\) by the pullback assertion, and the preceding bound for the inverse \(I_B\times_{I_D}I_C\to I_A\) makes the inclusion on the left strict. This proves (5.4).

Proposition 5.3.

For every unit-ideal datum \(\alpha\) as above, the canonical sequence of graph quotients

\begin{equation*} 0\longrightarrow A_\alpha\longrightarrow B_\alpha\oplus C_\alpha\longrightarrow D_\alpha\longrightarrow 0 \end{equation*}

is strict exact, and \(C_\alpha\to D_\alpha\) is a strict surjection. Equivalently,

\begin{equation*} A_\alpha\cong B_\alpha\times_{D_\alpha}C_\alpha. \end{equation*}

Lean (loc_row_exact)Lean (loc_pair_isEmbedding)Lean (locψC_lipschitz)Lean (locψC_surjective)Lean (locψC_isOpenMap)Lean (bridgeFwd_natural_B)Lean (bridgeFwd_natural_C)Lean (bridgeFwd_natural_legB)Lean (bridgeFwd_natural_legC)Lean (valueRow_injective)Lean (valueRow_glue)Lean (valueRow_embedding)Lean (loc_row_exact)Lean (loc_pair_isEmbedding)Lean (locRhoC_surjective)Lean (locRhoC_continuous)Lean (locRhoC_isOpenMap)Lean (presheafValueMapC_restriction)Lean (presheafValueMapB_restriction)

Proof.

The ideals \(I_B,I_C,I_D\) are closed by Lemma 5.1, and \(I_A\) is closed by Lemma 5.2. Thus

\begin{equation*} E_\alpha=T_E/I_E \qquad(E=A,B,C,D). \end{equation*}

We first prove algebraic exactness. If a representative \(p\in T_A\) maps into both \(I_B\) and \(I_C\text{,}\) the pullback assertion in Lemma 5.2 gives an element of \(I_A\) with the same two images. Injectivity of \(T_A\to T_B\oplus T_C\) then shows that \(p\in I_A\text{.}\) This gives injectivity on the left. Conversely, take compatible classes in \(T_B/I_B\) and \(T_C/I_C\) and choose representatives \(b\) and \(c\text{.}\) Their defect in \(T_D\) belongs to \(I_D\text{.}\) Lift this defect to an element of \(I_C\) using the strict surjection in (5.4), and add it to \(c\text{.}\) The corrected representatives agree in \(T_D\text{,}\) so (5.3) lifts them to \(T_A\text{.}\) This proves algebraic exactness.

For the topology on the left, let \(x\in A_\alpha\) and put

\begin{equation*} M=\max\{\lVert x_B\rVert,\lVert x_C\rVert\}. \end{equation*}

Choose representatives \(b\in T_B\) and \(c\in T_C\) whose norms are arbitrarily close to the quotient norms of \(x_B\) and \(x_C\text{.}\) Their defect lies in \(I_D\text{.}\) The norm estimate for \(I_C\to I_D\) proved in Lemma 5.2 gives a constant \(C_0\) and a correction \(y\in I_C\) mapping to this defect such that

\begin{equation*} \lVert y\rVert\leq C_0\lVert b_D-c_D\rVert. \end{equation*}

Thus \(b\) and \(c+y\) agree in \(T_D\) and lift to \(p\in T_A\text{.}\) The max-norm identity for the ambient pullback gives, after letting the error in the representatives tend to zero,

\begin{equation*} \lVert x\rVert\leq C M \end{equation*}

for a constant \(C\) depending only on the datum. The two quotient maps are norm-nonincreasing, so this estimate says precisely that \(A_\alpha\to B_\alpha\oplus C_\alpha\) is a topological embedding.

The coefficientwise section \(T_D\to T_C\) shows directly that \(C_\alpha\to D_\alpha\) is surjective. More precisely, choose a representative in \(T_D\) whose norm is arbitrarily close to the quotient norm of a given class in \(D_\alpha\text{,}\) and apply the norm-preserving section. Its class in \(C_\alpha\) has no larger norm. Thus the surjection is open; together with continuity, this says that it is strict.

Applying the preceding two results to the finite-jet square gives the strict localised Milnor rows used below. For this square, the coefficient maps in the identifications commute with rational restriction. The same abstract result applies after adjoining any finite number of Tate variables.

Section 6 Milnor descent and strong sheafiness

The preceding localisation result gives the following general descent criterion.

Theorem 6.1. Milnor descent.

Let \(R,B,C,D\) be complete nonarchimedean Huber rings in a commutative square

\begin{equation*} \begin{matrix} R&\longrightarrow&C\\ \big\downarrow&&\big\downarrow\\ B&\longrightarrow&D. \end{matrix} \end{equation*}

Assume that rational data, covers, and compatible families can be transported around the square, compatibly with restriction and passage to common refinements. Suppose also that, for every rational datum on \(R\text{,}\) the equaliser and topological-embedding conclusions of Proposition 5.3 hold for the induced data. If \(B,C,D\) are sheafy, then \(R\) is sheafy.

Lean

Proof.

Let \(U=\bigcup_iU_i\) be a finite rational cover. A compatible family glues over \(B\) and \(C\text{.}\) The two resulting sections have the same image over \(D\text{,}\) so the equaliser property gives a unique section over \(R\text{.}\) The topological-embedding property, together with the corresponding property for \(B\) and \(C\text{,}\) gives the topological sheaf condition. The rational-basis theorem now gives the sheaf condition on all opens [bib-Stacks, Tag 009O].

Corollary 6.2.

For every \(s\geq0\) and every ring of integral elements

\begin{equation*} A_s^+\subseteq A\langle V_1,\ldots,V_s\rangle^\circ, \end{equation*}

the Huber pair

\begin{equation*} \bigl(A\langle V_1,\ldots,V_s\rangle,A_s^+\bigr) \end{equation*}

is sheafy. In particular, \(A\) is strongly sheafy.

Lean (isSheafy_JetA_of_dvr)Lean (finiteJet_isSheafyFor_of_dvr)Lean (finiteJet_isSheafyTateRing_of_dvr)Lean (finiteJet_structurePresheaf_isSheafOfTopologicalRings_all_of_dvr)Lean (finiteJet_tateExt_isSheafyComplete)

The proof below works over the complete discretely valued base fixed in the introduction. More generally, it only assumes that the base is a complete ultrametric field with a chosen uniformizer and noetherian norm unit ball.

Proof.

The estimates (3.2) make the structural maps morphisms of Huber pairs. The rings \(B,C,D\) are strongly noetherian affinoid \(k\)-algebras and hence sheafy by Huber’s theorem [bib-Huber94, Theorem 2.2]. Proposition 5.3, together with its compatibility under refinement, supplies the hypotheses of Theorem 6.1. This proves sheafiness for \(A\text{,}\) independently of the choice of its ring of integral elements.

After adjoining \(V_1,\ldots,V_s\text{,}\) the square retains its coefficientwise section of \(C\to D\text{,}\) and the strict exact rows of Proposition 5.3 remain strict exact for every unit-ideal datum, while \(B\text{,}\) \(C\) and \(D\) remain strongly noetherian. Applying the same theorem proves the assertion for every \(s\) and every \(A_s^+\text{.}\)

Proof of Theorem 1.1.

Proposition 3.1 proves that \(A\) is complete, uniform, non-noetherian, and a domain. Strong sheafiness is Corollary 6.2, and failure of stable uniformity is Proposition 4.2.

Section 7 Problems 24 and 28

Problem 24 of the Nonarchimedean Scottish Book asks whether the map of rings underlying a rational localisation of Tate Huber pairs must be flat. Problem 28 asks whether a non-zero-divisor which generates a closed ideal can restrict to zero on a nonempty rational subspace [bib-Scottish, Problems 24 and 28]. The same rational datum, together with multiplicativity of the Gauss norm, answers both questions. We keep the notation of the introduction. In fact, the argument only uses that \(k\) is complete and ultrametric and that \(0<|\varpi|<1\text{;}\) neither conclusion uses sheafiness. For Problem 28 this answers the Tate-ring case; we do not address the separate perfectoid case.

Proposition 7.1.

Let \(k\) be any complete ultrametric normed field, choose \(\varpi\in k^\times\) with \(0<|\varpi|<1\text{,}\) and form \(A\) as above. Let

\begin{equation*} U=\{x\in\Spa(A,A^\circ):|W(x)|\leq|\varpi(x)|\}. \end{equation*}

Then \(U\) is nonempty, the rational localisation

\begin{equation*} A\longrightarrow \mathcal O(U) =A\left\langle\frac{W}{\varpi}\right\rangle \end{equation*}

is not flat, and multiplication by \(Q^2\) is a strict embedding with closed image even though \(Q^2\) maps to zero in \(\mathcal O(U)\text{.}\)

Lean (hypothesis on the base field)Lean (the p-adic finite-jet ring)Lean (evaluation at W=Q=0)Lean (the point lies in the chart)Lean (multiplication by Q² is an isometry)Lean (Q² restricts to zero)Lean (Problem 28 witness)Lean (nonflat completed chart)

Proof.

The composite

\begin{equation*} A\longrightarrow B=k\langle W,Q\rangle/(Q^2) \longrightarrow k, \qquad f_0(W)+Qf_1(W)+Q^2h\longmapsto f_0(0), \end{equation*}

is norm-nonincreasing. It therefore sends \(A^\circ\) into \(k^\circ\text{,}\) and pulling back the norm valuation on \(k\) gives a continuous valuation belonging to \(\Spa(A,A^\circ)\text{.}\) At this point \(W\) has value zero and \(\varpi\) has nonzero value, so the point lies in \(U\text{.}\)

Since the restricted Gauss norm on \(A\) is multiplicative and \(\lVert Q\rVert=1\text{,}\) for every \(a\in A\) we have

\begin{equation*} \lVert Q^2a\rVert=\lVert a\rVert. \end{equation*}

Thus multiplication by \(Q^2\) is an isometry. Its map onto its image, with the subspace topology, is consequently a homeomorphism, so the inclusion is strict. Moreover, an isometric image of the complete space \(A\) is closed in \(A\text{.}\) Since \(\lVert Q^2\rVert=1\text{,}\) the element \(Q^2\) is nonzero; multiplication by it is therefore injective because \(A\) is a domain.

On the other hand, the calculation (4.1) says directly that the canonical map to the completed rational localisation kills \(Q^2\text{.}\) The isomorphism of Proposition 4.1 identifies this localisation with the nonzero ring

\begin{equation*} A\longrightarrow k\langle X,Q\rangle/(Q^2), \qquad W\longmapsto\varpi X,\quad Q\longmapsto Q. \end{equation*}

If the canonical map were flat, the non-zero-divisor \(Q^2\) would still act injectively on \(\mathcal O(U)\text{;}\) equivalently, tensoring the injection

\begin{equation*} 0\longrightarrow A\xrightarrow{\,\cdot Q^2\,}A \end{equation*}

with \(\mathcal O(U)\) would make multiplication by the image of \(Q^2\) injective. Its image is zero, however, so this multiplication map is zero on the nonzero ring \(\mathcal O(U)\text{,}\) a contradiction.

Section 8 A second example

In the finite-jet construction, the bad rational localisation is non-reduced. In our second example it is an integral domain; the loss of uniformity is instead caused by an unbounded family of non-nilpotent power-bounded elements.

The formal statements in this section use the following base hypotheses: \(k\) is a complete nontrivially normed ultrametric field, its norm unit ball is noetherian, and \(\varpi\) is a chosen uniformizer.

Theorem 8.1.

Let \(w:\mathbb N_{>0}\to\mathbb N\) satisfy \(w(n)\geq1\) for every \(n\) and be unbounded. The complete Tate \(k\)-algebra \(\mathcal A_w\) defined below has the following properties.

\(\mathcal A_w\) is a uniform, non-noetherian integral domain and \(\mathcal A_w^\circ=\mathcal A_{w,0}\text{,}\) where \(\mathcal A_{w,0}\) is defined below.
The ring \(\mathcal A_w\) is strongly sheafy; in particular, the Huber pair \((\mathcal A_w,\mathcal A_w^\circ)\) is sheafy.
The rational localisation

\begin{equation*} \mathcal B_w=\mathcal A_w\left\langle\frac{W}{\varpi}\right\rangle \end{equation*}

is an integral domain but is not uniform.

Consequently \(\mathcal A_w\) is not stably uniform. In particular, failure of stable uniformity need not be caused by a nilpotent in the bad rational localisation.

Lean (Tate structure)Lean (norm_wpa_mul)Lean (isUniform_WPA)Lean (powerBoundedSubring_eq_unitBall)Lean (not_isNoetherianRing_WPA)Lean (wp_isSheafyComplete)Lean (isDomain_chart)Lean (not_isUniform_chart)Lean (not_isStablyUniform_WPA)Lean (wp_tateExt_isSheafyComplete)Lean (uniformity)Lean (domain)Lean (power-bounded elements)Lean (non-noetherianity)Lean (sheafiness)Lean (chart is a domain)Lean (chart is nonuniform)Lean (weightedParity_not_stablyUniform_of_dvr)Lean (wp_tateExt_isSheafyComplete_of_dvr)

Taking \(w(n)=n\) gives the example announced in the introduction. We prove the component statements below for the weakest hypotheses on \(w\) that they require.

Subsection 8.1 The weighted-parity algebra

We write \(\mathbb N=\{0,1,2,\ldots\}\text{,}\) put \(I=\mathbb N_{>0}\text{,}\) and fix an arbitrary function \(w:I\to\mathbb N\text{.}\) For a finite-support multi-index \(\nu=(\nu_n)_{n\in I}\in\mathbb N^{(I)}\text{,}\) put

\begin{equation} \omega_w(\nu)=\sum_{\substack{n\geq1\\ \nu_n\text{ odd}}} w(n).\tag{8.1} \end{equation}

To lighten the notation, write \(\omega=\omega_w\) for the rest of the section. Consider the submonoid

\begin{equation} S=\left\{(a,\nu)\in\mathbb N\times\mathbb N^{(I)}: a\geq\omega(\nu)\right\}.\tag{8.2} \end{equation}

The inequality

\begin{equation} \omega(\nu+\mu)\leq\omega(\nu)+\omega(\mu)\tag{8.3} \end{equation}

shows that \(S\) is closed under addition. It is locally finite: a fixed element of \(S\) has only finitely many decompositions as a sum of two elements of \(S\text{.}\)

Let \(k[S]\) be the monoid algebra with basis \(W^aU^\nu\text{,}\) where \(U^\nu=\prod_nU_n^{\nu_n}\text{.}\) Give it the Gauss norm

\begin{equation} \left\lVert\sum_{(a,\nu)\in S}c_{a,\nu}W^aU^\nu\right\rVert_G =\sup_{a,\nu}|c_{a,\nu}|.\tag{8.4} \end{equation}

Its completion is denoted by \(\mathcal A_w\text{,}\) or simply \(\mathcal A\) when \(w\) is understood:

\begin{equation} \mathcal A_w= \left\{ \sum_{(a,\nu)\in S}c_{a,\nu}W^aU^\nu: c_{a,\nu}\in k,\quad c_{a,\nu}\longrightarrow0 \right\},\tag{8.5} \end{equation}

where convergence to zero is over the discrete index set \(S\text{.}\) Local finiteness makes the coefficientwise convolution finite, and the submultiplicativity of the Gauss norm on \(k[S]\) extends multiplication continuously to \(\mathcal A\text{.}\) Put

\begin{equation*} \mathcal A_{w,0}= \left\{ \sum_{(a,\nu)\in S}c_{a,\nu}W^aU^\nu\in\mathcal A_w: c_{a,\nu}\in k^\circ \right\}. \end{equation*}

We henceforth abbreviate these rings to \(\mathcal A\) and \(\mathcal A_0\text{.}\) Then \(\mathcal A_0\) is the closed unit ball for (8.4), it is \(\varpi\)-adically complete, and \(\mathcal A=\mathcal A_0[1/\varpi]\text{.}\)

Put

\begin{equation*} Y_n=W^{w(n)}U_n,\qquad Z_n=U_n^2, \end{equation*}

and, for \(N\in\mathbb N\text{,}\) let \(\mathcal A^{(N)}\subset\mathcal A\) be the closed subring supported on monomials involving only \(W,U_1,\ldots,U_N\text{.}\) Thus \(\mathcal A^{(0)}=k\langle W\rangle\text{.}\) Let \(\mathcal T^{(N)}\subset\mathcal A^{(N)}\) be the subring in which every \(U_n\) has even exponent.

Lemma 8.2. Finite-variable subrings.

For every weight \(w\) and every \(N\in\mathbb N\text{,}\) substitution \(Z_n\mapsto U_n^2\) gives a norm-preserving ring isomorphism

\begin{equation*} k\langle W,Z_1,\ldots,Z_N\rangle \xrightarrow{\ \sim\ }\mathcal T^{(N)}. \end{equation*}

For \(N=0\) this is the evident identification of both sides with \(k\langle W\rangle\text{.}\) Every \(f\in\mathcal A^{(N)}\) can be written

\begin{equation} f=\sum_{\epsilon\in\{0,1\}^N} f_\epsilon Y^\epsilon, \qquad f_\epsilon\in\mathcal T^{(N)}, \qquad Y^\epsilon=\prod_{n=1}^NY_n^{\epsilon_n}.\tag{8.6} \end{equation}

Consequently \(\mathcal A^{(N)}\) is finite over \(\mathcal T^{(N)}\) and is a strongly noetherian Tate ring. The inclusions \(\mathcal A^{(N)}\to\mathcal A^{(M)}\to\mathcal A\) for \(N\leq M\) preserve the norm. Moreover, for every \(f\in\mathcal A\) and \(\ell\geq0\) there are \(N\) and \(f_N\in\mathcal A^{(N)}\) such that

\begin{equation*} \lVert f-f_N\rVert_G\leq |\varpi|^\ell\lVert f\rVert_G. \end{equation*}

In particular,

\begin{equation} \mathcal A=\widehat{\bigcup_{N\geq0}\mathcal A^{(N)}}.\tag{8.7} \end{equation}

Lean (even Tate algebra)Lean (norm preservation)Lean (finite decomposition)Lean (finite module)Lean (Tate structure)Lean (strong noetherianity)Lean (nested finite-variable rings)Lean (isometric inclusion)Lean (approximation and density)

Proof.

On even exponents, halving the \(U_n\)-coordinates identifies the support monoid with that of the Tate algebra \(k\langle W,Z_1,\ldots,Z_N\rangle\text{;}\) the coefficient map and its inverse preserve the Gauss norm. Write each exponent uniquely as \(\nu_n=2q_n+\epsilon_n\text{,}\) with \(\epsilon_n\in\{0,1\}\text{.}\) Since \(\omega(\nu)=\sum_{\epsilon_n=1}w(n)\text{,}\) every allowed monomial factors as

\begin{equation*} W^aU^\nu =W^{a-\omega(\nu)} \prod_{n=1}^NZ_n^{q_n} \prod_{n=1}^NY_n^{\epsilon_n}. \end{equation*}

Grouping the monomials with the same tuple \((\epsilon_1,\ldots,\epsilon_N)\) gives (8.6). The finitely many \(Y^\epsilon\) therefore generate \(\mathcal A^{(N)}\) over \(\mathcal T^{(N)}\text{.}\) The same argument after adjoining any finite number of Tate variables gives strong noetherianity. The inclusions are coefficientwise and hence isometric. Finally, approximate \(f\) to the required precision by a finite sum of monomials and choose \(N\) so that only \(U_1,\ldots,U_N\) occur in that sum. This gives the stated estimate and (8.7).

Proposition 8.3.

For every weight \(w\text{,}\) the ring \(\mathcal A_w\) is a complete uniform Tate \(k\)-algebra and an integral domain, with

\begin{equation*} \mathcal A_w^\circ=\mathcal A_{w,0}. \end{equation*}

Lean (Tate structure)Lean (norm_wpa_mul)Lean (isUniform_WPA)Lean (powerBoundedSubring_eq_unitBall)Lean (uniformity)Lean (domain)Lean (power-bounded elements)

Proof.

Let \(f\) and \(g\) be nonzero elements of \(k\langle W,U_1,U_2,\ldots\rangle\text{.}\) Since their coefficients tend to zero, each Gauss norm is attained by a coefficient. After dividing \(f\) and \(g\) by coefficients of maximal norm, we may assume that

\begin{equation*} \lVert f\rVert_G=\lVert g\rVert_G=1. \end{equation*}

Only finitely many coefficients of either series then have norm \(1\text{.}\) Consequently, reduction modulo the maximal ideal of \(k^\circ\) gives nonzero polynomials

\begin{equation*} \overline f,\overline g \in \widetilde{k}[W,U_1,U_2,\ldots]. \end{equation*}

This polynomial ring is an integral domain, so \(\overline f\,\overline g\neq0\text{.}\) Reduction commutes with multiplication: for each monomial, its coefficient in a product is a finite sum. Hence some coefficient of \(fg\) has norm \(1\text{,}\) and therefore

\begin{equation*} \lVert fg\rVert_G\geq1. \end{equation*}

The reverse inequality follows from submultiplicativity of the Gauss norm. Thus \(\lVert fg\rVert_G=1\text{,}\) and rescaling gives

\begin{equation*} \lVert fg\rVert_G=\lVert f\rVert_G\lVert g\rVert_G \end{equation*}

in general.

The algebra \(\mathcal A\) is a closed subring of this restricted Tate algebra, and its norm is the restriction of the Gauss norm. Its norm is therefore multiplicative, and \(\mathcal A\) is an integral domain.

If \(x\in\mathcal A_0\text{,}\) then \(\lVert x\rVert_G\leq1\text{,}\) so every power of \(x\) also lies in \(\mathcal A_0\text{.}\) If \(x\notin\mathcal A_0\text{,}\) then \(\lVert x\rVert_G>1\text{,}\) and multiplicativity gives

\begin{equation*} \lVert x^m\rVert_G=\lVert x\rVert_G^m, \end{equation*}

which is unbounded. Hence \(\mathcal A^\circ=\mathcal A_0\text{.}\) The subring \(\mathcal A_0\) is the norm unit ball and hence bounded, so \(\mathcal A\) is uniform. Completeness and the Tate property follow from (8.5) and the topologically nilpotent unit \(\varpi\text{.}\)

The multiplicativity argument for the countable restricted Tate algebra has also been formalised in Lean, using William Coram’s restricted-power-series code [bib-CoramCode].

Proposition 8.4.

If \(w(n)\geq1\) for every \(n\geq1\text{,}\) then \(\mathcal A_w\) is not noetherian.

Lean (not_isNoetherianRing_WPA)Lean (non-noetherianity)

Proof.

Assume that \(w(n)\geq1\) for every \(n\geq1\text{.}\) For \(m\geq1\text{,}\) let

\begin{equation*} I_m=(Z_1,\ldots,Z_m)\subset\mathcal A. \end{equation*}

We show that \(Z_{m+1}\notin I_m\text{.}\)

Let \(e_{m+1}\) denote the multi-index supported at \(m+1\text{,}\) with value \(1\) there. Define

\begin{equation*} \psi_m:\mathcal A\longrightarrow k\langle T\rangle \end{equation*}

by the formula

\begin{equation*} \psi_m\left(\sum_{a,\nu}c_{a,\nu}W^aU^\nu\right) =\sum_{q\geq0}c_{0,2q e_{m+1}}T^q. \end{equation*}

This is well defined because the retained coefficients still tend to zero.

We claim that \(\psi_m\) is multiplicative. A monomial in \(\mathcal A\) which involves no \(W\) and no \(U_j\) for \(j\neq m+1\) must be of the form \(U_{m+1}^{2q}\text{.}\) Indeed, an odd exponent of \(U_{m+1}\) would contribute \(w(m+1)\geq1\) to its weight and would therefore require a positive power of \(W\text{.}\) Since all exponents are nonnegative, a product can contribute \(U_{m+1}^{2q}\) only when the two monomials are \(U_{m+1}^{2q_1}\) and \(U_{m+1}^{2q_2}\text{,}\) with \(q_1+q_2=q\text{.}\) It follows that

\begin{equation*} \psi_m(fg)=\psi_m(f)\psi_m(g). \end{equation*}

For \(1\leq j\leq m\text{,}\) we have \(\psi_m(Z_j)=0\text{,}\) whereas \(\psi_m(Z_{m+1})=T\neq0\text{.}\) Thus \(\psi_m\) vanishes on \(I_m\) but not on \(Z_{m+1}\text{,}\) so \(Z_{m+1}\notin I_m\text{.}\) Since \(Z_{m+1}\in I_{m+1}\text{,}\) we obtain a strictly increasing chain

\begin{equation*} I_1\subsetneq I_2\subsetneq I_3\subsetneq\cdots, \end{equation*}

and therefore \(\mathcal A\) is not noetherian.

Subsection 8.2 Small perturbations of rational data

Lemma 8.5. Small perturbation lemma.

Let \((E,E^+)\) be a complete Tate Huber pair and let \(\alpha=(f_1,\ldots,f_m;g)\) be a rational datum in \(E\text{.}\) There is a neighbourhood \(V\) of zero in \(E\) such that, whenever

\begin{equation*} g'-g,\ f_1'-f_1,\ldots,f_m'-f_m\in V, \end{equation*}

the tuple \(\alpha'=(f_1',\ldots,f_m';g')\) is a rational datum and \(\alpha\) and \(\alpha'\) define the same rational subset of \(\Spa(E,E^+)\text{.}\) Their completed rational localisations are canonically bicontinuously isomorphic over \(E\text{.}\)

Lean (datum_isRational)Lean (rationalOpen_datum)Lean (equiv)Lean (equiv_continuous)Lean (equiv_symm_continuous)Lean (equiv_canonicalMap)

Proof.

Apply [bib-Huber93, Lemma 3.10] after including \(g\) among the numerators; see also [bib-KL, Remark 2.4.7]. The assertion about completed rational localisations follows from their universal property [bib-Huber94, Proposition 1.3].

Subsection 8.3 Rational localisations defined over finitely many variables

Fix \(N\in\mathbb N\text{.}\) Let \(\mu=(\mu_n)_{n>N}\) be a finitely supported family of nonnegative integers and put

\begin{equation*} e_\mu=W^{\omega(\mu)}U^\mu, \end{equation*}

where \(\mu\) is extended by zero for \(n\leq N\text{.}\) Every \(f\in\mathcal A\) has a unique convergent expression

\begin{equation} f=\sum_\mu f_\mu e_\mu, \qquad f_\mu\in\mathcal A^{(N)}, \qquad \lVert f_\mu\rVert_G\longrightarrow0,\tag{8.8} \end{equation}

and

\begin{equation*} \lVert f\rVert_G=\sup_\mu\lVert f_\mu\rVert_G. \end{equation*}

Multiplication is determined by

\begin{equation} e_\mu e_\lambda =W^{\omega(\mu)+\omega(\lambda)-\omega(\mu+\lambda)} e_{\mu+\lambda}.\tag{8.9} \end{equation}

The map

\begin{equation*} \rho_N:\mathcal A\longrightarrow\mathcal A^{(N)}, \qquad \sum_\mu f_\mu e_\mu\longmapsto f_0, \end{equation*}

is a norm-nonincreasing ring retraction.

Proposition 8.6. Coefficientwise localisation.

Let \(\alpha\) be a rational datum whose entries lie in \(\mathcal A^{(N)}\text{,}\) and put \(P=(\mathcal A^{(N)})_\alpha\text{.}\) There is a bicontinuous ring isomorphism

\begin{equation*} \mathcal A_\alpha \xrightarrow{\ \sim\ } \left\{ \sum_\mu p_\mu e_\mu: p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0 \right\}. \end{equation*}

The ring on the right has the supremum norm, and its multiplication is given by (8.9), with \(W\) replaced by its image in \(P\text{.}\) If a rational refinement is also represented by data in \(\mathcal A^{(N)}\) and \(P\to P'\) is the corresponding restriction map, then the induced restriction sends

\begin{equation*} \sum_\mu p_\mu e_\mu \longmapsto \sum_\mu (p_\mu|_{P'})e_\mu. \end{equation*}

Lean (coefficientwise equivalence)Lean (continuity)Lean (continuous inverse)Lean (restriction is coefficientwise)

Proof.

Apply the canonical map \(\mathcal A^{(N)}\to P\) to every coefficient in (8.8). This gives a continuous homomorphism

\begin{equation*} \Phi_0:\mathcal A\longrightarrow \left\{ \sum_\mu p_\mu e_\mu: p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0 \right\}. \end{equation*}

In the target, the image of \(g\) is a unit and each \(f_i/g\) is of norm at most \(1\text{,}\) by the defining property of \(P\text{.}\) Thus \(\Phi_0\) extends continuously to \(\mathcal A[1/g]\) for the rational-localisation topology, and then to the completion:

\begin{equation*} \Phi:\mathcal A_\alpha\longrightarrow \left\{ \sum_\mu p_\mu e_\mu: p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0 \right\}. \end{equation*}

In the other direction, the inclusion \(\mathcal A^{(N)}\to\mathcal A\) gives a continuous homomorphism \(P\to\mathcal A_\alpha\text{.}\) Each \(e_\mu\) lies in \(\mathcal A_0\text{,}\) and the canonical map to a rational localisation is bounded. Hence the family \((e_\mu)_\mu\) is bounded in \(\mathcal A_\alpha\text{.}\) Apply the homomorphism to every coefficient. If \(\lVert p_\mu\rVert\to0\text{,}\) the series

\begin{equation*} \sum_\mu p_\mu e_\mu \end{equation*}

converges in \(\mathcal A_\alpha\text{.}\) The resulting map \(\Psi\) is continuous, and (8.9) shows that it is multiplicative.

The composite \(\Phi\Psi\) fixes every term \(p e_\mu\text{,}\) and hence every finite sum of such terms. These finite sums are dense. The other composite fixes the dense image of \(\mathcal A[1/g]\text{.}\) Continuity therefore gives \(\Phi\Psi=1\) and \(\Psi\Phi=1\text{.}\) This proves the claimed isomorphism.

If \(P\to P'\) comes from a rational refinement, all the maps just used commute with this restriction map. On a finite sum, restriction simply applies \(P\to P'\) to each coefficient; continuity gives the stated formula for every convergent sum.

Corollary 8.7. Finite-variable presentation.

For every rational localisation of \(\mathcal A_w\text{,}\) there is \(N_0\) such that, for every \(N\geq N_0\text{,}\) it is bicontinuously isomorphic to a ring of the form

\begin{equation*} \left\{ \sum_\mu p_\mu e_\mu: p_\mu\in P,\quad \lVert p_\mu\rVert\longrightarrow0 \right\}, \end{equation*}

where \(P\) is a rational localisation of the strongly noetherian Tate ring \(\mathcal A^{(N)}\text{.}\)

Lean (finite-variable model)Lean (existence of the model)

Proof.

Start with a rational datum \(\alpha=(f_1,\ldots,f_m;g)\) in \(\mathcal A\text{.}\) Choose a scalar \(t\in k^\times\) with \(0<|t|<1\) and small enough that \(tg,tf_1,\ldots,tf_m\) lie in \(\mathcal A_0\text{.}\) Multiplying the datum by \(t\) does not change the rational subset or its localisation, so we may assume that \(g,f_1,\ldots,f_m\) lie in \(\mathcal A_0\text{.}\) Choose a neighbourhood \(V\) as in Lemma 8.5. By (8.7), for some \(N\) there are \(g',f_1',\ldots,f_m'\in\mathcal A^{(N)}\cap\mathcal A_0\) such that

\begin{equation*} g'-g,\ f_1'-f_1,\ldots,f_m'-f_m\in V. \end{equation*}

By Lemma 8.5, the datum \(\alpha'=(f_1',\ldots,f_m';g')\) gives the same rational subset and the same completed localisation. It is rational in \(\mathcal A\text{,}\) so applying \(\rho_N\) to a Bezout identity for its entries shows that it is already a rational datum in \(\mathcal A^{(N)}\text{.}\) The same datum belongs to every larger finite-variable ring, and the corresponding retraction shows from the same Bezout identity that it is rational there. Now apply Proposition 8.6 at every stage beyond \(N\text{.}\)

Subsection 8.4 A reduced rational chart which is not uniform

The ideal \((W,\varpi)\) is open because \(\varpi\) is a unit of \(\mathcal A\text{.}\) Define the complete \(k^\circ\)-algebra

\begin{equation} \mathcal B_{w,0}= \left\{ \sum_{\substack{\nu\in\mathbb N^{(I)},\ d\geq\omega(\nu)}} b_{d,\nu}X^dU^\nu: b_{d,\nu}\in\varpi^{\omega(\nu)}k^\circ, \quad \varpi^{-\omega(\nu)}b_{d,\nu}\longrightarrow0 \right\},\tag{8.10} \end{equation}

with norm

\begin{equation} \left\lVert\sum b_{d,\nu}X^dU^\nu\right\rVert_{\mathcal B} =\sup_{d,\nu}|\varpi|^{-\omega(\nu)}|b_{d,\nu}|.\tag{8.11} \end{equation}

The subadditivity (8.3) shows that \(\mathcal B_{w,0}\) is a ring. Put \(\mathcal B_w=\mathcal B_{w,0}[1/\varpi]\text{,}\) and abbreviate these rings to \(\mathcal B\) and \(\mathcal B_0\) when \(w\) is understood.

Proposition 8.8.

For every weight \(w\text{,}\) there is a bicontinuous ring isomorphism

\begin{equation*} \mathcal A_w\left\langle\frac{W}{\varpi}\right\rangle \xrightarrow{\ \sim\ }\mathcal B_w, \qquad W\longmapsto\varpi X. \end{equation*}

Lean (chartDatum)Lean (coefficientwise equivalence)Lean (continuity)Lean (continuous inverse)Lean (finite-variable chart ≃ k⟨X⟩)Lean (isometric identification)Lean (W ↦ ϖX)

Proof.

The datum \((W;\varpi)\) lies in \(\mathcal A^{(0)}=k\langle W\rangle\text{.}\) Put

\begin{equation*} P= \mathcal A^{(0)}\langle T\rangle/ \overline{(\varpi T-W)}. \end{equation*}

Evaluation at \(W=\varpi X\) and \(T=X\) gives a continuous map \(P\to k\langle X\rangle\text{.}\) Conversely, evaluation of \(k\langle X\rangle\) at the image of \(T\) gives a continuous map in the other direction. The two maps are inverse by polynomial density, and the norm estimates in the two universal properties show that the isomorphism is isometric.

Apply Proposition 8.6 with \(N=0\text{.}\) It describes the rational chart as the ring of sums

\begin{equation*} \sum_\nu p_\nu e_\nu, \qquad p_\nu\in P,\qquad \lVert p_\nu\rVert\longrightarrow0. \end{equation*}

Under \(P\cong k\langle X\rangle\text{,}\) this is precisely the model (8.10). Its sup norm is (8.11), because the term indexed by \(\nu\) is multiplied by \(\varpi^{\omega(\nu)}\text{.}\) The map from \(\mathcal A^{(0)}\) sends \(W\) to \(\varpi X\text{.}\)

Proposition 8.9.

For every weight \(w\text{,}\) the ring \(\mathcal B_w\) is an integral domain. If \(w\) is unbounded, then \(\mathcal B_w\) is not uniform.

Lean (isDomain_chart)Lean (not_isUniform_chart)Lean (not_isStablyUniform_WPA)Lean (chart is a domain)Lean (chart is nonuniform)

Proof.

Put \(R=k\langle X\rangle\text{.}\) Here

\begin{equation*} R[[U_1,U_2,\ldots]] =\left\{\sum_{\nu\in\mathbb N^{(I)}}a_\nu U^\nu:a_\nu\in R\right\} \end{equation*}

denotes the ring of all coefficient families indexed by finite-support multi-indices. Multiplication is convolution. For a fixed \(\nu\) there are only finitely many decompositions \(\nu=\lambda+\mu\text{,}\) so every coefficient of a product is a finite sum. Order \(\mathbb N^{(I)}\) by comparing two vectors at the largest index where they differ. This is an additive well-order. If two series are nonzero, the coefficient at the sum of their least nonzero exponents is the product of the corresponding coefficients and is nonzero. Thus \(R[[U_1,U_2,\ldots]]\) is a domain.

The coefficient description gives a homomorphism

\begin{equation*} \mathcal B\longrightarrow R[[U_1,U_2,\ldots]], \qquad \sum_\nu p_\nu e_\nu\longmapsto \sum_\nu(\varpi X)^{\omega(\nu)}p_\nu(X)U^\nu. \end{equation*}

It is a homomorphism by (8.9). If its image is zero, then

\begin{equation*} (\varpi X)^{\omega(\nu)}p_\nu(X)=0 \end{equation*}

for every \(\nu\text{.}\) Since \(k\langle X\rangle\) is a domain, every \(p_\nu\) is zero. The map is therefore injective, and hence \(\mathcal B\) is a domain.

Assume now that \(w\) is unbounded. Inside \(\mathcal A\) write \(Y_n=W^{w(n)}U_n\) and put

\begin{equation*} T_n=\varpi^{-w(n)}Y_n=X^{w(n)}U_n\in\mathcal B. \end{equation*}

Formula (8.11) gives

\begin{equation*} \lVert T_n\rVert_{\mathcal B}=|\varpi|^{-w(n)}, \qquad \lVert T_n^2\rVert_{\mathcal B}=1. \end{equation*}

The even powers of \(T_n\) have norm at most \(1\text{,}\) and the odd powers have norm at most \(\lVert T_n\rVert_{\mathcal B}\text{.}\) Thus every \(T_n\) is power-bounded. The family \((T_n)_{n\geq1}\) is not bounded, since its norms \(|\varpi|^{-w(n)}\) are unbounded. Hence \(\mathcal B^\circ\) is unbounded and \(\mathcal B\) is not uniform.

Subsection 8.5 Strong sheafiness

Theorem 8.10.

For every weight \(w\text{,}\) every \(s\geq0\text{,}\) and every ring of integral elements \(\mathcal A_{w,s}^+\) of \(\mathcal A_w\langle V_1,\ldots,V_s\rangle\text{,}\) the Huber pair

\begin{equation*} \bigl(\mathcal A_w\langle V_1,\ldots,V_s\rangle, \mathcal A_{w,s}^+\bigr) \end{equation*}

is sheafy. In particular, \(\mathcal A_w\) is strongly sheafy. No positivity or unboundedness hypothesis on \(w\) is needed here.

Lean (wp_isSheafyComplete)Lean (wp_stronglySheafy)Lean (wp_tateExt_isSheafyComplete)Lean (sheafiness)Lean (wp_tateExt_isSheafyComplete_of_dvr)

Proof.

We first work with a finite rational cover \(U=\bigcup_iU_i\text{.}\) Choose one \(N\) large enough to approximate the datum for \(U\) and the data for all the \(U_i\) in \(\mathcal A^{(N)}\text{.}\) The standard combined data for every pairwise intersection \(U_i\cap U_j\) then also lie in \(\mathcal A^{(N)}\text{.}\) The small perturbation lemma does not change the rational domains, and Proposition 8.6 gives compatible identifications

\begin{equation*} \mathcal O(U)\cong \left\{\sum_\mu p_\mu e_\mu: p_\mu\in P,\ \lVert p_\mu\rVert\to0\right\}, \end{equation*}

\begin{equation*} \mathcal O(U_i)\cong \left\{\sum_\mu p_{i,\mu}e_\mu: p_{i,\mu}\in P_i,\ \lVert p_{i,\mu}\rVert\to0\right\}, \end{equation*}

with coefficientwise restriction maps. Here \(P\) is a rational localisation of the strongly noetherian Tate ring \(\mathcal A^{(N)}\text{,}\) and the \(P_i\) are rational localisations corresponding to the \(U_i\text{.}\) Let \(V\) and \(V_i\) be the rational subsets of

\begin{equation*} \Spa\bigl(\mathcal A^{(N)},(\mathcal A^{(N)})^\circ\bigr) \end{equation*}

defined by the data giving \(P\) and \(P_i\text{.}\) Then \(V=\bigcup_iV_i\text{.}\) Indeed, if \(v\in V\text{,}\) the composite \(v\circ\rho_N\) is a point of \(\Spa(\mathcal A,\mathcal A^\circ)\text{,}\) since \(\rho_N\) sends power-bounded elements to power-bounded elements. For data in \(\mathcal A^{(N)}\text{,}\) membership in the corresponding rational subset is unchanged by this pullback because \(\rho_N\) is a retraction. Thus \(v\circ\rho_N\) belongs to \(U\text{,}\) and hence to some \(U_i\text{,}\) which gives \(v\in V_i\text{.}\) We may therefore apply sheafiness of the strongly noetherian ring \(\mathcal A^{(N)}\) to the cover \(V=\bigcup_iV_i\text{.}\)

Let \((x_i)_i\) be a compatible family and write \(x_i=\sum_\mu x_{i,\mu}e_\mu\text{.}\) Since \(\mathcal A^{(N)}\) is sheafy, the compatible family \((x_{i,\mu})_i\) glues to a unique \(q_\mu\in P\) for every \(\mu\text{.}\) It remains to check that \(\lVert q_\mu\rVert\to0\text{.}\) The restrictions of the \(q_\mu\) to every \(P_i\) tend to zero because the coefficients of each \(x_i\) do. The product restriction map

\begin{equation*} P\longrightarrow\prod_iP_i \end{equation*}

is a topological embedding, so it reflects convergence to zero. Hence \(q_\mu\to0\text{,}\) and \(\sum_\mu q_\mu e_\mu\) is the required section over \(U\text{.}\) The same coefficientwise argument proves separation.

The image of the product restriction map for \(\mathcal A\) is therefore the subspace of tuples whose restrictions to every pairwise intersection agree. This subspace is closed: it is the common zero locus of the continuous difference maps, and hence is a Banach \(k\)-space. The restriction map is a continuous bijection from the Banach \(k\)-space \(\mathcal O(U)\) to this closed subspace. The nonarchimedean open mapping theorem therefore makes it a homeomorphism. We have proved the topological sheaf condition on finite rational covers. The general rational-basis theorem upgrades this to the all-open structure presheaf, and its plus-ring independence gives the same conclusion for every ring of integral elements. In particular, \((\mathcal A,\mathcal A^\circ)\) is sheafy.

For \(s\geq0\text{,}\) the Tate extension \(\mathcal A\langle V_1,\ldots,V_s\rangle\) is bicontinuously isomorphic to the same weighted-parity construction with the first \(s\) weights equal to zero and the remaining weights shifted by \(s\text{.}\) The argument above applies to every weight function and is independent of the ring of integral elements, so this Tate extension is sheafy for every such choice. Hence \(\mathcal A\) is strongly sheafy.

Proof of Theorem 8.1.

The fact that \(\mathcal A\) is a uniform domain is Proposition 8.3, and its failure to be noetherian is Proposition 8.4. Strong sheafiness is Theorem 8.10. Finally, Proposition 8.8, Proposition 8.9 identify the rational chart \(|W|\leq|\varpi|\) as an integral domain which is not uniform.

Remark 8.11. Admissible blow-ups.

There is a common formal interpretation of the two bad rational charts. Let \(R_0\) denote \(A_0\) in the finite-jet example and \(\mathcal A_0\) in the weighted-parity example. The affine chart of the admissible blow-up of \(\operatorname{Spf}(R_0)\) along \((\varpi,W)\) on which the pullback of this ideal is generated by \(\varpi\) has ring

\begin{equation*} \widehat{R_0[W/\varpi]}. \end{equation*}

Here \(R_0[W/\varpi]\) means the subring of \(R_0[1/\varpi]\) generated by \(R_0\) and \(W/\varpi\text{,}\) and the hat denotes the \(\varpi\)-adic completion defined above. After inverting \(\varpi\text{,}\) its coordinate ring is the completed rational localisation \(R_0[1/\varpi]\langle W/\varpi\rangle\text{,}\) corresponding to \(|W|\leq|\varpi|\text{.}\) This description applies to our non-noetherian formal models because they are \(\varpi\)-adic and their ideal of definition \((\varpi)\) is principal; see [bib-FK, Chapter 0, Section 7.1(c), and Chapter II, Section 1.1(b)].

For \(R_0=A_0\text{,}\) the ring \(A_0[W/\varpi]\) is a domain, but the calculation in the proof of Proposition 4.1 shows that

\begin{equation*} Q^2\in\bigcap_{n\geq1}\varpi^nA_0[W/\varpi]. \end{equation*}

This intersection is the kernel of the completion map. Thus \(Q^2\) is killed, while \(Q\) survives, so this rational chart is non-reduced. The map from \(A\) to this completed rational localisation is also not flat by Proposition 7.1. For \(R_0=\mathcal A_0\text{,}\) the completed chart remains a domain, but its generic fibre is not uniform because the power-bounded elements \(T_n=X^{w(n)}U_n\) form an unbounded family. Thus the two examples give different failures on the same kind of affine blow-up chart.

The proof of sheafiness for \(\mathcal A\) uses the further fact that a rational datum can be approximated inside some strongly noetherian \(\mathcal A^{(N)}\text{,}\) after which localisation and restriction are computed coefficient by coefficient. The infinite monomial support and the unbounded power-bounded elements are in the tradition of the examples of Buzzard–Verberkmoes and Mihara; the approximation by the rings \(\mathcal A^{(N)}\) is what makes sheafiness accessible here.

Section 9 How the examples were found

The authors had for some time been interested in finding a counterexample to Problem 7 of the Nonarchimedean Scottish Book. Our attempts had centred on the example of [bib-BV, Section 4.5, Proposition 17], which is uniform but not stably uniform. We believe that this example is in fact sheafy, but we have not found a proof.

In January 2026 we began to experiment with AI tools, initially ChatGPT 5.2 Pro. Buzzard–Verberkmoes reduce exactness for a two-member Laurent cover to a boundedness condition on the relevant rings of definition [bib-BV, Lemma 2]. For a uniform ring this follows from boundedness of the power-bounded elements [bib-BV, Lemma 3 and Corollary 4]. Their reduction from general rational covers to Laurent covers is given in [bib-BV, Lemma 8 and the proof of Theorem 7]. For sheafiness these checks must also be made after rational localisation. Their Theorem 7 cannot be applied directly to Proposition 17, since one of the rational localisations in that example is not uniform. Our plan was instead to ask ChatGPT to write down many explicit rational covers and check the required exactness directly for each one, in the hope that a pattern, and eventually a proof, would emerge.

After a couple of weeks ChatGPT 5.2 Pro claimed to have a complete proof. The authors then began the slow process of understanding this proof, only to discover, with the help of ChatGPT 5.3, that one of its arguments used the following assertion:

If \(\phi:A\to B\) is a continuous homomorphism of Hausdorff topological abelian groups and \(A\) is complete, then \(\phi(A)\) is closed in \(B\text{.}\)

This assertion is false, and its use completely broke the purported proof.

Motivated by this, we began in parallel to use Claude Code to formalise the parts of the theory of adic spaces needed here, including the theorem that strongly noetherian Tate rings are sheafy. The aim was a practical one: future AI-generated proofs could be formalised before the human authors had spent days understanding an argument containing a fatal error near its end.

We then returned to writing down covers and looking for a pattern. This continued through ChatGPT 5.3 and subsequent versions. When ChatGPT 5.6 Sol became available, we asked, almost in passing, whether it could prove the result we wanted or find a new example. It produced the examples studied here. By then the Lean development was far enough advanced that we could use Claude Code to formalise the arguments quickly in Lean and check that they were correct.

At the time of writing, it is still possible to reproduce this by asking the agents to find an example of a uniform and sheafy non-noetherian ring which is not stably uniform. One point to note is that they sometimes reply that this is an open problem, which prevents them from proceeding. In such cases, saying an example exists; find it often produces an example.

Appendix A Lean formalisation and verification

This appendix records the Lean definitions and theorem statements. Theorem listings stop before their proof terms, and the links open the checked declarations. The formalisation is available as a self-contained repository, uniform-sheafy-tate-domains-lean [bib-SheafyLean], which carries the adic-spaces library, both examples and the Comparator certificates, and has mathlib as its only dependency. It is extracted from the development repository AINTLIB [bib-AINTLIB], whose commits the per-declaration links below pin; a few of those declarations sit on other public branches there. It uses Lean 4.33.0 [bib-Lean4] and mathlib 4.33.0 [bib-mathlib]. The headline statements for both examples have been checked with Comparator, which compares them with independent challenge statements, checks their axiom dependencies, and replays the proofs through the Lean kernel. The interactive appendix was prepared with PaperForge; each Lean button opens the corresponding declaration.

Subsection A.1 The predicate `IsSheafy`

Definition A.1. The rational-cover predicate.

The arguments in the paper use finite rational covers, and Lean therefore uses the following predicate. Here RationalCoveringData A consists of a rational domain together with a finite rational cover of it, C.IsRational imposes the usual open-ideal condition, and presheafValue D is the completed rational localisation attached to \(D\text{.}\)

      class IsSheafy (A : Type u) [CommRing A] [TopologicalSpace A]
  [IsTopologicalRing A] [inst₁ : PlusSubring A]
  [inst₂ : IsHuberRing A] [T2Space A] [NonarchimedeanRing A]
  [letI : UniformSpace A :=
    IsTopologicalAddGroup.rightUniformSpace A; CompleteSpace A]
  [IsRingOfIntegralElements (A⁺)] : Prop where
embedding : ∀ (C : RationalCoveringData A), C.IsRational →
  Topology.IsEmbedding (productRestrictionSub A C)
gluing : ∀ (C : RationalCoveringData A), C.IsRational →
  ∀ (f : ∀ (D : ↥C.covers), presheafValue D.1),
  (∀ (D₁ D₂ : ↥C.covers) (D₃ : RationalLocData A)
    (h₃₁ : rationalOpen D₃.T D₃.s ⊆
      rationalOpen D₁.1.T D₁.1.s)
    (h₃₂ : rationalOpen D₃.T D₃.s ⊆
      rationalOpen D₂.1.T D₂.1.s),
    restrictionMap D₁.1 D₃ h₃₁ (f D₁) =
      restrictionMap D₂.1 D₃ h₃₂ (f D₂)) →
  ∃ x : presheafValue C.base, ∀ (D : ↥C.covers),
    restrictionMap C.base D.1 (C.hsubset D.1 D.2) x = f D

The first field says that restriction to a finite rational cover is a topological embedding. The second says that every compatible family of sections glues; compatibility is expressed on common rational refinements. This is the topological sheaf condition on the rational basis. We use this form because it speaks directly about the rational localisations occurring in the paper.

Lean (covering data)Lean (rationality condition)Lean (completed rational localisation)Lean (rational-cover sheaf condition)

Subsection A.2 Comparison with Mathlib’s sheaf predicate

Remark A.2.

For an open subset \(V\subseteq\Spa(A,A^+)\text{,}\) limitSections V is the projective limit of the sections on rational subdomains contained in \(V\text{,}\) and limitRestrict is the restriction map between these limits. The predicate IsLimitSheaf is the separation, gluing and topological-embedding condition for arbitrary open covers. Lean proves:

    theorem isSheafy_iff_isLimitSheaf :
IsSheafy A ↔ IsLimitSheaf A

For a presheaf \(F\) as above, IsSheafOfTopologicalRings is Wedhorn’s condition that

\begin{equation*} U\longmapsto\operatorname{Hom}_{\mathrm{cont}}(T,F(U)) \end{equation*}

is a sheaf of sets for every topological commutative ring \(T\text{.}\) For the structure presheaf:

    theorem structurePresheaf_isSheafOfTopologicalRings_iff :
TopCat.Presheaf.IsSheafOfTopologicalRings
    (structurePresheaf A) ↔
  IsLimitSheaf A

It also proves the general comparison with Mathlib’s categorical predicate:

    theorem isSheafOfTopologicalRings_iff_forgetToTopCommRingCat_isSheaf :
F.IsSheafOfTopologicalRings ↔ TopCat.Presheaf.IsSheaf
  (F ⋙ CompleteTopCommRingCat.forgetToTopCommRingCat)

The forgetful functor retains the topology but forgets completeness and separatedness. Its target has all topological commutative rings as objects, which is precisely the class of test rings in Wedhorn’s formulation. Combining the preceding equivalences gives the direct comparison used here:

    theorem isSheafy_iff_structurePresheaf_forgetToTopCommRingCat_isSheaf
[DecidableEq A] [DecidableEq (RationalLocData A)] [IsTateRing A]
[IsRingOfIntegralElements (A⁺ : Subring A)] [T2Space A]
[NonarchimedeanRing A]
[letI : UniformSpace A :=
  IsTopologicalAddGroup.rightUniformSpace A; CompleteSpace A] :
IsSheafy A ↔
  TopCat.Presheaf.IsSheaf
    (structurePresheaf A ⋙
      CompleteTopCommRingCat.forgetToTopCommRingCat)

Thus IsSheafy is equivalent both to Wedhorn’s representable formulation and to Mathlib’s sheaf condition for the structure presheaf. It is used here because it is convenient, not because it defines a weaker or stronger notion.

The auxiliary class HasLocLiftPowerBounded constructs restriction maps between completed rational localisations. For an inclusion of rational domains it says that the old denominator becomes a unit and that the old numerator fractions are power-bounded on the smaller domain. It is supplied by the theory for the complete Tate pairs used here and is not an additional hypothesis in the main results.

Lean (rational covers ↔ all opens)Lean (Wedhorn Hom-sheaf)Lean (all opens ↔ Wedhorn)Lean (Wedhorn ↔ Mathlib)Lean (Mathlib ↔ all opens)Lean (IsSheafy ↔ Mathlib IsSheaf)

Subsection A.3 Sheafiness for Tate rings

For a complete Tate ring, the following definitions fix a ring of integral elements and then quantify over all such choices. The final definition also removes the choice of completion for a Tate ring which is not assumed complete.

    def IsSheafyFor (Aplus : RingOfIntegralElements A) : Prop :=
  letI := Aplus.toPlusSubring
  haveI : IsRingOfIntegralElements (A⁺ : Subring A) := Aplus.2
  haveI : HasLocLiftPowerBounded A :=
    hasLocLiftPowerBounded_faithful
  IsLimitSheaf A

def IsSheafyComplete : Prop :=
  ∀ Aplus : RingOfIntegralElements A, IsSheafyFor A Aplus

def IsSheafyTateRing : Prop :=
  ∀ (P : PairOfDefinition A)
    (Bplus : RingOfIntegralElements (CompletionModel A P)),
    IsSheafyFor (CompletionModel A P) Bplus

Thus IsSheafyFor A Aplus is sheafiness of \((A,A^+)\text{,}\) IsSheafyComplete A requires this for every ring of integral elements, and IsSheafyTateRing A requires it for every completion model.

Subsection A.4 Strong noetherianity

Definition A.3. Strong noetherianity.

Lean defines restricted power series and strong noetherianity as follows.

        def MvPowerSeries.IsRestricted {k : ℕ} {A : Type*}
    [CommRing A] [TopologicalSpace A]
    (f : MvPowerSeries (Fin k) A) : Prop :=
  Tendsto
    (fun s : Fin k →₀ ℕ => MvPowerSeries.coeff s f)
    cofinite (nhds 0)

class IsStronglyNoetherian (A : Type*) [CommRing A]
    [TopologicalSpace A] [NonarchimedeanRing A] : Prop where
  isNoetherianRing_restricted : ∀ k : ℕ,
    IsNoetherianRing (restrictedMvPowerSeriesSubring k A)

The first condition says exactly that the coefficients tend to zero. Hence the subring in the second declaration is \(A\langle T_1,\ldots,T_k\rangle\text{,}\) and the second declaration says that this ring is noetherian for every \(k\text{.}\) This is the usual notion of strong noetherianity [bib-Wedhorn, Proposition and Definition 6.36].

Lean (restricted series)Lean (restricted Tate algebra)Lean (strong noetherianity)Lean (IsStronglyNoetherianTateRing)Lean (isSheafyTateRing_of_stronglyNoetherianTateRing)Lean (isSheafyFor_of_stronglyNoetherianTate)Lean (isSheafyComplete_of_stronglyNoetherianTate)

For a Tate ring not assumed complete, the condition is imposed on a completion model. Lean then records Wedhorn’s sheafiness theorem at the same level of generality:

    def IsStronglyNoetherianTateRing [IsTateRing A] : Prop :=
  ∃ P : PairOfDefinition A,
    IsStronglyNoetherian (CompletionModel A P)

theorem isSheafyTateRing_of_stronglyNoetherianTateRing
    [IsTateRing A] (h : IsStronglyNoetherianTateRing A) :
    IsSheafyTateRing A

theorem isSheafyComplete_of_stronglyNoetherianTate
    [IsStronglyNoetherian A] :
    IsSheafyComplete A

The first theorem is independent of the chosen completion model; the second is its complete-ring specialisation. These are the formal versions of the strongly noetherian sheaf theorem [bib-Wedhorn, Theorem 8.28(b)].

Subsection A.5 The finite-jet example

Definition A.4. The finite-jet ring.

The four rings in the defining square and the finite-jet ring itself are represented as follows.

          abbrev L : Type u := RestrictedLaurent K

abbrev JetC : Type u := PowerSeries.Restricted (L K) (1 : ℝ)

abbrev JetB : Type u := DualNumber (PowerSeries.Restricted K (1 : ℝ))

abbrev JetD : Type u := DualNumber (L K)

noncomputable def jetSupport : Subring (JetC K) where
  carrier := {f |
    qCoeff K 0 f ∈ nonnegSubring K ∧
    qCoeff K 1 f ∈ nonnegSubring K}
  ...

abbrev JetA : Type u := ↥(jetSupport K)

Here RestrictedLaurent K is \(K\langle W,W^{-1}\rangle\text{,}\) while PowerSeries.Restricted R 1 is the radius-one restricted power-series ring over \(R\text{.}\) The condition defining jetSupport says that the coefficients of \(Q^0\) and \(Q^1\) have no negative powers of \(W\text{.}\) Thus JetA K is precisely

\begin{equation*} \left\{ f_0(W)+Qf_1(W)+Q^2h(W,W^{-1},Q): f_0,f_1\in K\langle W\rangle,\; h\in K\langle W,W^{-1}\rangle\langle Q\rangle \right\}. \end{equation*}

This is the coefficient description of \(A\) in (3.1) after inverting \(\varpi\text{.}\)

Lean (Laurent algebra)Lean (vertex C)Lean (vertex B)Lean (vertex D)Lean (coefficient condition defining A)Lean (finite-jet ring A)

For a complete nontrivially normed ultrametric field \(K\text{,}\) a uniformizer \(\varpi\text{,}\) and, where stated, a noetherian norm unit ball, the following are the formal counterparts of Proposition 3.1, Proposition 4.1, Proposition 4.2:

      theorem finiteJet_isUniform (ϖ : Uniformizer K) :
    TopologicalRing.IsUniform (JetA K)

theorem finiteJet_isDomain :
    IsDomain (JetA K)

theorem finiteJet_not_noetherian :
    ¬ IsNoetherianRing (JetA K)

def chartEquiv (ϖ : Uniformizer K) :
    presheafValue (chartDatum K ϖ) ≃+* JetB K := ...

theorem chartEquiv_continuous (ϖ : Uniformizer K) :
    Continuous (chartEquiv K ϖ)

theorem chartEquiv_symm_continuous (ϖ : Uniformizer K) :
    Continuous (chartEquiv K ϖ).symm

theorem finiteJet_not_stablyUniform (ϖ : Uniformizer K) :
    ¬ TopologicalRing.IsStablyUniform (JetA K)

The equivalence and the two continuity statements identify the completed rational localisation with

\begin{equation*} A\left\langle\frac{W}{\varpi}\right\rangle \simeq K\langle X,Q\rangle/(Q^2) \end{equation*}

as a topological ring. The domain and non-noetherianity statements do not require a uniformizer.

Ordinary sheafiness, independently of the choice of ring of integral elements, is recorded by

  theorem finiteJet_isSheafyComplete
(ϖ : Uniformizer K)
(hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
IsSheafyComplete (JetA K)

The formal statement of strong sheafiness is:

  theorem finiteJet_tateExt_isSheafyComplete
(ϖ : Uniformizer K)
(hK₀ : IsNoetherianRing (FiniteJet.unitBall K))
(n : ℕ) :
letI := mvTateAlgebraTopology' (A := JetA K) n
haveI := mvTate_isTateRing (A := JetA K) n
haveI := mvTate_t2Space (A := JetA K) n
haveI := mvTate_nonarchimedean (A := JetA K) n
haveI := mvTateAlgebraTopology'_isTopologicalRing
  (A := JetA K) n
haveI : @CompleteSpace
  ↥(restrictedMvPowerSeriesSubring n (JetA K))
  (IsTopologicalAddGroup.rightUniformSpace _) :=
    finiteJet_tateExt_completeSpace K n
IsSheafyComplete
  ↥(restrictedMvPowerSeriesSubring n (JetA K))

The restricted power-series subring here is \(A\langle V_1,\ldots,V_n\rangle\text{,}\) with its canonical Tate-algebra topology, and IsSheafyComplete says that it is sheafy for every ring of integral elements. This is precisely the strong-sheafiness assertion of Corollary 6.2. The separate _of_dvr theorem supplies \(\varpi\) and the noetherianity hypothesis from the assumption that \(\mathcal O[K]\) is a discrete valuation ring.

Subsubsection A.5.1 The Scottish Book statements

For Proposition 7.1, the base need only be a complete ultrametric normed field with a chosen nonzero element \(\varpi\) satisfying \(\lVert\varpi\rVert<1\text{;}\) Lean packages this as IsFJPBase. The element scottishWitness K is \(Q^2\text{.}\)

      class IsFJPBase (K : Type u) [NormedField K]
    [IsUltrametricDist K] [CompleteSpace K] where
  pseudoUniformizer : K
  pseudoUniformizer_ne_zero : pseudoUniformizer ≠ 0
  norm_pseudoUniformizer_lt_one :
    ‖pseudoUniformizer‖ < 1

theorem finiteJet_problem28 :
    (chartDatum K).IsRational ∧
    (rationalOpen
      (chartDatum K).T (chartDatum K).s).Nonempty ∧
    Nontrivial (presheafValue (chartDatum K)) ∧
    Function.Injective
      (fun a : JetA K => scottishWitness K * a) ∧
    Continuous
      (fun a : JetA K => scottishWitness K * a) ∧
    IsStrictMap
      (fun a : JetA K => scottishWitness K * a) ∧
    IsClosed
      (Set.range
        (fun a : JetA K => scottishWitness K * a)) ∧
    (chartDatum K).canonicalMap
      (scottishWitness K) = 0

theorem finiteJet_not_flat_canonicalMap :
    ¬ @Module.Flat
      (JetA K)
      (presheafValue (chartDatum K))
      _ _
      (RingHom.toModule (chartDatum K).canonicalMap)

The first theorem says that multiplication by the non-zero-divisor \(Q^2\) is a continuous strict injection with closed image, while \(Q^2\) becomes zero on a nonempty rational subspace with nonzero section ring. The second says that the canonical map to this completed rational localisation is not flat.

Subsubsection A.5.2 Koszul complexes and Milnor descent

The statement formalised for Lemma 5.1 is more general than its use in the finite-jet example. Let \(E\) be the complete ultrametric normed commutative ring appearing in the theorem below and put \(P(E,m)=E\langle T_1,\ldots,T_m\rangle\text{.}\) The graph sequence is \(r_i=gT_i-f_i\text{.}\)

  theorem koszulGraph_exact_strict_closed
[IsNoetherianRing (P E m)]
(hE₀ : IsNoetherianRing (unitBall E))
(t : E) (htu : IsUnit t)
(ht1 : ‖t‖ < 1) (ht0 : 0 < ‖t‖)
(hscale : ∀ x : E, ‖t * x‖ = ‖t‖ * ‖x‖)
(hE₀P : IsNoetherianRing (unitBall (P E m)))
(g : E) (f : Fin m → E)
(hunit : Ideal.span ({g} ∪ Set.range f) = ⊤)
(r : Fin m → P E m)
(hr : ∀ i, r i =
  polyToP
    (MvPolynomial.C g * MvPolynomial.X i -
      MvPolynomial.C (f i))) :
(∀ q, Function.Exact
  (koszulDifferential r (q + 1))
  (koszulDifferential r q)) ∧
(∀ q, IsStrictLinearMap
  (koszulDifferential r q)) ∧
(∀ q, IsClosed
  (Set.range (koszulDifferential r q)))

This is exactly the positive-degree exactness, strictness and closed-image part of Lemma 5.1. The ideal-denominator declaration and syzygy-denominator declaration state respectively the two denominator inclusions (5.1) and (5.2). The declarations attached to Lemma 5.2, Proposition 5.3 state the corresponding ideal pullback, exactness and topological-embedding results for the general corner square used there.

Finally, MilnorSquareData packages exactly the transport of rational data, covers and compatible families, together with the local equaliser and topological-embedding conditions of Theorem 6.1. The abstract theorem is:

  theorem isSheafy_of_milnorSquare
[DecidableEq (RationalLocData B)]
[DecidableEq (RationalLocData C)]
[DecidableEq (RationalLocData D)]
(phiB : R →+* B) (phiC : R →+* C)
(phiD : R →+* D)
(hphiB : Continuous phiB)
(hphiC : Continuous phiC)
(hphiD : Continuous phiD)
(sq : MilnorSquareData
  phiB phiC phiD hphiB hphiC hphiD)
(hB : IsSheafy B)
(hC : IsSheafy C)
(hD : IsSheafy D) :
IsSheafy R

The finite-jet square supplies this data, so the theorem specialises to the sheafiness statement used in the paper. No claim is made that an arbitrary strict Milnor square is sufficient.

Subsection A.6 The weighted-parity example

Let \(K\) be a complete nontrivially normed ultrametric field and let \(w:\mathbb N\to\mathbb N\text{.}\) Lean indexes the variables by \(\mathbb N\text{:}\) index \(0\) represents \(W\text{,}\) and index \(n\geq1\) represents \(U_n\text{.}\) The ambient restricted Tate algebra and the support condition defining \(\mathcal A_w\) are:

    abbrev Amb : Type _ :=
  MvPowerSeries.Restricted K (fun _ : ℕ => (1 : ℝ))

def wpWeight (w : ℕ → ℕ) (t : ℕ →₀ ℕ) : ℕ :=
  ∑ n ∈ t.support,
    if (t n).mod 2 = 1 ∧ n ≠ 0 then w n else 0

def WPMem (w : ℕ → ℕ) (t : ℕ →₀ ℕ) : Prop :=
  wpWeight w t ≤ t 0

noncomputable def wpSupport : Subring (Amb K) where
  carrier := {f | ∀ t : ℕ →₀ ℕ, ¬ WPMem w t →
    MvPowerSeries.coeff t f.1 = 0}
  ...

abbrev WPA : Type _ := ↥(wpSupport K w)

For an exponent \(t\text{,}\) t 0 is the exponent of \(W\text{,}\) while wpWeight w t is

\begin{equation*} \sum_{\substack{n\geq1\\t(n)\ {\rm odd}}}w(n). \end{equation*}

Thus WPMem w t is precisely the condition \(a\geq\omega_w(\nu)\) in (8.2), and wpSupport says that all coefficients outside this monoid vanish. Consequently WPA K w is exactly the ring \(\mathcal A_w\) of (8.5).

The formal counterparts of Proposition 8.3, Proposition 8.4 are:

    theorem norm_wpa_mul (a b : WPA K w) :
    ‖a * b‖ = ‖a‖ * ‖b‖

instance : IsDomain (WPA K w)

theorem powerBoundedSubring_eq_unitBall
    (ϖ : Uniformizer K) :
    powerBoundedSubring (WPA K w) =
      (FiniteJet.unitBall (WPA K w) : Set (WPA K w))

theorem isUniform_WPA (ϖ : Uniformizer K) :
    IsUniform (WPA K w)

theorem not_isNoetherianRing_WPA
    (hw : ∀ n, 1 ≤ n → 1 ≤ w n) :
    ¬ IsNoetherianRing (WPA K w)

The equality with FiniteJet.unitBall says exactly that \(\mathcal A_w^\circ=\mathcal A_{w,0}\text{,}\) and hw is the condition \(w(n)\geq1\) for \(n\geq1\text{.}\)

Strong sheafiness, including ordinary sheafiness when (s=0), is stated directly for the finite Tate extensions:

theorem wp_tateExt_isSheafyComplete
(ϖ : Uniformizer K)
(hK₀ : IsNoetherianRing (FiniteJet.unitBall K))
(s : ℕ) :
letI := mvTateAlgebraTopology' (A := WPA K w) s
haveI := mvTate_isTateRing (A := WPA K w) s
haveI := mvTate_t2Space (A := WPA K w) s
haveI := mvTate_nonarchimedean (A := WPA K w) s
haveI := mvTateAlgebraTopology'_isTopologicalRing
  (A := WPA K w) s
haveI : @CompleteSpace
  ↥(restrictedMvPowerSeriesSubring s (WPA K w))
  (IsTopologicalAddGroup.rightUniformSpace _) :=
    wp_tateExt_completeSpace (w := w) s
IsSheafyComplete
  ↥(restrictedMvPowerSeriesSubring s (WPA K w))

Here the restricted power-series subring is \(\mathcal A_w\langle V_1,\ldots,V_s\rangle\text{.}\) Hence this theorem is precisely the strong-sheafiness assertion of Theorem 8.10; it holds for every \(w\text{,}\) without a positivity or unboundedness assumption.

Finally, chartDatum is the rational datum \((W;\varpi)\text{.}\) The statements corresponding to Proposition 8.8, Proposition 8.9 are:

    theorem chartDatum_isRational (ϖ : Uniformizer K) :
    (chartDatum (w := w) ϖ).IsRational

theorem isDomain_chart
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    IsDomain (presheafValue
      (chartDatum (w := w) ϖ))

theorem not_isUniform_chart
    (hwu : ∀ M, ∃ n, 1 ≤ n ∧ M ≤ w n)
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    ¬ IsUniform (presheafValue
      (chartDatum (w := w) ϖ))

theorem not_isStablyUniform_WPA
    (hwu : ∀ M, ∃ n, 1 ≤ n ∧ M ≤ w n)
    (ϖ : Uniformizer K)
    (hK₀ : IsNoetherianRing (FiniteJet.unitBall K)) :
    ¬ IsStablyUniform (WPA K w)

The condition hwu says exactly that \(w\) is unbounded. Thus every positive unbounded weight gives all the assertions of Theorem 8.1; the paper takes \(w(n)=n\text{.}\)

Subsection A.7 Mathematical and code provenance

The definitions of rational localisation, the structure presheaf and the sheaf condition follow Huber [bib-Huber94] and Wedhorn [bib-Wedhorn]. The independence of the choice of ring of integral elements uses the standard rational-refinement formalism described by Kedlaya [bib-KedlayaAWS, Lemma 1.6.8 and Remark 1.6.9].

The restricted-power-series implementation includes code adapted from William Coram’s development [bib-CoramCode]. Its univariate Gauss-norm layer uses Fabrizio Barroero’s mathlib code [bib-BarroeroCode], while the multivariable power-series equivalences use code of Bingyu Xia [bib-XiaCode]. These are separate sources, and their attribution is retained in the corresponding source-file headers.

References

[bib-AINTLIB]

C. Birkbeck and contributors, AINTLIB: AdicSpaces formalisation, Lean 4 source code, Scottish Book snapshot 01116aca6, 2026, GitHub repository.

[bib-SheafyLean]

C. Birkbeck and A. Torzewski, Uniform sheafy Tate rings that are not stably uniform: the Lean formalisation, Lean 4 source code, snapshot 0a0d2be4c, 2026, GitHub repository.

[bib-BBK]

O. Ben-Bassat and K. Kremnizer, Non-Archimedean analytic geometry as relative algebraic geometry, Ann. Fac. Sci. Toulouse Math. (6) 26 (2017), no. 1, 49–126, DOI.

[bib-BK]

F. Bambozzi and K. Kremnizer, On the sheafyness property of spectra of Banach rings, J. Lond. Math. Soc. (2) 109 (2024), no. 1, e12855, DOI.

[bib-BV]

K. Buzzard and A. Verberkmoes, Stably uniform affinoids are sheafy, J. Reine Angew. Math. 740 (2018), 25–39.

[bib-BarroeroCode]

F. Barroero, Lean source code, mathlib source file.

[bib-CoramCode]

W. Coram, Lean source code, GitHub repository.

[bib-FK]

K. Fujiwara and F. Kato, Foundations of Rigid Geometry I, EMS Monographs in Mathematics, vol. 7, European Mathematical Society, 2018, DOI.

[bib-HK]

D. Hansen and K. S. Kedlaya, Sheafiness criteria for Huber rings, preprint, version of 23 April 2025, preprint PDF.

[bib-XiaCode]

B. Xia, Lean source code, mathlib pull request #36507.

[bib-Huber93]

R. Huber, Continuous valuations, Math. Z. 212 (1993), no. 3, 455–477, DOI.

[bib-Huber94]

R. Huber, A generalization of formal schemes and rigid analytic varieties, Math. Z. 217 (1994), 513–551, DOI.

[bib-KedlayaAWS]

K. S. Kedlaya, Sheaves, stacks, and shtukas, Arizona Winter School notes, 2017, course notes.

[bib-KL]

K. S. Kedlaya and R. Liu, Relative \(p\)-adic Hodge theory: Foundations, Astérisque 371 (2015), arXiv:1301.0792.

[bib-KST]

M. Kerz, S. Saito, and G. Tamme, \(K\)-theory of non-archimedean rings II, Nagoya Math. J. 251 (2023), 669–685.

[bib-Lean4]

L. de Moura and S. Ullrich, The Lean 4 theorem prover and programming language, in Automated Deduction—CADE 28, Lecture Notes in Comput. Sci., vol. 12699, Springer, 2021, 625–635, DOI.

[bib-mathlib]

The mathlib Community, The Lean mathematical library, in Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, ACM, 2020, 367–381, DOI.

[bib-Milnor]

J. Milnor, Introduction to Algebraic \(K\)-Theory, Annals of Mathematics Studies, vol. 72, Princeton University Press, Princeton, 1971.

[bib-Mihara]

T. Mihara, On Tate’s acyclicity and uniformity of Berkovich spectra and adic spectra, Israel J. Math. 216 (2016), no. 1, 61–105.

[bib-Scottish]

K. S. Kedlaya, The Nonarchimedean Scottish Book, Problems 7, 24, and 28, available online, Internet Archive snapshot of 24 November 2025 of the author’s wiki at MIT.

[bib-Stacks]

The Stacks Project Authors, The Stacks Project, project website.

[bib-Wedhorn]

T. Wedhorn, Adic spaces, 2019, arXiv:1910.05934.

PrevTopNext

Uniform sheafy Tate rings that are not stably uniform

Section 1 Introduction

Theorem 1.1.

Definition 1.2.

Remark 1.3. Relation with earlier work.

Section 2 Conventions and notation

Section 3 The finite-jet ring

Proposition 3.1.

Proof.

Section 4 A rational localisation which is not uniform

Proposition 4.1.

Proof.

Proposition 4.2.

Proof.

Section 5 Localisation of the Milnor square

Subsection 5.1 Koszul complexes for rational localisations

Lemma 5.1.

Proof.

Subsection 5.2 The defining ideals under pullback

Lemma 5.2.

Proof.

Proposition 5.3.

Proof.

Section 6 Milnor descent and strong sheafiness

Theorem 6.1. Milnor descent.

Proof.

Corollary 6.2.

Proof.

Proof of Theorem 1.1.

Section 7 Problems 24 and 28

Proposition 7.1.

Proof.

Section 8 A second example

Theorem 8.1.

Subsection 8.1 The weighted-parity algebra

Lemma 8.2. Finite-variable subrings.

Proof.

Proposition 8.3.

Proof.

Proposition 8.4.

Proof.

Subsection 8.2 Small perturbations of rational data

Lemma 8.5. Small perturbation lemma.

Proof.

Subsection 8.3 Rational localisations defined over finitely many variables

Proposition 8.6. Coefficientwise localisation.

Proof.

Corollary 8.7. Finite-variable presentation.

Proof.

Subsection 8.4 A reduced rational chart which is not uniform

Proposition 8.8.

Proof.

Proposition 8.9.

Proof.

Subsection 8.5 Strong sheafiness

Theorem 8.10.

Proof.

Proof of Theorem 8.1.

Remark 8.11. Admissible blow-ups.

Section 9 How the examples were found

Appendix A Lean formalisation and verification

Subsection A.1 The predicate IsSheafy

Definition A.1. The rational-cover predicate.

Subsection A.2 Comparison with Mathlib’s sheaf predicate

Remark A.2.

Subsection A.3 Sheafiness for Tate rings

Subsection A.4 Strong noetherianity

Definition A.3. Strong noetherianity.

Subsection A.5 The finite-jet example

Definition A.4. The finite-jet ring.

Subsubsection A.5.1 The Scottish Book statements

Subsubsection A.5.2 Koszul complexes and Milnor descent

Subsection A.6 The weighted-parity example

Subsection A.7 Mathematical and code provenance

References

Subsection A.1 The predicate `IsSheafy`