Zulip Chat Archive
Stream: new members
Topic: github access
Carlos Caralps (Apr 14 2021 at 10:41):
Hi there, I’m a math student. Last months I’ve been learning Lean being a participant of the Barcelona Lean Seminar. In this seminar we have focused our work in topological spaces with Lean and I’ve done some lemes about separation axioms.
I’d like to ask for permission to push to nonmaster branches of mathlib. I’d like to do my first PR with those lemmas.
carloscaralps
Thanks!
Kevin Buzzard (Apr 14 2021 at 10:42):
Your github userid is carloscaralps
? Nice stuff! Is this being run by Marc?
Markus Himmel (Apr 14 2021 at 10:43):
I sent you an invite, it should appear at https://github.com/leanprovercommunity/mathlib/invitations
Carlos Caralps (Apr 14 2021 at 10:45):
Yes, my userid is carloscaralps and @Marc Masdeu is running the seminar
Carlos Caralps (Apr 14 2021 at 10:47):
Thanks!
Kevin Buzzard (Apr 14 2021 at 10:51):
Great! I did some stuff with topological spaces with my students a couple of months ago: https://xenaproject.wordpress.com/2021/02/10/formalisingmathematicsworkshop4/
Marc Masdeu (Apr 14 2021 at 10:59):
Kevin, we are aware of your TCC workshops, the blog posts are extremely useful (at least to me). We did some basics (up to compacity and separation, you can see it at github.com/mmasdeu/barcelonaleanseminar), and one goal is to make the Topology Game. Right now, we decided to stop building topological spaces from scratch (we gave up when trying to prove that the Moebius band defined as a quotient of a square is homeomorphic to the strip as a subspace of R3), and move on to adapting all that we have to the Game.
Kevin Buzzard (Apr 14 2021 at 11:06):
Thanks for the link!
Patrick Massot (Apr 14 2021 at 13:56):
I can believe there are missing lemmas about the zoo of separation conditions in mathlib. However I'm a bit worried that the proof you will have won't blend nicely with mathlib if you didn't use filters all over the place.
Jon Eugster (May 22 2021 at 18:13):
I would like to get into contributing to mathlib, could I get permission to push to a nonmaster branch? My username is joneugster
.
I thought my first PR could be small contributions about fraction rings, like instance fraction_ring.char_zero [h: char_zero R]: char_zero (fraction_ring R)
as they should be very quick to review.
Johan Commelin (May 22 2021 at 18:22):
@Jon Eugster Voila: https://github.com/leanprovercommunity/mathlib/invitations
Jon Eugster (May 22 2021 at 18:27):
thank you!
Jon Eugster (May 24 2021 at 08:32):
Is it better to discuss mathlib PRs here on Zulip (i.e. file sturcture, generality) or to make a PR get feedback and refactor it afterwards?
Kevin Buzzard (May 24 2021 at 08:33):
If you're new to the PR process then there will be no harm in discussing potential PR's here.
Kevin Buzzard (May 24 2021 at 08:34):
But there is also no harm in making the PR and then starting a thread about it in #PR reviews . However if the PR costs hours of your time and then is instantly met with a "oh no we can't do it like that at all, for the following technical reason" then this would be a bit grim
Scott Morrison (May 24 2021 at 09:45):
The #PR reviews stream is also extremely useful if you don't get comments on your PR... Sometimes the queue exceeds our ability to shepherd it along, but lots of us are compulsively helpful here on zulip. :)
Jon Eugster (May 24 2021 at 09:53):
ok so I have a few questions about starting with mathlib PRs. I would like mathlib to know automatically that the characteristics of the fraction_ring R
of an integral domain is the same as the char. of R
. Something like:
import algebra.char_p.basic
import ring_theory.localization
namespace fraction_ring
variables (R: Type*) [integral_domain R] (p: ℕ)
instance char_p [h: char_p R p]: char_p (fraction_ring R) p := sorry
instance char_zero [h: char_zero R]: char_zero (fraction_ring R) := char_p.char_p_to_char_zero (fraction_ring R)
The main ingredient is that the algebra map R →+* fraction_ring R
is injective for an integral domain, which is (fraction_map.injective (fraction_ring.of R))

