Zulip Chat Archive

Stream: new members

Topic: PR permission


Chris Birkbeck (Jul 26 2021 at 15:31):

Hello. So I've been playing around with lean for a bit now, but have yet to make a PR so I was thinking I should try to figure out how to do this now.
I wanted to try this out by adding some lean code for general linear groups as invertible matrices. Specifically, I defined them as matrices with unit determinant (in contrast to what is in lean at the moment which only has them as invertible linear maps) and have proven some simple things about them (for example they form a group). I've also defined the subgroup of matrices invertible matrices with positive determinant.

I'm not sure if this needs to be pre-checked, if so I've put the code here: https://gist.github.com/CBirkbeck/f6d0272020b065f787d3fdc7a2aaa476
(any tips/comments on the lean code are also very welcome as I'm quite new to this).

If not, I'm assuming I can just do a PR (once I get permission) and then go from there? btw my github username is cbirkbeck.

Thank you

Johan Commelin (Jul 26 2021 at 15:32):

@Chris Birkbeck https://github.com/leanprover-community/mathlib/invitations

Chris Birkbeck (Jul 26 2021 at 15:33):

Thank you!

Yakov Pechersky (Jul 26 2021 at 15:45):

Chris, have you considered working with "units (matrix n n R)"?

Yakov Pechersky (Jul 26 2021 at 15:47):

Then you can show that there's a group iso between the two.

Chris Birkbeck (Jul 26 2021 at 15:48):

Ah interesting. No, I was basing this on the special_linear_group file and went in that direction. Would it be better to define it that way?

Yakov Pechersky (Jul 26 2021 at 15:49):

Well, you get that it is a group "for free". And units has all the nice coe lemmas too.

Yakov Pechersky (Jul 26 2021 at 15:49):

Mathematically, they're all the same (provably), it's just a matter of which lends itself to the easiest API

Yakov Pechersky (Jul 26 2021 at 15:50):

Plus, there's a lemma that says that is_unit A.det iff is_unit A

Chris Birkbeck (Jul 26 2021 at 15:50):

Yes I see what you mean. I don't really know what makes a good API so I'm happy to follow tips from others

Yakov Pechersky (Jul 26 2021 at 15:52):

Is there something you want to prove specifically about GLn matrices, or just define them?

Eric Wieser (Jul 26 2021 at 15:53):

Yakov Pechersky said:

Chris, have you considered working with "units (matrix n n R)"?

Indeed src#linear_map.general_linear_group is defined as units (M →ₗ[R] M), so reusing the same approach would be sensible.

Yakov Pechersky (Jul 26 2021 at 15:53):

Having a theorem in mind helps develop the API. Definitions are conceptually expensive, they require a lot of "cruft", a lot of those basic coe and application lemmas. Those can be avoided with neat definitions. But regardless of the definitions, the main target should be proving something interesting about them.

Chris Birkbeck (Jul 26 2021 at 15:54):

No, what I really wanted to define was the subgroup of invertible matrices with positive determinant, since this when you take this with real entries, you get a group that acts nicely on the upper half plane, which is related to the modular form stuff I'm thinking about. So, I just wanted the quickest way to define this and it felt wrong doing this and not GLn first.

Yakov Pechersky (Jul 26 2021 at 15:54):

-- The definition of GLₙ(ℝ) is group-equivalent to the mathlib definition
example {n : } : (GLₙ n ) ≃* linear_map.general_linear_group  (fin n  ) :=
units.map_equiv to_lin_alg_equiv'.to_mul_equiv

Yakov Pechersky (Jul 26 2021 at 15:55):

Chris, you can take a look at how I did something similar to you at https://github.com/pechersky/e222/blob/master/src/lecture01.lean

Eric Wieser (Jul 26 2021 at 15:55):

subgroup of invertible matrices with positive determinant

Arguably the mathlib way to do this would be to take the subgroup of invertible linear maps with positive docs#linear_map.det

Chris Birkbeck (Jul 26 2021 at 15:58):

Aha, is it then easy to go from linear maps to matrices? Since I'd want to define the action on the upper half space using the entries of the matrix. I guess I'm asking how easy it is pick a bases.

Yakov Pechersky (Jul 26 2021 at 15:59):

Chris, Eric's statement suggests that whatever you might prove about GLnR, you can prove about linear maps, and it will be "the same". You can provide a basis. The example I gave above gives precisely the group isomorphism between the two that allows you move between the two.

Chris Birkbeck (Jul 26 2021 at 15:59):

(this action is specific to the 2x2 case I should add)

Eric Wieser (Jul 26 2021 at 16:01):

Are you sure you want to use matrices at all here? It sounds like you're using matrix (fin 2) (fin 2) ℝ as an alternate representation of ℂ →ₗ[ℝ] ℂ. Is that correct?

Eric Wieser (Jul 26 2021 at 16:01):

Is there a reason that the former representation is more convenient for you?

Chris Birkbeck (Jul 26 2021 at 16:03):

Well I want to define the moebius transformation on the upper half plane. For this I wanted to work with 2x2 invertible matrices with positive determinant as this is what acts the upper half plane. The usual definition is to take a matrix (a b ; c d) and act on z by sending it to (az+b/cz+d).

Reid Barton (Jul 26 2021 at 16:05):

I think this is about https://en.wikipedia.org/wiki/Linear_fractional_transformation

Chris Birkbeck (Jul 26 2021 at 16:05):

I guess I'm not sure how I would define this using the linear map description (or if it would be worth even trying to as it seems it would look messy)

Chris Birkbeck (Jul 26 2021 at 16:05):

Reid Barton said:

I think this is about https://en.wikipedia.org/wiki/Linear_fractional_transformation

Yes exactly

Chris Birkbeck (Jul 26 2021 at 16:10):

Yakov Pechersky said:

Chris, you can take a look at how I did something similar to you at https://github.com/pechersky/e222/blob/master/src/lecture01.lean

Yes this looks like exactly what I was looking for when I started this. Do you plan on adding this to mathlib? (tbh I only considered trying to add this to mathlib as I thought it would be a good trial of how the PR system goes)

Yakov Pechersky (Jul 26 2021 at 16:11):

This repo is just a parallel formalization of a course, it's not meant to be as general as mathlib is. I've been formalizing it to see if formalizing an undergrad course is "easy" or clunky with current mathlib. I've PRed the parts that make it less clunky.

Yakov Pechersky (Jul 26 2021 at 16:12):

So for your modular forms stuff, try defining a group action using the subgroup of the units of the matrices, like Eric suggested.

Yakov Pechersky (Jul 26 2021 at 16:14):

In fact, you can define it on 2x2 matrices in general, and how that it is a group hom when acting on the subgroup?

Chris Birkbeck (Jul 26 2021 at 16:16):

Well you need the determinant to be positive otherwise it will send the upper half plane to the lower one and that's not something I want to do. But I see your point about using units of the matrices and going from there.

Eric Wieser (Jul 26 2021 at 16:24):

You can extract a, b, c, d, from f : ℂ →ₗ[ℝ] ℂ as something like (f 1).re, (f 1).im, (f I).re, (f I).im (or possibly the transpose of that), right?

Eric Wieser (Jul 26 2021 at 16:24):

Perhaps we're missing a lemma that expands linear_map.det on ℂ →ₗ[ℝ] ℂ componentwise?

Yakov Pechersky (Jul 26 2021 at 16:25):

What in saying is that the function is definable regardless of what a b c d are. The properties of the function you care about are relevant only given your hypothesis.

Yakov Pechersky (Jul 26 2021 at 16:25):

Similar to how division is defined without having to check for a nonzero denominator

Chris Birkbeck (Jul 26 2021 at 16:25):

Ah sorry, I see what you mean.

Johan Commelin (Jul 26 2021 at 16:27):

@Chris Birkbeck Concerning PRs, be sure to check out #howtoPR

Yakov Pechersky (Jul 26 2021 at 16:27):

Eric, you're asking for a lemma that expands the det, given an explicit basis?

Johan Commelin (Jul 26 2021 at 16:28):

I'm not an expert on modular forms, but given all the congruence subgroups that pop up, I think it is hard to avoid matrices.

Chris Birkbeck (Jul 26 2021 at 16:28):

Johan Commelin said:

Chris Birkbeck Concerning PRs, be sure to check out #howtoPR

AH thank you thats really helpful.

Johan Commelin (Jul 26 2021 at 16:29):

So I'm inclined to just define GL_plus n R for any [ordered_semiring R].

Eric Wieser (Jul 26 2021 at 16:29):

Eric Wieser said:

It sounds like you're using matrix (fin 2) (fin 2) ℝ as an alternate representation of ℂ →ₗ[ℝ] ℂ. Is that correct?

With the extra context I think my suggestion was not correct - you're parametrizing an arbitrary function with a 2x2 matrix, not the function I'm thinking of.

Johan Commelin (Jul 26 2021 at 16:30):

For the record: https://en.wikipedia.org/wiki/Congruence_subgroup
:this: is probably where Chris would like to move towards

Chris Birkbeck (Jul 26 2021 at 16:30):

Johan Commelin said:

I'm not an expert on modular forms, but given all the congruence subgroups that pop up, I think it is hard to avoid matrices.

Yes, this is why I was thinking about this as matrices and not linear maps. But I dont know if that leads to a good API, but at least its consistent with modular form literature

Chris Birkbeck (Jul 26 2021 at 16:30):

Johan Commelin said:

For the record: https://en.wikipedia.org/wiki/Congruence_subgroup
:this: is probably where Chris would like to move towards

Yes exactly

Yakov Pechersky (Jul 26 2021 at 16:33):

Then it's a hop skip and a jump to STW correct? ;-)

Chris Birkbeck (Jul 26 2021 at 16:34):

STW?

Yakov Pechersky (Jul 26 2021 at 16:35):

Chris, you can look at the other lecture notes and problem sets (in that repo) , to see how I deal with subgroups of GLn in mathlib style using the definition I shared.

Chris Birkbeck (Jul 26 2021 at 16:35):

Yes I'll do that. Those notes look great, so thank you for sharing them!

Yakov Pechersky (Jul 26 2021 at 16:36):

Shimura Taniyama Weil

Yakov Pechersky (Jul 26 2021 at 16:36):

Explicit computation with matrices is still slower/clunkier than I would like. But it is possible!

Chris Birkbeck (Jul 26 2021 at 16:37):

AH haha I see yes :)
Yakov Pechersky said:

