Interval rings as strict quotients of restricted series over radius rings #
For 0 < ρ₁ ≤ ρ₂ < 1 and v(ϖ)ⁿ ≤ ρ₁, the evaluation X ↦ [ϖ]ⁿ/p gives a continuous map
ψ : A^{ρ₂}{X} → B^{[ρ₁, ρ₂]} from the one-variable restricted series ring over the radius ring
to the interval ring
(RadiusRing.existsUnique_continuous_denseRange_restrictedSeries_toIntervalRing).
This file proves that ψ does not increase norms, and that it is a strict surjection when the
left endpoint is matched to [ϖ], that is, when v(ϖ)ⁿ = ρ₁: every x ∈ B^I is ψ f for a
series f whose coefficients have norm at most (1 + ε) ‖x‖. This presents B^I as a quotient
of A^{ρ₂}{X} with controlled lifts, which is how Kedlaya transfers the noetherianity of
restricted series over A^r (Theorem 3.2) to the interval rings (Theorem 4.10).
The lift of an element of the dense subring 𝕎 O[1/(p [ϖ])] is explicit. Write it as
y / (p [ϖ])ᵐ and split the Teichmüller expansion y = ∑_{i < m} [yᵢ] pⁱ + pᵐ b. Since
p⁻¹ = X / [ϖ]ⁿ in the image, y / (p [ϖ])ᵐ is the image of
b / [ϖ]ᵐ + ∑_{i < m} ([yᵢ] / [ϖ]^(m + n (m - i))) X^(m - i). Its coefficients have norm at most
max(λ_{ρ₁}, λ_{ρ₂})(y / (p [ϖ])ᵐ): the tail at ρ₂ and the terms [yᵢ] at ρ₁, where
v(ϖ)ⁿ = ρ₁ is used. Mathlib's successive approximation theorem controlled_closure_of_complete
then lifts every element of B^I, with the coefficient ring A^{ρ₂}{X} normed by its Gauss norm
through TauCeti.Huber.restrictedMvPowerSeriesGaussEquiv.
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),
IntervalLocalization.exists_sum_eq_mul_inv_pow). Consequently, for every left endpoint
ρ₁ ≤ ρ₂, evaluation at p⁻¹ is a surjection
A^{ρ₂}{T/c, U/ρ₁⁻¹} → B^{[ρ₁, ρ₂]}{T/c}, T ↦ T, U ↦ p⁻¹,
from restricted series at real radii. This is a form of the presentations of Kedlaya's Lemma 4.9,
which evaluate at [z] / p with z ∈ K instead; evaluating at p⁻¹ at the real radius ρ₁⁻¹
needs no element of K of prescribed norm, so ρ₁ is arbitrary. This is how the rings
B^{[ρ₁, ρ₂]}{T/c} inherit noetherianity from the radius ring.
Main results #
TauCeti.WittVector.RadiusRing.norm_restrictedSeries_toIntervalRing_le:ψ fhas norm at most any bound on the coefficient norms off.TauCeti.WittVector.RadiusRing.exists_restrictedSeries_toIntervalRing_eq: ifv(ϖ)ⁿ = ρ₁, everyx ∈ B^Iisψ ffor somefwhose coefficients have norm at most(1 + ε) ‖x‖.TauCeti.WittVector.RadiusRing.surjective_restrictedSeries_toIntervalRing: ifv(ϖ)ⁿ = ρ₁, thenψis surjective.TauCeti.WittVector.RadiusRing.restrictedEvalIntervalRing_surjective: evaluation atp⁻¹presentsB^{[ρ₁, ρ₂]}{T/c}as a quotient ofA^{ρ₂}{T/c, U/ρ₁⁻¹}.
References #
- K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016,
arXiv:1410.5160v3, Lemma 4.9 (the isomorphism
A^r{T}/(pT - [zⁿ]) ≅ B^{I'''}and the estimate (4.9.1) in its proof) and Theorem 4.10.
Evaluation at [ϖ]ⁿ/p does not increase norms. Let v(ϖ)ⁿ ≤ ρ₁ ≤ ρ₂, and let
ψ : A^{ρ₂}{X} → B^{[ρ₁, ρ₂]} be the continuous evaluation X ↦ [ϖ]ⁿ/p along the coefficient
map. If every coefficient of f has norm at most r, then ‖ψ f‖ ≤ r.
Strict surjectivity of A^{ρ₂}{X} → B^{[ρ₁, ρ₂]}, the surjective half of the third
isomorphism of Kedlaya's Lemma 4.9. Let
ψ : A^{ρ₂}{X} → B^{[ρ₁, ρ₂]} be the continuous evaluation X ↦ [ϖ]ⁿ/p along the coefficient
map, where v(ϖ)ⁿ = ρ₁ ≤ ρ₂. For every ε > 0, every x ∈ B^I is ψ f for a restricted series
f whose coefficients have norm at most (1 + ε) ‖x‖.
Surjectivity of A^{ρ₂}{X} → B^{[ρ₁, ρ₂]} (Kedlaya, Lemma 4.9). If
v(ϖ)ⁿ = ρ₁ ≤ ρ₂, the continuous evaluation X ↦ [ϖ]ⁿ/p from A^{ρ₂}{X} to B^{[ρ₁, ρ₂]}
is surjective.
Evaluation at p⁻¹ out of restricted series over the radius ring. For ρ₁ ≤ ρ₂, the
ring homomorphism
A^{ρ₂}{T/c, U/ρ₁⁻¹} → B^{[ρ₁, ρ₂]}{T/c}, T ↦ T, U ↦ p⁻¹,
with coefficients mapped by toIntervalRing. Here U = X 0 and T i = X i.succ, and U has
radius ρ₁⁻¹, the norm of p⁻¹ in B^{[ρ₁, ρ₂]}. It is surjective
(TauCeti.WittVector.RadiusRing.restrictedEvalIntervalRing_surjective), for every left endpoint
ρ₁.
Instances For
The presentation maps constants by toIntervalRing.
The presentation sends the variable U = X 0 to p⁻¹.
The presentation sends each variable T i = X i.succ to X i.
The presentation does not increase the Gauss norm.
The presentation is continuous for the Gauss norms.
Uniqueness of the presentation: a continuous ring homomorphism
A^{ρ₂}{T/c, U/ρ₁⁻¹} → B^{[ρ₁, ρ₂]}{T/c} that maps constants by toIntervalRing and sends U to
p⁻¹ and each T i to X i is restrictedEvalIntervalRing.
The interval ring as a quotient of restricted series over the radius ring. For ρ₁ ≤ ρ₂,
the evaluation
A^{ρ₂}{T/c, U/ρ₁⁻¹} → B^{[ρ₁, ρ₂]}{T/c}, T ↦ T, U ↦ p⁻¹,
is surjective, so B^{[ρ₁, ρ₂]}{T/c} is a quotient of a ring of restricted power series over the
radius ring A^{ρ₂} with one more variable. The left endpoint ρ₁ is arbitrary.