complexes indexed by N

Stream: condensed mathematics

[Johan Commelin]

With the new approach to complexes, we can have complexes indexed by $\N$. This is closer to the PDF, and it saves us a boatload of cruft about dealing with objects in negative degrees that are morally all the zero object.

 src/normed_snake.lean                            | 110 +++++++++++-----------
 src/normed_spectral.lean                         | 108 +++++++++-------------
 src/pseudo_normed_group/system_of_complexes.lean | 110 ++++++++++------------
 src/system_of_complexes/basic.lean               |  89 +++++++++---------
 src/system_of_complexes/completion.lean          |  70 +++++++-------
 src/system_of_complexes/double.lean              |  66 +++++++------
 src/system_of_complexes/soft_truncation.lean     | 447 ----------------------------------------------------------------------------------------
 src/system_of_complexes/truncate.lean            | 238 +++++++++++++++++++++++++++++++++++++++++++++++
 8 files changed, 503 insertions(+), 735 deletions(-)

[Johan Commelin]

I refactored everything on the branch refactor-Z-to-N

[Johan Commelin]

As you can see, we can throw away 200 lines of code

[Johan Commelin]

And I expect more savings in the future

[Johan Commelin]

The refactor was pretty straightforward.

[Patrick Massot]

Why isn't it in master then?

[Johan Commelin]

Because I just finished (-;

[Johan Commelin]

I am about to merge it into master

[Johan Commelin]

done

[Johan Commelin]

In particular, in the definition of the system of complexes attached to Mbar r' S, we no longer have ugly int.extend_from_nat etc...

[Patrick Massot]

I'm about to close my email client and switch off my phone, and try to have a Lean afternoon. Do you have a target for me?

[Johan Commelin]

@Patrick Massot certainly!

[Patrick Massot]

Should I work on

lemma completion (hC : C.is_weak_bounded_exact k K m c₀) :
  C.completion.is_weak_bounded_exact (k^2) K m c₀

[Johan Commelin]

There are two sorry's in system_of_complexes/truncate.lean

[Johan Commelin]

@Patrick Massot if you want to, you can work on that completion thing, but I don't think it is very urgent.

[Johan Commelin]

You proved the strong_of_complete lemma, which is the important bit. I don't think we actually need those other lemmas

[Johan Commelin]

Because in our final use case, everything is already complete. So we never have to make a completion step.

[Patrick Massot]

Why did we discuss this lemma then?

[Johan Commelin]

I guess it's more of a sanity check, in case we want to apply this to noncomplete systems in a theoretical other application. But we don't need it for first_target I think

[Riccardo Brasca]

If I remember correctly Peter sketched these arguments as a possible solution to a small problem in the normed snake lemma and I put them in the blueprint. I didn't now (and I still don't) the big picture, so it's very possible that in our case everything is already complete

[Riccardo Brasca]

There was also something about optimizing the constants

[Patrick Massot]

I'll work on is_weak_bounded_exact_of_truncate instead.