Add roadmap: adic spaces, up to the Fargues–Fontaine curve - #80
Draft
CBirkbeck wants to merge 12 commits into
Draft
Add roadmap: adic spaces, up to the Fargues–Fontaine curve#80CBirkbeck wants to merge 12 commits into
CBirkbeck wants to merge 12 commits into
Conversation
…horn Six layers on Mathlib's ValuativeRel substrate: Huber/Tate rings (prototyped seeds: PairOfDefinition, IsHuberRing, IsTateRing; Q_p is Tate, Z_p is not), Spv and its spectrality, Cont and Spa with rational subsets, rational localization and the structure presheaf with the category V, the sheafiness theorem for complete strongly noetherian Tate rings with full-degree Tate acyclicity, adic spaces as locally-V-isomorphic objects, and the finite-jet pinching example ([FJP]): a uniform non-noetherian sheafy domain that is not stably uniform, answering Hansen-Kedlaya Remark 3.16, with Buzzard-Verberkmoes proved alongside. Provenance pins AINTLIB dev/adic-spaces @ 2e5b1cf6 with a per-file sorry audit: foundations and the FJP directory sorry-free, the structure presheaf, Spv spectrality, and acyclicity as the open frontier, and the 828b sheafiness capstone gated on a dependency-cone axiom audit. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
… closing stress test The intro now leads with acyclicity-in-all-degrees (sheafiness as its degree-<=1 shadow) and adic spaces; Layer 6 becomes uniformity + BV with the finite-jet pinching algebra reframed as a suggested worked example exercising Layers 0-4, its strong-sheafiness refinement (Cor 5.5) explicitly not a target. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…heafy Layer 3 now defines IsSheafy (A, A+) := IsSheafOfTopologicalRings O_X — the category-valued sheaf condition in topological commutative rings, glued sections carrying the topology (Mathlib's sheaf-condition machinery and TopCommRingCat as substrate; name and shape after the Lean 3 perfectoid project) — with the finite-rational-cover embedding+gluing form, which is what the AINTLIB provenance carries, proved equivalent as a named milestone (Wedhorn 8.16-shape cofinality). Downstream sheafiness proofs (the strongly noetherian theorem, the FJP transfer) land in the two-part form and reach the definition of record across the equivalence; the provenance entry records that migrated capstones are re-expressed accordingly. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…alisation, not the unavailable preprint All [FJP] paper citations are removed: the stress test is now specified self-containedly in Layer 6 with the sorry-free AINTLIB formalisation (the FJP/ directory and its capstone exports) as its reference — recorded in the intro, the sources convention (one layer has no paper source, and the provenance evidences the specification), the Layer-6 bullet, the references list, the provenance entry, the migration cautions (there is no paper to consult), and the Suggested.lean Layer-6 comment. Strong sheafiness is now named by its content rather than a corollary number. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…it (Layer 7)
Rebuilt around the object the rest of the roadmap exists for. New Layer 7
specifies the curve for E = Q_p and a perfectoid field F of characteristic p
(algebraic closedness deliberately NOT assumed — nothing in the construction
needs it): A_inf as a complete Huber ring in the (p,[w])-adic "weak" topology
with A_inf+ = A_inf; Y as the nonempty open phi-stable locus v(p[w]) != 0,
with a Gauss point exhibited; rank-free radius predicates and the windows;
freeness and wandering; X = Y/phi^Z quasi-compact and T0; Kedlaya's interval
rings B^I strongly noetherian (Thm 4.10) hence sheafy BY LAYER 4 — the
roadmap's own theorem consumed by its summit; the descended phi-invariant
structure presheaf as a sheaf of topological rings and X as a V-object; and
the final clause, local isomorphism in V.
Conventions pinned after an adversarial review: the two Frobenius/point-action
conventions and which gives kappa . phi = p kappa; Y is D(p) cap D([w]), NOT
the analytic locus D(p) cup D([w]); "weak topology" means (p,[w])-adic here;
A+ = A_inf is right for A_inf but not for the Tate charts, where B^{I,+} is
the unit ball of lambda_I and its agreement with the rational-localization
plus ring is a theorem; the kappa-to-interval dictionary is INVERSE, with the
conversion lemma to be proved rather than assumed by notation; the breakpoint
c = (p+1)/2 is ours, not Kedlaya's 1 + 1/p (they agree only at p = 2); the
diagonal-closure model of B^I is faithful only subject to an explicit isometry
checklist, and elements of B^I need not have convergent Witt expansions;
quasi-compact does not mean affinoid; and independence of the pseudouniformizer
must be proved. A caveat flags that the sheafiness theorem is cited as 8.28(b)
here and in provenance while another version of Wedhorn numbers it 8.27(b) —
to be fixed once against the pinned revision.
Provenance re-pinned at dev/adic-spaces @ 59bbbe8b: the FarguesFontaine
directory is 39 files, ~1.9 MB, zero file-level sorries — with the honest
reading that it sits on the Layer-3/4 machinery that is not, and that the
V-level chart isomorphism is specification rather than migration. Structure
theory (bundles, HN, classification, fundamental exact sequence, B_dR/B_cris,
classical points, general E, relative curve, Proj + GAGA) is named as the
successor roadmap in dependency order. Mathlib's Perfectoid/FontaineTheta,
Untilt and BDeRham plus WittVector.Isocrystal are added to the consume list.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
CBirkbeck
changed the title
…cord Remark 8.27 as a second route Checked the source directly: the paper has only one version (v1, 14 Oct 2019), so the pinned revision is the current text. Definition 8.26 is sheafy/stably sheafy, Remark 8.27 is the pre-adic-space criterion, and Theorem 8.28(b) is the strongly-noetherian Tate sheafiness theorem — our citation and the provenance's Wedhorn828/828b names are correct; an external review reading a different edition had reported 8.27(b). Two findings folded in: 8.28 already carries the rational-cover acyclicity clause, so Layer 4's two headline statements are one theorem in the source; and Remark 8.27 gives Layer 7 a second route to the summit — a pre-adic space with an affinoid cover by stably sheafy rings is an adic space, and Kedlaya 4.10 supplies stable sheafiness — now recorded as a decision to take before starting. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This was referenced Jul 30, 2026
Updated wording for clarity and consistency in the README.
…review fixes
Reframe: the roadmap develops the theory of adic spaces, and Layer 7
applies it to construct the adic Fargues-Fontaine curve — no summit /
headline / stress-test / division-of-labour language, no file-size
flexing. Substantive corrections from the adversarial pass, each
verified independently: spectrality is Mathlib's bundled SpectralSpace
(the pin already has it, T0Space included — the four-class spelling
missed T0 and the 'Mathlib does not bundle' premise was false); the
kappa-to-rho radius dictionary corrected to the reciprocal form
kappa = alpha/r, window [a,b] <-> rho in [|w|^{1/a}, |w|^{1/b}] (the
two previously displayed forms contradicted each other); the Banach-OMT
non-applicability justified by the right reason (not a Banach space
over a valued field, rather than sigma-compactness); route (b) via
Wedhorn 8.27 priced honestly (pre-adic packaging still needed, plus
quotient permanence of strong noetherianness); the finite-jet sheaf
transfer's localized-Milnor-row and completed-localization steps named
as milestones; Witt-expansion warning stated as a warning. Citation
fixes: Henkel's exact title; Huebner's arXiv:2405.06435 is the 'Adic
spaces' lecture notes; AINTLIB is now Apache-2.0. A stale-edition
Wedhorn renumbering claim from the review was rejected — the README's
existing verified note against arXiv v1 stands.
Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…lliam Coram The fibre-product example is presented as what it is — an interesting ring built for this roadmap to prove sheafy (and which answers HK Remark 3.16) — not as a standard named object; 'finite-jet pinching' naming removed from prose (the provenance's FJP/ file names and Lean identifiers stay as code labels). The restricted-power-series development — Mathlib's PowerSeries.IsRestricted and the vendored Gauss-norm material — is credited to William Coram (verified against the Mathlib file's author line), with coordination noted. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Nineteen warning triangles and a checkmark removed; the sentences already say 'do not', 'note', 'must be proved' where it matters, and the signage was noise on top. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
…re, and prose Mathematical corrections: the completion map is an embedding only for Hausdorff A (kernel = closure of 0, dense image stated); strong noetherianness quantifies over completed algebras, so n = 0 gives noetherianity of the completion, of A itself only when complete, and the field case is stated at rank one (BGR 5.2.6); the Tate-ring openness criterion for rational data is (T)A = A, not the existence of a unit multiple among the elements; Henkel's open mapping theorem is stated with its hypotheses and its strictness corollary; Wedhorn's category ladder is restored (V^pre, affinoid pre-adic, pre-adic, V, adic), stalks are colimit rings with no claimed topology, and O+ is defined; sheafiness gets three named notions (pair, ring, stably) with their relations; Layer 4 claims the Cech-acyclicity theorem rather than verbatim 8.28's H^q clause; A+ becomes explicit data with a bundled HuberPair for categorical uses, replacing the PlusSubring typeclass. Specification upgrades: the rational-localization universal property in full (with the plus ring and the strictification milestones); the five-step flatness bridge; the expanded finite-cover sheaf criterion; the theorem-level Spv spectrality plan; the gluing specification and the open-disc cover; the power-comparability lemma behind the windows; the per-hypothesis list for applying Layer 4 to B^I (endpoint completions no longer called fields); the perfectoid input list and the five-step pseudouniformizer-independence theorem; the direct wandering-slice route fixed for the chart isomorphism, with stable sheafiness retained as a supporting theorem; the finite-jet example relabelled a proposed counterexample to Hansen-Kedlaya Remark 3.16 requiring independent review, with its verification requirements. Coordination: the roadmap now records mathlib4#38009/#42312/#42315 and defers Layer-0-2 names to upstream. Provenance is a status table with direct-sorry and transitive-audit columns; the pin is unified at 59bbbe8ba14a. Prose rewritten per the review: campaign vocabulary removed, each layer split into definitions / main results / dependencies / status. Suggested.lean synced (Layers 0-7, the coordination note, the three sheafiness names, the counterexample labelling). Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Drop the independent-review requirement: the construction answering Hansen-Kedlaya Remark 3.16 is proved in the FJP/ directory, and the only caveat is the Layer-4 dependency-cone audit every downstream result already carries. The former requirements list becomes the migration decomposition of what the proof contains. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
A roadmap for the foundations of Huber's theory of adic spaces (
TauCetiRoadmap/AdicSpaces/, README +Suggested.lean): Huber and Tate rings, the valuation spectrumSpv A, continuous valuations and the adic spectrumSpa (A, A⁺), rational localization and the structure presheaf, the sheafiness theorem with Čech acyclicity for strongly noetherian Tate rings (Wedhorn Theorem 8.28(b) / Huber), the definition of adic spaces, and — as the final application (Layer 7 of Layers 0–7) — the adic Fargues–Fontaine curve𝒳 = 𝒴/φ^ℤforE = ℚ_pand a perfectoid fieldFof characteristicp.Notes
Spvand its topology onValuativeRel), mathlib4#42312 (Huber rings), mathlib4#42315 (Spaas a topological space). The roadmap follows the upstream decisions:Spais a subspace ofSpv, points are valuations up to equivalence, and the Layer-0–2 names align with upstream at migration.A⁺is explicit data. Ring properties (IsHuberRing,IsTateRing,IsStronglyNoetherian,IsUniform) arePropmixins; theorems takeAplus : Subring Aexplicitly; a bundledHuberPair(with morphisms carrying continuity andf(A⁺) ⊆ B⁺) serves the categorical uses. No globalA⁺typeclass, and no globally bundled pair.𝒱^pre(presheafed spaces with stalk valuations) → affinoid pre-adic spaces → pre-adic spaces →𝒱(the sheaf subcategory) → adic spaces. Sheafiness comes in three named notions (IsSheafyPair,IsSheafyRing,IsStablySheafyRing), and Layer 4 proves the pair-level sheafiness theorem plus the all-degrees Čech acyclicity actually used by the applications (theH^q-vanishing form of 8.28 needs a Čech-to-sheaf-cohomology comparison; sheaf cohomology is not developed here).FJP/directory; its formal status inherits the Layer-4 dependency cone like every downstream result.𝒱^pre(the one genuinely new theorem; the topological charts exist in provenance), lists every hypothesis needed to apply Layer 4 to Kedlaya's interval ringsB^I, and states the power-comparability lemma the rank-free window covering rests on.B_dR, generalE, the relative and schematic curves) — a successor roadmap.dev/adic-spaces @ 59bbbe8ba14a(2026-07-28), with a per-milestone status table in the README separating directsorrycounts from the transitive#print axiomsaudit required at migration. The sheafiness capstone andSpvspectrality are the main incomplete parts; the quotient-curve topology and interval-ring strands are implemented but inherit that cone.🤖 Generated with Claude Code