Rational subsets of the adic spectrum

The set-level constructions beneath Wedhorn, Adic Spaces (arXiv:1910.05934v1), Definition 7.29 and Remark 7.30.

For a finite numerator set T and a denominator s, the rational subset is the trace on spa A⁺ of the basic open Spv(A)(T/s):

R(T/s) = {v ∈ spa A⁺ | v(t) ≤ v(s) ≠ 0 for every t ∈ T} = spa A⁺ ∩ Spv(A)(T/s).

As with spa itself, the definition is stated for arbitrary data: no hypothesis relates the topology of A to its ring operations, the subring is arbitrary, and Wedhorn's standing condition that the ideal T · A be open is not assumed. It is Wedhorn's rational subset of Spa (A, A⁺) under his hypotheses (a Huber ring, a ring of integral elements, T · A open); the open-ideal condition enters only in the results that need it — Wedhorn's admissibility setting, the basis claims of Definition 7.29, and the quasi-compactness of Theorem 7.35. The generalized unit-ideal standard-cover theorem itself requires no openness hypothesis.

The exported interface of the definition, the normalizations and the intersection identity inherited from Spv(A)(T/s), the whole-space case, containment in spa A⁺, and relative openness in the subspace all hold with no extra hypotheses. The file also proves the forward standard-cover implication of Corollary 7.53.

On the intersection identity, writing Uᵢ = insert sᵢ Tᵢ for each numerator set augmented by its own denominator (which costs nothing, by rationalSubset_insert_self),

R(T₁/s₁) ∩ R(T₂/s₂) = R(U₁U₂ / s₁s₂).

The augmentation is essential: with the bare products T₁T₂ the identity is false — for T₁ = {t} and T₂ = ∅ the right-hand side would forget the condition v(t) ≤ v(s₁). This identity is the set-level half of Wedhorn's Remark 7.30(5); his full statement also says the right-hand pair is again admissible (U₁U₂ · A open), which belongs to the open-ideal layer deferred above.

Main definitions

• TauCeti.ValuationSpectrum.rationalSubset : the rational subset R(T/s) of spa A⁺, as a Set (Spv A).

Main results

