truncation

Stream: condensed mathematics

[Johan Commelin]

@Peter Scholze I'm confused about the induction step in 9.6

[Peter Scholze]

OK...

[Johan Commelin]

We have defined a functor truncate that takes a cochain complex $C$ of normed groups (indexed by $\N$) and does the following:

• in degree 0 it places $\mathrm{coker}(d \colon C_0 \to C_1)$
• in degree i for i > 0 it places $C_{i+1}$

[Johan Commelin]

Now I thought that you wanted to use that C is bounded exact in degrees $\le m+1$ if and only if truncate C is bounded exact in degrees $\le m$.

[Johan Commelin]

But that seems fishy.

[Johan Commelin]

So you must be doing something smarter in the induction.

[Peter Scholze]

Hmm, why is that fishy :-)?

[Peter Scholze]

(Assuming you already know bounded exactness in degrees $\leq m$)

[Patrick Massot]

Could you expand on that last parenthesis? "bounded exactness in degrees $\le m$" of what?

[Peter Scholze]

Of $C$

[Peter Scholze]

I claim that if $C$ is bounded exact in degrees $\leq m$, then bounded exactness in degrees $\leq m+1$ is equivalent to bounded exactness in degrees $\leq m$ of its truncation

[Peter Scholze]

(I guess one could make a better statement about bounded exactness in an individual degree, but this formulation should do.)

[Peter Scholze]

Is there an issue with that statement? I may well be overlooking something...

[Patrick Massot]

This sounds fine. The issue with Johan's formulation is deducing information about the degree zero part of C from information about truncate C.

[Peter Scholze]

But isn't bounded exactness in degrees $\leq m$ part of the hypothesis of the result?

[Patrick Massot]

So I guess the question is why we don't need the fishy part.

[Patrick Massot]

Peter Scholze said:

But isn't bounded exactness in degrees $\leq m$ part of the hypothesis of the result?

Not in Johan's version.

[Johan Commelin]

Peter Scholze said:

But isn't bounded exactness in degrees $\leq m$ part of the hypothesis of the result?

I guess we should add this to the lemma that we are formalizing.

[Johan Commelin]

I made the induction step too crude

[Johan Commelin]

Let's add that assumption to the lemma, and then I'll refactor the rest of the induction step so that it provides that assumption

[Peter Scholze]

Hmm, I just checked in Analytic.pdf, and there it is an assumption

[Johan Commelin]

It is in the big list of conditions, I agree. But since the argument is now scattered over 4 lean files, this one got lost in the process somewhere

[Johan Commelin]

So the assumption is in the statement of analytic_9_6 but not in the sublemma that I wrote in another file.

[Johan Commelin]

My apologies to Patrick for creating this confusion

[Patrick Massot]

No problem

[Peter Scholze]

@4 lean files: What's the current ratio of lines of code vs lines in the paper? ;-)

[Peter Scholze]

(One question about how this project works internally: I am a bit surprised that no expanded "paper version" of the proof seems to be produced as an intermediate stage to the formalization. The closest thing seems to be the blueprint, but that actually seems to come after the formalization in order to document it, if I see it right. Is this impression correct?)

[Mario Carneiro]

The blueprint contains many unfinished theorems currently, so I wouldn't say it's after the formalization

[Mario Carneiro]

I think we should be doing a lot more blueprinting than we currently do, it's a really good way to get formalizers with less mathematical experience involved

[Johan Commelin]

@Peter Scholze there are currently ~12000 lines in the repo... this includes everything, empty lines, config files, etc...

[Johan Commelin]

476616 characters

[Kevin Buzzard]

When we wrote the perfectoid project, Patrick was always saying that we should have a proper blueprint, but I was very happy just to work from Wedhorn's notes, which I thought were very thorough. I think that for the cap set project they wrote down a proper 25 page version of the (much shorter) paper.

[Peter Scholze]

Hmm, I think the parts of the blueprint that are not formalized are the parts that are essentially copied verbatim from Analytic.pdf

[Johan Commelin]

vs 339056 Analytic.tex as character count for the TeX

[Johan Commelin]

which of course contains a lot more than just section 9

[Kevin Buzzard]

right!

[Peter Scholze]

So maybe factor ~10?

[Kevin Buzzard]

On the other hand our formalisation contains a lot more than just section 9 as well because we've had to make a bunch of infrastructure which is assumed in the paper

[Peter Scholze]

True.

[Patrick Massot]

I keep saying we should write the detailed blueprint before formalization, but I can't get anyone else on board with that idea...

