9.4 for profinite S

Stream: condensed mathematics

[Johan Commelin]

To derive 9.4, there is one crucial place where we currently use that S is finite, namely 9.8. All the other stuff doesn't care about S.
I'm now thinking about how to generalize to profinite S.

The first 4 lines of the proof of 9.8 show how to prove it for profinite S. So we can do that, and then 9.4 for profinite S will follow. My impression is that this is the easiest way. (@Peter Scholze did you have a different path in mind for LTE, when it comes to reducing 9.4 for profinite S to the finite case?)

[Peter Scholze]

Johan Commelin said:

To derive 9.4, there is one crucial place where we currently use that S is finite, namely 9.8. All the other stuff doesn't care about S.
I'm now thinking about how to generalize to profinite S.

The first 4 lines of the proof of 9.8 show how to prove it for profinite S. So we can do that, and then 9.4 for profinite S will follow. My impression is that this is the easiest way. (Peter Scholze did you have a different path in mind for LTE, when it comes to reducing 9.4 for profinite S to the finite case?)

There are two paths: a) as in the manuscript, directly deal with profinite $S$, which only requires a small extra step in 9.8; b) formally deduce 9.4 for profinite $S$ from 9.4 for finite $S$ by passing to a limit and using that weak exactness behaves well under passing to filtered colimits and passing to completions.

I originally presumed you would be taking path b). But you might as well take path a) if that's less trouble.