• TauCeti.ValuationSpectrum.rationalSubset_def and TauCeti.ValuationSpectrum.mem_rationalSubset_iff : the set-level and membership-level characterizations — the definition is not exposed across the module boundary, so these two are the exported interface, as for spa_def/mem_spa_iff.
• TauCeti.ValuationSpectrum.rationalSubset_subset_spa : every rational subset is contained in the adic spectrum.
• TauCeti.ValuationSpectrum.rationalSubset_subset_rationalSubset_of_subset : the rational subset is antitone in its numerator set.
• TauCeti.ValuationSpectrum.rationalSubset_mul_subset_rationalSubset : refining a presentation by a cofactor shrinks the rational subset.
• TauCeti.ValuationSpectrum.rationalSubset_subset_rationalSubset_of_le : refinement of bundled presentations shrinks the rational subset.
• TauCeti.ValuationSpectrum.rationalSubset_union_of_forall_vle and TauCeti.ValuationSpectrum.rationalSubset_insert_of_forall_vle : numerators already dominated by the denominator throughout R(T/s) may be adjoined to T without changing the subset, a finite set of them at a time or one at a time.
• TauCeti.ValuationSpectrum.rationalSubset_insert_self : the denominator may be inserted among the numerators.
• TauCeti.ValuationSpectrum.rationalSubset_image_mul_right : multiplying every numerator and the denominator by the same unit does not change the rational subset.
• TauCeti.ValuationSpectrum.rationalSubset_singleton_one : the whole spectrum is the rational subset R({1}/1) — Wedhorn's "Spa (A, A⁺) itself is rational".
• TauCeti.ValuationSpectrum.val_preimage_rationalSubset : on the subtype spa A⁺, a rational subset is just the trace of its ambient basic open.
• TauCeti.ValuationSpectrum.isOpen_val_preimage_rationalSubset : a rational subset is relatively open in the subspace spa A⁺.
• TauCeti.ValuationSpectrum.rationalSubset_inter : the intersection identity above — the set-level half of Remark 7.30(5).
• TauCeti.ValuationSpectrum.rationalSubset_eq_biInter_singleton : over a nonempty T, a rational subset is the intersection of its one-numerator pieces R({t}/s), the decomposition a refinement to a standard rational cover consumes.
• TauCeti.ValuationSpectrum.exists_refinement_of_subset : the re-presentation step of Wedhorn §8.2 — from R(T'/s') ⊆ R(T/s), a presentation R(T''/(s · s')) of the smaller subset whose denominator has each original denominator as a factor and whose numerators contain t · s' for t ∈ T and t' · s for t' ∈ T'. Constructing a restriction map needs one further, algebraic input beyond these, the standing HasDenominatorPower hypothesis for the new pair, which this file does not supply.
• TauCeti.ValuationSpectrum.spa_eq_biUnion_rationalSubset_of_span_eq_top : a finite set generating the unit ideal gives a standard rational cover, the forward implication of Corollary 7.53.
• TauCeti.ValuationSpectrum.span_eq_top_iff_forall_mem_spa_exists_not_vle_zero : Corollary 7.53 in pointwise form — T generates the unit ideal exactly when no point vanishes on all of it.

References

• T. Wedhorn, Adic Spaces, arXiv:1910.05934v1, Definition 7.29, Remark 7.30, and Corollary 7.53.
• AINTLIB (github.com/CBirkbeck/AINTLIB, Apache-2.0) at commit 2baa76f742bdb4fb8ee323fabba41203bd390e08, projects/AdicSpaces/Adic spaces/RationalSubsets.lean, is the roadmap's designated prior formalisation of this material and was consulted. It develops the same statements around a standalone rationalOpen and an existential IsRationalSubset predicate, with the intersection identity conditioned on each denominator lying in its numerator set and the same insert-absorption discharging that condition. Here the rational subset is instead the trace of the merged Spv A-level basicOpenFinset, so the identities are inherited from basicOpenFinset_insert_self and basicOpenFinset_inter rather than reproved; no proof code is taken from that file.
• rationalSubset_eq_biInter_singleton is adapted from a different AINTLIB file and revision: commit 37bbdaeb9ad9e3bc9f0d660feadc2779e455a91c, projects/AdicSpaces/Adic spaces/LaurentRefinementCore.lean, theorem rationalOpen_eq_iInter_singleton (line 48). The statement is restated for this repository's API — that development spells the object rationalOpen, takes A⁺ from a [PlusSubring A] instance and carries the spa conjunct inline, whereas rationalSubset takes (Aplus : Subring A) explicitly and cuts inside spa Aplus — but the proof follows the source closely: the same ext/constructor split, the same three-part destructuring, and the same use of a witness from hT to transport the two t-independent conditions. Only the unfolding step differs, mem_rationalSubset_iff here against rationalOpen there.

def TauCeti.ValuationSpectrum.rationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : Set (ValuationSpectrum A)

The rational subset R(T/s) of the adic spectrum: the trace on spa A⁺ of the basic open Spv(A)(T/s). Under Wedhorn's hypotheses — a Huber ring, a ring of integral elements, and the ideal T · A open — this is his Definition 7.29; the definition itself asks for none of them, and the open-ideal condition matters only for results such as Wedhorn's admissibility setting or the basis claims, not for the definition nor the generalized unit-ideal cover.

Equations

• TauCeti.ValuationSpectrum.rationalSubset Aplus T s = TauCeti.ValuationSpectrum.spa Aplus ∩ TauCeti.ValuationSpectrum.basicOpenFinset T s

theorem TauCeti.ValuationSpectrum.rationalSubset_def {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : rationalSubset Aplus T s = spa Aplus ∩ basicOpenFinset T s

The set-level characterization of a rational subset. The definition is not exposed across the module boundary, so this equation is how consumers apply set-level results to rationalSubset — for instance rationalSubset_def _ _ _ ▸ Set.inter_subset_left for the containment in spa A⁺, which rationalSubset_subset_spa records.

@[simp]

theorem TauCeti.ValuationSpectrum.mem_rationalSubset_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) (v : ValuationSpectrum A) : v ∈ rationalSubset Aplus T s ↔ v ∈ spa Aplus ∧ (∀ t ∈ T, t ≤ᵥ s) ∧ ¬s ≤ᵥ 0

Membership in R(T/s): a point of the adic spectrum where every numerator is dominated by the denominator and the denominator is not in the support.

theorem TauCeti.ValuationSpectrum.rationalSubset_subset_spa {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : rationalSubset Aplus T s ⊆ spa Aplus

Every rational subset is contained in the adic spectrum.

theorem TauCeti.ValuationSpectrum.rationalSubset_subset_rationalSubset_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T T' : Finset A) (s s' : A) : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s ↔ ∀ v ∈ rationalSubset Aplus T' s', (∀ t ∈ T, t ≤ᵥ s) ∧ ¬s ≤ᵥ 0

The containment criterion for rational subsets. One rational subset is contained in another exactly when, at every point of the smaller, the larger one's numerators are dominated by its denominator and that denominator is off the support.

Containment in spa A⁺ is automatic on both sides, so it drops out of the criterion: only the T-over-s conditions are left to check. This is the set-level input to Wedhorn's comparison of two presentations (§8.2) — it says which valuation-theoretic facts a containment gives you, leaving the passage from those facts to invertibility of s and power-boundedness of t/s in the coordinate ring as a separate, genuinely algebraic step.

theorem TauCeti.ValuationSpectrum.rationalSubset_subset_rationalSubset_of_subset {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) {T T' : Finset A} (h : T ⊆ T') (s : A) : rationalSubset Aplus T' s ⊆ rationalSubset Aplus T s

Enlarging the numerator set shrinks the rational subset. Each numerator carries one domination condition, so asking for more of them can only cut the subset down. This is the containment that makes Wedhorn's chain of Remark 7.55 descend.

theorem TauCeti.ValuationSpectrum.rationalSubset_mul_subset_rationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) {T T' : Finset A} {s r : A} (hT : ∀ t ∈ T, t * r ∈ T') : rationalSubset Aplus T' (s * r) ⊆ rationalSubset Aplus T s

Refining a presentation shrinks the rational subset. If a cofactor r carries every numerator of T into T', then R(T'/(s · r)) ⊆ R(T/s): at a point of the smaller subset r is off the support, so it cancels from v(t · r) ≤ v(s · r). This is the containment behind a refinement of presentations, whose restriction map goes from A⟨T/s⟩ to A⟨T'/(s · r)⟩.

