Zulip Chat Archive

Stream: condensed mathematics

Topic: profinite sets are limits of discrete finite sets

view this post on Zulip Calle Sönne (Feb 17 2021 at 18:33):

On the Profinite2 branch I have formalized that profinite sets are limits of finite discrete sets. "Only" ~500 lines. I will start splitting this up into a bunch of smaller PRs soon. Meanwhile, Im looking at Proposition 1.7 in the Condensed mathematics notes as a potential next goal. What was the consensus for what we should do about cardinal bounds? I recall someone (maybe Kevin) saying that we could ignore them by working in a higher universe or something?

view this post on Zulip Johan Commelin (Feb 17 2021 at 18:36):

Yup, ignore the set-theoretic issues (for now).

view this post on Zulip Kevin Buzzard (Feb 17 2021 at 18:42):

I am right now very much into the "blunder on, ignoring set-theoretic issues" attitude. Occasionally we might have to go all etale cohomology of diamonds section 4 in order to manage some issue, but honestly I think these things are the least of our problems right now.

Last updated: May 09 2021 at 22:13 UTC