A formal characterization of discrete condensed objects

Stream: maths

[Dagur Asgeirsson]

I have a new preprint "A formal characterization of discrete condensed objects" https://arxiv.org/abs/2410.17847

It's about the subtle notion of discreteness in condensed mathematics, and provides a few conditions characterizing condensed sets/modules as discrete. All results are formalized and in mathlib.

(For those who were in Banff last year, it's a greatly improved version of the stuff I talked about there.)

Comments are very welcome!

[Ruben Van de Velde]

You might want to change "Omitting the proof of naturality (mathilb-link)," on page 16

[Dagur Asgeirsson]

Oops, thanks!

[Dagur Asgeirsson]

Stupid typo "mathilb" made this slip through...