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

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