The points of the closed unit disc

Let K be an algebraically closed complete nontrivially normed nonarchimedean field and X = Spa (K⟨T⟩, K⟨T⟩°) the closed unit disc. Wedhorn's Example 7.57 sorts the points of X into five types. This file recognises the points of types (2), (3) and (5) among all points of X, and proves that every point of X is of one of the five types.

The points of types (2) and (3) are the Gauss points η_{a,r} of the discs D(a, r) = {y : ‖y - a‖ ≤ r} (TauCeti.ValuationSpectrum.discPoint). Next to each η_{a,r} sit the refined Gauss points η_{a,r⁺} and η_{a,r⁻} (TauCeti.ValuationSpectrum.discPointAbove, TauCeti.ValuationSpectrum.discPointBelow). For r ∈ |Kˣ| these are the rank-two points of type (5); for other radii they need not differ from η_{a,r}. This file characterises each of η_{a,r}, η_{a,r⁺} and η_{a,r⁻}, for every radius, among all points of X by the position of x(T - a) relative to the constants.

A point x is η_{a,r} exactly when

• x(T - a) ≤ x(T - b) for every b ∈ D(a, r), so a minimises b ↦ x(T - b) on the disc, and
• x(T - a) sits at r relative to the constants: x(T - a) ≤ x(c) exactly when r ≤ ‖c‖, and x(c) ≤ x(T - a) exactly when ‖c‖ ≤ r.

The second condition says that x(T - a) has the same position in the value group of x as the real number r among the norms of K. The first condition fails for the point η_{b,s} with s < r = ‖b - a‖, whose value on T - a is again r.

A point x is η_{a,r⁺} exactly when x(T - a) ≤ x(c) holds for precisely the constants with r < ‖c‖, and η_{a,r⁻} exactly when x(c) ≤ x(T - a) holds for precisely the constants with ‖c‖ < r. So x(T - a) lies infinitesimally above, respectively below, the constants of norm r. Since the norms of K are dense, these conditions make x(T - a) strictly larger or strictly smaller than every x(c), and no minimality condition is needed: x(T - b) is then x(T - a) or x(b - a) by the ultrametric equality.

All three characterisations rest on one comparison. Suppose two points x and y compare T - a with every constant in the same way, x(T - a) and y(T - a) are nonzero, and there is a set P of centres with x(T - b) = x(T - a) for b ∈ P and x(T - b) = x(b - a) otherwise, and likewise for y. Over an algebraically closed field every polynomial is a constant times a product of linear factors T - b, so x and y take the values x(c) x(T - a)^m and y(c) y(T - a)^m on it, for the same c and m. Taking m-th roots in K shows that x and y compare these values in the same way. Polynomials are dense in K⟨T⟩ (TauCeti.Huber.denseRange_eval₂RingHom_weightedX) and both points are continuous with trivial support, so x = y (Valuation.IsContinuous.isEquiv_of_dense). Trivial support holds because a point with nonzero support kills some T - b (TauCeti.ValuationSpectrum.exists_weightedX_sub_weightedC_mem_supp).

