Radius rings inside interval rings #
For 0 < ρ₁ ≤ ρ₂ < 1, the radius ring with Gauss norm λ_{ρ₂} embeds isometrically in
the interval ring with norm max(λ_{ρ₁}, λ_{ρ₂}). On Witt vectors, and hence after inverting
[ϖ], the maximum is λ_{ρ₂}. Completing therefore gives a closed coefficient ring in
the interval ring. Adjoining the inverse of p to this coefficient ring gives a dense subring.
These maps are the coefficient maps used in restricted-series presentations of interval rings.
Quantitatively, every element of 𝕎 O[1/(p [ϖ])] is a polynomial in p⁻¹ with coefficients in
𝕎 O[1/[ϖ]] whose weighted norms are bounded by its interval norm (Kedlaya's estimate (4.9.1)).
If v(ϖ)^b ≤ ρ₁^a with a ≠ 0, evaluation at [ϖ]^b/p^a defines a continuous map from the
one-variable restricted series ring over the radius ring with dense image in the interval ring.
The constructions use Mathlib’s UniformSpace.Completion.mapRingHom and
TauCeti.Huber.existsUnique_continuous_ringHom_weightedRestrictedSubring.
The parameters are the coefficient weights in λ_ρ(∑ [xₙ] pⁿ) = supₙ v(xₙ) ρⁿ; they
are related to Kedlaya's parameter r by ρ = p^(-1/r).
Main results #
TauCeti.WittVector.RadiusRing.isometry_toIntervalRing: the radius ring embeds isometrically in the interval ring.TauCeti.WittVector.RadiusRing.existsUnique_continuous_denseRange_restrictedSeries_toIntervalRing: evaluation at[ϖ]^b/p^aout ofA^{ρ₂}⟨X⟩has dense image.TauCeti.WittVector.IntervalLocalization.exists_sum_eq_mul_inv_pow: Kedlaya's estimate (4.9.1).
References #
- K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, arXiv:1410.5160v3, Definitions 2.4 and 4.2 and Lemma 4.9.
The map W(O)[1/[ϖ]] → W(O)[1/(p[ϖ])], before completion.
Instances For
For ordered radii, inverting [ϖ] preserves the radius norm in the interval norm.
For ordered radii, the map of uncompleted localisations is an isometry.
Kedlaya's estimate (4.9.1) in the normalisation λ_ρ(p) = ρ. Every
d ∈ 𝕎 O[1/(p [ϖ])] is a polynomial ∑_{i ≤ m} zᵢ p^(-(m - i)) in p⁻¹ whose coefficients zᵢ
lie in 𝕎 O[1/[ϖ]] and satisfy λ_{ρ₂}(zᵢ) ρ₁^(-(m - i)) ≤ λ_{[ρ₁, ρ₂]}(d). Writing
d = y / (p [ϖ]) ^ m and splitting y = ∑_{i < m} [yᵢ] pⁱ + pᵐ b, one takes zᵢ = [yᵢ] / [ϖ] ^ m
for i < m and zₘ = b / [ϖ] ^ m.
The coefficient map from the radius ring with weight ρ₂ to the interval ring with
endpoint weights ρ₁ ≤ ρ₂, obtained by completing the localisation map.
Instances For
The completed coefficient map agrees with the map of uncompleted localisations.
The completed coefficient map respects the maps from Witt vectors.
The radius ring embeds isometrically in the interval ring.
The coefficient map preserves norms.
The image of the radius ring is a closed coefficient ring in the interval ring.
Every element of the uncompleted interval localisation becomes a coefficient after
multiplication by a power of p.
Adjoining p⁻¹ to the image of the radius ring gives a dense subring of the interval
ring. Equivalently, elements which become coefficients after multiplication by some power
of p are dense.
Evaluation at [ϖ]^b/p^a, for a ≠ 0, gives a unique continuous map with dense image from
the one-variable restricted series ring over the radius ring to the interval ring, whenever the
variable has norm at most one at both endpoints, that is, v(ϖ)^b ≤ ρ₁^a. Uniqueness requires
only continuity and the coefficient and variable equations.