Zulip Chat Archive

Stream: condensed mathematics

Topic: github issues


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

We are reaching a point where we can branch into little subprojects again. (The past two weeks consisted in tying lots of loose ends together into the proof of 9.6)
To keep some overview of who is doing what, I suggest that we assign github issues to whoever is working (or wants to work on) a particular subproject. See https://github.com/leanprover-community/lean-liquid/issues
As you can see, I've assigned Gordan's lemma to @Damiano Testa and Proposition 8.17 to @Patrick Massot

view this post on Zulip Damiano Testa (Mar 15 2021 at 15:12):

Johan,

thank you so much for your efforts! I will be more active on a proof of Gordan's lemma, once this week is over: it is the last week of term and I am very busy most of the day, most of the days!

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

If you're splitting into small things again, another such thing is 9.2. (Besides its importance for 9.4 => 9.1, it's also used in the proof of 9.5)

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

yes, I noticed that

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

One actually needs a slightly more general version, replaceing Mr(S)ca\overline{\mathcal M}_{r'}(S)^a_{\leq c} with Hom(Λ,Mr(S))ca\mathrm{Hom}(\Lambda,\overline{\mathcal M}_{r'}(S))^a_{\leq c}

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

Shouldn't it be true for any profinitely_filtered_pseudo_normed_group_with_Tinv?

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

Oh, yes, of course

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

I'll change this in the blueprint right now

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

@Johan Commelin I don't know if I got the procedure you had in mind right, but I went to the issues page and assigned myself to Lemma 9.7.

view this post on Zulip Johan Commelin (Mar 15 2021 at 18:13):

Thanks, sounds good


Last updated: May 09 2021 at 22:13 UTC