Adic Spaces — Lean blueprint🔗

This is the blueprint for the Adic-Spaces formalisation (Birkbeck) of Huber's theory of adic spaces — the point-set foundations of p-adic geometry and perfectoid spaces, following Wedhorn's Adic Spaces notes. It develops Huber rings and Tate rings, power-bounded and topologically nilpotent elements, the valuation spectrum \mathrm{Spv}, convex subgroups and coarsenings, continuous valuations, rings of integral elements, the adic spectrum \mathrm{Spa}, its quasi-compactness and rational subsets, the analytic locus, Tate algebras, and (in progress) the structure sheaf.

Each node carries a (lean := …) reference to the actual declaration in the «Adic spaces» library, so Verso reads its completion status directly from Lean, and its prose cites the corresponding numbered result in Wedhorn. The dependency graph at the foot of the page records how the constructions build on one another.