Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.Polydisc.ClassicalPoint

The points of the closed unit disc with nonzero support #

Let K be a complete nonarchimedean normed field and K⟨T⟩ the coordinate ring of the closed unit disc closedPolydisc 1 K. The points of the disc fall into two kinds according to their support. A point with trivial support is not classical (TauCeti.ValuationSpectrum.ne_classicalPoint_of_supp_eq_bot). This file shows that, when K is algebraically closed, every point with nonzero support is a classical point x_a : f ↦ |f(a)| for some a with ‖a‖ ≤ 1. These are the points of type (1) in Wedhorn's description of the closed unit disc (Example 7.57). The points of his other types (2) to (5) have trivial support; they are not classified here.

The algebraic input is the remainder theorem in K⟨T⟩: for ‖a‖ ≤ 1, T - a divides f - f(a) for every f, so the kernel of evaluation at a is the ideal generated by T - a. This is Weierstrass division by T - a, which is distinguished of degree 1 at the unit radius. It follows that a point whose support contains T - a compares two series as the norm compares their values at a, which is how the classical point at a compares them.

For the classification, a nonzero prime ideal of K⟨T⟩ is generated by a monic polynomial (Weierstrass preparation). Over an algebraically closed field that polynomial is a product of linear factors, one of which, T - a, lies in the support. The bound ‖a‖ ≤ 1 comes from the point itself: it is at most one on T, and it gives T and a the same value. Without algebraic closedness the monic generator need not have a root in K, and the points with nonzero support correspond to the closed points of Spec K⟨T⟩, which need not be K-rational.

Main results #

References #

source
theorem TauCeti.ValuationSpectrum.weightedX_sub_weightedC_dvd_sub_weightedC_evalAtHom {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)) (f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) :
Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) (a 0) ∣ f - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) ((evalAtHom a ha) f)

The remainder theorem in K⟨T⟩. For a in the closed unit disc (power-bounded, that is ‖a‖ ≤ 1), T - a divides f - f(a) for every restricted power series f in one variable over a complete nonarchimedean field. This is the analogue of Mathlib's Polynomial.X_sub_C_dvd_sub_C_eval.

source
theorem TauCeti.ValuationSpectrum.ker_evalAtHom_eq_span_weightedX_sub_weightedC {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)) :
RingHom.ker (evalAtHom a ha) = Ideal.span {Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) (a 0)}

The kernel of evaluation at a is generated by T - a in the coordinate ring K⟨T⟩ of the closed unit disc over a complete nonarchimedean field. This is the analogue of Mathlib's Polynomial.ker_evalRingHom.

source
theorem TauCeti.ValuationSpectrum.supp_classicalPoint_eq_span_weightedX_sub_weightedC {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (x : ↑(spa (Huber.powerBoundedSubring K))) (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)) :
(↑(classicalPoint x a ha)).supp = Ideal.span {Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) (a 0)}

The support of the classical point at a is generated by T - a, for every point x of Spa (K, K°) over a complete nonarchimedean field.

source
theorem TauCeti.ValuationSpectrum.eq_classicalPoint_of_weightedX_sub_weightedC_mem_supp {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (v : ↑(closedPolydisc 1 K)) (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)) (hv : Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) (a 0) ∈ (↑v).supp) (x : ↑(spa (Huber.powerBoundedSubring K))) :
v = classicalPoint x a ha

A point of the closed unit disc whose support contains T - a is the classical point at a, built from any point x of Spa (K, K°), over a complete nonarchimedean field.

source
theorem TauCeti.ValuationSpectrum.isClosed_singleton_classicalPoint {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] (x : ↑(spa (Huber.powerBoundedSubring K))) (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)) :
IsClosed {classicalPoint x a ha}

The classical points of the closed unit disc are closed, over a complete nonarchimedean field: the classical point at a is the only point whose support contains T - a, and the locus of points whose support contains a given ideal is closed. These are the points of type (1) in Wedhorn's Example 7.57.

source
theorem TauCeti.ValuationSpectrum.exists_weightedX_sub_weightedC_mem_supp {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] [IsAlgClosed K] (v : ↑(closedPolydisc 1 K)) (hv : (↑v).supp ≠ ⊥) :
∃ (a : K), ‖a‖ ≤ 1 ∧ Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0 - (Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a ∈ (↑v).supp

A point of the closed unit disc with nonzero support kills some T - a with ‖a‖ ≤ 1, over an algebraically closed complete nonarchimedean field.

source
theorem TauCeti.ValuationSpectrum.supp_ne_bot_iff_exists_eq_classicalPoint {K : Type u_1} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] [IsAlgClosed K] (v : ↑(closedPolydisc 1 K)) :
(↑v).supp ≠ ⊥ ↔ ∃ (x : ↑(spa (Huber.powerBoundedSubring K))) (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)), v = classicalPoint x a ha

The points of the closed unit disc with nonzero support are exactly the classical points, over an algebraically closed complete nonarchimedean field: the points of type (1) in Wedhorn's description of the closed unit disc (Example 7.57).