To see that the five types exhaust X, recall that a point with nonzero support is classical, of type (1) (TauCeti.ValuationSpectrum.supp_ne_bot_iff_exists_eq_classicalPoint). For a point x with trivial support and a centre b of the disc, let ρ(b) be the infimum of the norms of the constants c with x(T - b) ≤ x(c): so x(T - b) lies above the constants of norm less than ρ(b) and below those of norm greater than ρ(b). It is positive because x is continuous and does not vanish on T - b, and the ultrametric inequality gives ρ(b) ≤ max(ρ(b'), ‖b - b'‖). If ρ(b') < ρ(b) then x(T - b) = x(b - b'), so ρ(b) = ‖b - b'‖.

• If ρ attains its infimum r at a centre a, compare x(T - a) with the constants of norm r. If there are none, or x(T - a) equals their value, x = η_{a,r}, unless some x(T - b) with ‖b - a‖ ≤ r is smaller; such an x(T - b) lies just below the constants of norm r, and x = η_{b,r⁻}. If x(T - a) lies strictly below or above them, x = η_{a,r⁻} or η_{a,r⁺}.
• Otherwise choose centres aₙ along which ρ decreases strictly to its infimum. The discs D(aₙ, ρ(aₙ)) decrease, have radius ρ(aₙ) = ‖aₙ - aₙ₊₁‖, and have no common point in K, since every centre b has ρ(b) > ρ(aₙ) for some n. On T - b both x and the point attached to these discs take the value of the constant b - aₙ, so they are equal.

Main results

• TauCeti.ValuationSpectrum.eq_discPoint_iff: a point of the closed unit disc over an algebraically closed field is η_{a,r} if and only if it satisfies the two conditions above.
• TauCeti.ValuationSpectrum.eq_discPointAbove_iff and TauCeti.ValuationSpectrum.eq_discPointBelow_iff: it is η_{a,r⁺}, respectively η_{a,r⁻}, if and only if x(T - a) lies just above, respectively just below, the constants of norm r.
• TauCeti.ValuationSpectrum.forall_lt_and_forall_gt_of_vle_weightedC and TauCeti.ValuationSpectrum.forall_lt_and_forall_gt_of_weightedC_vle: in that case x(T - a) is strictly larger or strictly smaller than the value of every constant.
• exists_eq_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint, in the namespace TauCeti.ValuationSpectrum: a point with trivial support is of type (2), (3), (4) or (5).
• exists_eq_classicalPoint_or_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint: every point of the closed unit disc is of one of the five types.
• TauCeti.ValuationSpectrum.eq_of_forall_valuation_weightedX_sub_weightedC_eq: two points that take the value of one and the same nonzero constant on every T - b are equal.

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 classification of the rank-one points by nested discs, which the argument above follows.
• P. Scholze, Perfectoid spaces, Publ. Math. IHÉS 116 (2012), Example 2.20.

Values on the linear polynomials

Two points that compare T - a with the constants in the same way

theorem TauCeti.ValuationSpectrum.forall_lt_and_forall_gt_of_vle_weightedC {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] {r : ℝ} [IsUltrametricDist K] [IsAlgClosed K] {x : ↑(closedPolydisc 1 K)} {a : K} (hr₀ : 0 < r) (h : ∀ (c : K), Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ≤ᵥ (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ↔ r < ‖c‖) : (∀ (c : K), ‖c‖ ≤ r → (↑x).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c) < (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a)) ∧ ∀ (c : K), ¬‖c‖ ≤ r → (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a) < (↑x).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c)

If x(T - a) ≤ x(c) holds for exactly the constants with r < ‖c‖, then x(T - a) is strictly larger than the values of the constants with ‖c‖ ≤ r and strictly smaller than the values of the others, because the norms of K are dense.

theorem TauCeti.ValuationSpectrum.forall_lt_and_forall_gt_of_weightedC_vle {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] {r : ℝ} [IsUltrametricDist K] [IsAlgClosed K] {x : ↑(closedPolydisc 1 K)} {a : K} (h : ∀ (c : K), (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ≤ᵥ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ↔ ‖c‖ < r) : (∀ (c : K), ‖c‖ < r → (↑x).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c) < (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a)) ∧ ∀ (c : K), ¬‖c‖ < r → (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a) < (↑x).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c)

If x(c) ≤ x(T - a) holds for exactly the constants with ‖c‖ < r, then x(T - a) is strictly larger than the values of the constants with ‖c‖ < r and strictly smaller than the values of the others, because the norms of K are dense.

The radius of a point about a centre

Equality of two points that compare T - a with the constants in the same way

Two points that take the value of a constant on every T - b

theorem TauCeti.ValuationSpectrum.eq_of_forall_valuation_weightedX_sub_weightedC_eq {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] {x y : ↑(closedPolydisc 1 K)} (h : ∀ (b : K), ∃ (e : K), e ≠ 0 ∧ (↑x).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b) = (↑x).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) e) ∧ (↑y).valuation (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b) = (↑y).valuation ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) e)) : x = y

Two points of the closed unit disc that take the value of one and the same nonzero constant on every T - b are equal, over an algebraically closed field. Both then have trivial support and compare polynomials as the norm compares constants, and polynomials are dense.

The characterisations

