def

ValuationSpectrum.RationalCoveringData.IsRational

Mathematical summary.

For a covering datum C, C.IsRational means that its base and every covering piece satisfy the rationality condition: the finite numerator set T generates an open ideal of A. For a Tate ring, this is equivalent to T generating the unit ideal.

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

Original Lean docstring

Wedhorn Definition 7.29 for coverings: a RationalCoveringData is *rational* when
its base and every piece satisfy Definition 7.29's openness condition (T·A open in
A, wedhorn.txt:3100) — i.e. it is a covering of a rational subset by rational subsets
("a finite covering of X be rational subsets", wedhorn.txt:4143). The sheaf condition
(Definition 8.26 / Theorem 8.28) quantifies over exactly these coverings.

Used in the paper for: Appendix A (rationality condition); Appendix: rationality of a finite covering

def RationalCoveringData.IsRational {A : Type*} [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [PlusSubring A] (C : RationalCoveringData A) : Prop :=
  C.base.IsRational ∧ ∀ D ∈ C.covers, D.IsRational

Pinned source: Adic spaces/Presheaf.lean:1912–1914
Commit 0a0d2be4c1104e5f52dc147cd28f1fec59fec6a3.

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