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 e3514f12e382a8ef8f0d2b8822ed9b792bcaf838.

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