The rational basis of the adic spectrum #
Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.29, Remark 7.30(5), and Theorem 7.35.
Let P = (A₀,I) be a pair of definition of a Huber ring. The rational subsets
R(T/s) = {v ∈ Spa(A,A⁺) : v(t) ≤ v(s) ≠ 0 for every t ∈ T}
for which the ideal T · A is open form a basis of quasi-compact opens of Spa(A,A⁺).
The proof compares them with the rational basis of Spv(A,IA). By Wedhorn Lemma 6.6,
openness of T · A implies admissibility for IA; conversely, an admissible pair (T,s)
has open numerator ideal after inserting s among the numerators, which does not change its
rational subset. This comparison also transports closure under intersections and quasi-compactness.
Closure under intersection appears in two strengths. Remark 7.30(5) is the binary statement,
recorded here as inter_mem_spaRationalFamily; Theorem 7.35(2) asserts the stronger claim that
the basis is stable under finite intersection. The finite form is the one a common refinement
of a finite rational cover consumes, and it carries no nonemptiness hypothesis.
The plus ring is arbitrary here. The additional condition that it be a ring of integral elements is part of calling the resulting space the adic spectrum of a Huber pair, but none of the basis arguments uses it.
Main definitions #
TauCeti.ValuationSpectrum.spaRationalFamily: the family of rational subsets with open numerator ideal, viewed as subsets ofspa Aplus.TauCeti.ValuationSpectrum.spaRationalOpens: the same family presented as a set ofOpens, the form the sheaf-theoretic consumers take.
Main results #
TauCeti.ValuationSpectrum.inter_mem_spaRationalFamily: the family is closed under binary intersections, which is Wedhorn Remark 7.30(5).TauCeti.ValuationSpectrum.biInter_mem_spaRationalFamily: the family is closed under finite intersections, which is the stability clause of Wedhorn Theorem 7.35(2). It is stated over aFinsetindex, withTauCeti.ValuationSpectrum.iInter_mem_spaRationalFamilyfor a finite index type andTauCeti.ValuationSpectrum.sInter_mem_spaRationalFamilyfor a finite subfamily, the form a refinement argument produces.TauCeti.ValuationSpectrum.finiteInter_spaRationalFamily: the same closure as Mathlib'sFiniteInterstructure, which the three forms above are read off.TauCeti.ValuationSpectrum.inf_mem_spaRationalOpensandTauCeti.ValuationSpectrum.finsetInf_mem_spaRationalOpens: the same two closure statements in the bundledOpensform, together withTauCeti.ValuationSpectrum.top_mem_spaRationalOpens.TauCeti.ValuationSpectrum.isTopologicalBasis_spaRationalFamily: the family is a basis for the topology ofspa Aplus, withTauCeti.ValuationSpectrum.isBasis_spaRationalOpensthe same statement in theOpens.IsBasisform.TauCeti.ValuationSpectrum.isCompact_of_mem_spaRationalFamily: every member of the family is quasi-compact. Each result also has an_of_pairOfDefinitionform for use with a specified pair of definition.TauCeti.ValuationSpectrum.spaComap_preimage_mem_spaRationalFamily: a rational open pulls back to a rational open when the ring map sends open ideals to open ideals.TauCeti.ValuationSpectrum.exists_finite_spaRationalFamily_refinement: every open cover of a member of the family admits a finite refinement by members of the family — the basis and compactness results combined, and the form a sheaf criterion on this basis consumes.TauCeti.ValuationSpectrum.spa_eq_biUnion_rationalSubset_of_isTateRing_of_isOpen: over a Tate ring, if a finite setTgenerates an open ideal, then the standard rational subsets coverspa Aplus(Wedhorn Corollary 7.53 specialization).TauCeti.ValuationSpectrum.exists_unit_forall_mem_spa_exists_vlt: for a finite standard cover of a Tate ring, a unit is strictly dominated at every point by some numerator.
References #
- T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 7.29, Remark 7.30, Theorem 7.35, Corollaries 7.32 and 7.53, Lemmas 6.6 and 8.34.
One correction to the source: Wedhorn's proof of Theorem 7.35(2) cites Remark 7.30(4) for
stability under finite intersection, but 7.30(4) is the statement that R(T/s) is rational
for a unit s. The binary intersection this file iterates is Remark 7.30(5).
Open numerator ideals and admissibility #
An open numerator ideal is admissible for the extended ideal of every pair of definition. This is Wedhorn Lemma 6.6 applied to the inclusion of the numerator span into the span obtained after adjoining the denominator.
An admissible numerator set becomes an open numerator ideal after adjoining its denominator. The rational subset itself is unchanged by this operation.
The rational family #
The rational family of Spa(A,A⁺): rational subsets R(T/s) whose numerator ideal
T · A is open, viewed as subsets of the subtype spa Aplus.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Membership in the rational family is a presentation as R(T/s) with open numerator ideal.
Rational opens pull back to rational opens when images of open ideals are open.
The whole adic spectrum belongs to its rational family, presented as R({1}/1).
Wedhorn Remark 7.30(5). Rational subsets with open numerator ideal are closed under
intersection. The set identity is rationalSubset_inter; admissibility is multiplicative in
Spv(A,IA), and adjoining the product denominator turns it back into openness.
Wedhorn Remark 7.30(5). Over a Huber ring, the rational family is closed under binary intersection, without choosing a pair of definition.
The rational family is closed under finite intersection, from a specified pair of
definition, as Mathlib's FiniteInter structure.
The rational family is closed under finite intersection, over a Huber ring.
Wedhorn Theorem 7.35(2), finite-intersection half, for a finite subfamily: an intersection
of finitely many rational subsets is again rational. This is the unindexed form, and the one a
refinement argument produces, where the finite family comes out of quasi-compactness rather than
out of an index type — see exists_finite_spaRationalFamily_refinement.
Wedhorn Theorem 7.35(2), finite-intersection half, indexed by a Finset. This is the form
Wedhorn's Theorem 7.35(2) states — "a basis of quasi-compact open subsets which is stable under
finite intersection" — whereas inter_mem_spaRationalFamily gives only the binary case.
Wedhorn Theorem 7.35(2), finite-intersection half, for a finite index type.
Basis and quasi-compactness #
Rational subsets form a basis of Spa(A,A⁺). The statement is made from an explicit
pair of definition. Every rational neighbourhood in the basis of Spv(A,IA) becomes a member
of spaRationalFamily after adjoining its denominator.
Every neighbourhood of a point of Spa(A,A⁺) contains the rational subset of an admissible
presentation containing the point.
Rational subsets form a basis of Spa(A,A⁺), without choosing a pair of definition
of the Huber ring.
Every member of the rational family of Spa(A,A⁺) is quasi-compact. Its counterpart in
Spv(A,IA) is a quasi-compact open, and its intersection with the pro-constructible trace of
spa Aplus stays quasi-compact.
Every rational subset with open numerator ideal in the adic spectrum of a Huber ring is quasi-compact, without choosing a pair of definition.
The rational basis as a family of opens #
The rational family of Spa(A,A⁺), presented as a set of Opens rather than of sets. This is
the form Opens.IsBasis and the sheaf criteria on a basis take.
Equations
Instances For
An open lies in spaRationalOpens exactly when its underlying set is rational.
An open is a rational open exactly when it is a basic open R(T/s) whose numerator ideal
T · A is open. This is mem_spaRationalFamily_iff for Opens, with the basic open
spaBasicOpen Aplus T s in place of the preimage of rationalSubset Aplus T s.
The rational opens are a basis in the Opens.IsBasis sense, which is the form the sheaf
criterion on a basis consumes.
The whole space is a rational open, presented as R({1}/1).
The basic open R(T/s) is a rational open as soon as its numerator ideal T · A is open.
Wedhorn Remark 7.30(5) in the bundled form: the rational opens are closed under binary
meet. Meet of Opens is intersection of the underlying sets, so this is
inter_mem_spaRationalFamily read through mem_spaRationalOpens.
Wedhorn Theorem 7.35(2), finite-intersection half, in the bundled form: the rational
opens are closed under Finset.inf. This is the shape a sheaf criterion on the basis takes,
where the finite intersections of a cover are formed in Opens rather than in Set.
Finite rational refinements #
Every open cover of a rational subset admits a finite refinement by rational subsets. This is the previous two results combined: being a basis shrinks each point's cover member to a rational neighbourhood, and quasi-compactness then keeps finitely many of them. It is the shape a sheaf criterion on the rational basis consumes, where the cover is arbitrary but the Čech complex must be built from the basis itself.
The two-step argument follows AINTLIB's exists_finite_rational_refinement_huber and its Tate-only
exists_finite_rational_refinement (branch dev/adic-spaces, commit 37bbdaeb, Apache 2.0), in
projects/AdicSpaces/Adic spaces/RestrictedLimitSheaf.lean. Two differences: quasi-compactness is a
hypothesis there and is discharged here by isCompact_of_mem_spaRationalFamily; and the conclusion
there is a Finset of a bundled index type over RationalLocData, whereas this states a finite
subfamily of spaRationalFamily with the containment as a side condition, matching the vocabulary
this file already uses.
Standard rational covers #
Over a Tate ring, if a finite set T generates an open ideal, then the standard rational
subsets (R(T/t))_{t ∈ T} cover spa Aplus.
A dominating unit for a standard rational cover (the input to Wedhorn Lemma 8.34(ii)).
Let A be a Tate ring and T a finite set generating the unit ideal. Then some unit ϖ of A
is strictly dominated at every point of Spa (A, A⁺) by an element of T.
This supplies the unit used to form the Laurent generators ϖ⁻¹ t in part (ii).