Zulip Chat Archive

Stream: condensed mathematics

Topic: status update


view this post on Zulip Johan Commelin (Mar 29 2021 at 09:28):

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 T1T^{-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".

view this post on Zulip Scott Morrison (Mar 29 2021 at 09:33):

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

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 09:36):

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.

view this post on Zulip Johan Commelin (Mar 29 2021 at 09:38):

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

view this post on Zulip Johan Commelin (Mar 29 2021 at 09:38):

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.

view this post on Zulip Johan Commelin (Mar 29 2021 at 09:39):

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

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 09:40):

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

view this post on Zulip Riccardo Brasca (Mar 29 2021 at 09:41):

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

view this post on Zulip Patrick Massot (Mar 29 2021 at 10:56):

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

view this post on Zulip Johan Commelin (Mar 29 2021 at 11:51):

I will try to give a (very informal!) lecture on this proof tomorrow. I propose that we start .
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.

view this post on Zulip Johan Commelin (Mar 29 2021 at 11:59):

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.

view this post on Zulip Kevin Buzzard (Mar 29 2021 at 12:11):

Will you video it?

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

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

view this post on Zulip Riccardo Brasca (Mar 29 2021 at 12:37):

I have a pro account

view this post on Zulip Peter Scholze (Mar 29 2021 at 12:53):

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

view this post on Zulip Johan Commelin (Mar 29 2021 at 12:54):

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

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

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

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

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

view this post on Zulip Johan Commelin (Mar 29 2021 at 12:57):

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

view this post on Zulip Peter Scholze (Mar 29 2021 at 12:58):

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

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

Ok, se we reschedule to ? Is that ok with @Riccardo Brasca @Julian Külshammer @Kevin Buzzard @Patrick Massot @Scott Morrison ?

view this post on Zulip Riccardo Brasca (Mar 29 2021 at 12:59):

OK for me

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

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

view this post on Zulip Peter Scholze (Mar 29 2021 at 12:59):

Sounds good to me!

view this post on Zulip Damiano Testa (Mar 29 2021 at 13:00):

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!

view this post on Zulip Adam Topaz (Mar 29 2021 at 13:00):

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:

view this post on Zulip Johan Commelin (Mar 29 2021 at 13:01):

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

view this post on Zulip Filippo A. E. Nuccio (Mar 29 2021 at 13:02):

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

view this post on Zulip Johan Commelin (Mar 29 2021 at 13:05):

Zulip shows times enytered with <time in your local timezone

view this post on Zulip Mario Carneiro (Mar 29 2021 at 13:05):

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

view this post on Zulip Filippo A. E. Nuccio (Mar 29 2021 at 13:08):

@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.

view this post on Zulip Riccardo Brasca (Mar 29 2021 at 13:27):

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

view this post on Zulip Mario Carneiro (Mar 29 2021 at 14:25):

view this post on Zulip Riccardo Brasca (Mar 29 2021 at 14:29):

The "official" starting time is , I will open the zoom meting a little in advance just to be sure that everything works

view this post on Zulip Johan Commelin (Mar 30 2021 at 08:45):

I finished my preparations :sweat_smile:

view this post on Zulip Johan Commelin (Mar 30 2021 at 10:56):

2021_03_lte_overview.pdf

view this post on Zulip Johan Commelin (Mar 30 2021 at 10:57):

:up: slides for the lecture

view this post on Zulip Scott Morrison (Mar 30 2021 at 10:57):

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". :-)

view this post on Zulip Scott Morrison (Mar 30 2021 at 11:08):

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. :-)

view this post on Zulip Johan Commelin (Mar 30 2021 at 11:09):

breen_deligne/functorial_map.lean

view this post on Zulip Adam Topaz (Mar 30 2021 at 13:31):

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

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 13:33):

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

view this post on Zulip Johan Commelin (Mar 30 2021 at 13:47):

yes, fine with me

view this post on Zulip Johan Commelin (Mar 30 2021 at 13:47):

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

view this post on Zulip Peter Scholze (Mar 30 2021 at 13:49):

Not sure if it needs to be on youtube?

view this post on Zulip Johan Commelin (Mar 30 2021 at 13:52):

It doesn't really have to, I agree.

view this post on Zulip Johan Commelin (Mar 30 2021 at 13:52):

It's just that recordings are typically quite large

view this post on Zulip Adam Topaz (Mar 30 2021 at 13:57):

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

view this post on Zulip Peter Scholze (Mar 30 2021 at 13:58):

aren't the recordings saved locally?

view this post on Zulip Peter Scholze (Mar 30 2021 at 13:59):

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

view this post on Zulip Adam Topaz (Mar 30 2021 at 13:59):

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

view this post on Zulip Peter Scholze (Mar 30 2021 at 14:00):

I see

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:02):

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

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 14:06):

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

view this post on Zulip David Michael Roberts (Mar 30 2021 at 14:13):

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).

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:15):

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

view this post on Zulip David Michael Roberts (Mar 30 2021 at 14:16):

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.

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 14:22):

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

view this post on Zulip Johan Commelin (Mar 30 2021 at 14:27):

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

view this post on Zulip Johan Commelin (Mar 30 2021 at 14:27):

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

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 14:31):

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

view this post on Zulip Damiano Testa (Mar 30 2021 at 14:33):

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:

view this post on Zulip Filippo A. E. Nuccio (Mar 30 2021 at 14:35):

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

view this post on Zulip Peter Scholze (Mar 30 2021 at 14:43):

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

view this post on Zulip Kevin Buzzard (Mar 30 2021 at 14:47):

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

view this post on Zulip Adam Topaz (Mar 30 2021 at 14:51):

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 :)

view this post on Zulip Bhavik Mehta (Mar 30 2021 at 14:55):

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

view this post on Zulip Filippo A. E. Nuccio (Mar 30 2021 at 15:14):

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.

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 17:26):

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

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 17:27):

let me know if it doesn't work

view this post on Zulip Johan Commelin (Mar 30 2021 at 17:27):

How long does Zoom host it?

view this post on Zulip Johan Commelin (Mar 30 2021 at 17:28):

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.

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 17:28):

one year I think, but I am downloading it

view this post on Zulip Johan Commelin (Mar 30 2021 at 17:29):

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

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 17:30):

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

view this post on Zulip Riccardo Brasca (Mar 30 2021 at 17:50):

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

view this post on Zulip Filippo A. E. Nuccio (Mar 30 2021 at 17:52):

Works like a charm for me.

view this post on Zulip Johan Commelin (Mar 31 2021 at 06:17):

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


Last updated: May 09 2021 at 15:11 UTC