Interval rings of subintervals #
Let B^{[ρ₁, ρ₂]} be the interval ring of the Fargues–Fontaine curve
(TauCeti.WittVector.IntervalRing): the completion of 𝕎 O[1/(p [ϖ])] for the norm
λ_{[ρ₁, ρ₂]} = max(λ_{ρ₁}, λ_{ρ₂}), in the normalisation λ_ρ(p) = ρ, λ_ρ([x]) = v(x) of the
Gauss valuations. This file compares interval rings of nested intervals.
On 𝕎 O[1/(p [ϖ])] every term v(xₙ) ρ^(n - m) of λ_ρ(x / pᵐ) is monotone in ρ, so the Gauss
valuation at a radius inside [ρ₁, ρ₂] is at most λ_{[ρ₁, ρ₂]} (the Hadamard three circles
inequality, Kedlaya's Lemma 4.4). Hence for [ρ₁', ρ₂'] ⊆ [ρ₁, ρ₂] the identity of
𝕎 O[1/(p [ϖ])] extends to the restriction map B^{[ρ₁, ρ₂]} → B^{[ρ₁', ρ₂']} of Kedlaya's
Corollary 4.6.
The main result presents the interval ring of a smaller left endpoint ρ₁ ≤ ρ₁' ≤ ρ₂ as a
quotient of a ring of restricted power series over the larger one: the evaluation
B^{[ρ₁, ρ₂]}{T/c, U/ρ₁'⁻¹} → B^{[ρ₁', ρ₂]}{T/c}, T ↦ T, U ↦ p⁻¹,
is surjective. This is the form taken here by the first isomorphism of Kedlaya's Lemma 4.9, which
fixes the left endpoint of the interval. Kedlaya normalises the Gauss norms so that p has a
fixed norm and evaluates at a Teichmüller representative [z]; here the Teichmüller
representatives have norms independent of the radius, and the variable is sent to p⁻¹, of norm
ρ₁'⁻¹ on B^{[ρ₁', ρ₂]}. The evaluation is already surjective on the series with coefficients
in the radius ring A^{ρ₂} (TauCeti.WittVector.RadiusRing.restrictedEvalIntervalRing_surjective),
since restricting to the subinterval is compatible with the coefficient maps from A^{ρ₂}.
Main definitions #
TauCeti.WittVector.intervalRingRestrict: the restrictionB^{[ρ₁, ρ₂]} → B^{[ρ₁', ρ₂']}to a subinterval.TauCeti.WittVector.intervalRingRestrictedEval: the evaluationB^{[ρ₁, ρ₂]}{T/c, U/ρ₁'⁻¹} → B^{[ρ₁', ρ₂]}{T/c},U ↦ p⁻¹.
Main results #
TauCeti.WittVector.gaussValuationAway_le_max: the Hadamard three circles inequality on𝕎 O[1/(p [ϖ])].TauCeti.WittVector.norm_intervalRingRestrict_le: restriction to a subinterval does not increase the norm.TauCeti.WittVector.intervalRingRestrict_selfandTauCeti.WittVector.intervalRingRestrict_intervalRingRestrict: restriction is functorial.TauCeti.WittVector.intervalRingRestrict_toIntervalRing: restriction to a subinterval is compatible with the coefficient maps from the radius ring.TauCeti.WittVector.intervalRingRestrictedEval_surjective: the evaluation atp⁻¹is surjective.
References #
- K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, no. 8, 2544–2567; arXiv:1410.5160v3, Lemma 4.4, Corollaries 4.5 and 4.6 and Lemma 4.9.
The Hadamard three circles inequality on 𝕎 O[1/(p [ϖ])]. For radii
ρ₁ ≤ ρ ≤ ρ₂, the Gauss valuation λ_ρ is bounded by the larger of λ_{ρ₁} and λ_{ρ₂}, so
the interval norm of an interval dominates every Gauss valuation at a radius inside it.
Restriction to a subinterval (Kedlaya, Corollary 4.6). For a subinterval
[ρ₁', ρ₂'] ⊆ [ρ₁, ρ₂], the identity of 𝕎 O[1/(p [ϖ])] does not increase the interval norm,
by the Hadamard three circles inequality, so it extends to a 𝕎 O-algebra homomorphism
B^{[ρ₁, ρ₂]} → B^{[ρ₁', ρ₂']} of the completions.
Instances For
Restriction to a subinterval is the identity on fractions x / s with x ∈ 𝕎 O and s a
power of p [ϖ].
Restriction to a subinterval is continuous.
Restriction to a subinterval does not increase the interval norm.
Restriction of an interval to itself is the identity.
Restricting to a subinterval and then to a smaller one is restricting to the smaller one.
Restriction to subintervals is compatible with composition.
Restricting to a subinterval with the same right endpoint is compatible with the coefficient maps from the radius ring.
Evaluation at p⁻¹ onto a smaller left endpoint. For ρ₁ ≤ ρ₁' ≤ ρ₂, the ring
homomorphism
B^{[ρ₁, ρ₂]}{T/c, U/ρ₁'⁻¹} → B^{[ρ₁', ρ₂]}{T/c}, T ↦ T, U ↦ p⁻¹,
restricting the coefficients to the subinterval. 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.intervalRingRestrictedEval_surjective): this is the form of Kedlaya's
Lemma 4.9 that moves the left endpoint of an interval in the normalisation λ_ρ(p) = ρ.
Instances For
The presentation restricts constants to the subinterval.
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.
Kedlaya's Lemma 4.9, moving the left endpoint. For ρ₁ ≤ ρ₁' ≤ ρ₂, the evaluation
B^{[ρ₁, ρ₂]}{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
B^{[ρ₁, ρ₂]} with one more variable. It is already surjective on the series with coefficients in
the radius ring A^{ρ₂} (TauCeti.WittVector.RadiusRing.restrictedEvalIntervalRing_surjective).