## Stream: condensed mathematics

### Topic: status update

#### 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 $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 (Mar 29 2021 at 09:33):

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

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

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

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

#### Johan Commelin (Mar 29 2021 at 09:39):

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

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

#### 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!

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

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

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

#### Kevin Buzzard (Mar 29 2021 at 12:11):

Will you video it?

#### 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?

#### Riccardo Brasca (Mar 29 2021 at 12:37):

I have a pro account

#### 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

#### Johan Commelin (Mar 29 2021 at 12:54):

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

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

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

#### Peter Scholze (Mar 29 2021 at 12:56):

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

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

#### 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 ;-)

#### 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 ?

OK for me

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

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

#### Peter Scholze (Mar 29 2021 at 12:59):

Sounds good to me!

#### 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!

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

#### Johan Commelin (Mar 29 2021 at 13:01):

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

#### Filippo A. E. Nuccio (Mar 29 2021 at 13:02):

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

#### Johan Commelin (Mar 29 2021 at 13:05):

Zulip shows times enytered with <time in your local timezone

#### 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

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

#### 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

Meeting ID: 814 4445 6365
Passcode: 235711

#### 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

#### Johan Commelin (Mar 30 2021 at 08:45):

I finished my preparations :sweat_smile:

#### Johan Commelin (Mar 30 2021 at 10:56):

2021_03_lte_overview.pdf

#### Johan Commelin (Mar 30 2021 at 10:57):

:up: slides for the lecture

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

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

#### Johan Commelin (Mar 30 2021 at 11:09):

breen_deligne/functorial_map.lean

#### Adam Topaz (Mar 30 2021 at 13:31):

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

#### 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

#### Johan Commelin (Mar 30 2021 at 13:47):

yes, fine with me

#### Johan Commelin (Mar 30 2021 at 13:47):

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

#### Peter Scholze (Mar 30 2021 at 13:49):

Not sure if it needs to be on youtube?

#### Johan Commelin (Mar 30 2021 at 13:52):

It doesn't really have to, I agree.

#### Johan Commelin (Mar 30 2021 at 13:52):

It's just that recordings are typically quite large

#### Adam Topaz (Mar 30 2021 at 13:57):

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

#### Peter Scholze (Mar 30 2021 at 13:58):

aren't the recordings saved locally?

#### Peter Scholze (Mar 30 2021 at 13:59):

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

#### 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

I see

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

#### Riccardo Brasca (Mar 30 2021 at 14:06):

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

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

#### Adam Topaz (Mar 30 2021 at 14:15):

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

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

#### 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

#### Johan Commelin (Mar 30 2021 at 14:27):

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

#### 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

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

#### Filippo A. E. Nuccio (Mar 30 2021 at 14:35):

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

#### 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

#### Kevin Buzzard (Mar 30 2021 at 14:47):

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

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

#### 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

#### Filippo A. E. Nuccio (Mar 30 2021 at 15:14):

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 (Mar 30 2021 at 17:27):

let me know if it doesn't work

#### Johan Commelin (Mar 30 2021 at 17:27):

How long does Zoom host it?

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

#### 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

#### Riccardo Brasca (Mar 30 2021 at 17:50):

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

#### Filippo A. E. Nuccio (Mar 30 2021 at 17:52):

Works like a charm for me.

#### 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