status update

Stream: condensed mathematics

[Johan Commelin]

Hi everyone, today I'm stuck in our maths department that is currently being remodeled (-; I won't have much time for serious lean. Starting from Wednesday, there will be school holidays for ~10 days. There are rumours that schools might remain closed after that due to a new lockdown. We'll have to see.
Another update is that I think a full year of working from home is starting to take some toll of my body. I had some lower back pains for a while, but hoped that by changing my working position frequently they would go away. In the last two weeks it's been progressively getting a bit worse, with flaming pains rising higher up my back, and also down into my legs. It seems that the pains are also causing some form of dizziness. At the same time, I can still go for my 3km run and I don't have pain then.
Conclusion: in the next two weeks I'll probably avoid the coding marathons that I did in the last 3 months. I want to spend extra time with my family, and extra time exercising.

On the Lean side of things: Mario made a huge effort in refactoring the definition of the system of complexes attached to Breen-Deligne data and a profinitely filtered pseudo normed group with action of $T^{-1}$. The refactor is almost done, on the rescale_iso branch. I think I can finish it today or tomorrow. After that, it should be easier to use functoriality properties of this construction.
My hope is that this will bring the check of condition (3) in the proof of 9.5 "within arm's reach".

[Scott Morrison]

Take care of the back! I also had some lockdown induced back problems...

[Kevin Buzzard]

Johan, if you want to take a role more on the sidelines for the next month or so then please feel free to "hand over" the current state of the project, giving some overview of where we are, what needs doing next, what to read etc. Right now is a very good time for me to become more involved -- we are now on a month of summer break and next term my teaching load is very light. I have been catching up on my administrative duties over the last couple of weeks since my course finished and have a lot of time and enthusiasm for Lean right now.

[Johan Commelin]

Let's do a video call! I'll probably have time either tonight, or any time tomorrow.

[Johan Commelin]

I think I can still help with the overall strategy. But I shouldn't do 10-12 hours of Lean coding per day for the next two weeks.

[Johan Commelin]

But I should still be online on Zulip to help brainstorm with the strategy.

[Kevin Buzzard]

You can tell I am in a good place because my number of unread work emails is back down to three digits.

[Riccardo Brasca]

Thank you for all the time you spent teaching us how to do things, and take care!

[Patrick Massot]

Johan, please take care of yourself and your family. I'd be interested in the video call too.

[Johan Commelin]

I will try to give a (very informal!) lecture on this proof tomorrow. I propose that we start 2021-03-30T09:30:00+02:00 .
Anyone is welcome to attend, but it will certainly be very helpful if you have engaged with the project (Lean/PDF/blueprint) in some form. My goal is to give an overview of what has been done so far (thanks to the help of many people!) and what remains to be done.

[Johan Commelin]

I understand that this time is not ideal for @Adam Topaz, but I would like to reserve about 2hrs, and in the afternoon I have another appointment.

[Kevin Buzzard]

Will you video it?

[Johan Commelin]

If someone wants to record it, that's fine with me. Can someone host a zoom meeting?

[Riccardo Brasca]

I have a pro account

[Peter Scholze]

Would it be helpful if I'm present? I currently got two exams scheduled for tomorrow morning, but might also shift them

[Johan Commelin]

It might make more sense to shift my appointment, because it isn't very official

[Johan Commelin]

And yes, I think it would be very helpful if you want/can be present

[Peter Scholze]

Well, I'm mostly free this week, e.g. tomorrow from 11:00 (+epsilon)

[Johan Commelin]

If you aren't married to lunch at 12:00 (like some of my colleagues here in Freiburg) then that could certainly work.

[Peter Scholze]

Well, I have lunch at 12:30 usually, but it's fine if I go a bit later once ;-)

[Johan Commelin]

Ok, se we reschedule to 2021-03-30T11:05:00+02:00 ? Is that ok with @Riccardo Brasca @Julian Külshammer @Kevin Buzzard @Patrick Massot @Scott Morrison ?

[Riccardo Brasca]

OK for me

[Johan Commelin]

And @Damiano Testa @Filippo A. E. Nuccio and whoever else I'm forgetting right now

[Peter Scholze]

Sounds good to me!

[Damiano Testa]

I have an appointment at 11, but should be easy to reschedule!
My appointment became an exam later in the week, so I do not even need to reschedule!

[Adam Topaz]

That's 3:05 am for me, so I won't be there live, but pretend I'm there and I'll watch the recording later :wink:

[Johan Commelin]

@Mario Carneiro is 3:05 am a problem for you :rofl: ?

[Filippo A. E. Nuccio]

@Johan Commelin That's good for me: do you mean 11:05 AM CET?

[Johan Commelin]

Zulip shows times enytered with <time in your local timezone

[Mario Carneiro]

Actually I'm in a conference this week, so I probably won't be able to make that time unless the talks are boring :P

[Filippo A. E. Nuccio]

@Johan Commelin I have just read the whole conversation, and I am sorry to read about your back pains. Do take care, and thank you so much for the work done, and the help given, so far.

[Riccardo Brasca]

I zoom is OK for everybody here is the link

Riccardo Brasca is inviting you to a scheduled Zoom meeting.

Topic: LTE
Time: Mar 30, 2021 10:45 AM Paris

Join Zoom Meeting
https://u-paris.zoom.us/j/81444456365?pwd=VkJGb3RUeElkenU4dlUyQ1hzWmFtdz09

Meeting ID: 814 4445 6365
Passcode: 235711

[Mario Carneiro]

2021-03-30T10:45:00+02:00

[Riccardo Brasca]

The "official" starting time is 2021-03-30T11:05:00+02:00 , I will open the zoom meting a little in advance just to be sure that everything works

[Johan Commelin]

I finished my preparations :sweat_smile:

[Johan Commelin]

2021_03_lte_overview.pdf

[Johan Commelin]

:up: slides for the lecture

[Scott Morrison]

I'm curious that the construction Kom (Free (Mat C)) also appears in the construction of Khovanov homology (an old love of mine!), but for a somewhat more complicated category C than int. I'd love to have a better sense of "why". :-)

[Scott Morrison]

Where can I find @Kevin Buzzard's formalised statement about Free (Mat int)? I'd be happy to know the general statement replacing int with C. We'll have both Mat and Free separately in mathlib shortly (#6845, #6906, plus one more), and it would be nice to check that their API supports whatever this statement is. :-)

[Johan Commelin]

breen_deligne/functorial_map.lean

[Adam Topaz]

@Riccardo Brasca @Johan Commelin did the lecture end up being recorded?

[Riccardo Brasca]

Yes! zoom is " Processing Recording..." at the moment. I will put the link here if it's OK for @Johan Commelin

[Johan Commelin]

yes, fine with me

[Johan Commelin]

we can even upload it to the leanprover youtube account, if that is somehow useful

[Peter Scholze]

Not sure if it needs to be on youtube?

[Johan Commelin]

It doesn't really have to, I agree.

[Johan Commelin]

It's just that recordings are typically quite large

[Adam Topaz]

Also doesn't zoom delete recordings stored on their servers after a little while?

[Peter Scholze]

aren't the recordings saved locally?

[Peter Scholze]

(That was true when I recorded my lectures, I had the files on my computer...)

[Adam Topaz]

It depends on how it was recorded -- with zoom you can choose to record directly to their cloud, or to record locally

[Peter Scholze]

I see

[Adam Topaz]

And considering that Riccardo mentioned that zoom is processing something, I suspect it was recorded to the cloud.

[Riccardo Brasca]

Yes it's on the Cloud, but I can and will, download it

[David Michael Roberts]

It could be an unlisted YouTube video, so only people with the direct link can see it (and that could be shared on proviso of no posting on the public internet).

[Adam Topaz]

