Stream: condensed mathematics

Topic: complexes indexed by N

Johan Commelin (Mar 12 2021 at 12:34):

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 (Mar 12 2021 at 12:34):

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

Johan Commelin (Mar 12 2021 at 12:35):

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

Johan Commelin (Mar 12 2021 at 12:35):

And I expect more savings in the future

Johan Commelin (Mar 12 2021 at 12:35):

The refactor was pretty straightforward.

Patrick Massot (Mar 12 2021 at 12:35):

Why isn't it in master then?

Johan Commelin (Mar 12 2021 at 12:35):

Because I just finished (-;

Johan Commelin (Mar 12 2021 at 12:36):

I am about to merge it into master

done

Johan Commelin (Mar 12 2021 at 12:36):

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 (Mar 12 2021 at 12:37):

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 (Mar 12 2021 at 12:37):

@Patrick Massot certainly!

Patrick Massot (Mar 12 2021 at 12:37):

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 (Mar 12 2021 at 12:37):

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

Johan Commelin (Mar 12 2021 at 12:38):

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

Johan Commelin (Mar 12 2021 at 12:39):

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

Johan Commelin (Mar 12 2021 at 12:39):

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

Patrick Massot (Mar 12 2021 at 12:42):

Why did we discuss this lemma then?

Johan Commelin (Mar 12 2021 at 12:45):

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 (Mar 12 2021 at 12:46):

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 (Mar 12 2021 at 12:47):

There was also something about optimizing the constants

Patrick Massot (Mar 12 2021 at 13:12):

I'll work on is_weak_bounded_exact_of_truncate instead.

Last updated: May 09 2021 at 16:20 UTC