Proving that profinite spaces form a site I am trying to prove that the category of profinite spaces with families of finite jointly surjective maps as covers is a site (in an attempt to understand condensed sets).
The category would be all profinite spaces (Hausdorff, maximally disconnected and compact) and on a profinite space $X$, the covers on it would be any family of $(f_i : S_i \to X)_{i \in I}$ such that $\cup _{i \in J} f_i (S_i) = X$ for some finite $J \subseteq I$.
Clearly, ${\rm Hom}(-, X)$ would be a cover. I am struggling with the two other conditions to ensure it is a site.

*

*We need that if $S$ is a covering sieve on $X$, pullback by any function $Y \to X$ is also a covering sieve. It seems to me like you must somehow use the finite set of spaces that surject onto $X$ to get morphisms that surject onto $Y$. I tried using the fact that maps between compact Hausdorff spaces are quotient maps but I am stuck.


*We need that if $T$ is a sieve on $X$, $S$ is a covering sieve on $X$ and the pullback of $T$ by any function in $S$ is a covering sieve then $T$ is a covering sieve. I also have no idea how to prove this part.
 A: To avoid thinking about the huge sieves, it suffices to check that the class $\mathcal{T}'$ of finite covering families which generate them form a stable class; see Definition 2.2 in my recent preprint. Incidentally, that paper might have some handy facts about the resulting compactly generated topos that you can use.
The singleton families consisting of the identity maps are certainly in $\mathcal{T}'$. Since your covering families are defined to be jointly epimorphic, they are closed under multicomposition (finite covers of finitely many spaces covering $X$ assemble into a finite family covering $X$). If I'm not mistaken, a pullback of profinite spaces is profinite, so that given a covering family $\{f_i:Y_i \to X\}_{i \in I}$ on $X$ and a map $g:X' \to X$, we can simply pull back the $f_i$ along $g$ to obtain a covering family on $X'$ whose multicomposition with $g$ is contained in the original family. That's everything! $\mathcal{T}'$ is a stable class.
Incidentally, note that by pulling back the pairs of morphisms in a finite covering family on $X$, we produce a diagram of profinite spaces of which $X$ is the colimit, and this diagram is final in the covering sieve generated by this family, so all of the covering sieves are effective epimorphic. Moreover, since any jointly epimorphic family over a compact space has a finite covering subfamily, we've just indirectly shown that this is all of the effective epimorphic sieves, and that they are stable under pullback. So this topology coincides with the canonical topology on this category, and the canonical functor $\mathbf{Prof} \to \mathrm{Sh}(\mathbf{Prof},J_c)$ is full and faithful.
PS. I wrote this answer quickly. It relies on some facts which you should check, such as:

*

*Profinite spaces are stable under pullback

*Epimorphisms in the category of profinite spaces coincide with epimorphisms of topological spaces, which is to say surjective maps.

*That diagram has $X$ as a colimit (hint: the colimit in the category of topological spaces certainly exists; check that it's $X$!)

Since these issues are purely topological in nature, they might be more accessible to you. Good luck, and let me know if it turns out I've slipped up in there somewhere.
