Stream: condensed mathematics
Topic: topology on a valued ring
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