Documentation

TauCeti.AlgebraicGeometry.AdicSpace.Spa.Polydisc.GaussPoint

Gauss points of the closed unit disc #

Let K be a nontrivially normed nonarchimedean field and K⟨T⟩ the one-variable restricted power series ring, the coordinate ring of the closed unit disc closedPolydisc 1 K. For a radius 0 < r ≤ 1 the Gauss norm

|f|_r = sup_n ‖aₙ‖ rⁿ,    f = ∑ aₙ Tⁿ,

is a multiplicative ultrametric norm on K⟨T⟩, hence a valuation. It is continuous and at most one on the power-bounded elements, so it defines a point η_r of the closed unit disc. At r = 1 this is the Gauss point of the disc; for r < 1 it is the Gauss norm of the disc of radius r about the origin, one of the points of Wedhorn's Example 7.57. The valuation and its continuity need only a normed commutative ring with multiplicative ultrametric norm in place of K; the bound on power-bounded elements uses nonzero constants of small norm.

When K is complete, these points are not classical: the support of η_r is trivial, while the classical point at a kills T - a. Distinct radii give distinct points by comparing powers of T with constants. The file does not treat Wedhorn's classification of all points of the disc, nor discs about centres other than the origin.

Main definitions #

Main results #

References #

source
noncomputable def TauCeti.ValuationSpectrum.closedDiscGaussValuation {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) :
Valuation (↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) NNReal

The Gauss valuation of radius r on R⟨T⟩, for 0 < r ≤ 1: the valuation f ↦ sup_n ‖aₙ‖ rⁿ with values in ℝ≥0, where aₙ is the coefficient of Tⁿ in f.

Equations
Instances For
    source
    theorem TauCeti.ValuationSpectrum.coe_closedDiscGaussValuation {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) (f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) :
    ↑((closedDiscGaussValuation hr₀ hr₁) f) = ⨆ (n : ℕ), ‖(MvPowerSeries.coeff (Finsupp.single 0 n)) ↑f‖ * r ^ n

    The Gauss valuation of radius r is the supremum of the weighted coefficient norms.

    source
    theorem TauCeti.ValuationSpectrum.norm_coeff_mul_pow_le_closedDiscGaussValuation {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) (f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) (n : ℕ) :
    ‖(MvPowerSeries.coeff (Finsupp.single 0 n)) ↑f‖ * r ^ n ≤ ↑((closedDiscGaussValuation hr₀ hr₁) f)

    Every weighted coefficient norm ‖aₙ‖ rⁿ of f is bounded by its Gauss valuation.

    source
    theorem TauCeti.ValuationSpectrum.closedDiscGaussValuation_le_of_forall_norm_coeff_le {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) {f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} {ε : ℝ} (h : ∀ (ν : Fin 1 →₀ ℕ), ‖(MvPowerSeries.coeff ν) ↑f‖ ≤ ε) :
    ↑((closedDiscGaussValuation hr₀ hr₁) f) ≤ ε

    A common bound on the coefficient norms of f bounds its Gauss valuation, since r ≤ 1.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.closedDiscGaussValuation_weightedC {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) (a : R) :
    (closedDiscGaussValuation hr₀ hr₁) ((Huber.weightedC (fun (x : Fin 1) => {1}) ⋯) a) = ‖a‖₊

    The Gauss valuation of a constant is its norm.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.coe_closedDiscGaussValuation_weightedX {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) :
    ↑((closedDiscGaussValuation hr₀ hr₁) (Huber.weightedX (fun (x : Fin 1) => {1}) ⋯ 0)) = r

    The Gauss valuation of radius r takes the value r on the variable.

    source
    @[simp]
    theorem TauCeti.ValuationSpectrum.closedDiscGaussValuation_eq_zero_iff {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) {f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} :
    (closedDiscGaussValuation hr₀ hr₁) f = 0 ↔ f = 0

    The Gauss valuation vanishes only at zero.

    source
    theorem TauCeti.ValuationSpectrum.isContinuous_closedDiscGaussValuation {R : Type u_1} [NormedCommRing R] [IsUltrametricDist R] [NonarchimedeanRing R] {r : ℝ} [NormMulClass R] [NormOneClass R] (hr₀ : 0 < r) (hr₁ : r ≤ 1) :
    (closedDiscGaussValuation hr₀ hr₁).IsContinuous

    The Gauss valuation is continuous for 0 < r ≤ 1.

    source
    theorem TauCeti.ValuationSpectrum.closedDiscGaussValuation_le_one_of_isPowerBounded {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) {f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} (hf : Huber.IsPowerBounded f) :
    (closedDiscGaussValuation hr₀ hr₁) f ≤ 1

    The Gauss valuation is at most one on power-bounded elements of K⟨T⟩.

    source
    noncomputable def TauCeti.ValuationSpectrum.gaussPoint {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) :
    ↑(closedPolydisc 1 K)

    The Gauss point η_r of the closed unit disc, for 0 < r ≤ 1: the point of Spa (K⟨T⟩, K⟨T⟩°) given by the Gauss valuation f ↦ sup_n ‖aₙ‖ rⁿ. At r = 1 it is the Gauss point of the disc.

    Equations
    Instances For
      source
      theorem TauCeti.ValuationSpectrum.gaussPoint_val {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) :
      ↑(gaussPoint hr₀ hr₁) = ofValuation (closedDiscGaussValuation hr₀ hr₁)

      The underlying point in Spv K⟨T⟩ is defined by the Gauss valuation.

      source
      @[simp]
      theorem TauCeti.ValuationSpectrum.gaussPoint_vle_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) (f g : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)) :
      f ≤ᵥ g ↔ (closedDiscGaussValuation hr₀ hr₁) f ≤ (closedDiscGaussValuation hr₀ hr₁) g

      The Gauss point η_r compares two series by their Gauss valuations of radius r.

      source
      theorem TauCeti.ValuationSpectrum.gaussPoint_vle_zero_iff {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) {f : ↥(Huber.weightedRestrictedSubring (fun (x : Fin 1) => {1}) ⋯)} :
      f ≤ᵥ 0 ↔ f = 0

      A Gauss point η_r kills only the zero series.

      source
      @[simp]
      theorem TauCeti.ValuationSpectrum.supp_gaussPoint {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) :
      (↑(gaussPoint hr₀ hr₁)).supp = ⊥

      The support of a Gauss point is trivial.

      source
      theorem TauCeti.ValuationSpectrum.gaussPoint_ne_classicalPoint {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r : ℝ} [CompleteSpace K] (hr₀ : 0 < r) (hr₁ : r ≤ 1) (x : ↑(spa (Huber.powerBoundedSubring K))) (a : Fin 1 → K) (ha : ∀ (i : Fin 1), Huber.IsPowerBounded (a i)) :
      gaussPoint hr₀ hr₁ ≠ classicalPoint x a ha

      Gauss points over a complete field are not classical points.

      source
      theorem TauCeti.ValuationSpectrum.gaussPoint_inj {K : Type u_1} [NontriviallyNormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] {r s : ℝ} (hr₀ : 0 < r) (hr₁ : r ≤ 1) (hs₀ : 0 < s) (hs₁ : s ≤ 1) :
      gaussPoint hr₀ hr₁ = gaussPoint hs₀ hs₁ ↔ r = s

      Distinct radii 0 < r, s ≤ 1 give distinct Gauss points.