Zulip Chat Archive

Stream: condensed mathematics

Topic: normed group todo


Johan Commelin (Mar 22 2022 at 13:28):

Here's a standalone bit that needs to be done: https://leanprover-community.github.io/liquid/sect0010.html#normed-to-cond
Every normed group VV is a topological group, hence condensed: V(S)V(S) is the collection of continuous maps SVS → V.
But there is another description of this condensed abelian group: V(S)V(S) is also the completion of the group of locally constant maps SVS → V, for the sup-norm.
We need to know that the two points of view are equivalent.


Last updated: Dec 20 2023 at 11:08 UTC