Restricted power series

Stream: mathlib4

[William Coram]

This is an update on the discussion on restricted power series here

The predicate

variable {R : Type*} [NormedRing R] (c : ℝ)

/-- A power series over `R` is restricted of paramerter `c` if we have
`‖coeff R i f‖ * c ^ i → 0`. -/
def IsRestricted (f : PowerSeries R) :=
  Tendsto (fun (i : ℕ) ↦ (norm (coeff i f)) * c ^ i) atTop (𝓝 0)

is now in Mathlib.

A decision choice we have is now whether we want restricted power series to be their own type or not.

[William Coram]

Specifically, they form a group under addition (and a ring when R has the ultrametric property). So I would like some opinions on whether I show they are a subring of power series (so work with them as a subtype), or create a structure and give them their own type.

The first method would be something like this:

def subring [IsUltrametricDist R] : Subring (PowerSeries R) where
  carrier := IsRestricted c
  zero_mem' := IsRestricted.zero c
  add_mem' := IsRestricted.add c
  neg_mem' := IsRestricted.neg c
  one_mem' := IsRestricted.one c
  mul_mem' := IsRestricted.mul c

noncomputable
instance IsRing [IsUltrametricDist R] : Ring (Subtype (IsRestricted (R := R) c)) :=
    Subring.toRing (subring (R := R) c)

[William Coram]

Or I could create a structure:

structure cRestricted where
  series : PowerSeries R
  convergence : IsRestricted c series

and show they are a ring manually, e.g. part of the code could be

noncomputable
instance : AddCommGroup (cRestricted R c) where
  add f g :=⟨f.1 + g.1, IsRestricted.add c f.2 g.2⟩
  add_assoc f g h := by
    rw [cRestricted.mk.injEq]
    exact add_assoc f.1 g.1 h.1
  add_comm f g := by
    rw [cRestricted.mk.injEq]
    exact add_comm f.1 g.1
...

[Kenny Lau]

