The interval rings B^I of the Fargues–Fontaine curve #
Let O be the ring of integers of a valuation v : Valuation K ℝ≥0 on a field K, perfect of
characteristic p, and let ϖ ∈ O be a pseudouniformiser, 0 < v(ϖ) < 1; for instance
O = 𝒪_F for a perfect nonarchimedean field F of characteristic p with pseudouniformiser
ϖ, so that 𝕎 O = A_inf. For 0 < ρ < 1 the Gauss valuation
λ_ρ(∑ₙ [xₙ] pⁿ) = supₙ v(xₙ) ρⁿ
(TauCeti.WittVector.gaussValuation) does not vanish at p [ϖ], so it extends to the
localisation 𝕎 O[1/(p [ϖ])] (TauCeti.WittVector.gaussValuationAway, an instance of Mathlib's
Valuation.extendToLocalization).
For radii ρ₁, ρ₂ ∈ (0, 1) the interval norm λ_I = max(λ_{ρ₁}, λ_{ρ₂}) is an ultrametric
ring norm on 𝕎 O[1/(p [ϖ])], and the interval ring B^I is the completion of
𝕎 O[1/(p [ϖ])] for λ_I. Kedlaya normalises the Gauss norms by an exponent t > 0 instead,
as λ(α^t)(x) = supₙ v(xₙ)^t p^(-n), which is λ_ρ(x)^t for ρ = p^(-1/t), and builds B^I
for a closed interval I ⊂ (0, ∞) of exponents from the norms λ(α^t), t ∈ I. Since
t ↦ log λ(α^t)(x) is convex, these are bounded by the norms at the two endpoints, and a positive
power of a norm defines the same uniform structure; so the interval I = [s, r] of exponents
corresponds to the radii ρ₁ = p^(-1/s) and ρ₂ = p^(-1/r) here.
The ring B^I is a complete Hausdorff Tate ring: p becomes a unit of norm max(ρ₁, ρ₂) < 1,
hence a pseudouniformiser (TauCeti.WittVector.isPseudoUniformizer_natCast_intervalRing), and the
Tate structure of 𝕎 O[1/(p [ϖ])] comes from TauCeti.Huber.IsTateRing.of_isUnit_norm_lt_one.
The norm λ_I is power-multiplicative, though in general not multiplicative, and so is its
extension to B^I. Hence the power-bounded elements of B^I are exactly its unit ball
B^{I,+} = {x : λ_I(x) ≤ 1}, which is therefore a ring of integral elements, and B^I is uniform.
Main definitions #
TauCeti.WittVector.gaussValuationAway: the extension ofλ_ρto𝕎 O[1/(p [ϖ])].TauCeti.WittVector.IntervalLocalization:𝕎 O[1/(p [ϖ])]normed byλ_I.TauCeti.WittVector.intervalNorm: the ring normλ_I = max(λ_{ρ₁}, λ_{ρ₂}).TauCeti.WittVector.IntervalRing: the interval ringB^I, the completion ofIntervalLocalization.
Main results #
TauCeti.WittVector.gaussValuationAway_algHom: the extended Gauss valuations are preserved by𝕎 O-algebra homomorphisms between localisations away fromp [ϖ].TauCeti.WittVector.norm_algebraMap_intervalRing:‖x‖ = max(λ_{ρ₁}(x), λ_{ρ₂}(x))forx ∈ 𝕎 O.TauCeti.WittVector.isPseudoUniformizer_natCast_intervalRing:pis a pseudouniformiser ofB^I.TauCeti.WittVector.isPseudoUniformizer_teichmuller_intervalRing:[ϖ]is a pseudouniformiser ofB^I.TauCeti.WittVector.coe_powerBoundedSubring_intervalRing: the power-bounded subring ofB^Iis its unit ballB^{I,+};TauCeti.WittVector.IntervalLocalization.coe_powerBoundedSubringis the same statement on𝕎 O[1/(p [ϖ])].TauCeti.WittVector.isUniform_intervalRing:B^Iis uniform.TauCeti.WittVector.norm_ringInverse_natCast_intervalRing:‖p⁻¹‖ = max(ρ₁⁻¹, ρ₂⁻¹)inB^I.TauCeti.WittVector.continuous_algebraMap_intervalLocalizationandTauCeti.WittVector.continuous_algebraMap_intervalRing:𝕎 O → 𝕎 O[1/(p [ϖ])]and𝕎 O → B^Iare continuous for the(p, [ϖ])-adic topology on𝕎 O.TauCeti.WittVector.exists_norm_le_one_algebraMap_eq_mul_intervalRing: ifλ_ρ(x) ≤ λ_ρ(y)at both radii andyis a unit of𝕎 O[1/(p [ϖ])], thenx / ylies in the unit ball ofB^I.TauCeti.WittVector.IntervalLocalization.instIsTateRing:𝕎 O[1/(p [ϖ])]with the interval norm is a Tate ring, so its completionB^Iis a complete Hausdorff Tate ring byTauCeti.Huber.IsTateRing.completion.
References #
- K. S. Kedlaya, Noetherian properties of Fargues–Fontaine curves, IMRN 2016, no. 8,
2544–2567, for the rings
B^I. - K. S. Kedlaya, Sheaves, stacks, and shtukas, lecture notes, Arizona Winter School 2017, §3.1.
- L. Fargues and J.-M. Fontaine, Courbes et fibrés vectoriels en théorie de Hodge p-adique, Astérisque 406 (2018), Chapter 1.
For 0 < ρ < 1 and ϖ ≠ 0, the Gauss valuation λ_ρ does not vanish at p [ϖ].
The Gauss valuation on 𝕎 O[1/(p [ϖ])]: the extension of λ_ρ to a localisation B of
𝕎 O away from p [ϖ], for 0 < ρ < 1 and ϖ ≠ 0.
Instances For
The extended Gauss valuation agrees with λ_ρ on 𝕎 O.
The extended Gauss valuation of a fraction x / s is λ_ρ(x) / λ_ρ(s).
The Gauss valuation at radius ρ of the numerator y of the fraction y / (p [ϖ]) ^ m is
the norm of the fraction at radius ρ, times (ρ v(ϖ)) ^ m.
The extended Gauss valuation vanishes only at zero.
The Gauss valuations of two localizations of 𝕎 O away from p [ϖ] correspond under any
𝕎 O-algebra homomorphism between them.
𝕎 O[1/(p [ϖ])] with the interval norm. This is the localisation of 𝕎 O away from
p [ϖ], for a pseudouniformiser ϖ (0 < v(ϖ) < 1), normed by λ_I = max(λ_{ρ₁}, λ_{ρ₂})
(TauCeti.WittVector.intervalNorm); its completion is the interval ring B^I.
Instances For
p is a unit of 𝕎 O[1/(p [ϖ])].
[ϖ] is a unit of 𝕎 O[1/(p [ϖ])].
The interval norm λ_I = max(λ_{ρ₁}, λ_{ρ₂}) on 𝕎 O[1/(p [ϖ])]: a ring norm, which is
ultrametric and submultiplicative because each λ_ρ is a valuation, and vanishes only at zero
because λ_{ρ₁} does.
Instances For
The interval norm is the larger of the two Gauss valuations.
The norm of 𝕎 O[1/(p [ϖ])] is the interval norm λ_I.
On 𝕎 O, the interval norm is max(λ_{ρ₁}, λ_{ρ₂}).
The interval norm of p is max(ρ₁, ρ₂).
The interval norm of p is less than one.
𝕎 O[1/(p [ϖ])] with the interval norm is a Tate ring, with pseudouniformiser p.
The interval norm is power-multiplicative: λ_I(x ^ n) = λ_I(x) ^ n, because λ_{ρ₁} and
λ_{ρ₂} are multiplicative.
The power-bounded elements of 𝕎 O[1/(p [ϖ])] are the unit ball of λ_I, since λ_I is
power-multiplicative and p is a unit of norm less than one.
Scalar multiplication by 𝕎 O is uniformly continuous, so that the 𝕎 O-algebra structure
extends to the completion B^I.
The interval ring B^I: the completion of 𝕎 O[1/(p [ϖ])] for the interval norm
λ_I = max(λ_{ρ₁}, λ_{ρ₂}), for radii ρ₁, ρ₂ ∈ (0, 1) and a pseudouniformiser ϖ
(0 < v(ϖ) < 1). It is a complete Hausdorff normed commutative ring and a Tate ring.
Instances For
On 𝕎 O, the norm of B^I is max(λ_{ρ₁}, λ_{ρ₂}).
The map 𝕎 O → B^I is injective.
The norm of p in B^I is max(ρ₁, ρ₂).
p is a pseudouniformiser of B^I: it is a unit of norm max(ρ₁, ρ₂) < 1.
[ϖ] is a pseudouniformiser of B^I: the Teichmüller lift of the pseudouniformiser ϖ
is a unit of norm v(ϖ) < 1.
Ring.inverse p in B^I is the image of p⁻¹ ∈ 𝕎 O[1/(p [ϖ])].
The norm of p⁻¹ in B^I is max(ρ₁⁻¹, ρ₂⁻¹).
The norm of B^I is power-multiplicative: ‖x ^ n‖ = ‖x‖ ^ n.
The power-bounded elements of B^I are its unit ball: x ∈ B^I is power-bounded exactly
when λ_I(x) ≤ 1.
The unit ball B^{I,+} of B^I is its power-bounded subring (B^I)°. In particular it
is a ring of integral elements of B^I, the plus ring of the Huber pair
TauCeti.Huber.Pair.powerBounded (IntervalRing p hv hϖ hϖ' hρ₁ hρ₂).
B^I is uniform: its power-bounded subring, the unit ball, is bounded.
The map 𝕎 O → 𝕎 O[1/(p [ϖ])] is continuous for the interval norm, when 𝕎 O carries the
(p, [ϖ])-adic topology: the Gauss valuations λ_{ρ₁} and λ_{ρ₂} are continuous valuations, so
λ_I = max(λ_{ρ₁}, λ_{ρ₂}) is small on a neighbourhood of 0.
The map 𝕎 O → B^I is continuous for the (p, [ϖ])-adic topology on 𝕎 O: it is the
continuous map 𝕎 O → 𝕎 O[1/(p [ϖ])] (continuous_algebraMap_intervalLocalization) followed
by the completion map.
Division by a unit of 𝕎 O[1/(p [ϖ])] within the unit ball. If y ∈ 𝕎 O becomes a unit
of 𝕎 O[1/(p [ϖ])] and λ_ρ(x) ≤ λ_ρ(y) at both radii, then x = z y in B^I for some z in
the unit ball B^{I,+} = {z : λ_I(z) ≤ 1}, namely z = x / y.
B^I is a complete Hausdorff Tate ring: completeness and separatedness hold for every
completion, and the Tate structure is that of 𝕎 O[1/(p [ϖ])], carried to the completion by
TauCeti.Huber.IsTateRing.completion (Wedhorn, Remark 6.8).