Properties of non-archimedean rings

Stream: maths

[Mitchell Lee]

I am interested in formalizing some enumerative combinatorics in Lean. That means that I am going to be doing some algebra in the ring $\mathbb{Q}[\![t]\!]$ of formal power series. However, I am also making an effort to state the lemmas that I need in as as general a setting as possible, rather than merely stating them for power series rings. So I have the following questions. I know very little about non-archimedean geometry, so please go easy on me if some of these questions are stupid.

Let $R$ be a non-archimedean ring. By this I mean that $R$ is a topological ring and there is a neighborhood basis of $0$ consisting of open additive subgroups.

1. Assume that $R$ is complete. If a sequence $\{a_n\}_n$ of elements of $R$ tends to $1$ on the cofinite filter, does it follow that the product $\prod_{n} a_n$ converges unconditionally?
2. Is the topology on $R$ necessarily induced by an absolute value $|\cdot| \colon R \to \mathbb{R}_{\geq 0}$ which satisfies the ultrametric triangle inequality? (And if the answer is "no", is that just because $\mathbb{R}_{\geq 0}$ isn't "big enough" and there's some other totally ordered commutative semigroup that would work?)
3. Is there necessarily an open subring $R' \subseteq R$ such that there is a neighborhood basis of $0$ consisting of $R'$-submodules of $R$?

[Mitchell Lee]

Also, if the answer to any of these questions is "no", what is a reasonable extra assumption that I could add that would make the answer "yes"?

[Mitchell Lee]

Also, just to be clear, a big part of the reason I am asking these questions is simply that I'm curious.

[Johan Commelin]

(3) is close to being a "Huber ring". See https://math.stanford.edu/~conrad/Perfseminar/Notes/L5.pdf

[Mitchell Lee]

Thanks. It does seem that the first and the third of these properties hold for Huber rings. It is not clear to me whether the second one holds, but that one is probably the least important of the three for my purposes.

I don't know if it'd make sense for me to formalize the theory of Huber rings just so I can take some infinite products of power series, but this is good to know about regardless.

Are there any well-known examples of non-archimedean rings which are not Huber?

[Kevin Buzzard]

Is R assumed commutative?

[Mitchell Lee]

Yes

[Kevin Buzzard]

For 2 there's certainly examples where you need something bigger than NNReal (these might even be in mathlib) but I don't know any examples of nonarchimedean rings that aren't Huber so I'm not much help with these questions. I would imagine that if you have a norm to some totally ordered group with zero then the things of norm at most 1 give you 3.

[Mitchell Lee]

If you allow something bigger than NNReal, can you always do 2?

[Mitchell Lee]

Maybe I should ask this on stackexchange

[Kevin Buzzard]

Let's assume that there's a nonarchimedean ring which isn't Huber (and this doesn't sound unreasonable, or else why would the notion of Huber exist). Then you won't be able to do 2 because I think 2 will imply Huber.

[Mitchell Lee]

I see. That isn't clear to me, but it sounds reasonable. I guess you would take the ideal to be everything with absolute value less than 1, then.

[Kevin Buzzard]

Oh I'd forgotten about the fg ideal assumption. In the rank 1 case you don't do this because it might not be fg (consider C_p, where you use I=(p) ). Basically we need a good example of an Archimedean ring which isn't Huber before we can get a good feeling for these questions.

[Mitchell Lee]

What about something like a Puiseux series ring? It seems like that wouldn't be Huber. But I think it still satisfies all the properties I asked about, unless I am making a mistake.

[Mitchell Lee]

Oh, sorry, this is Huber

[Mitchell Lee]

I was just not using my imagination enough when considering what the ideal could be

[Antoine Chambert-Loir]

I'm not sure additive subgroups are enough. But ideals are. With @María Inés de Frutos Fernández , we formalized “LinearTopology” to mean that, we should PR it relatively soon.

[Antoine Chambert-Loir]

We also define a topology on docs#MvPowerSeries. There is one obvious choice there, taking the product topology, given a topology on the ring of coefficients — possibly the discrete topology. In this case, this is a linear topology, complete and Hausdorff, and the polynomials are dense in it (see Bourbaki, Algebre, Chap. 4, §5). We use that to define evaluation of/substitutions within power series.

[Mitchell Lee]

Thanks; that should be very useful. I've been waiting for the power series compositions.

[Mitchell Lee]

I know there are non-archimedean rings that are not linearly topologized; for example, any field. I guess my question comes down to "Does every non-archimedean ring have a linearly topologized open subring?"

[Mitchell Lee]

Also, I think there are two different reasonable choices for the topology on a multivariate power series ring: the product topology and the $I$-adic topology, where $I$ is the ideal generated by the variables. These happen to be the same when there are finitely many variables, so maybe it doesn't matter too much.

[Antoine Chambert-Loir]

In general, the I-adic topology is poorly behaved.