Points of the closed unit disc attached to decreasing sequences of discs #
Let K be a complete nontrivially normed nonarchimedean field and K⟨T⟩ the coordinate ring of
the closed unit disc closedPolydisc 1 K. A decreasing sequence of closed discs in the unit disc
D(a₀, |c₀|) ⊇ D(a₁, |c₁|) ⊇ D(a₂, |c₂|) ⊇ ⋯, ‖aₙ₊₁ - aₙ‖ ≤ ‖cₙ‖, ‖cₙ₊₁‖ ≤ ‖cₙ‖,
gives a point η of the disc, the limit of the Gauss norms of the discs:
η : f ↦ inf_n |f|_{D(aₙ, |cₙ|)} = lim_n |f|_{D(aₙ, |cₙ|)}.
When K is algebraically closed and the discs have no common point in K, these are the points
of type (4) in Wedhorn's description of the closed unit disc (Example 7.57). Decreasing sequences
of discs with no common point exist exactly when K is not spherically complete. This is the case
for every algebraically closed separable K, such as ℂ_p: its norms decrease strictly to a
positive limit along a sequence, and discs with these radii can avoid the points of a dense
sequence one at a time. The comparisons with the other points hold over every complete K;
recognising η among all points needs K to be algebraically closed.
The Gauss norms of f on the discs decrease, since the Gauss norm of radius r is unchanged by
moving the centre within the disc of radius r and increases with the radius. A decreasing limit
of multiplicative ultrametric norms is again one, so η is a valuation with values in ℝ≥0. It is
bounded by the Gauss norm of the whole disc, which makes it continuous and at most one on
power-bounded elements.
The point η lies in a disc D(b, |d|) exactly when d ≠ 0 and
inf_n max(‖cₙ‖, ‖aₙ - b‖) ≤ ‖d‖; in particular it lies in every D(aₙ, |cₙ|). This determines
how it relates to the other points of the disc.
- If the discs have a common point
b ∈ Kand their radii have a positive infimumρ, thenηis the pointη_{b,ρ}of the discD(b, ρ), andηis a pointη_{b,s}in no other case. - If the discs have no common point in
K, thenηis not a classical point (type (1)), not a pointη_{b,s}(types (2) and (3)), and not one of the rank-two pointsη_{b,s⁻}andη_{b,s⁺}(type (5)).
If the discs have no common point in K, then for every b some disc D(aₙ, |cₙ|) avoids b,
and every point x of that disc takes the value x(aₙ - b) of a constant on T - b. So
b ↦ η(T - b) attains no minimum, and, over an algebraically closed K, η is the only point
lying in every disc: two points that take the value of one nonzero constant on each T - b agree
on polynomials, which split into linear factors, and polynomials are dense. Conversely, if
b ↦ x(T - b) attains no minimum, then every value x(T - b) is the value x(e) of a constant,
the norms ‖e‖ have an infimum which is not attained, and the discs D(b, |e|) along a sequence
of norms decreasing to it have no common point and contain x. So the points of type (4) are
exactly the points at which b ↦ x(T - b) attains no minimum.
The support of η is not computed here, and the points at which b ↦ x(T - b) attains a minimum
are not sorted into Wedhorn's types here.
The complete five-type classification is proved in
TauCeti.AlgebraicGeometry.AdicSpace.Spa.Polydisc.Classification.
Main definitions #
TauCeti.ValuationSpectrum.nestedDiscValuation: the infimum of the Gauss norms on a decreasing sequence of discs, as a valuation onK⟨T⟩with values inℝ≥0.TauCeti.ValuationSpectrum.nestedDiscPoint: the corresponding point of the closed unit disc.
Main results #
TauCeti.ValuationSpectrum.tendsto_nestedDiscValuation: the Gauss norms offon the discs tend toη(f).TauCeti.ValuationSpectrum.nestedDiscPoint_mem_closedSubdisc_iff:ηlies inD(b, |d|)exactly whend ≠ 0andinf_n max(‖cₙ‖, ‖aₙ - b‖) ≤ ‖d‖; in particularTauCeti.ValuationSpectrum.nestedDiscPoint_mem_closedSubdisc,ηlies in everyD(aₙ, |cₙ|).TauCeti.ValuationSpectrum.mem_closedSubdisc_of_nestedDiscPoint_specializes: when the discs have no common point inK, every specialization ofηlies in every defining disc.TauCeti.ValuationSpectrum.nestedDiscPoint_eq_discPoint_iff:η = η_{b,s}exactly whenblies in every disc andsis the infimum of the radii.TauCeti.ValuationSpectrum.nestedDiscPoint_ne_classicalPoint,TauCeti.ValuationSpectrum.nestedDiscPoint_ne_discPoint,TauCeti.ValuationSpectrum.nestedDiscPoint_ne_discPointBelowandTauCeti.ValuationSpectrum.nestedDiscPoint_ne_discPointAbove: when the discs have no common point inK,ηis none of the points of types (1), (2), (3), or (5).TauCeti.ValuationSpectrum.not_exists_forall_nestedDiscPoint_vle: when the discs have no common point inK,b ↦ η(T - b)attains no minimum. The recognition theorems below live inPolydisc.Classification:TauCeti.ValuationSpectrum.eq_nestedDiscPoint_iff: over an algebraically closedK, when the discs have no common point,ηis the only point lying in everyD(aₙ, |cₙ|).TauCeti.ValuationSpectrum.exists_eq_nestedDiscPoint_iff: over an algebraically closedK, the points of type (4) are exactly the pointsxat whichb ↦ x(T - b)attains no minimum.TauCeti.ValuationSpectrum.exists_seq_forall_exists_lt_norm_sub: over an algebraically closed separableK, such asℂ_p, there is a decreasing sequence of discs with no common point.exists_forall_ne_classicalPoint_discPoint_discPointAbove_discPointBelow, in the namespaceTauCeti.ValuationSpectrum: hence the closed unit disc over suchKhas a point of type (4), one that is not of types (1), (2), (3), or (5).
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 7.57.
- V. G. Berkovich, Spectral theory and analytic geometry over non-Archimedean fields, Mathematical Surveys and Monographs 33, AMS, 1990, §1.4.4, for the points attached to decreasing sequences of discs.
- P. Scholze, Perfectoid spaces, Publ. Math. IHÉS 116 (2012), Example 2.20.
- A. M. Robert, A Course in p-adic Analysis, Graduate Texts in Mathematics 198, Springer, 2000,
Chapter 3, for the separability of
ℂ_pand its failure to be spherically complete.
The valuation #
The valuation of a decreasing sequence of discs D(aₙ, |cₙ|) in the closed unit disc:
f ↦ inf_n |f|_{D(aₙ, |cₙ|)}, the infimum of the Gauss norms of radius ‖cₙ‖ about aₙ. The
hypotheses ‖aₙ₊₁ - aₙ‖ ≤ ‖cₙ‖ and ‖cₙ₊₁‖ ≤ ‖cₙ‖ say that the discs decrease, which makes the
infimum a limit and hence multiplicative.
Instances For
The valuation of the discs is the infimum of the Gauss norms of radius ‖cₙ‖ about aₙ.
The Gauss norms of f on the discs tend to its valuation.
The valuation of the discs takes the value ‖x‖ on the constant x.
The valuation of the discs takes the value inf_n max(‖cₙ‖, ‖aₙ - b‖) on T - b.
The valuation of the discs is continuous, since it is bounded by the Gauss norm of the whole disc.
The valuation of the discs is at most one on power-bounded elements of K⟨T⟩.
The point #
The point of the closed unit disc attached to a decreasing sequence of discs
D(aₙ, |cₙ|): the point of Spa (K⟨T⟩, K⟨T⟩°) given by f ↦ inf_n |f|_{D(aₙ, |cₙ|)}. When K
is algebraically closed and the discs have no common point in K, it is a point of type (4).
Instances For
The underlying point in Spv K⟨T⟩ is defined by the valuation of the discs.
The point compares two series by the valuation of the discs.
The point lies in D(b, |d|) exactly when inf_n max(‖cₙ‖, ‖aₙ - b‖) ≤ ‖d‖ and
d ≠ 0.
The point lies in every disc D(aₙ, |cₙ|) of the sequence.
Every specialization of a nested-disc point with no common field-valued centre remains in every defining disc.
Comparison with the other points of the disc #
The point is the point η_{b,s} of the disc D(b, s) exactly when b lies in every disc
D(aₙ, |cₙ|) and s is the infimum of their radii.
With no common point of the discs in K, the point is not a point η_{b,s} (types (2) and
(3)).
With no common point of the discs in K, the point is not classical (type (1)): a
classical point x_b lies only in the discs containing b.
With no common point of the discs in K, the point is not a rank-two point η_{b,r⁻}
just below a point η_{b,r} (type (5)).
With no common point of the discs in K, the point is not a rank-two point η_{b,r⁺}
just above a point η_{b,r} (type (5)).
Existence of points of type (4) #
Decreasing sequences of discs with no common point exist over an algebraically closed
separable field K, such as ℂ_p (PadicComplex.separableSpace): there are discs
D(aₙ, |cₙ|) in the closed unit disc satisfying the hypotheses of nestedDiscPoint such that
every b ∈ K lies outside one of them. In other words, K is not spherically complete. This
specialises IsUltrametricDist.exists_antitone_closedBall_iInter_eq_empty to the unit disc.
The closed unit disc over an algebraically closed separable field has points of type (4),
for instance over ℂ_p: there is a point that is not classical (type (1)), not a point η_{b,s}
(types (2) and (3)), and not a rank-two point η_{b,s⁺} or η_{b,s⁻} (type (5)). It is the point
of a decreasing sequence of discs with no common point (exists_seq_forall_exists_lt_norm_sub).
Recognising the point #
With no common point of the discs in K, b ↦ η(T - b) attains no minimum: if the disc
D(aₙ, |cₙ|) avoids a, then η(T - aₙ) ≤ ‖cₙ‖ < ‖aₙ - a‖ = η(T - a).