Zulip Chat Archive

Stream: condensed mathematics

Topic: pseudo normed abelian groups

view this post on Zulip Kevin Buzzard (Apr 04 2021 at 16:03):

Is it going to be a problem that we have defined pseudo normed abelian groups to be abelian groups (i.e. types plus a group structure), whereas on p66 of analytic.pdf after the proof of Prop 9.10 Peter defines them in an arbitrary topos?

view this post on Zulip Peter Scholze (Apr 04 2021 at 19:57):

It shouldn't be a problem for the intended application of the notion; Johan has formalized "profinitely filtered pseudo normed abelian groups" which is the relevant kind of internal example (a special kind of pseudo normed abelian groups internally in condensed sets)

Last updated: May 09 2021 at 22:13 UTC