Adic Spaces — Lean blueprint

9. Tate algebras and restricted power series🔗

Definition9.1
uses 1used by 1✓L∃∀N

A power series \sum a_\nu T^\nu is restricted if its coefficients tend to 0 along the cofinite filter (\texttt{IsRestricted}); these form the subring A\langle T_1, \dots, T_k\rangle (\texttt{restrictedMvPowerSeriesSubring}). A topological ring is strongly noetherian if every such ring is noetherian (\texttt{IsStronglyNoetherian}) (Definition 1.1). Following Wedhorn Definition 6.9.

Lean code for Definition9.1●3 definitions
  • defdefined in «Adic spaces»/RestrictedPowerSeries.lean
    complete
    def MvPowerSeries.IsRestricted.{u_1} {k : ℕ} {A : Type u_1} [CommRing A]
  [TopologicalSpace A] (f : MvPowerSeries (Fin k) A) : Prop
    def MvPowerSeries.IsRestricted.{u_1} {k : ℕ}
  {A : Type u_1} [CommRing A]
  [TopologicalSpace A]
  (f : MvPowerSeries (Fin k) A) : Prop
    An element `f` of the multivariate power series ring `A⦃X₁, …, Xₖ⦄` is **restricted**
if its coefficients converge to `0` along the cofinite filter on multi-indices. That is,
for every open neighborhood `U` of `0` in `A`, all but finitely many coefficients of `f`
lie in `U`. This is the defining property of elements of `A⟨T₁, …, Tₖ⟩`.

See Wedhorn, §6.9.
  • defdefined in «Adic spaces»/RestrictedPowerSeries.lean
    complete
    def restrictedMvPowerSeriesSubring.{u_1} (k : ℕ) (A : Type u_1) [CommRing A]
  [TopologicalSpace A] [NonarchimedeanRing A] :
  Subring (MvPowerSeries (Fin k) A)
    def restrictedMvPowerSeriesSubring.{u_1}
  (k : ℕ) (A : Type u_1) [CommRing A]
  [TopologicalSpace A]
  [NonarchimedeanRing A] :
  Subring (MvPowerSeries (Fin k) A)
    The set of restricted power series forms a subring of `MvPowerSeries (Fin k) A`.

The closure under multiplication (convolution of tendsto-0 coefficient sequences)
requires that `A` is a nonarchimedean topological ring (so that finite sums of elements in an
open additive subgroup remain in the subgroup). This is the canonical definition of
`A⟨T₁, …, Tₖ⟩` (Wedhorn, §6.9).
  • class(1 method)defined in «Adic spaces»/RestrictedPowerSeries.lean
    complete
    class IsStronglyNoetherian.{u_1} (A : Type u_1) [CommRing A]
  [TopologicalSpace A] [NonarchimedeanRing A] : Prop
    class IsStronglyNoetherian.{u_1} (A : Type u_1)
  [CommRing A] [TopologicalSpace A]
  [NonarchimedeanRing A] : Prop
    A topological ring `A` is **strongly noetherian** if the ring of restricted power series
`A⟨T₁, …, Tₖ⟩` is noetherian for all `k ≥ 0` (Definition 6.9 of Wedhorn).

This is a fundamental finiteness condition in nonarchimedean geometry, introduced by
Huber. For a noetherian Tate ring, being strongly noetherian is equivalent to saying
that the theory of formal models is well-behaved.

    Methods

    isNoetherianRing_restricted : ∀ (k : ℕ), IsNoetherianRing ↥(restrictedMvPowerSeriesSubring k A)
    The restricted power series ring in `k` variables is noetherian for all `k`.
Definition9.2
Statement uses 3
Statement dependency previews
Preview
Definition 1.2
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 3
Reverse dependency previews
Preview
Theorem 9.3
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The Tate algebra A\langle X \rangle over a Tate ring A (Definition 1.2, Definition 9.1) is the ring of restricted power series in one variable — the building block of functions on the closed unit disc. Its Laurent variant A\langle \zeta, \zeta^{-1}\rangle (\texttt{LaurentTateAlgebra}, the quotient A\langle X, Y\rangle/(XY-1)) inverts the coordinate and gives the annular pieces of rational covers (Definition 7.1). In Adic-Spaces: \texttt{TateAlgebra}. Following Wedhorn Definition 7.29 (§6.9).

Lean code for Definition9.2●2 definitions
  • abbrevdefined in «Adic spaces»/TateAlgebra.lean
    complete
    abbrev TateAlgebra.{u} (A : Type u) [CommRing A] [TopologicalSpace A]
  [NonarchimedeanRing A] : Subring (MvPowerSeries (Fin 1) A)
    abbrev TateAlgebra.{u} (A : Type u) [CommRing A]
  [TopologicalSpace A]
  [NonarchimedeanRing A] :
  Subring (MvPowerSeries (Fin 1) A)
    The univariate Tate algebra `A⟨X⟩`, the ring of restricted power series in one variable.
