Exactness for Cech complex

Stream: condensed mathematics

[Adam Topaz]

Hi everyone,

I'm thinking about how to prove the first step of 8.4 from the blueprint aka 8.19 from analytic.pdf aka (essentially) the first step of 3.3 from condensed.pdf

The situation is this: we have a surjective map of finite sets $f : X \to B$. Obviously $f$ has a splitting, say $\sigma : B \to X$.
Form the Cech nerve $C(f)$. This is a simplicial object whose $n$-term is $X \times_B X \times_B \cdots \times_B X$ (n+1 times), and there is an augmentation $C(f) \to B$ where $B$ denotes the constant simplicial object with value $B$. We need to prove that the complex induced by $C(f)$ (the alternating-face-map complex):

$0 \to \hat M(B) \to \hat M(X) \to \hat M(X \times_B X) \to \cdots$

is exact (in a strong sense, see below).

I'm fairly sure I see how to get the exactness using $\sigma$ explicitly, but it seems that one needs the stronger assertion that there is a contracting homotopy $\hat M(C(f)_{n+1}) \to \hat M(C(f)_n)$ arising from applying $\hat M$ (a contravariant functor) to one map $C(f)_n \to C(f)_{n+1}$ (one for each $n$). The issue is that I'm failing to explicitly describe this single map $C(f)_n \to C(f)_{n+1}$ in terms of $\sigma$. What am I missing?

[Adam Topaz]

Hmm... playing around a bit, I think the correct maps $C(f)_n \to C(f)_{n+1}$ are something approximately like
$(x_0,\ldots,x_n) \mapsto (\sigma(f(x_0)),x_0,x_1,\ldots,x_n)$
where one identifies $C(f)_n$ with a subset of the $n+1$-fold product of $X$. Is this correct?

[Peter Scholze]

That sounds right

[Peter Scholze]

(I will also get some signs and indices wrong, but modulo such problems this is right.)

[Johan Commelin]

@Adam Topaz Thanks for starting on 8.19! This feels like we're starting the final attack!

[Johan Commelin]

There is still a lot to be done (Gordan, polyhedral lattice quotients, homotopy glue, random sorries). But still, this is really exciting.

[Adam Topaz]

A quick update: The first part (well, the first part of the first part) of 8.19 is now done.
The contracting homotopy is here:
https://github.com/leanprover-community/lean-liquid/blob/c8ba3b56a2691ab5798cc1f59a4689cbec8c2cfe/src/for_mathlib/cech/contracting_homotopy.lean#L52

[Adam Topaz]

This is stated in a more general form, for any functor into a preadditive catetgory from a category where tthe Cech nerve makes sense.