Zulip Chat Archive

Stream: PR reviews

Topic: Discrete condensed objects #14027 #15321 #15566 #15569

Dagur Asgeirsson (Sep 19 2024 at 13:48):

My PR #14027 gives a characterization of discrete condensed sets and modules (both in the light and the "classical" setting). All preliminary refactors and additions are now merged and the proper content of this can now finally be reviewed.

It depends on:
#15321 which is now ready for review. This proves that the sections of a discrete condensed set are given by locally constant maps.
#15566 which proves that discreteness of condensed sets can be stated in terms of preserving certain filtered colimits.
#15569 which relates discreteness of a condensed module with discreteness of the underlying condensed set.

#15566 and #15569 are mutually independent but both depend on #15321.

Finally, #14027 puts everything together in big tfae statements.

Each PR is about 400 lines, a bit big but it doesn't make sense to split them up further. Hopefully not too bad. Reviews welcome!

Johan Commelin (Sep 19 2024 at 15:49):

I left a minor comment on the locally-constant PR. But basically LGTM.

Dagur Asgeirsson (Sep 20 2024 at 10:07):

Thanks! I applied the suggestion and shortened some more names.

Dagur Asgeirsson (Sep 23 2024 at 12:43):

:ping_pong: @Johan Commelin

Johan Commelin (Sep 24 2024 at 05:56):

I kicked #15321 on the queue

Dagur Asgeirsson (Sep 26 2024 at 09:29):

#15569 is now ready for review, #15566 will be ready shortly after I've done some cleanup

Dagur Asgeirsson (Sep 26 2024 at 10:51):

#15566 is ready for review!

Dagur Asgeirsson (Oct 04 2024 at 09:01):

As suggested by @Johan Commelin, I've added a bunch of API lemmas to #15566. It now depends on three small PRs #17380, #17381, #17383, and the original file has grown quite a bit.

#15569 remains ready for review as well.