Closed polydiscs as adic spaces

Over a complete nonarchimedean normed field K, the spectrum Spa(K, K°) and every closed unit polydisc are affinoid adic spaces. The polydisc is presented by the ordinary restricted-series ring over K; completeness identifies that ring with the completed Tate algebra, so its strong noetherianness follows from the strong noetherianness of K.

For a complete nontrivially normed field with an ultrametric norm — a complete rank-one nonarchimedean field — the Tate-ring hypothesis is supplied by TauCeti.Huber.IsTateRing.of_nontriviallyNormedField, and the examples at the end of the file record that both results then apply with no further hypotheses.

The construction keeps a pair of definition explicit. This is the same presentation dependence as TauCeti.ValuationSpectrum.presentationLimitPreAdicSpace; the underlying adic spectrum and the sheafiness conclusion do not choose a global pair of definition.

Main definitions

• TauCeti.ValuationSpectrum.closedPolydiscPreAdicSpace: the presentation-limit pre-adic space whose underlying topological space is the closed polydisc, with closedPolydiscPreAdicSpace_def as its characteristic equation.
• TauCeti.ValuationSpectrum.closedPolydiscBasicOpen: a rational open of the closed-polydisc pre-adic space.
• TauCeti.ValuationSpectrum.closedPolydiscBasicOpenIso: the restriction to an admissible rational open is the pre-adic space of the completed rational localisation.
• TauCeti.ValuationSpectrum.closedPolydiscPreAdicSpaceHomeomorph: the points of the closed-polydisc pre-adic space are the points of the closed polydisc.

Main results

• TauCeti.ValuationSpectrum.isAdic_spa_powerBounded_of_normedField: Spa(K, K°) with its presentation-limit structure sheaf is an adic space.
• TauCeti.ValuationSpectrum.isAdic_closedPolydiscPreAdicSpace: every closed unit polydisc over K is an affinoid adic space.
• TauCeti.ValuationSpectrum.closedPolydiscBasicOpen_mem_affinoidOpens: admissible rational opens are open affinoid subspaces.

References

• Bosch, Güntzer, Remmert, Non-Archimedean Analysis, §5.2.6, for strong noetherianness of Tate algebras.
• T. Wedhorn, Adic Spaces (arXiv:1910.05934v1), Example 7.57 and Theorem 8.28(b).

theorem TauCeti.ValuationSpectrum.isAdic_spa_powerBounded_of_normedField {K : Type u} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] [Huber.IsTateRing K] (P : Huber.PairOfDefinition K) : (presentationLimitPreAdicSpace P (Huber.powerBoundedSubring K) ⋯ ⋯).isAdic

The adic spectrum Spa(K, K°) of a complete nonarchimedean field is an adic space. Here K° is the power-bounded subring and P is any pair of definition of the Tate field.

noncomputable def TauCeti.ValuationSpectrum.closedPolydiscPreAdicSpace {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) : PreAdicSpace

The presentation-limit pre-adic space of the closed unit k-polydisc over K. Its coordinate ring is the ordinary restricted-series ring, its plus ring is the power-bounded subring, and its pair of definition is obtained from P coefficientwise.

theorem TauCeti.ValuationSpectrum.closedPolydiscPreAdicSpace_def {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) : closedPolydiscPreAdicSpace k P = presentationLimitPreAdicSpace (P.weighted ⋯) (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) ⋯ ⋯

The closed-polydisc pre-adic space is the presentation-limit spectrum for the coefficientwise pair of definition and the power-bounded plus ring.

noncomputable def TauCeti.ValuationSpectrum.closedPolydiscBasicOpen {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) (T : Finset ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) (s : ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) : TopologicalSpace.Opens ↑(closedPolydiscPreAdicSpace k P).toTopCat

A basic rational open of the closed-polydisc pre-adic space.

@[simp]

