MO question

Stream: condensed mathematics

[Kevin Buzzard]

I'm in a talk right now but I just spotted this new MO question https://mathoverflow.net/questions/429809/condensed-mathematics . Is it possible to give an answer of the form "we checked this in Lean, here it is"?

[Johan Commelin]

Yes, Adam did this. Let me try to find it.

[Johan Commelin]

I can't promise it is readable.

[Yuyang Zhao]

"If you know about Lean, here is the full formal verification where you can check all the details"?

[Johan Commelin]

I think https://github.com/leanprover-community/lean-liquid/blob/master/src/condensed/extr/equivalence.lean#L311 is a statement that shows you don't need condition (ii) for sheaves on ExtrDisc.

[Riccardo Brasca]

It also seems almost readable!

[Riccardo Brasca]

I think this is the only mathematically relevant result (I've added a comment to the question).

[Adam Topaz]

I think rather the following is the relevant result:
https://github.com/leanprover-community/lean-liquid/blob/a1f009de0f88731492e998e4fd8f27de3f6952af/src/condensed/extr/basic.lean#L262

The proof just boils down to splitting the cofork diagram (which implies that the fork you get after applying the presheaf is again split, hence a coequalizer cofork).

[Johan Commelin]

Aah, good catch. I was looking in the wrong file.