[Peter Scholze]

Not too bad in any case

[Mario Carneiro]

The thing is, there are very few people who can write the blueprint, and most of them are going straight to formalization ATM

[Johan Commelin]

Well, I consistently catch a lot of small mistakes when I write things in Lean, whereas with a blueprint I would seriously mess up.

[Johan Commelin]

That's why it is a lot easier to expand the blueprint after the fact

[Johan Commelin]

And since we split the constant k into two parts, some of the proofs have to change... and I don't find it very easy to predict how

[Mario Carneiro]

I think it's already good enough to just "go over" the proof and reproduce it with a bit more "type inference"

[Mario Carneiro]

You will of course catch errors at every level, but try to make sure that the big ones are caught before formalization, because the blueprint is a lot easier to modify

[Johan Commelin]

Also, and this is my personal opinion which is a bit the opposite of Patrick's: my dream is that at some point a system like Lean is usable without a detailed blueprint

[Mario Carneiro]

Lean is certainly usable without a detailed blueprint, that's not the problem

[Mario Carneiro]

the problem is that you need to be a really good mathematician and a really good lean user to formalize this proof

[Mario Carneiro]

the point of a blueprint is to allow users who are one or the other but not both to contribute to the project

[Peter Scholze]

@Johan Commelin The way you work certainly makes it look like this to me -- you just seem to target one lemma after the next, formalizing it on-the-fly

[Johan Commelin]

Yes, it's going really well, I'm quite happy

[Johan Commelin]

In some sense, I think Analytic.pdf is already a very good blueprint

[Johan Commelin]

sometimes there are some inequalities I get stuck on, but then Peter is quick to get me unstuck

[Peter Scholze]

I find this genuinely surprising, as I thought it was really flexing even for human readers

[Patrick Massot]

I think Johan is working pretty hard...

[Johan Commelin]

(and sometimes I forget to plug -y into a stupid formula, and I make myself look completely stupid :face_palm: :grinning: )

[Peter Scholze]

I know :-)

[Mario Carneiro]

I want to point out that @Johan Commelin and @Kevin Buzzard are really good mathematicians so I don't trust their judgment here :)

[Johan Commelin]

Well, I wouldn't put myself on the same level as Kevin...

[Mario Carneiro]

I don't see a lot of undergrads in the project, unlike mathlib

[Johan Commelin]

That's true... but that is maybe to be expected.

[Johan Commelin]

@Mario Carneiro I certainly think that you can contribute here, because you are a good mathematician

[Johan Commelin]

But writing a blueprint that is easy enough to follow for people that don't know any of the maths will take a lot of time. It's not clear to me that this is worth it.

[Johan Commelin]

Also, I must admit that I don't get dopamine kicks out of writing a blueprint, whereas killing sorrys is extremely rewarding.

[Mario Carneiro]

I mostly don't contribute that much because I don't have the time to dedicate to this project this close to the end of the PhD

[Johan Commelin]

Yes, I completely understand that.

[Peter Scholze]

So the way I see it you are getting dangerously close to attacking the proof of 9.5, right? I'd be really surprised if that one can still be done on-the-fly

[Johan Commelin]

If I grind down to a halt, I'll start writing a blueprint (-;

[Kevin Buzzard]

OK so I cannot see any reason why we personally want to have this minus sign in our truncation any more. Whether the signs are there or not is just a convention, and we can choose our conventions; I choose no signs because they're silly in this context. Everything is nat-indexed and we're moving from C0 -> C1 -> C2 -> ... to (C1/im(C0))->C2->C3->... . Maybe in the category theory library there are arguments for randomly inserting minuses, but right now we're only using this truncation construction in the proof of normed_spectral a far as I can see, and the minus signs literally give no advantage and just mean that a whole bunch of refls have to be changed to simp [map_neg, neg_neg] etc etc. In the branch truncate_sign_refactor I remove these minus signs; now the sorrys in normed_spectral are much easier to fill in. Note that we are not using the category theory shift any more and I am not proposing changing conventions in category theory, just in our repo for this auxiliary construction and where the signs are just awful and pointless in this context.

[Kevin Buzzard]

OK I've been working on the sorrys in normed_spectral. With the sign change removed the generic case sorry in cond3b_truncate is a one-liner:

| _ (q'+2) _ rfl rfl hq := condM.cond3b (q' + 2) (q' + 3) (q' + 4) rfl rfl $ nat.succ_le_succ hq

With the sign change it's horrible, involving convert nearly_this using 7 :D and then doing some sign rewriting.