Zulip Chat Archive

Stream: condensed mathematics

Topic: truncation


view this post on Zulip Johan Commelin (Mar 12 2021 at 14:55):

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

view this post on Zulip Peter Scholze (Mar 12 2021 at 14:56):

OK...

view this post on Zulip Johan Commelin (Mar 12 2021 at 14:58):

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

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

view this post on Zulip Johan Commelin (Mar 12 2021 at 14:59):

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

view this post on Zulip Johan Commelin (Mar 12 2021 at 14:59):

But that seems fishy.

view this post on Zulip Johan Commelin (Mar 12 2021 at 14:59):

So you must be doing something smarter in the induction.

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:00):

Hmm, why is that fishy :-)?

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:00):

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

view this post on Zulip Patrick Massot (Mar 12 2021 at 15:01):

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

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:02):

Of CC

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:02):

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

view this post on Zulip 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.)

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:03):

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

view this post on Zulip 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.

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:04):

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

view this post on Zulip Patrick Massot (Mar 12 2021 at 15:04):

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

view this post on Zulip Patrick Massot (Mar 12 2021 at 15:04):

Peter Scholze said:

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

Not in Johan's version.

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:04):

Peter Scholze said:

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

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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:05):

I made the induction step too crude

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:06):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:08):

My apologies to Patrick for creating this confusion

view this post on Zulip Patrick Massot (Mar 12 2021 at 15:08):

No problem

view this post on Zulip 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? ;-)

view this post on Zulip 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?)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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...

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:23):

476616 characters

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:23):

vs 339056 Analytic.tex as character count for the TeX

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:23):

which of course contains a lot more than just section 9

view this post on Zulip Kevin Buzzard (Mar 12 2021 at 15:23):

right!

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:24):

So maybe factor ~10?

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:24):

True.

view this post on Zulip 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...

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:25):

Not too bad in any case

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:26):

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

view this post on Zulip 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

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:29):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:31):

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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:31):

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

view this post on Zulip 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

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:31):

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

view this post on Zulip Patrick Massot (Mar 12 2021 at 15:32):

I think Johan is working pretty hard...

view this post on Zulip 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: )

view this post on Zulip Peter Scholze (Mar 12 2021 at 15:32):

I know :-)

view this post on Zulip 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 :)

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:32):

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

view this post on Zulip Mario Carneiro (Mar 12 2021 at 15:33):

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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:33):

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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:35):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:39):

Yes, I completely understand that.

view this post on Zulip 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

view this post on Zulip Johan Commelin (Mar 12 2021 at 15:42):

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

view this post on Zulip 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.

view this post on Zulip 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