Stream: condensed mathematics
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?
Johan Commelin (Feb 17 2021 at 18:36):
Yup, ignore the set-theoretic issues (for now).
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