github access

Stream: new members

[Carlos Caralps]

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 non-master branches of mathlib. I’d like to do my first PR with those lemmas.
carloscaralps
Thanks!

[Kevin Buzzard]

Your github userid is carloscaralps? Nice stuff! Is this being run by Marc?

[Markus Himmel]

I sent you an invite, it should appear at https://github.com/leanprover-community/mathlib/invitations

[Carlos Caralps]

Yes, my userid is carloscaralps and @Marc Masdeu is running the seminar

[Carlos Caralps]

Thanks!

[Kevin Buzzard]

Great! I did some stuff with topological spaces with my students a couple of months ago: https://xenaproject.wordpress.com/2021/02/10/formalising-mathematics-workshop-4/

[Marc Masdeu]

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]

Thanks for the link!

[Patrick Massot]

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]

I would like to get into contributing to mathlib, could I get permission to push to a non-master 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]

@Jon Eugster Voila: https://github.com/leanprover-community/mathlib/invitations

[Jon Eugster]

thank you!

[Jon Eugster]

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]

If you're new to the PR process then there will be no harm in discussing potential PR's here.

[Kevin Buzzard]

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]

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]

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 the fraction_ring case and state the above for commutative rings/algebras with this injectivity assumption.
  3) go into the definition of a fraction_ring (i.e. look at localization.r) and prove it there.

• I could also see multiple places to locate this:
  1) a new file algebra/char_p/localization.lean
  2) in ring_theory/localization.lean (but seems silly to import char_p there)
  3) ring_theory/localization.lean is about 1700 lines long, the last 30 thereof defining fraction_ring, at which point does it make sense to split this up into ring_theory/localization/basic.lean and ring_theory/localization/fraction_ring.lean?

Any recommendations?

[Scott Morrison]

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]

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]

Certainly don't go with 2) --- adding new imports to already big files is a pain.

[Ender Doe]

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 Gin-ge Chen]

Invite sent! https://github.com/leanprover-community/mathlib/invitations

[Paul Lezeau]

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 Paul-Lez.
Thanks a lot !

[Anne Baanen]

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]

I'll have a look. Where can I find invitations I have received on GitHub ?

[Anne Baanen]

In your notifications I believe: https://github.com/notifications

[Anne Baanen]

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]

Oh ok ! Well I haven't received any invite.

[Alex J. Best]

I'm also having issues with github right now, so probably its a global thing?

[Anne Baanen]

Just tried for a third time, looks like I can't make it work :(

[Eric Wieser]

https://www.githubstatus.com/

[Anne Baanen]

Oh yeah, https://www.githubstatus.com/ is reporting a lot of issues

[Paul Lezeau]

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]

Oh, that would be a great addition!

[Anne Baanen]

(Did another of the @maintainers already try giving Paul-Lez access?)

[Bryan Gin-ge Chen]

I think I managed to send an invitation just now: https://github.com/leanprover-community/mathlib/invitations @Paul Lezeau

[Paul Lezeau]

That worked, thanks a lot !

[Kevin Buzzard]

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

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]

My post-doc 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 Cassels-Froelich.