PR permission

Stream: new members

[Chris Birkbeck]

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]

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

[Chris Birkbeck]

Thank you!

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Chris Birkbeck]

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]

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

[Yakov Pechersky]

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

[Yakov Pechersky]

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

[Chris Birkbeck]

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]

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

[Eric Wieser]

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]

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]

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]

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

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]

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]

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]

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]

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

[Eric Wieser]

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]

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

[Chris Birkbeck]

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]

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

[Chris Birkbeck]

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]

Reid Barton said:

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

Yes exactly

[Chris Birkbeck]

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]

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]

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]

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]

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]

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]

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

[Yakov Pechersky]

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]

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

[Chris Birkbeck]

Ah sorry, I see what you mean.

[Johan Commelin]

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

[Yakov Pechersky]

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

[Johan Commelin]

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]

Johan Commelin said:

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

AH thank you thats really helpful.

[Johan Commelin]

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

[Eric Wieser]

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]

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

[Chris Birkbeck]

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]

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]

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

[Chris Birkbeck]

STW?

[Yakov Pechersky]

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]

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

[Yakov Pechersky]

Shimura Taniyama Weil

[Yakov Pechersky]

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

[Chris Birkbeck]

AH haha I see yes :)
Yakov Pechersky said:

Shimura Taniyama Weil

[Yakov Pechersky]

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

[Yakov Pechersky]

Feel free to DM me with questions

[Chris Birkbeck]

I will do, thank you!

[Johan Commelin]

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]

Kevin probably has that shelf in his office

[Johan Commelin]

@Chris Birkbeck See also #8377

[Chris Birkbeck]

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]

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

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

[Johan Commelin]

Recording the inverse explicitly will probably be helpful.

[Johan Commelin]

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

[Chris Birkbeck]

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

[Johan Commelin]

constructor = function building some object

[Yakov Pechersky]

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]

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]

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]

OK great. Ill try that. Thank you!

[Chris Birkbeck]

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]

(#8466)