Zulip Chat Archive

Stream: condensed mathematics

Topic: Exactness for Cech complex


Adam Topaz (Apr 23 2021 at 02:13):

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:XBf : X \to B. Obviously ff has a splitting, say σ:BX\sigma : B \to X.
Form the Cech nerve C(f)C(f). This is a simplicial object whose nn-term is X×BX×B×BXX \times_B X \times_B \cdots \times_B X (n+1 times), and there is an augmentation C(f)BC(f) \to B where BB denotes the constant simplicial object with value BB. We need to prove that the complex induced by C(f)C(f) (the alternating-face-map complex):

0M^(B)M^(X)M^(X×BX) 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 M^(C(f)n+1)M^(C(f)n)\hat M(C(f)_{n+1}) \to \hat M(C(f)_n) arising from applying M^\hat M (a contravariant functor) to one map C(f)nC(f)n+1C(f)_n \to C(f)_{n+1} (one for each nn). The issue is that I'm failing to explicitly describe this single map C(f)nC(f)n+1C(f)_n \to C(f)_{n+1} in terms of σ\sigma. What am I missing?

Adam Topaz (Apr 23 2021 at 03:34):

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

Peter Scholze (Apr 23 2021 at 07:43):

That sounds right

Peter Scholze (Apr 23 2021 at 07:44):

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

Johan Commelin (Apr 23 2021 at 07:49):

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

Johan Commelin (Apr 23 2021 at 07:49):

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

Adam Topaz (Apr 25 2021 at 19:33):

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 (Apr 25 2021 at 19:33):

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


Last updated: Dec 20 2023 at 11:08 UTC