HEXAGONbeta

Uniform sheafy Tate rings that are not stably uniform

A mix of human-written and AI-generated textHuman understanding: all partsmath.AG — Algebraic Geometrymath.NT — Number Theory

Contributed by Christopher Birkbeck ↗, Alex Torzewski

Version 1 / Oct 26, 2026 / CC BY 4.0

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

Provenance statement

This was a problem we had thought about for some time, we then talked to ChatGPT and together produced these new examples.

Formalizations

Tools used

Lean
Lean
OpenAI
ChatGPTVersion 5.6 Sol
Anthropic
Claude Fable

References

  1. C. Birkbeck and contributors, AINTLIB: AdicSpaces formalisation , Lean 4 source code, Scottish Book snapshot 01116aca6 (https://github.com/CBirkbeck/AINTLIB/commit/01116aca6070283726008536cba16d165a01b505), 2026, GitHub repository (https://github.com/CBirkbeck/AINTLIB).link
  2. C. Birkbeck and A. Torzewski, Uniform sheafy Tate rings that are not stably uniform: the Lean formalisation , Lean 4 source code, snapshot e3514f12e (https://github.com/CBirkbeck/uniform-sheafy-tate-domains-lean/commit/e3514f12e382a8ef8f0d2b8822ed9b792bcaf838), 2026, GitHub repository (https://github.com/CBirkbeck/uniform-sheafy-tate-domains-lean).link
  3. 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 (https://doi.org/10.5802/afst.1526).DOI
  4. 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 (https://doi.org/10.1112/jlms.12855).DOI
  5. K. Buzzard and A. Verberkmoes, Stably uniform affinoids are sheafy , J. Reine Angew. Math. 740 (2018), 25--39.
  6. F. Barroero, Lean source code, mathlib source file (https://github.com/leanprover-community/mathlib4/blob/fd1d54bcac5caba4eff2ea3421c47d907333f515/Mathlib/RingTheory/PowerSeries/GaussNorm.lean).link
  7. W. Coram, Lean source code, GitHub repository (https://github.com/WilliamCoram/PhD/tree/e8fcf8fbff848a95475ab62ae2568cbb73961de8).link
  8. K. Fujiwara and F. Kato, Foundations of Rigid Geometry I , EMS Monographs in Mathematics, vol. 7, European Mathematical Society, 2018, DOI (https://doi.org/10.4171/135).DOI
  9. D. Hansen and K. S. Kedlaya, Sheafiness criteria for Huber rings , preprint, version of 23 April 2025, preprint PDF (https://kskedlaya.org/papers/criteria.pdf).link
  10. B. Xia, Lean source code, mathlib pull request #36507 (https://github.com/leanprover-community/mathlib4/pull/36507).link
Show all 22 referencesShow fewer references
  1. R. Huber, Continuous valuations , Math. Z. 212 (1993), no. 3, 455--477, DOI (https://doi.org/10.1007/BF02571668).DOI
  2. R. Huber, A generalization of formal schemes and rigid analytic varieties , Math. Z. 217 (1994), 513--551, DOI (https://doi.org/10.1007/BF02571959).DOI
  3. K. S. Kedlaya, Sheaves, stacks, and shtukas , Arizona Winter School notes, 2017, course notes (https://swc-math.github.io/aws/2017/2017KedlayaNotes.pdf).link
  4. K. S. Kedlaya and R. Liu, Relative pp-adic Hodge theory: Foundations , Astérisque 371 (2015), arXiv:1301.0792 (https://arxiv.org/abs/1301.0792).arXiv
  5. M. Kerz, S. Saito, and G. Tamme, KK-theory of non-archimedean rings II , Nagoya Math. J. 251 (2023), 669--685.
  6. 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 (https://doi.org/10.1007/978-3-030-79876-5_37).DOI
  7. 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 (https://doi.org/10.1145/3372885.3373824).DOI
  8. J. Milnor, Introduction to Algebraic KK-Theory , Annals of Mathematics Studies, vol. 72, Princeton University Press, Princeton, 1971.
  9. T. Mihara, On Tate's acyclicity and uniformity of Berkovich spectra and adic spectra , Israel J. Math. 216 (2016), no. 1, 61--105.
  10. K. S. Kedlaya, The Nonarchimedean Scottish Book , Problems 7, 24, and 28, available online (https://web.archive.org/web/20251124070248/https://scripts.mit.edu/~kedlaya/wiki/index.php?title=The_Nonarchimedean_Scottish_Book), Internet Archive snapshot of 24 November 2025 of the author's wiki at MIT.link
  11. The Stacks Project Authors, The Stacks Project , project website (https://stacks.math.columbia.edu).link
  12. T. Wedhorn, Adic spaces , 2019, arXiv:1910.05934 (https://arxiv.org/abs/1910.05934).arXiv

Version history

  1. v1Submitted by Christopher BirkbeckInitial depositCurrentOct 26, 2026