Hypercovers consisting of finite sets In this paper
on Page 21, the first line of the proof, Peter Scholze seems to claim that any hypercover, consisting of finite sets, splits. I find this hard to believe.
I am not familiar with categorical topology, but let's consider the constant simplicial set, where you map all simplices to a point and all arrows to the identity. It seems to me that this is a counterexample, is it not? And if not, why is Scholze's claim true?
EDIT: I need to explain my question a bit:
According to this source, a simplicial object $U_\bullet$ splits if for every $n$ there exists a subobject $NU_n$ of $U_n$ such that the map
$$
\coprod_{\phi:[n]\twoheadrightarrow [m]}NU_m\to U_n
$$
is an isomorphism. In my example we have $U_n=*$ the one pointed set. It has exactly two subobjects, the empty set or the point. The subobject cannot be the empty set, because then the coproduct (=disjoint union) would be empty, too. So it has to be $*$. In wich case we get an isomorphism between the coproduct of several copies of $*$ and $*$, which is absurd.
 A: Here is a summary of the discussion in the comments, as well as a few additional details.
First, the notion of "split hypercover" used by Clausen-Scholze in Condensed.pdf is what some people call "having extra degeneracies."
Explicitly, if $X_\bullet$ is a hypercover of $X_{-1}$, this condition asks for maps $\sigma : X_i \to X_{i+1}$, for $i \geq -1$, satisfying identities which are spelled out here (see Prop 3.3) or in this paper.
The notion of a split simplicial object from the stacks project (linked in the question) is different, and is sometimes called "having split degeneracies."
Any simplicial set satisfies this property -- see this lemma.
I will use the "extra degeneracies" notion below.
Let's say that $X_i$ are objects of a category $C$ and that $F : C \to A$ is a functor to an abelian category. One obtains the alternating face-map complex
$$ \cdots \to F(X_{i+1}) \to F(X_i) \to \cdots \to F(X_0) \to F(X_{-1}) \to 0.$$
It is relatively straightforward to see that $F(\sigma_i) : F(X_i) \to F(X_{i+1})$ yield a contracting homotopy of this complex, and thus the complex is exact (the caclulations here boil down to the identities for the extra degeneracies listed in the links above).
One can also phrase this using simplicial homotopy -- see the paper mentioned above.
To see why such a splitting always exists in the case where $C$ is the category of finite sets (and "covers" = "surjections"), one could argue as hinted to by Denis Nardin in the comments.
The hypercover condition says that $X_0 \to X_{-1}$ and the maps induced by the coskeleton adjunction
$$X_{n+1} \to (\operatorname{cosk}_n (\operatorname{sk}_n(X_\bullet)))_{n+1}$$
are all surjections.
One defines the maps for the splitting $\sigma_n$ by induction on $n$, starting with a splitting $\sigma_{-1} : X_{-1} \to X_0$ of the surjection $X_0 \to X_{-1}$.
The $(n+1)$-th component of the coskeleton is a certain (finite) limit, and one can obtain a map $X_n \to (\operatorname{cosk}_n (\operatorname{sk}_n(X_\bullet)))_{n+1}$ which satisfies the necessary identities (which involve the previously obtained $\sigma$'s) for the extra degeneracies by encoding these conditions in the various projections involved in this limit.
Since $X_{n+1}$ surjects onto this limit, we can lift the map above to a map $\sigma_n : X_n \to X_{n+1}$. The $\sigma_n$ will then be a splitting of this hypercover.
We can make this more explicit in the the case where $X_\bullet$ is the Čech hypercover associated to a surjection $f : X \to B$.
In this case it suffices to split $f$ itself.
Indeed, here we have $X_n = X \times_B \cdots \times_B X$ (with $n+1$ factors of $X$ appearing).
Since $f : X \to B$ is surjective, we can split it by some $\sigma : B \to X$.
Take $\sigma_n : X_n \to X_{n+1}$ to be the map
$$ (x_0,\ldots,x_n) \mapsto (\sigma(f(x_0)),x_0,\ldots,x_n). $$
These $\sigma_n$ then define a splitting of $X_\bullet$.
Splitting the Čech hypercovers was another result that was needed for the liquid tensor experiment. You can find a formalization of the contracting homotopy of the associated complexes here.
An argument similar to Theorem 3.3 from Condensed.pdf, which was needed for the formalization of Proposition 8.19 from Analytic.pdf, for Čech hypercovers, is formalized here.
Unfortunately, these files might be hard to read without prior Lean experience, but the proof is written in some detail in the blueprint for the liquid tensor experiment.