This is `restrictedMvPowerSeriesSubring 1 A`, specialized to the univariate case.
See Wedhorn, Definition 6.9.
  • defdefined in «Adic spaces»/TateAlgebra.lean
    complete
    def LaurentTateAlgebra.{u} (A : Type u) [CommRing A] [TopologicalSpace A]
  [NonarchimedeanRing A] : Type u
    def LaurentTateAlgebra.{u} (A : Type u)
  [CommRing A] [TopologicalSpace A]
  [NonarchimedeanRing A] : Type u
    The Laurent Tate algebra `A⟨ζ, ζ⁻¹⟩`, defined as the quotient of the bivariate
restricted power series ring `A⟨X, Y⟩` by the ideal `(XY - 1)`.

This models the ring of bilateral restricted power series
`∑_{n ∈ ℤ} aₙ ζⁿ` with `aₙ → 0` as `|n| → ∞`.

See Wedhorn, §8.29–8.33 (Definition 8.27).
Theorem9.3
uses 1used by 0✓L∃∀N

Evaluation at 0 is a surjective ring homomorphism A\langle X\rangle \to A (Definition 9.2): the constant term a_0 of a restricted power series. In Adic-Spaces: \texttt{evalZeroHom}, \texttt{evalZeroHom\_surjective}. Following Wedhorn §6.9.

Lean code for Theorem9.3●2 declarations
  • defdefined in «Adic spaces»/TateAlgebra.lean
    complete
    def TateAlgebra.evalZeroHom.{u} {A : Type u} [CommRing A]
  [TopologicalSpace A] [NonarchimedeanRing A] : ↥(TateAlgebra A) →+* A
    def TateAlgebra.evalZeroHom.{u} {A : Type u}
  [CommRing A] [TopologicalSpace A]
  [NonarchimedeanRing A] :
  ↥(TateAlgebra A) →+* A
    The constant term (evaluation at zero) is a ring homomorphism `A⟨X⟩ →+* A`.
  • theoremdefined in «Adic spaces»/TateAlgebra.lean
    complete
    theorem TateAlgebra.evalZeroHom_surjective.{u} {A : Type u} [CommRing A]
  [TopologicalSpace A] [NonarchimedeanRing A] :
  Function.Surjective ⇑TateAlgebra.evalZeroHom
    theorem TateAlgebra.evalZeroHom_surjective.{u}
  {A : Type u} [CommRing A]
  [TopologicalSpace A]
  [NonarchimedeanRing A] :
  Function.Surjective
    ⇑TateAlgebra.evalZeroHom
    The evaluation-at-zero map is surjective: every `a : A` is the constant term of the
constant power series `algebraMap A _ a`.
Proof for Theorem 9.3
uses 0

Sending \sum a_n X^n \mapsto a_0 respects sums and products of restricted power series (the product's constant term is a_0 b_0), so it is a ring hom. It is surjective because every a \in A is the image of the constant series a. Following Wedhorn §6.9.

Theorem9.4
uses 1used by 0✓L∃∀N

In the Laurent Tate algebra the coordinate \zeta is a unit, with explicit inverse \zeta^{-1} satisfying \zeta \cdot \zeta^{-1} = 1 (Definition 9.2). In Adic-Spaces: \texttt{zeta\_mul\_zetaInv}, \texttt{zetaInv\_mul\_zeta}. This invertibility is what makes A\langle \zeta, \zeta^{-1}\rangle the ring of functions on an annulus. Following Wedhorn §8.29.

Lean code for Theorem9.4●2 theorems
  • theoremdefined in «Adic spaces»/TateAlgebra.lean
    complete
    theorem LaurentTateAlgebra.zeta_mul_zetaInv.{u} {A : Type u} [CommRing A]
  [TopologicalSpace A] [NonarchimedeanRing A] :
  LaurentTateAlgebra.zeta * LaurentTateAlgebra.zetaInv = 1
    theorem LaurentTateAlgebra.zeta_mul_zetaInv.{u}
  {A : Type u} [CommRing A]
  [TopologicalSpace A]
  [NonarchimedeanRing A] :
  LaurentTateAlgebra.zeta *
      LaurentTateAlgebra.zetaInv =
    1
    The defining relation: `ζ · ζ⁻¹ = 1` in `A⟨ζ, ζ⁻¹⟩`.
  • theoremdefined in «Adic spaces»/TateAlgebra.lean
    complete
    theorem LaurentTateAlgebra.zetaInv_mul_zeta.{u} {A : Type u} [CommRing A]
  [TopologicalSpace A] [NonarchimedeanRing A] :
  LaurentTateAlgebra.zetaInv * LaurentTateAlgebra.zeta = 1
    theorem LaurentTateAlgebra.zetaInv_mul_zeta.{u}
  {A : Type u} [CommRing A]
  [TopologicalSpace A]
  [NonarchimedeanRing A] :
  LaurentTateAlgebra.zetaInv *
      LaurentTateAlgebra.zeta =
    1
    The defining relation: `ζ⁻¹ · ζ = 1` in `A⟨ζ, ζ⁻¹⟩`.
Proof for Theorem 9.4
uses 0

By construction A\langle\zeta,\zeta^{-1}\rangle = A\langle X,Y\rangle/(XY-1) with \zeta, \zeta^{-1} the images of X, Y. The defining relation XY - 1 = 0 becomes \zeta \cdot \zeta^{-1} = 1 in the quotient, and commutativity gives the reverse product too. Following Wedhorn §8.29.