def

ValuationSpectrum.presheafValue

Mathematical summary.

For a rational datum D = (T/s), presheafValue D is 𝒪_X(R(T/s)) = A⟨T/s⟩: the completion of A[1/s] for the rational-localisation topology determined by the fractions t/s, with t ∈ T. It is the section ring assigned to that rational subset.

The mathematical summary is editorial text for this paper. The declaration below is extracted verbatim from the pinned source.

Original Lean docstring

The presheaf value 𝒪_X(R(T/s)) := A⟨T/s⟩, the completion of
Localization.Away s with the localization topology
(§8.1, eq. 8.1.1 of Wedhorn).

Used in the paper for: Appendix A (completed rational localisation); Appendix: sections on a rational domain

noncomputable def presheafValue (D : RationalLocData A) : Type _ :=
  @UniformSpace.Completion (Localization.Away D.s) D.uniformSpace

Pinned source: Adic spaces/Presheaf.lean:296–297
Commit 0a0d2be4c1104e5f52dc147cd28f1fec59fec6a3.

View this pinned source on GitHub. The declaration above is also embedded here so that the paper remains independent of branch movement.