github issues

Stream: condensed mathematics

[Johan Commelin]

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

[Damiano Testa]

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!

[Peter Scholze]

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)

[Johan Commelin]

yes, I noticed that

[Peter Scholze]

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

[Johan Commelin]

Shouldn't it be true for any profinitely_filtered_pseudo_normed_group_with_Tinv?

[Peter Scholze]

Oh, yes, of course

[Johan Commelin]

I'll change this in the blueprint right now

[Filippo A. E. Nuccio]

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

[Johan Commelin]

Thanks, sounds good

[Filippo A. E. Nuccio]

It seems to me that github is experiencing some issues...I can't push getting an error fatal error in commit_refs, and also when I try to modify a file online I get a error 500, "Looks like something went wrong!". Someone else with the same problem?

[Alex J. Best]

Yes same :C