structure

ValuationSpectrum.RationalCoveringData

Mathematical summary.

A RationalCoveringData A consists of one rational-localisation datum for the base and a finite family of such data for the covering pieces. It records that every piece lies in the base and that their rational subsets cover the base. Rationality of the data themselves is imposed separately by C.IsRational.

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

Original Lean docstring

A *rational covering* of R(T/s) (Wedhorn §8.1).

Used in the paper for: Appendix A (finite rational-cover data); Appendix: finite rational covering data

structure RationalCoveringData (A : Type*) [CommRing A] [TopologicalSpace A]
    [IsTopologicalRing A] [PlusSubring A] where
  /-- The base rational localization datum. -/
  base : RationalLocData A
  /-- The covering rational localization data. -/
  covers : Finset (RationalLocData A)
  /-- Each covering piece is contained in the base. -/
  hsubset : ∀ D ∈ covers, rationalOpen D.T D.s ⊆ rationalOpen base.T base.s
  /-- The covering pieces cover the base. -/
  hcover : ∀ v ∈ rationalOpen base.T base.s,
    ∃ D ∈ covers, v ∈ rationalOpen D.T D.s

Pinned source: Adic spaces/Presheaf.lean:1895–1905
Commit 0a0d2be4c1104e5f52dc147cd28f1fec59fec6a3.

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