How does one define "public internet"? https://leanprover-community.github.io/archive/

[David Michael Roberts]

Yeah, I mean if the link is going to be shared here, then I'm genuinely curious as to what the objection is for hosting on a stable platform like YouTube. But I mean not Twitter or Reddit or whatever.

[Riccardo Brasca]

There is also the informal discussion at the end, that definitely doesn't deserve to be made public, but we can of course just cut it

[Johan Commelin]

Ok, I can just host the entire thing, including discussion on my server, behind a password.

[Johan Commelin]

But I don't guarantee fast download times (-;

[Riccardo Brasca]

Zoom is still processing and I think I will go for a walk enjoying the sunny day :sunny: before the curfew. I will post the link later this evening

[Damiano Testa]

I am happy for the recording to be private or public. Honestly, even if it did go public, I do not think that it would be the next Gangnam style, nor that, if it did, it would be bad! Quite the opposite, actually! :lol:

[Filippo A. E. Nuccio]

I'm happy with whatever decision you come up with.

[Peter Scholze]

OK, I don't know, do as you please; it just felt like more of an internal group meeting to me (so it makes sense to make it public here), so I found it a bit strange to host it on youtube

[Kevin Buzzard]

Yes -- why not just circulate it to interested parties?

[Adam Topaz]

I agree, I think it should be behind a password in some way. In my experience, the zoom cloud recordings have a password associated with them (although this might depend on Riccardo's setup in this case). Johan's basement server would work too :)

[Bhavik Mehta]

It's also possible to make it unlisted on youtube, so people can't find it without the link but it's still easily accessible to those who do have the link

[Filippo A. E. Nuccio]

Adam Topaz said:

