Zulip Chat Archive

Stream: Copenhagen Masterclass 2023

Topic: Profinite/Etrx disc are precoherent

Riccardo Brasca (Jun 26 2023 at 11:12):

I am working on it. Everyone is welcome to collaborate

Moritz Firsching (Jun 26 2023 at 11:13):

that sounds like fun

Ashvni Narayanan (Jun 26 2023 at 11:18):

I'll join too¬

Moritz Firsching (Jun 27 2023 at 10:47):

Does this need pr-ing to mathlib now, or are there dependencies missing? If so, which ones?

Riccardo Brasca (Jun 27 2023 at 10:48):

This depends on https://github.com/adamtopaz/CopenhagenMasterclass2023/pull/9

Riccardo Brasca (Jun 27 2023 at 10:48):

When that one is merged we can merge master and open a PR

Dagur Asgeirsson (Jun 27 2023 at 10:51):

Branch: dagur_ExtrDiscExplicitSheaves

Riccardo Brasca (Jun 27 2023 at 11:22):

https://github.com/adamtopaz/CopenhagenMasterclass2023/pull/10

Riccardo Brasca (Jun 27 2023 at 11:25):

We've mixed up two branches with about the equivalent conditions... let's just clean everything after the statement is merged.

Kevin Buzzard (Jun 27 2023 at 12:33):

The branch doesn't compile (I left a comment), but other than that it looks good.

Riccardo Brasca (Jun 27 2023 at 13:19):

It should be OK now

Last updated: Dec 20 2023 at 11:08 UTC