Zulip Chat Archive
Stream: condensed mathematics
Topic: isometry
Johan Commelin (May 25 2021 at 15:59):
Do we have somewhere that if f is an iso in SemiNormedGroup then f.hom is an isometry iff and only iff f.inv is?
Johan Commelin (May 25 2021 at 15:59):
I think this will be helpful for the canonical isom that I'm working on.
Adam Topaz (May 25 2021 at 15:59):
I have something like this...
Adam Topaz (May 25 2021 at 15:59):
Take a look at strict_iso
Adam Topaz (May 25 2021 at 16:00):
In prop819/strict_complex_iso
Adam Topaz (May 25 2021 at 16:00):
I should probably refactor that to use isometry at some point...
Adam Topaz (May 25 2021 at 16:02):
This strict_iso structure might just be enough for your canonical isomorphism
Johan Commelin (May 25 2021 at 16:11):
I see. But I'm fairly quickly reducing to an iso of simplicial profinite sets.
Last updated: Dec 20 2023 at 11:08 UTC