I agree, I think it should be behind a password in some way. In my experience, the zoom cloud recordings have a password associated with them (although this might depend on Riccardo's setup in this case). Johan's basement server would work too :smile:

Yes, I agree.

[Riccardo Brasca]

Here is the link
https://u-paris.zoom.us/rec/share/d_B1sRU_v8Xr001jgKU1CmruILdG8Shm2YI8czPndzWjux9VPJOM4eBhGWIQrNgm.99xJgMg4Fe9s9bB8

[Riccardo Brasca]

let me know if it doesn't work

[Johan Commelin]

How long does Zoom host it?

[Johan Commelin]

Otherwise I suggest that everyone who wants a copy, just downloads it. And if someone shows up 3 months from now, and needs a copy, then one of us can send it.

[Riccardo Brasca]

one year I think, but I am downloading it

[Johan Commelin]

Ooh, I don't actually see how to download it

[Riccardo Brasca]

no problem, let me download it (it is not that fast) and upload it to my (university) server

[Riccardo Brasca]

https://webusers.imj-prg.fr/~riccardo.brasca/files/LTE.mp4
This should work for everybody

[Filippo A. E. Nuccio]

Works like a charm for me.

[Johan Commelin]

It's only half a GB. Compression these days... :rofl:

[Johan Commelin]

Bhavik just told us that Gordan is completely sorry-free! I took the liberty of pushing it a column to the right in https://github.com/leanprover-community/lean-liquid/projects/1

[Johan Commelin]

@Adam Topaz Do you think that #16 is also ready to move to Done?

[Johan Commelin]

And maybe https://github.com/leanprover-community/lean-liquid/issues/17 (aka 8.19) should now move towards In progress?

[Adam Topaz]

There is nothing about arbitrary hypercovers, but I was under the impression that Cech nerves suffice for what we need? If so, maybe change the wording and mark 16 as done? And yes 8.19 is "in progress" :smile:

[Johan Commelin]

@Adam Topaz sounds good to me

[Adam Topaz]

I think the next step for 8.19 involves some additional work involving complexes, so I've been hesitant to start on this before we incorporate the new complexes from mathlib.

[Johan Commelin]

Yup, understood

[Johan Commelin]

I think the homotopy PR is getting close though, isn't it?

[Adam Topaz]

#7478 is ready to be merged as far as I'm concerned, but I saw you added some comments...

[Adam Topaz]

And looks like that's the last dependency for the homotopy PR

[Johan Commelin]

I think we can convert my comment into a TODO. But it will have to be fixed if we want the R-linear version (which is probably soonish)

[Johan Commelin]

#7478 is now merged. Now we only need the homotopy PR.

[Johan Commelin]

@Bhavik Mehta I refactored the "dual is free" proof, and merged your gordan branch into master.

[Johan Commelin]

Do you think that

variables (Λ : Type*) [polyhedral_lattice Λ]

/-- In a polyhedral lattice the ball around the origin of radius `c` is finite. -/
lemma filtration_finite (c : ℝ≥0) : (filtration Λ c).finite :=
begin
  admit
end

is now also easy to do?

[Johan Commelin]

That is from the file polyhedral_lattice/topology.lean

[Johan Commelin]

Gordan is now also green in the dependency graph

[Riccardo Brasca]

Is someone working on filtration_finite? I have some time this week to try to do it.

[Johan Commelin]

I have been thinking about it. But it's Lean-nontrivial

[Johan Commelin]

I think it would be best if we can get some help from Bhavik and/or Yael, because they understand all the machinery behind their proof of Gordan.

[Johan Commelin]

I think Bhavik might have some time this week.

[Johan Commelin]

@Riccardo Brasca there is also a sorry left in polyhedral_lattice/cech.lean. But again, I think this one is non-trivial, and might need stuff about convex polyhedra.

[Johan Commelin]

It's the claim that the quotient norm on the quotient lattices is actually generated by finitely many elements.

[Johan Commelin]

Intuitively, I want to say: the image of a convex polyhedron under a linear map is again a convex polyhedron.

[Johan Commelin]

But that doesn't constitute a Lean proof.

[Riccardo Brasca]

Hm, I see, that seems indeed non trivial..

[Riccardo Brasca]

In the meantime I am doing the easy sorry in polyhedral_lattice/topology

[Johan Commelin]

Yes, but I'm now not so sure that approach will help.

[Johan Commelin]

I guess it can be made to work.

[Johan Commelin]

But given a list of $\lambda_1, \dots, \lambda_n$ that generate the norm, we need a bound on the denominator $d$ for elements $\frac{c_1\lambda_1 + \dots c_n\lambda_n}{d}$ whose norm is less than $\varepsilon$

[Johan Commelin]

And I guess that bound will be something like the maximum of all $\lambda_{i_1} \wedge \dots \wedge \lambda_{i_k}$, where $k$ is the rank of $\Lambda$.

[Riccardo Brasca]

Ah, you mean the lemmas about star are there only to be used to prove filtration_finite? If this is the case it's probably better to wait to have a proof of that, I agree

[Johan Commelin]

Would you be interested in converting for_mathlib/finite_free into mathlib API for module.free?

[Johan Commelin]

It's not a simple copy-paste.

[Riccardo Brasca]

Sure!

[Peter Scholze]

Johan Commelin said:

Intuitively, I want to say: the image of a convex polyhedron under a linear map is again a convex polyhedron.

Actually, why is that nontrivial? A convex polyhedron is the convex hull of finitely many points, and the image is just the convex hull of the finitely many image points. Now I'm not sure what the current implicit definition of "convex polyhedron" is, but I think it's actually quite close to "the convex hull of finitely many points".

[Peter Scholze]

Johan Commelin said:

But given a list of $\lambda_1, \dots, \lambda_n$ that generate the norm, we need a bound on the denominator $d$ for elements $\frac{c_1\lambda_1 + \dots c_n\lambda_n}{d}$ whose norm is less than $\varepsilon$

Maybe a better question is: Why is this relevant?

[Johan Commelin]

@Peter Scholze I think that claim shouldn't be hard. The trouble is to show that "$\lambda_1, \dots, \lambda_n$ generate the norm" is equivalent to "the unit ball is a convex polyhedron"

[Johan Commelin]

We need to translate between "convex hull of vertices" point of view and "finitely many faces given by affine hyperspaces" point of view

[Johan Commelin]

Concerning the other question: if we can bound the number of such d (assuming the c_i are coprime), then I have a proof of finiteness for $\{x : \|x\| \le \varepsilon\}$ without going through convex polyhedra

[Kevin Buzzard]

I think that @Bhavik Mehta might have dealt with this (convex hull = intersection of affine hyperspaces). About ten days ago when Bhavik said he wanted to take on the proof of Gordan he showed me a reference which claimed to prove a Gordan's Lemma and I pointed out to him that it had a different definition of convex polyhedron to the one in LTE and it was too late to change the LTE definition. We looked through a proof that the two notions were equivalent and my understanding was that Bhavik seemed optimistic that it was do-able and my impression was that for him to prove Gordan this way he was going to have to do it. So I suspect he's done it. Bhavik am I right?

[Kevin Buzzard]

Bhavik and I also talked a lot at CLUG last Wed about this finiteness issue.

[Johan Commelin]

No, not completely. Bhavik has so far only done intersections of linear halfspaces, not affines.

[Johan Commelin]

But I agree that the easiest way forward it to build on what Bhavik has done.

[Peter Scholze]

Sorry for the late answer, but do we really need this translation here, between "convex hull of vertices" and "finitely many faces given by affine hyperspaces"? I had the feeling that in $\Lambda$, we take convex hulls of vertices, and then in 9.7 (~ Gordan's lemma) we pass to the dual side, and look at intersections of halfspaces. But for those quotients of polyhedral lattice, we're staying purely on the side of $\Lambda$.

[Johan Commelin]

@Peter Scholze Sure, but how should we prove that $\{x : \|x\| \le \varepsilon\}$ is finite? I wanted that finiteness to deduce that $\Lambda$ is discrete, which in turn is used to show that we take quotients by closed subgroups, so that the quotient is separated.

[Johan Commelin]

I think the easiest way is to show that it's the intersection of $\Lambda$ and a compact subset of $\Lambda \otimes \R$

[Johan Commelin]

But to show that $\{ x\in \Lambda \otimes \R : \|x\| \le \varepsilon\}$ is compact, I thought that the "finitely many faces given by affine hyperspaces" POV was the best approach

[Peter Scholze]

OK, I see. It sounded to me like there are two problems: Show that the quotient is still normed (as opposed to semi-normed), and show that its norm is polyhedral. But it seems to me that the second is not a problem?

[Johan Commelin]

The second is also a problem (for me)

[Johan Commelin]

I have the following proof state:

x: fin m →₀ Λ'
d: ℕ
hd: 0 < d
c: ι → ℕ
H1: d • x = ∑ (i : ι), c i • l i
H2: ↑d * ∥x∥ = ∑ (i : ι), ↑(c i) * ∥l i∥
⊢ ↑d * ∥quotient_add_group.mk x∥ = ∑ (i : ι), ↑(c i) * ∥⇑(quotient_add_group.mk' (L f m)) (l i)∥

[Johan Commelin]

Let me try to translate it to maths

[Johan Commelin]

So the l i generate the norm, and I've used that to get the hypotheses H1 and H2

[Johan Commelin]

x: fin m →₀ Λ' should be read as $x \in (\Lambda')^m$.

[Johan Commelin]

And now we need to prove $d \cdot \|\bar x\| = \sum_i c_i \cdot \|\overline{l_i}\|$

[Johan Commelin]

Here $\bar x$ and $\overline{l_i}$ denote the projections into $\Lambda/L_m$

[Peter Scholze]

Well, the inequality $\leq$ ought to be clear by the triangle inequality; while $\geq$ follows by using the same property on $\Lambda$; I think...

[Peter Scholze]

(Sorry, I'm writing this while simultaneously attending a lecture, so I'm slow and can't think too much...)

[Johan Commelin]

Hmm, I will think about it again. I must admit that I postponed thinking about this for a while

[Peter Scholze]

I'm only now starting to understand what's written in the code there. Why are there different quotient_add_group.mk commands on the two sides?

[Bhavik Mehta]

Kevin Buzzard said:

I think that Bhavik Mehta might have dealt with this (convex hull = intersection of affine hyperspaces). About ten days ago when Bhavik said he wanted to take on the proof of Gordan he showed me a reference which claimed to prove a Gordan's Lemma and I pointed out to him that it had a different definition of convex polyhedron to the one in LTE and it was too late to change the LTE definition. We looked through a proof that the two notions were equivalent and my understanding was that Bhavik seemed optimistic that it was do-able and my impression was that for him to prove Gordan this way he was going to have to do it. So I suspect he's done it. Bhavik am I right?

As Johan says, I only did linear halfspaces - more specifically we talked about polyhedral cones (intersection of linear halfspaces) but what's needed now is for polyhedra (intersection of affine halfspaces). But again as I mentioned to Johan the other day, it seems like you can use the linear version to get to the affine version

[Peter Scholze]

Maybe the missing link here is the following: The discreteness you want to be prove to show that the quotient is still normed should also include the statement that for all $\overline{x}$ you can find some $x$ with $||x|| = ||\overline{x}||$ -- as there are only finitely many $x$'s with bounded norm, so the infimum is actually a minimum. Then if you use such a lift $x$ in the above, you get

$d ||\overline{x}|| = d ||x|| = \sum_i c_i ||l_i||\geq \sum_i c_i ||\overline{l}_i||,$

while by the triangle inequality $d||\overline{x}||\leq \sum_i c_i ||\overline{l}_i||$, so you get the desired equality.

[Riccardo Brasca]

Peter Scholze said:

I'm only now starting to understand what's written in the code there. Why are there different quotient_add_group.mk commands on the two sides?

quotient_add_group.mk and quotient_add_group.mk' are essentially the same thing, you can ignore the difference.
Technically the first work also if the subgroup is not normal (but the quotient is not a group of course), while the latter works only for normal subgroups.

[Johan Commelin]

@Peter Scholze yes, that sounds familiar. I think some time ago I came to the conclusion that we needed to know that the infimum is a minimum. (But then I forgot again that we needed this :face_palm:)
I guess technically this can be done by showing that polyhedral lattices are complete, since discrete

[Yaël Dillies]

Johan Commelin said:

Peter Scholze I think that claim shouldn't be hard. The trouble is to show that "$\lambda_1, \dots, \lambda_n$ generate the norm" is equivalent to "the unit ball is a convex polyhedron"

This has very much a LCTVS flavor, doesn't it? :stuck_out_tongue_wink:
What I would like to do if I weren't bound to proving Szemerédi's Theorem or losing my wit to Vector Calculus calculations would be to define LCVTS and make them an API that would talk about (convex) polytopes as intersections of halfspaces, polyhedrons as convex hulls of finsets, and would bridge between both.

[Kevin Buzzard]

Yes, I think everything should be done for locally convex topological vector spaces really.

[Kevin Buzzard]

But not until after your exams :-)

[Yaël Dillies]

Johan Commelin said:

Peter Scholze yes, that sounds familiar. I think some time ago I came to the conclusion that we needed to know that the infimum is a minimum. (But then I forgot again that we needed this :face_palm:)
I guess technically this can be done by showing that polyhedral lattices are complete, since discrete

That too is something I want to do. Can't wait for the exams to be over!

[Yaël Dillies]

And yeah I agree that bounded intersection of closed halfspaces <=> convex hull of a finset is relatively easy. What's hard is to translate that to space of a pure simplificial complex.

[Johan Commelin]

But we don't need that last part (-;

[Peter Scholze]

Actually, I wonder whether this part of the argument can be simplified by modifying the definition of a polyhedral lattice. What happens if you simply get rid of the integer factor $d\geq 1$, replacing it by $1$?

[Peter Scholze]

In that case, polyhedral lattices may not satisfy $||nx||=n||x||$ for $n\geq 1$, but I think that's never used (is it?)

[Johan Commelin]

No, that isn't used, because I haven't proved it yet.

[Johan Commelin]

I will check asap whether removing the d works.

[Johan Commelin]

(I am about to start a board game with my son.)

[Johan Commelin]

I can confirm that the proof of 9.8 still works after setting d = 1

[Johan Commelin]

I'm now building the rest of the project. But this looks good!

[Johan Commelin]

Several proofs simplified (-;

[Johan Commelin]

Yup, no problems in the rest of the project either :tada:

[Peter Scholze]

Great!! So no more sorry's involving (cech conerves of) polyhedral lattices?

[Johan Commelin]

Hmm, almost none atm

[Johan Commelin]

The finiteness is now sorry-free

[Johan Commelin]

I still have

lemma norm_lift (y : obj f m) :
  ∃ x, quotient_add_group.mk' (L f m) x = y ∧ ∥x∥ = ∥y∥ :=
sorry

lemma norm_generator {ι : Type*} [fintype ι]
  (l : ι → (fin m →₀ Λ')) (hl : generates_norm l) (i : ι) :
  ∥quotient_add_group.mk' (L f m) (l i)∥ = ∥l i∥ :=
sorry

[Johan Commelin]

norm_lift should be easy, given the finiteness.

[Johan Commelin]

For norm_generator, I guess we really need to look under the hood of the definition of $L_m$ again.

[Peter Scholze]

That sounds good! But I'm still a little lost math-wise. Isn't norm_generator what we discussed above, as a consequence of norm_lift?

[Johan Commelin]

@Peter Scholze norm_lift says that there exists a pre-image with the same norm as y in the quotient.

[Johan Commelin]

But for norm_generator we claim that the $\lambda_i$ that generate the norm upstairs have the same norm when projected into the quotient.

[Johan Commelin]

If one of the $\lambda_i$ where in the subgroup that we take a quotient by, that is obviously false. So we need to do something.

[Peter Scholze]

Oh I see. But that's probably not true, is it? Do we actually need that statement?

[Johan Commelin]

hmm, maybe I misunderstood how you want to use norm_lift.

[Johan Commelin]

But I was under the impression that norm_generator is true in our setting.

[Johan Commelin]

Ooh, your proof is a lot easier... :smiley:

[Johan Commelin]

Polyhedral quotients are now completely sorry-free! :tada:

[Scott Morrison]

What is the status with mathlib bumping at the moment? There are a few minor PRs that have merged that I would like to bump, but I'm not sure to what extent, if any, the new homological complex design has been incorporated.

[Scott Morrison]

I can look into doing this, but I suspect Johan has the comparative advantadge here!

[Johan Commelin]

I'm working on the homological refactor in a separate branch

[Johan Commelin]

I think I'm halfway done

[Johan Commelin]

The homotopy fix landed yesterday, and I'm going to see if that helps now

[Johan Commelin]

But feel free to fix other things on master at the same time

[Johan Commelin]

master is already bumped to latest mathlib-master

[Johan Commelin]

Hmm, I first need to sleep two more hours.

[Johan Commelin]

I've pushed to homological-refactor

[Johan Commelin]

@Scott Morrison feel free to hack on it

[Peter Scholze]

Wow, that must have been a short night! Thanks for all the great work Johan!

[Peter Scholze]

Sounds like it's down to the path 8.19 --> 9.2 --> column exactness in the proof of 9.5 (and then verify that all constants can be chosen to satisfy the required constraints)!

[Patrick Massot]

Johan can smell the 9.5 finish line, he no longer sleeps.

[Johan Commelin]

Peter Scholze said:

Wow, that must have been a short night! Thanks for all the great work Johan!

More like a broken night... 11pm -- 3:30, and then 5:00 -- 7:00

[Patrick Massot]

I can find Lean time today, I'll work on 9.2

[Peter Scholze]

Maybe now is a good time to point out that in the proof of the column exactness of 9.5, I once refer to 9.10, but actually this reference doesn't really work as one is passing to a kernel complex instead of a cokernel complex. On the other hand, the situation is actually much easier than in 9.10.

What I really mean to say: After 8.19 and 9.2 are done, one should first "marry" them and prove the version of 8.19 where all terms $\hat{M}(S)$ are replaced by $\hat{V}(S)^{T^{-1}}$

[Peter Scholze]

Hmm actually probably I should write up more precisely what I mean

[Patrick Massot]

Having a precise write up would be lovely.

[Peter Scholze]

OK, will try to do, maybe later today

[Peter Scholze]

Peter Scholze said:

Maybe now is a good time to point out that in the proof of the column exactness of 9.5, I once refer to 9.10, but actually this reference doesn't really work as one is passing to a kernel complex instead of a cokernel complex. On the other hand, the situation is actually much easier than in 9.10.

What I really mean to say: After 8.19 and 9.2 are done, one should first "marry" them and prove the version of 8.19 where all terms $\hat{M}(S)$ are replaced by $\hat{V}(S)^{T^{-1}}$

Upon further reflection, I think the situation isn't really much different than in 9.10; it's just "dual". So I don't think there's a point in "marrying" 8.19 and 9.2. But one has to prove the dual version of 9.10, for passing to kernel complexes instead of cokernel complexes. (@Riccardo Brasca ?)

[Riccardo Brasca]

I forgot all the details of the proof of 9.10, but if the strategy is similar (I mean, completely explicit) I am sure we can prove the dual version without problems

[Peter Scholze]

Yes, I expect that this should be extremely similar.

[Peter Scholze]

Of course, taking kernels in (semi)normed groups is easier than taking cokernels, so maybe some technical problems disappear

[Johan Commelin]

Is it clear what the constants will do? If it's not immediately clear @Riccardo Brasca, then I would suggest just adding random new constants k_new and K_new and starting the proof. Along the way you'll then figure out what they must be.

[Riccardo Brasca]

The precise statement we need is exactly the same as 9.10 (modulo a different constant), but $N_c^\bullet$ is the kernel of $f_c^\bullet$?

[Johan Commelin]

So we will have $0 \to M_1 \to M_2 \to M_3 \to 0$ maps of systems of complexes, and on each level this gives a short exact sequence of abelian groups. But the map $M_2 \to M_3$ does not satisfy the quotient property of normed group homs, I think.

[Johan Commelin]

So we have $f \colon M_1 \to M_2$ and $g \colon M_2 \to M_3$, and the image of $f$ is the kernel of $g$ (as abelian groups).
Also the norm on $M_1$ is strictly compatible with the norm on $M_2$.

[Johan Commelin]

But $g$ satisfies something like $\|g(x)\| \le (1 + r^{-1})\|x\|$. And also, for every $y$ and $\varepsilon > 0$, there exists an $x$ such that $g(x) = y$ and $\|x\| \le (1 + \varepsilon)\frac{r}{1-r}\|y\|$.

[Johan Commelin]

This will roll out of 9.2.

[Johan Commelin]

Here $0 < r < 1$.

[Peter Scholze]

Well, kind of dualize 9.10: You have a map $f^i_c: M^i_c\to N^i_c$ of systems of complexes, both are $(k,K)$-weak exact, and I think you can even assume that each map $f^i_c$ is surjective, of bounded norm, and any element has a lift of bounded norm (as Johan just wrote as I was typing this :stuck_out_tongue: ). Then you want to show that the system of kernels is also $(k_{new},K_{new})$-weak exact

[Riccardo Brasca]

OK, I guess we need a predicate is_kernel dual to is_quotient

[Johan Commelin]

I don't know... in this case I think you can just phrase it as ad hoc assumption to the statement

[Johan Commelin]

But I certainly would advise to use a predicate, instead of the actual ker construction.

[Peter Scholze]

So one thing is slightly better than in 9.10: Each map $f^i_c$ is already surjective (in 9.10, the maps are not required to be injective, only up to some $k$-rescaling. You might do the same here, but I think it's not required.)

[Riccardo Brasca]

lemma weak_normed_snake_dual {k k' k'' K K' K'' : ℝ≥0}
  [hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')] [hk'' : fact (1 ≤ k'')]
  {m : ℕ} {c₀ : ℝ≥0}
  (hM : M.is_weak_bounded_exact k K (m+1) c₀)
  (hM' : M'.is_weak_bounded_exact k' K' (m+1) c₀)
  (hM'_adm : M'.admissible)
  (hg : ∀ c i (x : M (k'' * c) i), ∥g x∥ ≤ (1 + r⁻¹)*∥x∥)
  (Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (y : M' (k'' * c) i),
    ∃ (x : M (k'' * c) i), g x = y ∧ ∥x∥ ≤ (1 + ε) * r * ∥x∥/(1-r))
  (hg : ∀ c i, (f.apply : N c i ⟶ M c i).range = g.apply.ker)
  (hgker : system_of_complexes.is_kernel f) : --is_kernel to be defined, maybe here
  N.is_weak_bounded_exact (k''*k*k') (K'*(K*K'' + 1)) m c₀

[Riccardo Brasca]

The constants have to be changed of course

[Riccardo Brasca]

0 < r < 1 is arbitrary?

[Johan Commelin]

I think you can maybe abstract the (1 + r\inv) away.

[Johan Commelin]

And similarly for the $(1+\epsilon) \frac{r}{1-r}$

[Johan Commelin]

Just replace them by some constants from nnreal

[Johan Commelin]

Maybe you need to know that $1 + r^{-1}$ is larger than 1, I don't know. Probably it doesn't matter.

[Riccardo Brasca]

Yes, this is my question, 1 + r⁻¹ can be anything bigger than 1 (or 0, or whatever) and (1 + ε) * r /(1-r) can be anything positive?

[Peter Scholze]

I think both can be arbitrary positive numbers for this lemma

[Riccardo Brasca]

I created the normed_snake_dual branch, with a file normed_snake_dual.lean. I will take care of the proof, but at last you can test if it is the statement we want

[Peter Scholze]

In the statement, the $k''$ seems to serve no role?

[Riccardo Brasca]

Ops, copy/paste mistake, fixed

[Patrick Massot]

Abstracting constants away is good because the natural constant coming out of the proof of 9.2 will probably be different. Currently the project uses two different ways of saying "a constant almost as good as C": "∀ ε > 0, C + ε works" and "∀ ε > 0, C(1 + ε) works". Of course this is completely immaterial, but sticking to one way makes reusing stuff easier.

[Peter Scholze]

The two ways are different when $C=0$! (This comment is not as stupid as it may sound.)

[Peter Scholze]

(But I think for the concerns right now it is indeed immaterial.)

[Yaël Dillies]

Dumb question: Is there any need whatsoever for open polyhedrons? Should the halfspaces we intersect be forced closed, or should I allow them to be open?

[Yaël Dillies]

I think you shouldn't care much here because your polyhedrons arise in discrete spaces, right?

[Johan Commelin]

@Yaël Dillies we actually found a way around needing polyhedra yesterday night

[Yaël Dillies]

Oh well! That's one thing off my todo list :sweat_smile:

[Johan Commelin]

Short update about this afternoon: together with Scott I finished the homological refactor. So LTE is now using mathlib's cochain complexes, etc.
(Apart from 1 file, that is waiting for 1 more mathlib PR to be merged, but that file is currently a leaf of LTE.)

[Johan Commelin]

Then, after that, Adam stated 8.19 in Lean.

[Johan Commelin]

Which means the game is on.

[Johan Commelin]

Independently, Riccardo started working on snake_lemma2.

[Patrick Massot]

I've made progress on 9.2, I really hope I'll be done before going to bed.

[Johan Commelin]

Great!

[Riccardo Brasca]

Should I merge master while working to snake_lemma2?

[Riccardo Brasca]

I mean, did you changed something that will break my proof?

[Riccardo Brasca]

I did it anyway :grinning:

[Adam Topaz]

Bors is really taking it's time with #7643

[Bryan Gin-ge Chen]

(I think it was just waiting in the queue for a while. Maintainers can check the log here. From what I can tell there were a few batches that failed, so it only got to the top of the queue again 2 hours ago.)

[Riccardo Brasca]

I am a little confused about the pen and paper proof of the dual snake lemma: we have $f^\bullet \colon M^\bullet \to N^\bullet$, of controlled norm and almost surjective. Let $K^\bullet$ be the system of kernels (let's ignore all the $c$, $kc$ and so on, so no restriction). We want to prove that $K^\bullet$ is blah blah exact. Let $x \in K^i$, so $x \in M^i$ and I can use exactness of $M^\bullet$ to produce $y \in M^{i-1}$. But then I don't know what to do... maybe check the proof the standard snake lemma...

[Adam Topaz]

what are the assumptions on f?

[Riccardo Brasca]

variables (M M' N : system_of_complexes.{u}) (f : N ⟶ M) (g : M ⟶ M')

lemma weak_normed_snake_dual {k k' K K' r₁ r₂ : ℝ≥0}
  [hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')]
  {m : ℕ} {c₀ : ℝ≥0}
  (hM : M.is_weak_bounded_exact k K (m+1) c₀)
  (hM' : M'.is_weak_bounded_exact k' K' (m+1) c₀)
  (hM_adm : M.admissible)
  (hg : ∀ c i (x : M c i), ∥g x∥ ≤ r₁ * ∥x∥)
  (Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (y : M' c i),
    ∃ (x : M c i), g x = y ∧ ∥x∥ ≤ r₂ * ∥y∥)
  (hg : ∀ c i, (f.apply : N c i ⟶ M c i).range = g.apply.ker)
  (hfker : system_of_complexes.is_kernel f) :
  N.is_weak_bounded_exact (k * k') (K' * (K + 1)) m c₀

[Riccardo Brasca]

The constants are random

[Riccardo Brasca]

I mean, the constants in the last line will be what it's given by the proof

[Riccardo Brasca]

is_kernel means morally that it is the inclusion of the kernel. With pen and paper N is the kernel of f.

[Adam Topaz]

Oh so the M and N are backwards in the above?

[Adam Topaz]

Ah that helps :)

[Riccardo Brasca]

Yes... sorry. (To double confuse someone will read this in 15 minutes, now the two messages have the same variables).

[Riccardo Brasca]

Mmh, maybe it is enough to go to $\cdot^{i-2}$

[Adam Topaz]

I mean the usual trick is to map the y with respect to g and see what happens.

[Adam Topaz]

What do you mean by going to i-2?

[Riccardo Brasca]

Let $z = g(y)$. Use exactness of $M'$ to produce $z_1 \in M'^{i-2}$, lift it to $y_1 \in M^{i-2}$. Now $d(y_1)-y \in N^{i-1}$.

[Adam Topaz]

Yeah that sounds right (at least from the usual snake lemma)

[Riccardo Brasca]

Yes, for some reasons I wanted to play with $M^{i-1}$ and $M^{i+1}$ rather than using $M^{i-2}$

[Riccardo Brasca]

Riccardo Brasca said:

Let $z = g(y)$. Use exactness of $M'$ to produce $z_1 \in M'^{i-2}$, lift it to $y_1 \in M^{i-2}$. Now $d(y_1)-y \in N^{i-1}$.

Hmm, $d(y_1)-y \in N^{i-1}$ it's not true... I will think about it tomorrow.

[Patrick Massot]

I'll be able to help tomorrow evening if sleeping on it is not enough.

[Kevin Buzzard]

What's the question? What is $y$?

[Patrick Massot]

No idea. I haven't been following this at all, I can only see this is in the portion of the project where I can easily help.

[Riccardo Brasca]

Riccardo Brasca said:

I am a little confused about the pen and paper proof of the dual snake lemma: we have $g^\bullet \colon M^\bullet \to M'^\bullet$, of controlled norm and almost surjective. Let $N^\bullet$ be the system of kernels (let's ignore all the $c$, $kc$ and so on, so no restriction). We want to prove that $N^\bullet$ is blah blah exact. Let $n \in N^i$, so $n\in M^i$ and I can use exactness of $M^\bullet$ to produce $y \in M^{i-1}$. But then I don't know what to do... maybe check the proof the standard snake lemma...

This was my original question

[Riccardo Brasca]

I am trying to prove this

variables (M M' N : system_of_complexes.{u}) (f : N ⟶ M) (g : M ⟶ M')

lemma weak_normed_snake_dual {k k' K K' r₁ r₂ : ℝ≥0}
  [hk : fact (1 ≤ k)] [hk' : fact (1 ≤ k')]
  {m : ℕ} {c₀ : ℝ≥0}
  (hM : M.is_weak_bounded_exact k K (m+1) c₀)
  (hM' : M'.is_weak_bounded_exact k' K' (m+1) c₀)
  (hM_adm : M.admissible)
  (hg : ∀ c i (x : M c i), ∥g x∥ ≤ r₁ * ∥x∥)
  (Hg : ∀ (c : ℝ≥0) [fact (c₀ ≤ c)] (i : ℕ) (hi : i ≤ m+1+1) (y : M' c i),
    ∃ (x : M c i), g x = y ∧ ∥x∥ ≤ r₂ * ∥y∥)
  (hg : ∀ c i, (f.apply : N c i ⟶ M c i).range = g.apply.ker)
  (hfker : system_of_complexes.is_kernel f) :
  N.is_weak_bounded_exact (k * k') (K' * (K + 1)) m c₀

Where the constants at the end can be changed to whatever needed.

[Peter Scholze]

Small typo: In the blueprint, in Definition 5.11, the complex looks like a homological complex, but it's cohomological

[Johan Commelin]

Thanks, fixed.

[Peter Scholze]

So around $2^3$ or so. Impressive! It's about the factor I'd have expected for a properly digested normal writeup.

[Kevin Buzzard]

I'm still trying to get back up to speed mathematically. is_weak_bounded_exact k K m c₀ is presumably the "weakly $\leq k$-exact in degrees $\leq m$ and for $c\geq c_0$ with bound $K$" in Def 4.8 of the blueprint.

[Kevin Buzzard]

and the claim is basically of the form "the kernel of a surjection of weakly bounded exact systems of complexes is weakly bounded exact (with some different constants, and in particular the degree changes a bit)"

[Peter Scholze]

Right. It's like 4.13 in the blueprint, and the proof ought to be similar

[Kevin Buzzard]

oh this is so cool, I can click on the blueprint and go directly to the Lean code

[Johan Commelin]

Status update:

• @Patrick Massot and @Scott Morrison worked out all the constants! :tada: :octopus:
• @Adam Topaz is making really good progress on 8.19. I get the impression he's 90% done. (Correct me if I'm wrong.)
• I'm working on col_exact and things are going according to plan. My guess is that in a couple of days this will be done.

So I hope that 9.5 will be sorry-free around the end of the month.

[Johan Commelin]

I've made some updates to the blueprint. In particular, I commented out some of the lemmas that we don't really need. So the graph now looks as follows: https://leanprover-community.github.io/liquid/dep_graph.html

[David Michael Roberts]

Nice! normedcompletion looks a little lonely there, with no child notes, though... It looks important, though, so I guess it will actually come into play later?

[Johan Commelin]

No, I think we actually don't need it.

[Johan Commelin]

So I just pushed a commit that also comments that one out.

[Johan Commelin]

In the formal proof everything goes via locally constant functions.

[David Michael Roberts]

I like how in canonical_iso_2 it's written as LHS=RHS. :wink: @Kevin Buzzard would be proud

[Johan Commelin]

Right! It's canonical :wink:

[Adam Topaz]

@Johan Commelin not sure about 90% :wink: I spent all of yesterday afternoon proving that the terms in the Cech nerve commute with limits. Tidy decided to give up on me from the beginning, so it was much harder than I expected :)

[Johan Commelin]

Hmmz, that's unfortunate.

[Johan Commelin]

So is 75% more realistic?

[Adam Topaz]

Let's say 80%

[Adam Topaz]

Adam Topaz said:

Let's say 80%

Make that 90% -- The proof of exists_clopen is finished, showing that when a profinite set $X$ is a cofiltered limit of profinite sets $X_i$, any clopen set $U$ of $X$ arises from some clopen $U_i$ in some $X_i$.

[Peter Scholze]

What's left?

[Adam Topaz]

I still need to promote that to arbitrary discrete quotients.

[Adam Topaz]

Once that's done, the final three sorry's for 8.19 should be doable

[Adam Topaz]

To be fair, the index category I've been working with here is a semilattice_inf not a general cofiltered category, because we don't have the definition of cofiltered in mathlib :expressionless: (we have filtered but working with opposites is a huge pain), so the result is a bit specialized for our context.

[Peter Scholze]

OK, that's fine...

[Peter Scholze]

(I mean, I hope that the profinite sets that Johan wants to apply this to have the required shape)

[Adam Topaz]

They do. The terms in the Cech nerve of an arrow $X \to Y$ are limits over the discrete quotients of X, which is such a semilattice_inf

[Adam Topaz]

But I hope that Johan doesn't have to worry about such things once 8.19 is done :wink:

[Johan Commelin]

I'm already using 8.19 as stated. It works great.

[Peter Scholze]

Oh right, I see, you have the freedom to write your profinite sets in any way you like.

[Johan Commelin]

I just showed that the canonical hom between the simplicial profinite sets is compatible with restriction inclusion maps coming from $c_1 \le c_2$.
Sorry count:

3       src/prop819.lean
1       src/thm95/pfpng_iso.lean
2       src/thm95/col_exact.lean
2       src/prop819/locally_constant.lean
3       src/for_mathlib/Profinite/clopen_limit.lean
1       src/for_mathlib/Profinite/locally_constant.lean
Total:  12

[Johan Commelin]

For col_exact (modulo 8.19) I need to show that this canonical hom that comes from the Cech nerve adjunction is bijective.
And we need this $(rescale M^n)^N = rescale ((M^N)^n)$ isomorphism, and show that it is compatible with the summation maps $\sum \colon \_ \to M^n$

[Scott Morrison]

Adam Topaz said:

(we have filtered but working with opposites is a huge pain)

I don't particularly mind doing the copy-and-paste dualisation to obtain cofiltered, if you'd then use it.

[Adam Topaz]

Adam Topaz said:

I still need to promote that to arbitrary discrete quotients.

This is now done..

[Adam Topaz]

Scott Morrison said:

Adam Topaz said:

(we have filtered but working with opposites is a huge pain)

I don't particularly mind doing the copy-and-paste dualisation to obtain cofiltered, if you'd then use it.

I would be happy to use it! At some point we should add to mathlib the fact that Profinite is equivalent to Pro(Fintype), and it would surely be useful for that. For now, in LTE, I'm happy sticking to the semilattice_inf's

[Scott Morrison]

#7731

[Adam Topaz]

Adam Topaz said:

Let's say 80%

Make that 100%

[Adam Topaz]

Now it's time to catch up on 1591 emails

[Johan Commelin]

The covid numbers in NL have gone down enough that Germany thinks it is safe to visit again. So we have just packed all our bags, and tomorrow we'll be driving to NL for 8 hours to visit family for a week.

[Johan Commelin]

This means that the final sorry will have to wait a bit before it is killed. It might be Monday before I have time again.
Sorry for the cliff hanger.

[Johan Commelin]

1       src/polyhedral_lattice/cosimplicial_extra.lean
Total:  1

[Johan Commelin]

Hahaha, as usual, when you give up and go to bed... you can't sleep. And then you realize the correct proof. And you have to finish it.

[Johan Commelin]

I'm currently building locally. :time_ticking:

[Johan Commelin]

Pushed :octopus: :tada: :checkered_flag:

[Johan Commelin]

Now I really need to go to bed

[Scott Morrison]

Compiles at this end as well!

[Adam Topaz]

I'm still staring at a yellow dot on github...

[Scott Morrison]

It's gone green!

[Adam Topaz]

The octocat agrees! :boom:
Screenshot_2021-05-28-leanprover-community-lean-liquid.png

[David Michael Roberts]

Awesome. Next step? ;-P

[Scott Morrison]

Empty the for_mathlib directory? :-)

[Scott Morrison]

bitrot in 3... 2... 1... :-)

[Adam Topaz]

Scott Morrison said:

Empty the for_mathlib directory? :-)

Despite the emoji, I think this might be the correct answer...

[Scott Morrison]

I guess one step that is probably worth doing now is to install the "automatically upgrade mathlib, and notify us if things break" script, as an initial step to avoid bitrot.

[Scott Morrison]

That however makes interesting next steps slightly harder, because we probably still want manual control of bumping mathlib while new targets are being worked on.

[Scott Morrison]

#7740

[Scott Morrison]

#7741 and #7742!

[Adam Topaz]

docs#homological_complex.eval_at

[Adam Topaz]

Just pointing it out.... it's a bit late here and I'm tired so I probably shouldn't review these tonight, but if they're still up I'll look tomorrow

[Scott Morrison]

Thanks! I'll deduplicate.

[Scott Morrison]

#7743 and #7744

[Scott Morrison]

After PR'ing something then realising it wasn't actually used in LTE, I took the liberty of moving files in for_mathlib that aren't actually imported outside that directory into a for_mathlib/unused/ folder. Hopefully authors can salvage and delete those.

[Johan Commelin]

Scott Morrison said:

I guess one step that is probably worth doing now is to install the "automatically upgrade mathlib, and notify us if things break" script, as an initial step to avoid bitrot.

That's already done. It plays very well with manual bumps. The script has taken care of 50% of our mathlib bumps, I think.

[Johan Commelin]

Thanks everyone for the really cool journey to first_target. I'll see when I'm in NL. Now the 8hr car trip :car: :sweat_smile:

[Riccardo Brasca]

Have a safe trip! The perfect moment for taking a break!!

[Peter Scholze]

Whohoo!! Congratulations!! Truly amazing work!!! :champagne:

[Kevin Buzzard]

Yes, congratulations Johan and everyone else. I agree that for_mathlib should at least be where our attention goes for a while, even though it's boring work. I've designed and redesigned gradings on rings and I've still not made the PR but we saw with our own eyes in the perfectoid project that it's really important to remember that files which compile fine and do interesting things in directories called things like for_mathlib are still unfinished work, and the longer you leave it to finish them the harder it gets

[Patrick Massot]

There is something even more urgent than emptying the for_mathlib folder, at least if we want to communicate about this first step (knowing Kevin, I'm probably writing the message too late). We should identify the trusted code base and review it. I'm not talking about Lean here. I'm perfectly happy to trust the logical foundations of Lean and the Lean kernel. I'm talking about the definitions in the project. We need to list all definitions (transitively) entering the main statement and make sure they are checked by people who really understand the math.

[Patrick Massot]

This goes with another step which can be parallel to the PRing step: improving documentation through all the project.

[Kevin Buzzard]

I was tempted to tweet about it last night but Johan encouraged me to hold off until the graph was updated

[Sebastien Gouezel]

Is the linter happy about the project?

[Patrick Massot]

I really think nobody should tweet about this before Peter is ready to say: I checked they got all definitions and the statement of 9.4 right, and Lean checked the proofs. I know it sounds like I'm giving orders to Peter, but I'm very confident he is interested enough in this project to know this is the right thing to do.

[Patrick Massot]

I don't think there is any linter setup here.

[Scott Morrison]

The linter would certainly not be happy with the status of doc-strings...

[Sebastien Gouezel]

Setting it up would be extremely helpful, both for documentation (it would force you to document all the defs) and for spotting thousands of tiny mistakes.

[Scott Morrison]

I'm supportive of Patrick's suggestion to hold off for a bit. I don't think there is urgency is make an announcement. Some tidying up of documentation would go a long way to making the effort intelligible to outsiders who come to have a look after such an announcement.

[Patrick Massot]

I would say that adding all those docstrings (including module docstrings), with very special emphasis for the one that are needed to double check the statement of the first target, is now our top priority.

[Patrick Massot]

But we can work on mathlib PR in parallel.

[Scott Morrison]

How hard is it to add links back to the blueprint from doc-strings? I think having links in both directions for every important definition is a good idea.

[Patrick Massot]

From docstrings where? On GitHub? In VSCode? On a dedicated webpage?

[Peter Scholze]

I agree! I also thought to myself that now is the time to really verify that you've actually proved the right theorem. What's the best way to proceed? I think I've seen enough Lean code that I can more-or-less parse its grammar and so should be able to tell whether a definition is correct (but I might overlook things where it looks correct but Lean reads it differently than you might think). Maybe you can put some links here to things for me to look at?

[Scott Morrison]

I just meant putting actual URLs in the doc-strings.

[Scott Morrison]

So there's no need for a rendering step that converts tags to clickable links.

[Patrick Massot]

Peter, we are not quite ready. We need to write more documentation for you and we need to build an accurate list of what you should review.

[Patrick Massot]

Hopefully we can do this pretty quickly.

[Peter Scholze]

Sure, take your time! I just wondered about how we'll proceed. In any case, let me know when/what I should look at.

[Patrick Massot]

Actually we have to do it quickly, before the enthusiasm goes down.

[David Michael Roberts]

Whoops, I got excited and told the world. But I'm not part of the team, so I hope it's treated as unofficial

[Kevin Buzzard]

That's fine

[Kevin Buzzard]

News gets around anyway

[Kevin Buzzard]

People on the Discord know because I was talking about it on the voice chat

[Kevin Buzzard]

@Patrick Massot Johan is away for the weekend but I think I should have some time and I'm happy to do some stuff. Can you suggest a concrete job which I would be capable of doing competently so I can work on it today?

[Kevin Buzzard]

Otherwise I can keep working on the algebraic grading stuff. Johan has suggested a complete refactor of that so I have plenty to do

[Kevin Buzzard]

I was complaining that I was making an API for additive monoids graded by submonoids and also additive groups graded by subgroups and he suggested that if l restrict to the case where addition is commutative (which covers all use cases I know about) then I could just be grading modules by submodules over some fixed base semiring which could be nat or int if I want to recover the other cases

[Mario Carneiro]

Can someone summarize what was accomplished? Is it the whole project or just an intermediate lemma? first_target sounds like there might be a second target

[Patrick Massot]

David Michael Roberts said:

Whoops, I got excited and told the world. But I'm not part of the team, so I hope it's treated as unofficial

It's probably only because I'm a grumpy old man who understands nothing to Tweeter, but I think we live in a very weird world. I think this is not only incredibly rude to everyone who has been actively involved, especially Peter and Johan. It's also extremely unwise for advertisement purposes. If it turns out we messed up something and need a couple of weeks or even months to fix it then everybody will only remember that formalized mathematics can be wrong.

[Patrick Massot]

Mario, you very correctly interpreted that name. The official target of the project, as defined in Peter's original blog post is not formalized yet. Johan estimated that we are half way through.

[Patrick Massot]

Kevin, you have a very concrete job that you know how to do: docstrings, docstrings, docstrings.

[Kevin Buzzard]

OK I will go for top down docstrings.

[Peter Scholze]

@Mario Carneiro Yes, it's the first target. But as far as the mathematical content that I was unsure about is concerned, all of it is in this first target. So the experiment is not yet done, but now I am 100% confident that the argument works. (Will double-check the theorem statement of course, but I'm confident that you formalized the right thing.)

[Kevin Buzzard]

So let me try and understand the state of things. All references to theorem numbers refer to [Analytic].

• Peter's challenge is to formalise a statement and proof of a special case of 9.1
• Directly under the statemnt of 9.4 there is a very short proof that 9.4 -> 9.1
• We've got a formal proof of 9.4 in the sense that there is some explicit sorry-free line in the repo which we are claiming is this.

Am I right so far?

[Kevin Buzzard]

Questions which one might want to address in the README:
1) Is it meaningful to attach a de Bruijn factor to the work? What are the issues which mathematicians might have with this metric or an implementation of it?
2) The precise line of code which we are claiming is a proof of 9.4 and comments about what we might mean by this claim.

[Chris Birkbeck]

That is amazing! Congratulations!

[Peter Scholze]

@Kevin Buzzard Yes, that's a good summary. It should be noted that the proof of 9.4 --> 9.1 uses a lot of preliminary work: In particular, it is here that any actual condensed mathematics enters. So the relevant part of the manuscript is much more (and much more diffuse) than those few lines of [Analytic].

Another thing worth taking note of is that there's even a bit of work to do to see that 9.1 implies the statement of the challenge; namely, the comparison between those spaces of measures over the crazy ring $\mathbb Z((T))_r$, and the spaces of $p$-measures over the reals. This is in Lecture 7, and rather simple, but might also take a little bit of time to do in Lean.

[Patrick Massot]

Clearly we will have a lot of blueprint work to do before starting the formalization of this second target.

[Patrick Massot]

Actually we also have blueprint work to do on the first target. For instance the blueprint still pretends this proposition isn't used anywhere

[Patrick Massot]

and also that it hasn't been formalized

[Adam Topaz]

Patrick Massot said:

Actually we also have blueprint work to do on the first target. For instance the blueprint still pretends this proposition isn't used anywhere

Yeah, I kind of bypassed it

[Patrick Massot]

Really? did you at least used this one somewhere?

[Patrick Massot]

It's a bit frustrating that several of the lemmas I was asked to prove weren't actually useful (the other one was the fact that weakly exact implies strongly exact for complete groups).

[Adam Topaz]

I used controlled_exactness

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/blob/3f8ca3bf7f0eae69606a931b4c423fd6276f71bc/src/normed_group/controlled_exactness.lean#L18

[Patrick Massot]

Oh, so you didn't bypass anything. The lemma I pointed out took all its content from controlled_exactness

[Adam Topaz]

Sure. I didn't actually see why we needed the 4-term complex version (i.e.. the one you pointed to)

[Patrick Massot]

So we should simply remove the lemmas that is stated in terms of 4-term complexes

[Johan Commelin]

Patrick Massot said:

It's a bit frustrating that several of the lemmas I was asked to prove weren't actually useful (the other one was the fact that weakly exact implies strongly exact for complete groups).

That's going to be one of the first things that we will use in the proof 9.4 => 9.1. So don't worry, it will be used in the end.

[Patrick Massot]

Well, the 4-terms complexes version is Peter's version

[Patrick Massot]

Hey! Are you done with driving?

[Johan Commelin]

Yes, we arrived around 14:00

[Adam Topaz]

just a word of warning: I had to increase the default deterministic timeout bound to work on src/prop819.lean after Scott's changes from yesterday

[Patrick Massot]

I noticed this file takes a lot of time

[Adam Topaz]

it was slow before, but something changed yesterday that pushed it over the edge (I'm not sure what)

[Adam Topaz]

I'm working on cleaning it up

[Patrick Massot]

Beware I just pushed

[Johan Commelin]

Concerning the blueprint, I will write a detailed proof of col_exact now that I know the precise argument.

[Johan Commelin]

But it might be a couple of days before I get round to that.

[Patrick Massot]

Yes, this is part of the documentation effort we need to make now.

[Patrick Massot]

Where is 8.19 in the blueprint?

[Johan Commelin]

cechcover-exact

[Kevin Buzzard]

I have tidied up the README so that it now gives a global overview of what is done and what is not done, explained in a way which (hopefully) a mathematician with no Lean background can understand.

[Peter Scholze]

@Patrick Massot Actually, without your proof that weak exact implies exact, I still wouldn't be 100% confident in the proof

[Patrick Massot]

Nice!

[Peter Scholze]

So I only regard the current first_target in combination with that fact to push it to 100% confidence level (note that the actual formulation of 9.4 in [Analytic] is for actual exactness)

[Johan Commelin]

Tiny remark: technicaly, right now, there is no formal proof of a statement that exactly matches 9.4 or 9.5.

(i) Both statements use strong exactness, we only have formal proofs of weak exactness. But together with Patrick's lemma, we can very easily move from weak exactness to strong exactness.
(ii) The statement of 9.4 in [Analytic] is for $\overline{\mathcal M}_{r'}(S)$ with $S$ profinite. We have only formalized Mbar r' S for finite S at the moment.

Conclusion: we can easily state and prove an exact match of 9.5 right now. For 9.4 we need to do more work, because we need to generalize the definition of Mbar r' S (and in particular make it functorial in S) and then deduce weak-but-profinite-9.4 from weak-and-finite-9.4 (which we have). After that, we can derive strong-and-profinite-9.4 using Patrick's lemma.

Peter pointed out that the other side of the square weak-and-finite-9.4 -> strong-but-finite-9.4 -> strong-and-profinite-9.4 leads to worse constants, because the finite -> profinite step pushes you to go via weak-but-profinite-9.4 anyways.

[Johan Commelin]

I regard all of this as part of second_target.

[Johan Commelin]

But if we want to announce a formal proof of 9.5, we can of course spend 5 minutes to state and prove the strong exact version. It's good to be aware that we will not actually use that precise version in second_target which is why I hadn't bothered stating it so far.

[Peter Scholze]

As long as you didn't smuggle in any dependence on the finite set $S$ into the constants, I regard the difference between these statements as tiny. Still, for PR purposes, it might be good to make the small step of stating the precise version of 9.5 from [Analytic]; this would also make it more obvious that there are no leaves in the dependency graph. (The only other leaves are statements ensuring that the hypotheses of 9.5 can actually be satisfied.)

[Johan Commelin]

I am currently on a horrible internet connection. So I can't use Lean interactively on the beast in my cellar back in Germany.

[Johan Commelin]

If someone else wants to do the proper version of 9.5, that would be great.

[Johan Commelin]

I'll restrict myself to working on the blueprint and docstrings. Because that can be done in text-only mode.

[Johan Commelin]

Haha, I've got a better internet connection now, and now that I try to do this, it is of course more work than 5 minutes :rofl:

[Johan Commelin]

First, it became clear that due to some carelessness there were unused assumptions in the theorems

[Johan Commelin]

Secondly, we need to show that we are working with a system of complexes whose objects are separated and complete.

[Johan Commelin]

And this is not true by definition, because we are taking those $T^{-1}$-invariants.

[Johan Commelin]

Quick update: I'll be visiting family next week. So I won't be very active.