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