Summation in an adic complete ring/topological ring

Stream: Is there code for X?

[Jiang Jiedong]

Is there a way to write an infinite summation in an adic complete ring/complete topologial ring?

To be more precise, given a sequence of p-adic integers $a_n$, and condition that the multiplicative valuation $v(a_n) \to 0$, what is the best way to define the summation of these elements in $\mathbb{Z}_p$? What about $a_n \in \mathbb{Q}_p$?

[Andrew Yang]

If you already have a topology on the ring, then I think docs#tsum is the way to go. But I also needed this for sums on $R[[X]]$ where there isn't necessary a topology yet (and I'm not sure if we want the $X$-adic topology), and I still don't have a satisfactory answer on how to proceed there.

[Jiang Jiedong]

I want to take infinite sums on the Witt vectors. However, the Witt vector can have different topologies, just like $R[[X]]$.

[Anatole Dedecker]

Andrew Yang said:

If you already have a topology on the ring, then I think docs#tsum is the way to go. But I also needed this for sums on $R[[X]]$ where there isn't necessary a topology yet (and I'm not sure if we want the $X$-adic topology), and I still don't have a satisfactory answer on how to proceed there.

There should be everything needed if you open PowerSeries.WithPiTopology (and endow your ring with the topology you want, which is probably the discrete one)

[Anatole Dedecker]

It is indeed the adic topology in the single variable case, but in more variables you can't write it as an adic topology.

[Jiang Jiedong]

My situation is like this:

1. There are two topologies on the Witt Vectors,
   (1) the p-adic topology, and
   (2) the inverse limit topology.

2. I prefer to define the inverse limit topology as the instance on the Witt vectors. However, I have to develop the existence of Teichmuller expansion first, which is an infinite sum in the p-adic topology.

[Jiang Jiedong]

If there is an API for infinite summation that is defined for adic complete rings and does not involve actual topology, it would be a good choice to establish the Teichmuller expansion using it.

[Anatole Dedecker]

I'm not familiar with the mathematics here, but probably you can declare each topology in a namespace, and then hide the use of the p-adic topology inside a concrete definition wich makes no reference to a topology. This is what @Antoine Chambert-Loir is doing for power series substitution in an ongoing series of PRs: the substitution is defined by performing an infinite sum in an appropriate topology, but once we will have the definition we will be able to talk about substitutions without mentioning topologies anymore.

[Jiang Jiedong]

Anatole Dedecker said:

I'm not familiar with the mathematics here, but probably you can declare each topology in a namespace, and then hide the use of the p-adic topology inside a concrete definition wich makes no reference to a topology.

Thank you! I'll try this!

[Anatole Dedecker]

Jiang Jiedong said:

To be more precise, given a sequence of p-adic integers $a_n$, and condition that the multiplicative valuation $v(a_n) \to 0$, what is the best way to define the summation of these elements in $\mathbb{Z}_p$? What about $a_n \in \mathbb{Q}_p$?

Coming back to this precise example, $\mathbb{Z}_p$ and $\mathbb{Q}_p$ do come with their topology, so you can use docs#NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero. In your general setup, this will probably be used to develop the API.

[Antoine Chambert-Loir]

When coefficients of your power series are in $\mathbf Z_p$, what is already done for evaluation of power series in #15019 will freely allow you to evaluate them at elements of $p\mathbf Z_p$ (once you have proved that they are topologically nilpotent). And some API is given to show that $f\mapsto f(a)$ is a morphism of algebras.

[Antoine Chambert-Loir]

The generality of #15019 is that of complete Hausdorff algebras which have a linear topology.
But this will say nothing for coefficients in $f\in \mathbf Q_p[[T]]$ and $a\in\mathbf Q_p$. Then, one has to define radius of convergence, and prove the necessary analysis.

[Junyan Xu]

docs#FormalMultilinearSeries.hasFPowerSeriesOnBall probably relevant, see also docs#AnalyticAt

[Antoine Chambert-Loir]

Note that those fancy rings, powerseries or witt vector, may carry various natural topologies, hence no instance should be declared globally. For power series, there is the product topology which is accessed using open scoped PiTopology, but there is the also the X-adic topology, and it's not the same in general.

[Anatole Dedecker]

It is in the univariate case and when the scalar ring is discrete, right?

[Antoine Chambert-Loir]

The difficulty for evaluation or substitution of power series is that it is not well defined everywhere and choices. The evaluation in complete Hausdorff linear topologies is well behaved on a subspace of tuples (each coordinate should be topologically nilpotent, and they have to tend to 0 if there are infinitely many indeterminates). Outside of this, we define evaluation as 0. Now, proving algebraic relations is rapidly a mess.

[Antoine Chambert-Loir]

Anatole Dedecker said:

It is in the univariate case and when the scalar ring is discrete, right?

If I'm not mistaken, the condition is discrete scalars and finitely many coefficients. (This is not yet proved, but not so hard.)