Zulip Chat Archive

Stream: condensed mathematics

Topic: topology on a valued ring


view this post on Zulip Kevin Buzzard (Dec 08 2020 at 18:04):

There is a bunch of stuff in the perfectoid project which needs to be ported to mathlib -- this is true independent of the challenge. Patrick and I are currently working on porting some stuff about the topology on a ring induced by a valuation. One should really do this properly so the proposal is to port a whole bunch of perfectoid stuff about topologies on groups induced by filter bases at 1 which play well with respect to the group structure.


Last updated: May 09 2021 at 15:11 UTC