theorem TauCeti.ValuationSpectrum.closedPolydiscBasicOpen_sections {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) (T : Finset ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) (s : ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) : (closedPolydiscPreAdicSpace k P).toPresheafedSpace.presheaf.obj (Opposite.op (closedPolydiscBasicOpen k P T s)) = presentationLimit (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) (spaBasicOpen (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) T s)

The sections on a basic open of the closed polydisc are the presentation limit over that rational subset of its adic spectrum.

theorem TauCeti.ValuationSpectrum.closedPolydiscBasicOpen_mem_affinoidOpens {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) {T : Finset ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} {s : ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} (hT : IsOpen ↑(Ideal.span ↑T)) : closedPolydiscBasicOpen k P T s ∈ (closedPolydiscPreAdicSpace k P).affinoidOpens

A rational open of the closed polydisc whose numerators span an open ideal is an open affinoid subspace.

noncomputable def TauCeti.ValuationSpectrum.closedPolydiscBasicOpenIso {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) {T : Finset ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} {s : ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} (hT : IsOpen ↑(Ideal.span ↑T)) : (closedPolydiscPreAdicSpace k P).restrict ⋯ ≅ presentationLimitPreAdicSpace ((P.weighted ⋯).completionLocalization (↑T) s (Localization.Away s) ⋯) ((P.weighted ⋯).completedPlusSubring (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) T s (Localization.Away s) ⋯) ⋯ ⋯

The coordinate ring of an admissible rational open of the closed polydisc. Restricting the closed polydisc to R(T/s), for numerators spanning an open ideal, gives the presentation-limit pre-adic space of the completed rational localisation A⟨T/s⟩, where A is the restricted-series ring.

@[simp]

theorem TauCeti.ValuationSpectrum.closedPolydiscPreAdicSpace_carrier {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) : ↑(closedPolydiscPreAdicSpace k P).toPresheafedSpace = ↧↑(closedPolydisc k K)

The topological space underlying closedPolydiscPreAdicSpace is the closed polydisc Spa(K⟨T₁, …, Tₖ⟩, K⟨T₁, …, Tₖ⟩°).

noncomputable def TauCeti.ValuationSpectrum.closedPolydiscPreAdicSpaceHomeomorph {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) : ↑(closedPolydiscPreAdicSpace k P).toTopCat ≃ₜ ↑(closedPolydisc k K)

The points of the closed-polydisc pre-adic space are the points of the closed polydisc. On underlying valuations this is the identity.

@[simp]

theorem TauCeti.ValuationSpectrum.mem_closedPolydiscBasicOpen {K : Type u} [NormedField K] [NonarchimedeanRing K] (k : ℕ) (P : Huber.PairOfDefinition K) {T : Finset ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} {s : ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)} {x : ↑(closedPolydiscPreAdicSpace k P).toTopCat} : x ∈ closedPolydiscBasicOpen k P T s ↔ ↑((closedPolydiscPreAdicSpaceHomeomorph k P) x) ∈ rationalSubset (Huber.powerBoundedSubring ↥(Huber.weightedRestrictedSubring (fun (x : Fin k) => {1}) ⋯)) T s

A point lies in the basic rational open R(T/s) of the closed-polydisc pre-adic space exactly when the corresponding point of the closed polydisc lies in R(T/s).

theorem TauCeti.ValuationSpectrum.isAdic_closedPolydiscPreAdicSpace {K : Type u} [NormedField K] [IsUltrametricDist K] [NonarchimedeanRing K] [CompleteSpace K] [Huber.IsTateRing K] (k : ℕ) (P : Huber.PairOfDefinition K) : (closedPolydiscPreAdicSpace k P).isAdic

Every closed unit polydisc over a complete nonarchimedean field is an affinoid adic space. Its restricted-series coordinate ring is complete, Tate, and strongly noetherian.

Complete rank-one nonarchimedean fields

A complete nontrivially normed field with an ultrametric norm is a Tate ring, hence nonarchimedean, by instances, so both results apply to it.