non-archimedean rings

Stream: maths

[Kevin Buzzard]

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]

interesting concept. Pretty sure it's not in mathlib

[Mario Carneiro]

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

[Kevin Buzzard]

/me renames nonarchimedean_ring.lean to nonarchimedean_group.lean

[Mario Carneiro]

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

[Kevin Buzzard]

yup

[Kevin Buzzard]

there are a lot of people who aren't Archimedes

[Kevin Buzzard]

it's pretty grim notation to be honest

[Kevin Buzzard]

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

[Mario Carneiro]

two?

[Kevin Buzzard]

I think so

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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]

that well known nonarchimedean ring

[Mario Carneiro]

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]

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

[Kevin Buzzard]

/me renames nonarchimedean_group.lean to nonarchimedean_ring.lean