Shimura Taniyama Weil

Yakov Pechersky (Jul 26 2021 at 16:37):

(there are also pdfs of what the lecture was actually saying)

Yakov Pechersky (Jul 26 2021 at 16:37):

Feel free to DM me with questions

Chris Birkbeck (Jul 26 2021 at 16:37):

I will do, thank you!

Johan Commelin (Jul 26 2021 at 16:43):

Yakov Pechersky said:

Then it's a hop skip and a jump to STW correct? ;-)

The world record is something like 18 meters, right? I think you could fit all the necessary literature on an 18m bookshelf (-;

Ruben Van de Velde (Jul 26 2021 at 16:45):

Kevin probably has that shelf in his office

Johan Commelin (Jul 27 2021 at 14:45):

@Chris Birkbeck See also #8377

Chris Birkbeck (Jul 28 2021 at 07:58):

Johan Commelin said:

Chris Birkbeck See also #8377

Yes I've talked to Heather about this. Generalizing this action from SL(2,RR) to GL_2(RR)+ was part of my motivation.

Chris Birkbeck (Jul 28 2021 at 14:09):

@Yakov Pechersky So I've been trying to update my definition of GLn to the one which you suggested. What is still not clear to me is which definition leads to a better API. It seems if I define them as units(matrices n n R) then to write one down I need to give 4 pieces of information the matrix, its inverse, and two proofs. But if one defines them to be matrices with invertible determinant one only needs to provide two pieces of information, the matrix and proof the determinant is a unit. Is it clear that giving 4 pieces of information leads to a better API?

Johan Commelin (Jul 28 2021 at 14:10):

@Chris Birkbeck You can write a custom constructor, that only takes the two pieces of info.

Johan Commelin (Jul 28 2021 at 14:11):

Recording the inverse explicitly will probably be helpful.

Johan Commelin (Jul 28 2021 at 14:11):

It allows Lean to know that 1^-1 = 1 (defeq), instead of merely knowing the existence.

Chris Birkbeck (Jul 28 2021 at 14:11):

Aha, ok I'm not sure what a constructor is, but I'll have a look.

Johan Commelin (Jul 28 2021 at 14:11):

constructor = function building some object

Yakov Pechersky (Jul 28 2021 at 14:12):

But it will like just be A^-1. It's just the proof of that is_unit A.det that allows you to prove that that is actually the left and right inverse.

Chris Birkbeck (Jul 28 2021 at 14:13):

Oh I see so I should make a constructor that takes in the matrix and the proof that the det is a unit and gives an element of units(matrices n n R)

Johan Commelin (Jul 28 2021 at 14:13):

Right, and you call it GL.mk' or so. See for example docs#add_monoid_hom.mk' (which constructs a monoid hom between groups, and therefore doesn't need the map_zero data, because it is automatic)

Chris Birkbeck (Jul 28 2021 at 14:14):

OK great. Ill try that. Thank you!

Chris Birkbeck (Jul 29 2021 at 15:36):

Ok I've made the PR now. Thanks for all your help. I expect more things will need modifying, but I'll wait and see.

Eric Wieser (Jul 29 2021 at 16:03):

(#8466)


Last updated: Dec 20 2023 at 11:08 UTC