theorem TauCeti.ValuationSpectrum.rationalSubset_subset_rationalSubset_of_le {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) {p q : P.Presentation} (h : p ≤ q) : rationalSubset Aplus q.num q.den ⊆ rationalSubset Aplus p.num p.den

A refinement of presentations shrinks the rational subset: if q refines p, then R(q) ⊆ R(p).

@[simp]

theorem TauCeti.ValuationSpectrum.rationalSubset_insert_self {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : rationalSubset Aplus (insert s T) s = rationalSubset Aplus T s

Inserting the denominator among the numerators changes nothing — Wedhorn's "one may replace T by T ∪ {s}" (Definition 7.29).

theorem TauCeti.ValuationSpectrum.rationalSubset_union_of_forall_vle {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T T' : Finset A) (s : A) (hT' : ∀ u ∈ T', ∀ v ∈ rationalSubset Aplus T s, u ≤ᵥ s) : rationalSubset Aplus (T ∪ T') s = rationalSubset Aplus T s

Numerators dominated by the denominator may be adjoined for free. If every element of T' is dominated by s at every point of R(T/s), then adjoining all of T' to the numerators leaves the rational subset unchanged.

Only T' is constrained, and only where it has to be: nothing is asked of the ideal T' · A, and the domination is required at the points of R(T/s) alone rather than throughout spa A⁺. The one-numerator case is rationalSubset_insert_of_forall_vle.

theorem TauCeti.ValuationSpectrum.rationalSubset_insert_of_forall_vle {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s u : A) (hu : ∀ v ∈ rationalSubset Aplus T s, u ≤ᵥ s) : rationalSubset Aplus (insert u T) s = rationalSubset Aplus T s

A numerator dominated by the denominator may be adjoined for free. If every point of R(T/s) satisfies v(u) ≤ v(s), then adjoining u to the numerators does not change the rational subset.

This is the step that closes Wedhorn's chain of Remark 7.55 at Xₙ = U: the whole point of choosing u dominated by s on U is that the extra numerator condition it contributes is already satisfied there.

@[simp]

theorem TauCeti.ValuationSpectrum.rationalSubset_image_mul_right {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s u : A) (hu : IsUnit u) : rationalSubset Aplus (Finset.image (fun (t : A) => t * u) T) (s * u) = rationalSubset Aplus T s

Multiplying a presentation by a unit changes nothing. If u is a unit, then multiplying every numerator and the denominator of R(T/s) by u gives the same rational subset.

No injectivity of t ↦ t * u is needed.

@[simp]

theorem TauCeti.ValuationSpectrum.rationalSubset_singleton_one {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) : rationalSubset Aplus {1} 1 = spa Aplus

The whole adic spectrum is the rational subset R({1}/1) — Wedhorn's observation that Spa (A, A⁺) itself is rational. The single condition v(1) ≤ v(1) ≠ 0 holds at every point.

@[simp]

theorem TauCeti.ValuationSpectrum.val_preimage_rationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : Subtype.val ⁻¹' rationalSubset Aplus T s = Subtype.val ⁻¹' basicOpenFinset T s

On the subtype spa A⁺, the preimage of R(T/s) is the preimage of the ambient basic open Spv(A)(T/s): the spa A⁺ condition is automatic from the subtype. This is the form used to compare the rational bases of Spa(A,A⁺) and Spv(A,I).

theorem TauCeti.ValuationSpectrum.isOpen_val_preimage_rationalSubset {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : IsOpen (Subtype.val ⁻¹' rationalSubset Aplus T s)

The preimage of R(T/s) under the coercion of the subtype spa A⁺ is open: a rational subset is relatively open in the adic spectrum.

def TauCeti.ValuationSpectrum.spaBasicOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (s : A) : TopologicalSpace.Opens ↑(spa Aplus)

The basic open R(T/s), as an Opens of spa A⁺. This packages rationalSubset with its openness; it is a rational subset in Wedhorn's sense exactly when Ideal.span (T : Set A) is open, which is not assumed here.

Equations

• TauCeti.ValuationSpectrum.spaBasicOpen Aplus T s = { carrier := Subtype.val ⁻¹' TauCeti.ValuationSpectrum.rationalSubset Aplus T s, is_open' := ⋯ }

@[simp]

theorem TauCeti.ValuationSpectrum.mem_spaBasicOpen {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {T : Finset A} {s : A} {v : ↑(spa Aplus)} : v ∈ spaBasicOpen Aplus T s ↔ ↑v ∈ rationalSubset Aplus T s

Membership in spaBasicOpen is membership in the underlying rationalSubset.

theorem TauCeti.ValuationSpectrum.spaBasicOpen_le_spaBasicOpen_iff {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {T T' : Finset A} {s s' : A} : spaBasicOpen Aplus T' s' ≤ spaBasicOpen Aplus T s ↔ rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s

Containment of basic opens is containment of the underlying rational subsets, since every rational subset already lies in spa A⁺.

theorem TauCeti.ValuationSpectrum.rationalSubset_eq_of_spaBasicOpen_eq {A : Type u_1} [CommRing A] [TopologicalSpace A] {Aplus : Subring A} {T T' : Finset A} {s s' : A} (h : spaBasicOpen Aplus T s = spaBasicOpen Aplus T' s') : rationalSubset Aplus T s = rationalSubset Aplus T' s'

Equal basic opens have equal rational subsets: the presentation data (T, s) is not determined by the subset it presents, but the subset is determined by the basic open, by antisymmetry of spaBasicOpen_le_spaBasicOpen_iff.

@[simp]

theorem TauCeti.ValuationSpectrum.rationalSubset_inter {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T₁ T₂ : Finset A) (s₁ s₂ : A) : rationalSubset Aplus T₁ s₁ ∩ rationalSubset Aplus T₂ s₂ = rationalSubset Aplus (insert s₁ T₁ * insert s₂ T₂) (s₁ * s₂)

The set-level half of Wedhorn Remark 7.30(5): writing Uᵢ = insert sᵢ Tᵢ for each numerator set augmented by its own denominator, R(T₁/s₁) ∩ R(T₂/s₂) = R(U₁U₂ / s₁s₂). The augmentation costs nothing (rationalSubset_insert_self) and is essential — with the bare products the identity fails for T₂ = ∅. Wedhorn's full Remark 7.30(5) additionally says the right-hand pair is again admissible; that is TauCeti.Huber.PairOfDefinition.isOpen_span_insert_mul_insert, which needs the open-ideal criterion and so lives downstream of this file. This identity is the form Theorem 7.35's own proof consumes.

theorem TauCeti.ValuationSpectrum.spaBasicOpen_commonRefinement {A : Type u_1} [CommRing A] [TopologicalSpace A] {P : Huber.PairOfDefinition A} (Aplus : Subring A) (p q : P.Presentation) : spaBasicOpen Aplus (p.commonRefinement q).num (p.commonRefinement q).den = spaBasicOpen Aplus p.num p.den ⊓ spaBasicOpen Aplus q.num q.den

The rational open of the common refinement of two presentations is their intersection.

theorem TauCeti.ValuationSpectrum.rationalSubset_eq_biInter_singleton {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T : Finset A) (hT : T.Nonempty) (s : A) : rationalSubset Aplus T s = ⋂ t ∈ T, rationalSubset Aplus {t} s

A rational subset is the intersection of its one-numerator pieces: R(T/s) = ⋂ t ∈ T, R({t}/s) for nonempty T. This is the finite-family companion of rationalSubset_inter, and it unfolds directly from Definition 7.29 — a point dominates every numerator by s exactly when it dominates each one separately. It is the decomposition that a refinement to a standard rational cover consumes.

Nonemptiness of T cannot be dropped. Each R({t}/s) carries the ambient spa A⁺ condition and the requirement that the denominator be off the support, alongside its own numerator condition, so some member of the family is what transports those two to the left-hand side. For T = ∅ the left-hand side is still cut out inside spa A⁺ while the empty intersection is everything, so the two sides need not agree. (They can still coincide: if Spv A is empty — as it is over the zero ring — both sides are empty.)

Deliberately not @[simp]: the right-hand side is again a rational subset over a singleton, which matches the left-hand pattern, so the rewrite re-fires on each factor instead of terminating.

Re-presenting a contained rational subset

theorem TauCeti.ValuationSpectrum.exists_refinement_of_subset {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (T T' : Finset A) (s s' : A) (h : rationalSubset Aplus T' s' ⊆ rationalSubset Aplus T s) : ∃ (T'' : Finset A), rationalSubset Aplus T' s' = rationalSubset Aplus T'' (s * s') ∧ (∀ t ∈ T, t * s' ∈ T'') ∧ ∀ t' ∈ T', t' * s ∈ T''

A containment of rational subsets yields a presentation of the smaller one over the product denominator. If R(T'/s') ⊆ R(T/s) then R(T'/s') has a presentation R(T''/(s · s')) whose numerators contain t · s' for every t ∈ T and t' · s for every t' ∈ T'.

The denominator is the point: it is divisible by s, so in a localisation presented by this pair s is invertible by construction, and each numerator condition makes the fractions of one of the two original presentations distinguished fractions of the new one. Those are the set-level inputs a restriction map A⟨T/s⟩ → A⟨T''/(s · s')⟩ is built from, and this is the re-presentation step of Wedhorn §8.2.

They are not by themselves enough to construct that map. A presentation also carries the standing hypothesis HasDenominatorPower for the new pair, an algebraic obligation about the ideal of definition that this file does not supply — nothing here mentions coordinate rings at all.

Both numerator conditions are given rather than only the one for T, because discharging that standing hypothesis for a product denominator needs the fractions of each factor; a consumer holding one alone could not use it.

theorem TauCeti.ValuationSpectrum.mem_rationalSubset_of_span_eq_top_of_mem_spa {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) {T : Finset A} (hT : Ideal.span ↑T = ⊤) {v : ValuationSpectrum A} (hv : v ∈ spa Aplus) : ∃ s ∈ T, v ∈ rationalSubset Aplus T s

Generalization of the pointwise forward implication of Wedhorn Corollary 7.53 (which assumes a complete Hausdorff affinoid ring): for an arbitrary commutative ring A and subring A⁺, if T generates the unit ideal of A, then every point v ∈ spa Aplus belongs to the standard rational subset R(T/s) for some s ∈ T.

theorem TauCeti.ValuationSpectrum.spa_eq_biUnion_rationalSubset_of_span_eq_top {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) {T : Finset A} (hT : Ideal.span ↑T = ⊤) : spa Aplus = ⋃ t ∈ T, rationalSubset Aplus T t

Generalization of the forward implication of Wedhorn Corollary 7.53 (which assumes a complete Hausdorff affinoid ring): for an arbitrary commutative ring A and subring A⁺, if a finite set T generates the unit ideal of A, then the standard rational subsets (R(T/t))_{t ∈ T} cover spa Aplus.

theorem TauCeti.ValuationSpectrum.span_eq_top_iff_forall_mem_spa_exists_not_vle_zero {A : Type u_1} [CommRing A] [TopologicalSpace A] (Aplus : Subring A) (hmax : ∀ (𝔪 : Ideal A), 𝔪.IsMaximal → IsOpen ↑𝔪) {T : Finset A} : Ideal.span ↑T = ⊤ ↔ ∀ v ∈ spa Aplus, ∃ t ∈ T, ¬t ≤ᵥ 0

Wedhorn Corollary 7.53. A finite set T generates the unit ideal exactly when no point of Spa(A, A⁺) vanishes on all of it. Combined with spa_eq_biUnion_rationalSubset_of_span_eq_top, this is what makes the standard family (R(T/t))_{t ∈ T} an open covering rather than merely a family.

Wedhorn assumes a complete affinoid ring, where every maximal ideal is open. Here that is the explicit hypothesis hmax, and only the ← direction uses it: the forward direction is mem_rationalSubset_of_span_eq_top_of_mem_spa, which holds over an arbitrary commutative ring. A consumer who has Ideal.span T = ⊤ and wants the cover should use that lemma directly rather than this iff, so as not to acquire hmax for nothing.