theorem TauCeti.ValuationSpectrum.eq_discPoint_iff {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] {r : ℝ} [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] (x : ↑(closedPolydisc 1 K)) {a : K} (ha : ‖a‖ ≤ 1) (hr₀ : 0 < r) (hr₁ : r ≤ 1) : x = discPoint a ha hr₀ hr₁ ↔ (∀ (b : K), ‖b - a‖ ≤ r → Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ≤ᵥ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b) ∧ (∀ (c : K), Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ≤ᵥ (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ↔ r ≤ ‖c‖) ∧ ∀ (c : K), (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ≤ᵥ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ↔ ‖c‖ ≤ r

The points η_{a,r} among the points of the closed unit disc, over an algebraically closed complete nonarchimedean field: a point x is η_{a,r} if and only if x(T - a) ≤ x(T - b) for every b with ‖b - a‖ ≤ r, and x(T - a) compares with the constants as r compares with their norms. These are the points of types (2) and (3) in Wedhorn's Example 7.57.

theorem TauCeti.ValuationSpectrum.eq_discPointAbove_iff {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] {r : ℝ} [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] (x : ↑(closedPolydisc 1 K)) {a : K} (ha : ‖a‖ ≤ 1) (hr₀ : 0 < r) (hr₁ : r < 1) : x = discPointAbove a ha hr₀ hr₁ ↔ ∀ (c : K), Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ≤ᵥ (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ↔ r < ‖c‖

The points η_{a,r⁺} among the points of the closed unit disc, over an algebraically closed complete nonarchimedean field: a point x is η_{a,r⁺} if and only if x(T - a) ≤ x(c) holds for exactly the constants c with r < ‖c‖, so that x(T - a) lies just above the constants of norm r. For r the norm of an element of K these are the points of type (5) written a_{>r} in Wedhorn's Example 7.57.

theorem TauCeti.ValuationSpectrum.eq_discPointBelow_iff {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] {r : ℝ} [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] (x : ↑(closedPolydisc 1 K)) {a : K} (ha : ‖a‖ ≤ 1) (hr₀ : 0 < r) (hr₁ : r ≤ 1) : x = discPointBelow a ha hr₀ hr₁ ↔ ∀ (c : K), (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) c ≤ᵥ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ↔ ‖c‖ < r

The points η_{a,r⁻} among the points of the closed unit disc, over an algebraically closed complete nonarchimedean field: a point x is η_{a,r⁻} if and only if x(c) ≤ x(T - a) holds for exactly the constants c with ‖c‖ < r, so that x(T - a) lies just below the constants of norm r. For r the norm of an element of K these are the points of type (5) written a_{<r} in Wedhorn's Example 7.57.

Every point of the disc is of one of the five types

Recognising points of type (4)

theorem TauCeti.ValuationSpectrum.eq_nestedDiscPoint_iff {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] [IsUltrametricDist K] [CompleteSpace K] {a c : ℕ → K} (ha : ∀ (n : ℕ), ‖a n‖ ≤ 1) (hc₀ : ∀ (n : ℕ), c n ≠ 0) (hc₁ : ∀ (n : ℕ), ‖c n‖ ≤ 1) (hac : ∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) (hcc : ∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖) [IsAlgClosed K] (hempty : ∀ (b : K), ∃ (n : ℕ), ‖c n‖ < ‖b - a n‖) (x : ↑(closedPolydisc 1 K)) : x = nestedDiscPoint a ha c hc₀ hc₁ hac hcc ↔ ∀ (n : ℕ), x ∈ closedSubdisc (a n) (c n)

With no common point of the discs in K, the point is the only point lying in all of them, over an algebraically closed field: a point x of the closed unit disc is η if and only if x ∈ D(aₙ, |cₙ|) for every n. These are the points of type (4) in Wedhorn's Example 7.57.

Points without a minimum on linear polynomials

theorem TauCeti.ValuationSpectrum.exists_eq_nestedDiscPoint_iff {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] (x : ↑(closedPolydisc 1 K)) : (∃ (a : ℕ → K) (ha : ∀ (n : ℕ), ‖a n‖ ≤ 1) (c : ℕ → K) (hc₀ : ∀ (n : ℕ), c n ≠ 0) (hc₁ : ∀ (n : ℕ), ‖c n‖ ≤ 1) (hac : ∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) (hcc : ∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖), (∀ (b : K), ∃ (n : ℕ), ‖c n‖ < ‖b - a n‖) ∧ x = nestedDiscPoint a ha c hc₀ hc₁ hac hcc) ↔ ¬∃ (a₀ : K), ∀ (b : K), Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a₀ ≤ᵥ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) b

The points of type (4) of the closed unit disc, over an algebraically closed complete nonarchimedean field: a point x is the point attached to a decreasing sequence of discs with no common point in K if and only if b ↦ x(T - b) attains no minimum.

theorem TauCeti.ValuationSpectrum.exists_eq_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] (x : ↑(closedPolydisc 1 K)) (hx : (↑x).supp = ⊥) : (∃ (a : K) (ha : ‖a‖ ≤ 1) (r : ℝ) (hr₀ : 0 < r) (hr₁ : r ≤ 1), x = discPoint a ha hr₀ hr₁) ∨ (∃ (a : K) (ha : ‖a‖ ≤ 1) (c : K) (hc₀ : 0 < ‖c‖) (hc₁ : ‖c‖ < 1), x = discPointAbove a ha hc₀ hc₁) ∨ (∃ (a : K) (ha : ‖a‖ ≤ 1) (c : K) (hc₀ : 0 < ‖c‖) (hc₁ : ‖c‖ ≤ 1), x = discPointBelow a ha hc₀ hc₁) ∨ ∃ (a : ℕ → K) (ha : ∀ (n : ℕ), ‖a n‖ ≤ 1) (c : ℕ → K) (hc₀ : ∀ (n : ℕ), c n ≠ 0) (hc₁ : ∀ (n : ℕ), ‖c n‖ ≤ 1) (hac : ∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) (hcc : ∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖), (∀ (b : K), ∃ (n : ℕ), ‖c n‖ < ‖b - a n‖) ∧ x = nestedDiscPoint a ha c hc₀ hc₁ hac hcc

The points of the closed unit disc with trivial support, over an algebraically closed complete nonarchimedean field: every such point is one of

• a point η_{a,r} (types (2) and (3) in Wedhorn's Example 7.57);
• a rank-two point η_{a,r⁺} or η_{a,r⁻} with r the norm of an element of K (type (5));
• the point attached to a decreasing sequence of discs D(aₙ, |cₙ|) with no common point in K (type (4)).

theorem TauCeti.ValuationSpectrum.exists_eq_classicalPoint_or_discPoint_or_discPointAbove_or_discPointBelow_or_nestedDiscPoint {K : Type u_1} [NontriviallyNormedField K] [NonarchimedeanRing K] [IsUltrametricDist K] [CompleteSpace K] [IsAlgClosed K] (x : ↑(closedPolydisc 1 K)) : (∃ (y : ↑(spa (Huber.powerBoundedSubring K))) (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)), x = classicalPoint y a ha) ∨ (∃ (a : K) (ha : ‖a‖ ≤ 1) (r : ℝ) (hr₀ : 0 < r) (hr₁ : r ≤ 1), x = discPoint a ha hr₀ hr₁) ∨ (∃ (a : K) (ha : ‖a‖ ≤ 1) (c : K) (hc₀ : 0 < ‖c‖) (hc₁ : ‖c‖ < 1), x = discPointAbove a ha hc₀ hc₁) ∨ (∃ (a : K) (ha : ‖a‖ ≤ 1) (c : K) (hc₀ : 0 < ‖c‖) (hc₁ : ‖c‖ ≤ 1), x = discPointBelow a ha hc₀ hc₁) ∨ ∃ (a : ℕ → K) (ha : ∀ (n : ℕ), ‖a n‖ ≤ 1) (c : ℕ → K) (hc₀ : ∀ (n : ℕ), c n ≠ 0) (hc₁ : ∀ (n : ℕ), ‖c n‖ ≤ 1) (hac : ∀ (n : ℕ), ‖a (n + 1) - a n‖ ≤ ‖c n‖) (hcc : ∀ (n : ℕ), ‖c (n + 1)‖ ≤ ‖c n‖), (∀ (b : K), ∃ (n : ℕ), ‖c n‖ < ‖b - a n‖) ∧ x = nestedDiscPoint a ha c hc₀ hc₁ hac hcc

Every point of the closed unit disc is of one of Wedhorn's five types, over an algebraically closed complete nonarchimedean field (Example 7.57): a classical point x_a (type (1)), a point η_{a,r} (types (2) and (3)), the point attached to a decreasing sequence of discs D(aₙ, |cₙ|) with no common point in K (type (4)), or a rank-two point η_{a,r⁺} or η_{a,r⁻} with r the norm of an element of K (type (5)).