Zulip Chat Archive

Stream: maths

Topic: non-archimedean rings


view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Mar 09 2019 at 21:19):

interesting concept. Pretty sure it's not in mathlib

view this post on Zulip Mario Carneiro (Mar 09 2019 at 21:20):

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

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:40):

/me renames nonarchimedean_ring.lean to nonarchimedean_group.lean

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:46):

yup

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:46):

there are a lot of people who aren't Archimedes

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:47):

it's pretty grim notation to be honest

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:47):

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

view this post on Zulip Mario Carneiro (Mar 09 2019 at 21:47):

two?

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:48):

I think so

view this post on Zulip 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"

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:48):

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

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:48):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 09 2019 at 21:50):

that well known nonarchimedean ring

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 09 2019 at 21:52):

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

view this post on Zulip 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