I could see this be stated in different generalities:
1) as above
2) have the injectivity as an instance for thefraction_ring
case and state the above for commutative rings/algebras with this injectivity assumption.
3) go into the definition of afraction_ring
(i.e. look atlocalization.r
) and prove it there. 
I could also see multiple places to locate this:
1) a new filealgebra/char_p/localization.lean
2) inring_theory/localization.lean
(but seems silly to importchar_p
there)
3)ring_theory/localization.lean
is about 1700 lines long, the last 30 thereof definingfraction_ring
, at which point does it make sense to split this up intoring_theory/localization/basic.lean
andring_theory/localization/fraction_ring.lean
?
Any recommendations?
Scott Morrison (May 24 2021 at 10:01):
I don't know this part of the library well, but I'll just say one thing: while splitting up large files (particularly where this significantly reduces imports to one or more chunks) is a good and valuable thing to do, it's often best to do it as a separate PR, either before or after the "content" PR, as it's much easier to review the content if we don't have to wade through the "just moving stuff" diffs.
Scott Morrison (May 24 2021 at 10:02):
Perhaps if this is your first PR it's safest to start off with using a new file, and then we'll remind you to move parts (or perhaps all) to other homes.
Scott Morrison (May 24 2021 at 10:03):
Certainly don't go with 2)  adding new imports to already big files is a pain.
Ender Doe (Aug 08 2021 at 22:31):
Hello :wave:, I have being working on formalizing the thomaes function with help from the Xena Discord, and along the way I think I have some lemmas worth PRing to mathlib.
I have been following this guide https://www.youtube.com/watch?v=Bnc8w9lxe8A, and am here to request credentials to push a branch.
Here is my GitHub account https://github.com/FrickHazard, cheers and thank you.
Bryan Ginge Chen (Aug 08 2021 at 22:32):
Invite sent! https://github.com/leanprovercommunity/mathlib/invitations
Paul Lezeau (Aug 10 2021 at 15:24):
Hi ! :wave:
I'm working on formalizing some algebraic number theory, and I have a few lemmas I'd like to PR to mathlib. Would it be possible to get PR access ? My GitHub username is PaulLez
.
Thanks a lot !
Anne Baanen (Aug 10 2021 at 15:30):
Hi! :wave: I tried to give you access, but I got an error 500. Maybe you already got the invite before GitHub broke?
Paul Lezeau (Aug 10 2021 at 15:32):
I'll have a look. Where can I find invitations I have received on GitHub ?
Anne Baanen (Aug 10 2021 at 15:32):
In your notifications I believe: https://github.com/notifications
Anne Baanen (Aug 10 2021 at 15:34):
What areas of algebraic number theory are you interested in? We are currently working on merging a proof of the finiteness of the class number in a number ring.
Paul Lezeau (Aug 10 2021 at 15:34):
Oh ok ! Well I haven't received any invite.
Alex J. Best (Aug 10 2021 at 15:35):
I'm also having issues with github right now, so probably its a global thing?
Anne Baanen (Aug 10 2021 at 15:36):
Just tried for a third time, looks like I can't make it work :(
Eric Wieser (Aug 10 2021 at 15:37):
Anne Baanen (Aug 10 2021 at 15:37):
Oh yeah, https://www.githubstatus.com/ is reporting a lot of issues
Paul Lezeau (Aug 10 2021 at 15:37):
Anne Baanen said:
What areas of algebraic number theory are you interested in? We are currently working on merging a proof of the finiteness of the class number in a number ring.
I'm working on formalizing Dedekind's theorem on factoring ideals $(p)$ in the ring of integers of a number field (under @Damiano Testa's supervision). It's great that you've already done so much !
Anne Baanen (Aug 10 2021 at 15:39):
Oh, that would be a great addition!
Anne Baanen (Aug 10 2021 at 15:40):
(Did another of the @maintainers already try giving PaulLez access?)
Bryan Ginge Chen (Aug 10 2021 at 16:45):
I think I managed to send an invitation just now: https://github.com/leanprovercommunity/mathlib/invitations @Paul Lezeau
Paul Lezeau (Aug 10 2021 at 16:51):
That worked, thanks a lot !
Kevin Buzzard (Aug 11 2021 at 06:41):
@Paul Lezeau A useful theorem to have would be proving that if $L/K$ is a finite extension of number fields and $P$ is a prime of $\mathcal{O}_K$ then $P\mathcal{O}_L$ factors as $\prod_{I=1}^gQ_i^{e_i}$ with $\sum_ie_if_i=[L:K].$
Paul Lezeau (Aug 11 2021 at 07:33):
A while back, you mentioned this could be obtained as a corollary of the result :
Kevin Buzzard said:
Here is something I would very much like to have in Lean: if $L/K$ is a finite extension of global fields and $P$ is a prime of $K$ which splits as $\prod_iQ_i^{e_i}$ in $L$ then $K_P\otimes_KL=\bigoplus_iL_{Q_i}$ for some value of $=$ (probably
≃+*
).
I'd be happy to work on it once I'm done with Dedekind's theorem. Do you have any references where I could find the proof ?
Kevin Buzzard (Aug 11 2021 at 07:44):
My postdoc Maria is thinking about adeles in Lean and she is going to need this kind of thing too, but this stream probably isn't the best place to talk about technicalities (it's about GitHub access). My instinct with global fields by the way is to not attempt to unify the definition and work with number fields and function fields separately. The proof I know of the completion result is in CasselsFroelich.
Last updated: Dec 20 2023 at 11:08 UTC