I have a little technical question on Peter Scholze's [lectures on condensed mathematics](https://www.math.uni-bonn.de/people/scholze/Condensed.pdf).


On page 12, right above the Proof of Theorem 2.2, he says that for extremally disconnected sets the condition (ii) on page 7 is automatic. I can't see why. I understand that the map is injective under the presence of sections, but why is it surjective?


This assertion is then used in the proof of Theorem 2.2 and I guess, it was the reason for introducing extremally disconnected spaces here, so I believe that it is true, but I just can't see why.



Condensed mathematics
The key point is to use the fact that extremally disconnected sets are projective (in the category of compact Hausdorff spaces) to note the coequalizer diagram involved in the analogue of condition (ii) is a [*split* coequalizer.](https://ncatlab.org/nlab/show/split+coequalizer)


I'll explain some additional details in the next paragraphs, but first it's worthwhile to note that there is a small subtlety in formulating the analogue of condition (ii) because the pullback of extremally disconnected sets need not be extremally disconnected. Rather, you can always find an extremally disconnected presentation of the pullback.


So one way to formulate the analogue of condition (ii), for a presheaf $T$ on the category of extremally disconnecteds, is as follows:
For all surjective morphisms $X \to B$ of extremally disconnected sets, and all surjective morphisms $R \to X \times\_B X$ where $R$ is extremally disconnected (and the pullback is computed in $\mathrm{CompHaus}$, say), the corresponding diagram
$$T(B) \to T(X) \rightrightarrows T(R)$$
is an equalizer diagram.


This diagram is obtained by applying $T$ to the coequalizer diagram
$$R \rightrightarrows X \to B,$$
where the two maps $R \to X$ are the compositions of $R \to X \times\_B X$ with the two projections.


To see that the first diagram is a (split) equalizer, it suffices to show that the second is a split coequalizer.
We can construct such a splitting as follows.
First, since $\pi : X \to B$ is surjective, and $B$ is projective, we can find a splitting $\sigma : B \to X$, so that $\pi \circ \sigma = 1$.
Next, consider the map $X \to X \times\_B X$ whose composition with the first projection to $X$ is the identity and whose composition with the second projection is $\sigma \circ \pi$ (since $\sigma$ is a splitting of $\pi$, the two maps to $B$ do indeed coincide, so we get such a map from the universal property of the pullback).
Now the map $R \to X \times\_B X$ is surjective and $X$ is projective, so we can lift this map $X \to X \times\_B X$ to a map $\tau : X \to R$ with the property that the compositions $X \to R \to X\times\_B X \to X$ are $1$ and $\sigma\circ\pi$ respectively.
The two maps $\sigma$ and $\tau$ then give us the desired splitting of the coequalizer diagram.


Finally, to add to the comments on the original question, this was formalized in Lean (as part of the Liquid Tensor Experiment) as the following lemma:
<https://github.com/leanprover-community/lean-liquid/blob/a1f009de0f88731492e998e4fd8f27de3f6952af/src/condensed/extr/basic.lean#L262>


