Condensed.pdf Thm 3.3

Stream: condensed mathematics

[David Michael Roberts]

Someone on MO is wondering about the first line of the proof , which says

Assume first that $S$ and all $S_i$ are finite. Then the hypercover splits, ...

https://mathoverflow.net/questions/430481/hypercovers-consisting-of-finite-sets

In particular the user seems to have a counterexample under the assumption that "splits" here means it's a split hypercover as usually stated. But was there another meaning of 'split' it could be? The notes don't help. Has this been formalised in LTE?

[Kevin Buzzard]

Thanks for flagging this David!

[Adam Topaz]

In LTE, we only had to do this for the Cech nerve of a map f, in which case the splitting boils down to splitting f.

[Adam Topaz]

Re the OPs counter example:
https://stacks.math.columbia.edu/tag/017R

[Joël Riou]

split simplicial objects are now in mathlib (docs#simplicial_object.splitting). I shall use this for the Dold-Kan correspondence, and I am also working on the skeletal filtration of split simplicial objects (e.g. simplicial sets).

[Adam Topaz]

In any case, I think what Z. M says in the comments is correct.

[Joël Riou]

Indeed, the "splitting of hypercovers" in Scholze's notes might be related to the notion of extra degeneracy on augmented simplicial objects (see PR #16411)

[David Michael Roberts]

My assumption was that 'splitting' here meant in the sense that there was a suitable family of sections, just from the vibe of the thing, so it's good to know my intuition was correct. If this is, additionally, only being applied to a Cech nerve rather than a general hypercover, then I guess this would be good to point out explicitly.

[Reid Barton]

In my world, the normal terminologies are "free degeneracies" or "split degeneracies", and "extra degeneracies".

[Kevin Buzzard]

It's a great opportunity for someone to answer explicitly referencing what we do in LTE. There will be plenty of people who are still unaware that all this stuff has been typed into a proof checker and posting links to lean code is a good way of promoting the project

[Johan Commelin]

Except that the corresponding Lean code is probably very hard to parse.

[Kevin Buzzard]

So in the answer you explain it

[Kevin Buzzard]

People searching for condensed mathematics are going to run into this question

[Kevin Buzzard]

Unfortunately I'm organising a conference next week and another conference the week after so I'm a bit snowed under at the minute, but an answer of the form "don't worry, this line of computer code checks that the paper is ok, I know it's written in code, here's a brief human-readable summary of what it means" is the kind of answer which makes people go "wow what the heck is going on in the lean community, what they're doing looks pretty amazing" and will also be highly ranked in search engines

[Kevin Buzzard]

"Don't worry, there is definitely nothing wrong here" is exactly what we are offering to the mathematical community right now. The question deserves a Lean answer. It's just unfortunate that I'm not in a position to give it right now

[Johan Commelin]

Okokok, you convinced me :wink:

[Adam Topaz]

What we did for this (again, only with the Cech nerve) is mostly in src\prop819.lean (there is some general Cech-stuff in the for_mathlib folder as well).

[Adam Topaz]

The file for_mathlib/Cech/{split,homotopy} is where the exactness of the associated complex is done, assuming a splitting.

[Adam Topaz]

Johan, are you planning to post an answer on MO? If not, then I could (but it's 4am here, so that won't happen for a little while).

[Adam Topaz]

The blueprint proof is actually fairly detailed in this case:
https://leanprover-community.github.io/liquid/sect0004.html#cechcover-exact

[Johan Commelin]

@Adam Topaz Please go ahead! You wrote the Lean code, so I think it makes sense that you answer.

[Adam Topaz]

I hope I didn't say anything stupid :)

[Adam Topaz]

https://mathoverflow.net/a/430595/490721

[Kevin Buzzard]

Thanks so much Adam!