Nonarchimedean norms / ultrametric spaces in general

Stream: maths

[Yakov Pechersky]

I've been thinking about formalizing evaluation of power series over nonarchimedean rings, following Gouvea and KConrad's notes. To do this, one needs to set up lemmas about the topology of balls (they're clopen) on nonarchimedean spaces, and lemmas about how finset sums and tsums behave and commute under norms.

We have several ways of referring to nonarchimedean rings in mathlib currently.

• Topologically nonarchimedean (docs#NonarchimedeanRing), that is, continuous ring ops and that neighborhoods of 0 contains open additive subgroups; evident that nonarchimedean norm implies this, not obvious (to me) the reverse implication
• docs#IsNonarchimedean, a proposition on arbitrary functions to the reals, used in docs#NormedField.toValued
• docs#Valued, a typeclass that extends docs#UnformAddGroup
• docs#WithIdeal (a typeclass) which installs a UniformAddGroup and NonarchimedeanRing via docs#Ideal.adicTopology
• docs#NonarchAddGroupNorm, which is a structure bundling the strong triangle inequality etc

I've also started a PR #14433 adding IsUltrametricDist, a mixin on (pseudo)metric spaces asserting the strong triangle inequality, and further, a local branch where that mixin on NormedAddCommGroup and friends allows for statements like that the image of Z are norm <= 1.

There are also papers on generalizing a nonarchimedean nature to uniform spaces and that under the right assumptions, topological nonarchimedean groups imply an ultrametric in metrizable spaces.

Given our general propensity of setting things up in the right generality and having one consistent way to set things up, what is the desired way to specify a type such that something like Strassman's theorem can be stated and proved? Gouvea provides a proof that doesn't require the p-adic Weierstrass preparation theorem.

Some of these options evidently imply another one, but possibly with the need to set up some general theory linking them. So, if one wants to state and prove that two formal series over a nonarchimedean foo that have the same derivative on a disk of convergence must differ only by a constant on that disk, what should the typeclass on the type be?

[Yakov Pechersky]

/poll Ultrametric / nonarchimedean typeclass
NonarchimedeanUniformity (mixin on UniformSpace)
IsUltrametricDist (mixin on Dist)
NonarchimedeanNormed (mixin on Norm)
Fact (IsNonarchimedean (norm : K -> R))

[Yakov Pechersky]

cc @Filippo A. E. Nuccio , @María Inés de Frutos Fernández , @Mitchell Lee who have done a lot of work setting up the existing classes.

[Mitchell Lee]

I think IsUltrametricDist is right, but that NonarchimedeanUniformity should also exist.

[Mitchell Lee]

Also, I think that a normed group can be nonarchimedean as a uniform space without the norm being nonarchimedean.

[Johan Commelin]

cc @Antoine Chambert-Loir who already did a bunch on evaluation of power series

[Antoine Chambert-Loir]

Yes, @María Inés de Frutos Fernández and I have formalized evaluation maps to complete Hausdorff linearly topologized algebras , following Bourbaki, Algebra, chapter IV, §4. This is not yet PRed to Mathlib but can be found in the GitHub repository for our Divided power project.

[Antoine Chambert-Loir]

Then we do substitution of power series.

[Antoine Chambert-Loir]

(In fact we slightly differ from Bourbaki because we consider a different, possibly stronger, topology on power series which takes into account a given topology on the ring of coefficients. Bourbaki takes the discrete topology.)

[Yakov Pechersky]

Cool! Is it here? https://github.com/AntoineChambert-Loir/divided_powers

[Yakov Pechersky]

Can I work on moving some of the mv_power_series topology to mathlib? And include a specialization to plain power series? Do you have a preference for how to indicate the nonarchimedean nature of the ring of coefficients?

[Filippo A. E. Nuccio]

Let me also ping @Sophie Morel who worked on this in Lyon.

[Antoine Chambert-Loir]

Its at https://github.com/AntoineChambert-Loir/DividedPowers4
Regarding moving this to mathlib, why not, if @María Inés de Frutos Fernández agrees.

[Antoine Chambert-Loir]

The topological condition on the target ring that allows for the evaluation is IsLinearTopology.

[Yakov Pechersky]

Regarding defining eval via a topology on the mv power series itself and inducing from polynomial eval, how does that contrast vs showing that they're a completion first? Or ever defining it directly as a tsum of coeff n * x ^ n instead of that being propositionally equal?

[Antoine Chambert-Loir]

Then you're preparing yourself to redo all the classic job of extending partial maps which are uniformly continuous, etc