short exact skeleton

Stream: condensed mathematics

[Johan Commelin]

• I've developed an API for constructing short exact sequences of condensed abelian groups. This API is mostly sorry-free (modulo trivialities). It's in condensed/condensify.lean.
• In for_mathlib/derived/les_facts.lean I've put two lemmas about Ext groups being zero if other maps are isomorphisms, etc... These are sorrys, which will need the LES to prove them.
• I've used the API to build a skeleton for the short exact sequences that feature in the main proof. There are now dozens of rather elementary sorries that need to be filled in. About maps between profinitely filtered pseudo-normed groups, etc...

Sorry count:

3       src/condensed/rescale.lean
1       src/condensed/exact.lean
5       src/condensed/condensify.lean
1       src/Lbar/ext.lean
7       src/Lbar/ses.lean
1       src/breen_deligne/main.lean
5       src/breen_deligne/eval.lean
1       src/free_pfpng/main.lean
1       src/invpoly/basic.lean
2       src/laurent_measures/thm69.lean
3       src/laurent_measures/ext.lean
2       src/laurent_measures/ses2.lean
5       src/laurent_measures/ses.lean
5       src/for_mathlib/complex_extend.lean
32      src/for_mathlib/derived/derived_cat.lean
2       src/for_mathlib/derived/les_facts.lean
Total:  76

[Kevin Buzzard]

4 src/condensed/condensify.lean do I just push to master? It wasn't too hard :-)

[Johan Commelin]

The whole framework for short exact sequences of condensed abelian groups is done and applied.
Plenty of sorries left though:

1 src/free_pfpng/main.lean
1 src/free_pfpng/acyclic.lean
6 src/invpoly/ses.lean
3 src/invpoly/basic.lean
5 src/laurent_measures/ses.lean
2 src/laurent_measures/ext.lean
3 src/laurent_measures/ses2.lean
2 src/Lbar/ext.lean
5 src/for_mathlib/complex_extend.lean
8 src/Lbar/ses.lean
2 src/laurent_measures/thm69.lean
32 src/for_mathlib/derived/derived_cat.lean
2 src/for_mathlib/derived/les_facts.lean
1 src/breen_deligne/main.lean
5 src/breen_deligne/eval.lean
1 src/condensed/exact.lean
3 src/condensed/rescale.lean
4 src/condensed/condensify.lean
86 total

[Damiano Testa]

I just removed a sorry from Lbar.ses, and pushed it.

[Johan Commelin]

Thanks!