your second solution is "reinventing the wheel" (you're basically doing the first one again) and for the first one I would replace the name subring with restricted and then there's no need to type Subtype because it's automatic and also the ring instance is also automatic

[Kenny Lau]

in other words,

import Mathlib.RingTheory.PowerSeries.Restricted

namespace PowerSeries

def restricted (R : Type*) [NormedRing R] [IsUltrametricDist R] (c : ℝ) :
    Subring (PowerSeries R) where
  carrier := IsRestricted c
  zero_mem' := IsRestricted.zero c
  add_mem' := IsRestricted.add c
  neg_mem' := IsRestricted.neg c
  one_mem' := IsRestricted.one c
  mul_mem' := IsRestricted.mul c

variable (R : Type*) [NormedRing R] [IsUltrametricDist R] (c : ℝ)

#check restricted R c

variable (f g : restricted R c)

#check f + g

end PowerSeries

[William Coram]

Thanks that definitely looks nicer. I guess my question is more motivated by Riccardo's comment on the original PR.

That is what do people want to do with these things? Personally I want to work with Tate algebras, so when R is a complete ultrametric field, and in this case surely it should be its own type?

[Kenny Lau]

@William Coram I think you got distracted with the implementation, the comment is clearly asking about if it's more likely to be used as a type than as a subring, not about how you would implement it

[William Coram]

Ah, I definitely did get confused

[William Coram]

Opinions on this matter, is still something I would like to hear.

[Kenny Lau]

I don't work with restricted power series, can you share a theorem involving it since you mentioned that you're working with Tate algebras?

[Jovan Gerbscheid]

Nice! @Paul Lezeau and some others including me had worked on convergence of powerseries, and in particular exp and log. The IsRestricted c predicate seems to me like a good assumption for some convergence lemmas that we worked on.

I'm not sure what you have proved about IsRestricted but it would be good to avoid duplicating work!

[William Coram]

Kenny Lau said:

I don't work with restricted power series, can you share a theorem involving it since you mentioned that you're working with Tate algebras?

The main use for me will be in the theory of Newton polygons (see Gouvea's padic numbers book for many theorems). But an immediate use will be for the Weierstrass preparation theorem (5.2.2 BGR - Non-Archimedean analysis) - I can send a picture of it later if you need.

[William Coram]

Jovan Gerbscheid said:

I'm not sure what you have proved about IsRestricted but it would be good to avoid duplicating work!

Right now it is just results showing they form a ring.

[Jovan Gerbscheid]

Are you also interested in results about convergence of these powerseries?

[William Coram]

For R being a complete non-archimedean field, restricted power series of parameter c coincide with functions that converge on the ball of radius c. This is mentioned on page 239 in Gouvea and on page 197 of BGR.

[Kevin Buzzard]

I think that the answer is that restricted power series should be their own type, like polynomial rings are a type (as opposed to a subring of power series). There is a big theory of restricted power series, developed in e.g. Bosch--Guentzer--Remmert "Nonarchimedean analysis", they deserve their own definition. If they're a subring then typeclass inference will forever be going haywire, trying to find an action on a module over a restricted power series ring by realising that it suffices to find an action of the full power series ring (which might not exist) and then spending a long time timing out.

[Kevin Buzzard]

Screenshot from 2025-10-22 21-54-40.png
(there's over 100 pages of this stuff)

[Kenny Lau]

Kevin Buzzard said:

typeclass inference will forever be going haywire

isn't instance priority designed to help with this
(this is not a vote from me in either direction, i'm just asking a question)

[Kevin Buzzard]

The bottom line is that there is a huge theory of restricted power series rings in the nonarchimedean case, they are the building blocks of rigid geometry like commutative rings are the building blocks of algebraic geometry, they should definitely be their own type.

[Kevin Buzzard]

I would definitely recommend defining them as a subring and then immediately promoting to a type, like we do with integers of number fields here.

[Yakov Pechersky]

Why should it be that way if we don't do that for Polynomial? Not being difficult, just curious. Historical reasons?

[Kenny Lau]

subring of what?

[Kenny Lau]

I think polynomial is more fundamental than power series

[Yakov Pechersky]

PowerSeries. We have that LaurentSeries are a specialization of HahnSeries. There are all sorts of choices here, how one defines RatFunc as well. Or Polynomial a subtype / specialization of MvPolynomial similar to PowerSeries and MvPowerSeries.

The actual implementation is probably best by the way that bring the most technical ease. Is the largest determinant of that transferring instances, or preventing typeclass timeouts, or making it easy to have embedding into larger rings?

[Kenny Lau]

@Yakov Pechersky it seems hard to define the UMP "computably" (read: sensibly) if you're just given a power series and proof that it stops somewhere

[Kenny Lau]

i don't think defining r[x] as subtype of r[[x]] is the right choice

[Judith Ludwig]

Let me add something to the discussion that hopefully doesn't confuse things too much.

When I first learned about Tate algebras (at the beginning of my PhD) it was from the viewpoint of "subring of power series". But then when you work with them you need different ways to think about them. One other perspective is as follows:

Let's consider $T_{n,K}:=K\langle X_1,...,X_n\rangle$ for $K$ a non-archimedean field as a subring of the power series. Then $T_{n,K}$ is isomorphic to the localisation of the $\varpi$-adic completion of the polynomial ring over the ring of integers $\mathcal{O}_K$ ($\varpi$ being a pseudo-uniformiser in $K$), i.e.,
$T_{n,K} \cong \varprojlim \mathcal{O}_K[ X_1,...,X_n]/(\varpi^n) \left[\frac{1}{\varpi}\right].$
This might sound trickier than the power series definition but as it turns out it gives an effective way to argue about it. I'm currently teaching non-archimedean geometry (i.e. adic spaces) and I started with a discussion about Tate algebras (over non-archimedean fields $K$)). I ended up taking the "$\varpi$-adic completion version" as the definition following these notes.
In fact with adic spaces in mind I think this is the better definition (at least for my course). E.g. one thing that is easy to see in this approach, is that they form a ring.

[William Coram]

I would definitely recommend defining them as a subring and then immediately promoting to a type

I will continue by working with this method for now then.

Moreover, everything I have done thus far has been in only one variable - but we should really have multivariate restricted power series. Should I approach this the same as we have done for power series and multivariate power series?