## Stream: maths

### Topic: non-archimedean rings

#### Kevin Buzzard (Mar 09 2019 at 21:08):

A topological ring is non-archimedean if every open neighbourhood of 0 contains an open subgroup. Do we have non-archimedean rings in mathlib? @Patrick Massot @Patrick Massot did you need these for ring completion?

#### Mario Carneiro (Mar 09 2019 at 21:19):

interesting concept. Pretty sure it's not in mathlib

#### Mario Carneiro (Mar 09 2019 at 21:20):

quibble: isn't that a property of topological groups?

#### Kevin Buzzard (Mar 09 2019 at 21:40):

/me renames nonarchimedean_ring.lean to nonarchimedean_group.lean

#### Mario Carneiro (Mar 09 2019 at 21:46):

also doesn't nonarchimedean mean at least two other things, even if you put "ring"/"group" at the end?

yup

#### Kevin Buzzard (Mar 09 2019 at 21:46):

there are a lot of people who aren't Archimedes

#### Kevin Buzzard (Mar 09 2019 at 21:47):

it's pretty grim notation to be honest

#### Kevin Buzzard (Mar 09 2019 at 21:47):

and there are nonarchimedean norms, nonarchimedean valuations, and two areas called nonarchimedean analysis

two?

I think so

#### Kevin Buzzard (Mar 09 2019 at 21:48):

I once met someone who said "do you know something about nonarchimedean analysis?" and I said "yes, I'm kind of an expert in that"

#### Kevin Buzzard (Mar 09 2019 at 21:48):

and then they asked me a bunch of questions I couldn't understand at all

#### Kevin Buzzard (Mar 09 2019 at 21:48):

and it turned out that they meant another kind of nonarchimedean analysis

#### Kevin Buzzard (Mar 09 2019 at 21:50):

I'm not sure I can find anything online about the other kinds. The kind I know something about is Banach spaces over fields complete with respect to a non-trivial nonarchimedean norm, like the p-adic numbers

#### Kevin Buzzard (Mar 09 2019 at 21:50):

that well known nonarchimedean ring

#### Mario Carneiro (Mar 09 2019 at 21:52):

From googling it looks like the only people who care about nonarchimedean rings in this sense also care about Huber rings and perfectoid spaces, so maybe it's best staying in the perfectoid project

#### Mario Carneiro (Mar 09 2019 at 21:52):

wiki doesn't have an entry on it that I can find

#### Kevin Buzzard (Mar 09 2019 at 21:53):

/me renames nonarchimedean_group.lean to nonarchimedean_ring.lean

Last updated: May 09 2021 at 11:09 UTC