## Stream: condensed mathematics

### Topic: truncation

#### Johan Commelin (Mar 12 2021 at 14:55):

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

OK...

#### Johan Commelin (Mar 12 2021 at 14:58):

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

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

But that seems fishy.

#### Johan Commelin (Mar 12 2021 at 14:59):

So you must be doing something smarter in the induction.

#### Peter Scholze (Mar 12 2021 at 15:00):

Hmm, why is that fishy :-)?

#### Peter Scholze (Mar 12 2021 at 15:00):

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

#### Patrick Massot (Mar 12 2021 at 15:01):

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

#### Peter Scholze (Mar 12 2021 at 15:02):

Of $C$

#### Peter Scholze (Mar 12 2021 at 15:02):

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

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

#### Peter Scholze (Mar 12 2021 at 15:03):

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

#### Patrick Massot (Mar 12 2021 at 15:04):

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

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

#### Patrick Massot (Mar 12 2021 at 15:04):

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

#### Patrick Massot (Mar 12 2021 at 15:04):

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

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

I made the induction step too crude

#### Johan Commelin (Mar 12 2021 at 15:06):

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

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

#### Johan Commelin (Mar 12 2021 at 15:07):

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

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

#### Johan Commelin (Mar 12 2021 at 15:08):

My apologies to Patrick for creating this confusion

No problem

#### Peter Scholze (Mar 12 2021 at 15:10):

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

#### Peter Scholze (Mar 12 2021 at 15:15):

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

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

#### Mario Carneiro (Mar 12 2021 at 15:20):

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

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

#### Johan Commelin (Mar 12 2021 at 15:23):

476616 characters

#### Kevin Buzzard (Mar 12 2021 at 15:23):

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

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

vs 339056 Analytic.tex as character count for the TeX

#### Johan Commelin (Mar 12 2021 at 15:23):

which of course contains a lot more than just section 9

right!

#### Peter Scholze (Mar 12 2021 at 15:24):

So maybe factor ~10?

#### Kevin Buzzard (Mar 12 2021 at 15:24):

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

True.

#### Patrick Massot (Mar 12 2021 at 15:24):

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

Not too bad in any case

#### Mario Carneiro (Mar 12 2021 at 15:25):

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

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

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

#### Johan Commelin (Mar 12 2021 at 15:27):

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

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

#### Mario Carneiro (Mar 12 2021 at 15:29):

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

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

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

#### Mario Carneiro (Mar 12 2021 at 15:29):

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

#### Mario Carneiro (Mar 12 2021 at 15:30):

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

@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 (Mar 12 2021 at 15:31):

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

#### Johan Commelin (Mar 12 2021 at 15:31):

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

#### Johan Commelin (Mar 12 2021 at 15:31):

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

#### Peter Scholze (Mar 12 2021 at 15:31):

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

#### Patrick Massot (Mar 12 2021 at 15:32):

I think Johan is working pretty hard...

#### Johan Commelin (Mar 12 2021 at 15:32):

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

I know :-)

#### Mario Carneiro (Mar 12 2021 at 15:32):

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

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

#### Mario Carneiro (Mar 12 2021 at 15:33):

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

#### Johan Commelin (Mar 12 2021 at 15:33):

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

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

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

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

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

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

#### Mario Carneiro (Mar 12 2021 at 15:37):

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

Yes, I completely understand that.

#### Peter Scholze (Mar 12 2021 at 15:41):

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

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

#### Kevin Buzzard (Mar 14 2021 at 17:11):

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 (Mar 14 2021 at 17:39):

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.

Last updated: May 09 2021 at 16:20 UTC