The rational localisation of π O at a window is the interval ring B^I #
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. Give π O its
(p, [Ο])-adic topology. For nonnegative rationals q = a / b and q' = a' / b' in lowest
terms, the window {q β€ ΞΊ β€ q'} of the FarguesβFontaine curve is cut out by the inequalities
v([Ο]) ^ b β€ v(p) ^ a and v(p) ^ a' β€ v([Ο]) ^ b'. Over the denominator s below, these are
the conditions v(t) β€ v(s) for the numerators t β T:
T = {[Ο] ^ (b + b'), p ^ (a + a')}, s = p ^ a [Ο] ^ b'
(TauCeti.WittVector.windowNumerators, TauCeti.WittVector.windowDenominator), whose fractions
are [Ο] ^ b / p ^ a and p ^ a' / [Ο] ^ b'. Wedhorn's topological localisation π O(T/s) puts
on π O[1/s] the topology with ring of definition
D = π O[[Ο] ^ b / p ^ a, p ^ a' / [Ο] ^ b'] (TauCeti.WittVector.windowSubring) and ideal of
definition (p, [Ο]) D.
When q β 0, the ring π O[1/s] is the localisation of π O away from p [Ο], which also
carries the interval norm Ξ»_I = max(Ξ»_{Οβ}, Ξ»_{Οβ})
(TauCeti.WittVector.IntervalLocalization). For the radii of the window,
Οβ = v(Ο) ^ (1 / q) and Οβ = v(Ο) ^ (1 / q'), the two topologies agree. Consequently the
completion π Oβ¨T/sβ© is the interval ring B^I, as topological rings and compatibly with the
maps from π O. With plus ring AβΊ = π O, this isomorphism carries the plus ring A_UβΊ of the
rational localisation onto B^{I,+}, so it is an isomorphism of Huber pairs.
Proof outline #
The localisation topology is at least as fine as the norm topology by the universal property of
π O(T/s): the map π O β π O[1/s] is continuous for the norm, because the Gauss valuations
are continuous for the (p, [Ο])-adic topology, and the two fractions are power-bounded for the
norm, because D is bounded. Conversely the n-th basic neighbourhood (p, [Ο]) ^ n D of the
localisation topology contains [Ο] ^ n D, the image of the norm-open subring D under
multiplication by the unit [Ο] ^ n.
Main definitions #
TauCeti.WittVector.windowNumerators,TauCeti.WittVector.windowDenominator: the numeratorsTand denominatorsattached to the window.TauCeti.WittVector.completionLocRingEquivIntervalRing: the ring isomorphismπ Oβ¨T/sβ© β+* B^I.
Main results #
TauCeti.WittVector.isLocalization_away_windowDenominator: forq β 0, a localisation away fromp [Ο]is a localisation away froms.TauCeti.WittVector.divBy_teichmuller_pow_windowDenominatorandTauCeti.WittVector.divBy_natCast_pow_windowDenominator: the fractions of the presentation are[Ο] ^ b / p ^ aandp ^ a' / [Ο] ^ b'.TauCeti.WittVector.locSubring_windowNumerators: the ring of definitionπ O[T/s]of the presentation is the window subring;TauCeti.WittVector.adjoin_top_windowNumeratorsis the same for the ringAβΊ[T/s]withAβΊ = π O.TauCeti.WittVector.isOpen_span_windowNumeratorsandTauCeti.WittVector.hasDenominatorPower_windowNumerators: the numerators span an open ideal, so the presentation satisfies the standing hypothesis of the localisation topology, for every pair of definition.TauCeti.WittVector.locTopology_windowNumerators: the localisation topology of the window is the interval-norm topology.TauCeti.WittVector.locUniformSpace_windowNumerators: the same for the uniformities.TauCeti.WittVector.continuous_completionLocRingEquivIntervalRingand itssymmcounterpart : the isomorphismπ Oβ¨T/sβ© β+* B^Iis a homeomorphism.TauCeti.WittVector.completionLocRingEquivIntervalRing_coeandTauCeti.WittVector.completionLocRingEquivIntervalRing_toCompletionLoc: it is the identity onπ O[1/(p [Ο])], hence compatible with the maps fromπ O.TauCeti.WittVector.map_completedPlusSubring_windowNumerators: it carries the plus ringA_UβΊof the window, forAβΊ = π O, ontoB^{I,+}.
References #
- K. S. Kedlaya, Sheaves, stacks, and shtukas, lecture notes, Arizona Winter School 2017,
Β§3.1, for the interval rings
B^Iand the windows. - T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition and Definition 5.51, and Β§8.1 for the plus ring of a rational localisation.
The presentation of a window #
The numerators {[Ο] ^ (b + b'), p ^ (a + a')} of the window {q β€ ΞΊ β€ q'}, for
q = a / b and q' = a' / b' in lowest terms. Over windowDenominator p Ο q q' = p ^ a [Ο] ^ b'
they give the fractions [Ο] ^ b / p ^ a and p ^ a' / [Ο] ^ b'.
Instances For
The numerators of a window are [Ο] ^ (b + b') and p ^ (a + a').
The denominator p ^ a [Ο] ^ b' of the window {q β€ ΞΊ β€ q'}, for q = a / b and
q' = a' / b' in lowest terms.
Instances For
A localisation away from p [Ο] is a localisation away from p ^ a [Ο] ^ b', if
q = a / b β 0: the two elements have the same radical, since a β₯ 1 and b' β₯ 1.
Over the denominator p ^ a [Ο] ^ b', the numerator [Ο] ^ (b + b') gives the fraction
[Ο] ^ b / p ^ a.
Over the denominator p ^ a [Ο] ^ b', the numerator p ^ (a + a') gives the fraction
p ^ a' / [Ο] ^ b'.
The ring of definition of the window presentation is the window subring: for a pair of
definition with ring of definition all of π O, the subring π O[T/s] generated by the fractions
of the presentation is π O[[Ο] ^ b / p ^ a, p ^ a' / [Ο] ^ b'].
The ring AβΊ[T/s] of the window presentation is the window subring, for the plus ring
AβΊ = π O: the subring generated over π O by the fractions of the presentation is
π O[[Ο] ^ b / p ^ a, p ^ a' / [Ο] ^ b']. This is the ring whose integral closure the plus ring
A_UβΊ of the rational localisation completes
(TauCeti.Huber.PairOfDefinition.completedPlusSubring).
The numerators of a window span an open ideal for the (p, [Ο])-adic topology: its
radical contains p and [Ο].
The window presentation satisfies the standing hypothesis of the localisation topology,
for every pair of definition of the (p, [Ο])-adic topology: its numerators span an open ideal
(isOpen_span_windowNumerators).
The localisation topology of a window is the interval-norm topology #
The localisation topology of a window is the interval-norm topology. Let π O carry the
(p, [Ο])-adic topology, with any pair of definition P, and let q = a / b and q' = a' / b'
in lowest terms with radii Οβ ^ a = v(Ο) ^ b, Οβ ^ a' = v(Ο) ^ b' and Οβ β€ Οβ. Then on
π O[1/(p [Ο])], which is also a localisation away from p ^ a [Ο] ^ b'
(isLocalization_away_windowDenominator, as q β 0), Wedhorn's localisation topology for the
numerators {[Ο] ^ (b + b'), p ^ (a + a')} and denominator p ^ a [Ο] ^ b' is the topology of the
interval norm Ξ»_I = max(Ξ»_{Οβ}, Ξ»_{Οβ}).
The localisation uniformity of a window is the interval-norm uniformity, under the
hypotheses of locTopology_windowNumerators: both are uniform additive group structures, and
their topologies agree.
The completed coordinate ring of a window is the interval ring: under the hypotheses of
locTopology_windowNumerators, the completion π Oβ¨T/sβ© of the localisation of π O at the
window presentation is isomorphic to B^I. The isomorphism is the identity of
π O[1/(p [Ο])] on the dense subrings; it is a homeomorphism
(continuous_completionLocRingEquivIntervalRing and its symm counterpart) and is compatible with
the maps from π O (completionLocRingEquivIntervalRing_toCompletionLoc).
Instances For
The isomorphism π Oβ¨T/sβ© β+* B^I is continuous.
The inverse of the isomorphism π Oβ¨T/sβ© β+* B^I is continuous.
The isomorphism π Oβ¨T/sβ© β+* B^I is the identity on π O[1/(p [Ο])]: it sends the image
of x in the completion for the localisation topology to the image of x in B^I.
The isomorphism π Oβ¨T/sβ© β+* B^I is compatible with the maps from π O: it carries the
structure map π O β π Oβ¨T/sβ© to the map π O β B^I.
The isomorphism π Oβ¨T/sβ© β+* B^I carries the plus ring of the window onto B^{I,+}. With
plus ring AβΊ = π O, the plus ring A_UβΊ of the rational localisation at the window is the
closure of the image of the integral closure of AβΊ[T/s], which is the window subring
(adjoin_top_windowNumerators). The isomorphism is a homeomorphism and the identity on
π O[1/(p [Ο])], so it carries that closure to the corresponding closure in B^I, which is
B^{I,+} = (B^I)Β° (topologicalClosure_map_coeRingHom_integralClosure_windowSubring). Hence the
isomorphism is one of Huber pairs (π Oβ¨T/sβ©, A_UβΊ) β
(B^I, B^{I,+}).