The closed polydisc and its classical points #
The closed polydisc of dimension k over a nonarchimedean ring A is the adic spectrum
Spa (A⟨T₁, …, Tₖ⟩, A⟨T₁, …, Tₖ⟩°) of the restricted power series ring with its power-bounded
subring as plus ring. For a complete nonarchimedean field this is the closed unit polydisc of rigid
geometry, the affinoid whose points Wedhorn classifies in Example 7.57; the rings of Definition
7.56 are its quotients.
Its first points are the classical ones, the "end points" of Wedhorn's picture. A point x of
Spa (A, A°) and a tuple a ∈ (A°)ᵏ give the point f ↦ x (f (a)): evaluation at a is a
continuous ring homomorphism A⟨T⟩ → A (Wedhorn, Proposition 5.50), it carries A⟨T⟩° into A°
because it retracts the continuous constant embedding weightedC — continuous ring homomorphisms
do not preserve power-boundedness in general — and the point is the pullback of x along it. When
x has trivial support, for instance whenever A is a field, distinct tuples give distinct
points.
The evaluation is taken along the identity of A, so A carries the hypotheses under which
Wedhorn's evaluation converges: complete, Hausdorff, and nonarchimedean as a uniform additive
group. For the polydisc itself, a nonarchimedean ring topology suffices.
Main definitions #
TauCeti.ValuationSpectrum.closedPolydisc: the closed polydiscSpa (A⟨T⟩, A⟨T⟩°), withmem_closedPolydisc_iffas its membership rule.TauCeti.ValuationSpectrum.evalAtHom: evaluation of restricted power series ata ∈ (A°)ᵏ, as a ring homomorphismA⟨T⟩ →+* A.TauCeti.ValuationSpectrum.classicalPoint: the classical point of the closed polydisc attached to a point ofSpa (A, A°)and a tuplea ∈ (A°)ᵏ.
Main results #
TauCeti.ValuationSpectrum.continuous_evalAtHomandTauCeti.ValuationSpectrum.evalAtHom_mem_powerBoundedSubring: evaluation atais a morphism of Huber pairs(A⟨T⟩, A⟨T⟩°) → (A, A°).TauCeti.ValuationSpectrum.classicalPoint_vle: the classical point comparesfandgasxcomparesf (a)andg (a).TauCeti.ValuationSpectrum.classicalPoint_injective: whenxhas trivial support, the classical points are parametrised faithfully by(A°)ᵏ;TauCeti.ValuationSpectrum.classicalPoint_injective_of_isFieldis the case of a field.
References #
- T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Proposition 5.50, Definition 7.56 and Example 7.57.
The closed polydisc of dimension k over A: the adic spectrum of the restricted power
series ring A⟨T₁, …, Tₖ⟩ with its power-bounded subring as plus ring. Over a complete
nonarchimedean field this is the closed unit polydisc (Wedhorn, Example 7.57 at k = 1).
Equations
Instances For
The set-level characterization of the closed polydisc. closedPolydisc is not @[expose]d,
so its body is invisible across the module boundary and this equation is how consumers apply
set-level results to it — the same role spa_def plays for spa, which is likewise unexposed.
Membership in the closed polydisc: a point of Spv (A⟨T₁, …, Tₖ⟩) lies on the polydisc
exactly when it is continuous and sub-unit on the power-bounded elements. This is mem_spa_iff
specialized to the polydisc, and is the elimination rule consumers use on a point of it.
Evaluation at a ∈ (A°)ᵏ as a ring homomorphism A⟨T₁, …, Tₖ⟩ →+* A: Wedhorn's
evaluation of restricted power series along the identity of A, which converges because the
coordinates of a are power-bounded.
Equations
Instances For
Evaluation at a is continuous.
Evaluation at a sends the variable Tᵢ to aᵢ.
Evaluation at a fixes the constants.
Evaluation at a carries A⟨T⟩° into A°. Together with continuous_evalAtHom this makes
evaluation a morphism of Huber pairs (A⟨T⟩, A⟨T⟩°) → (A, A°).
The classical point of the closed polydisc attached to a point x of Spa (A, A°) and a
tuple a ∈ (A°)ᵏ: the pullback of x along evaluation at a, the valuation f ↦ x (f (a)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The classical point at a compares f and g as x compares their values at a: the
elimination rule that rewrites a comparison at a classical point into one after evalAtHom.
Distinct tuples give distinct classical points when x has trivial support. The
hypothesis is ValuativeRel.supp = ⊥ for x, written out: the valuative relation here is the
term x.1.toValuativeRel, not an instance, so ValuativeRel.supp is not directly available.
Over a field every point of Spa (A, A°) has trivial support, so the classical points are
parametrised faithfully by (A°)ᵏ.