Notation in `UpperHalfPlane/MoebiusAction`

Stream: mathlib4

[Yury G. Kudryashov]

What's the reason to use

scoped notation:1024 "↑ₘ" A:1024 =>
  (((A : GL(2, ℝ)⁺) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) _)

instead of either

• introducing a new def GLPos.toFun and registering it as CoeFun;
• or introducing a FunLike instance?

P.S.: I would prefer the former, leaving FunLike to bundled operators with additional properties, but this should be probably discussed in a dedicated thread, as it affects docs#Finsupp and docs#DFinsupp as well.

[Yury G. Kudryashov]

BTW, the scoped notation ↑ₘ is never used.

[Yury G. Kudryashov]

Also, does it make sense to have an action of GL, not GLPos?

[Yury G. Kudryashov]

Answering myself: yes, if we want to have orientation-reversing isometries too.

[Yury G. Kudryashov]

What's the plan for $PSL$ action? Also, @David Loeffler , could you please expand the docstrings in file#LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo ? E.g.,

• write a module docstring;
• explain the motivation behind the names IsParabolic etc, both in the module docstring and in the individual docstrings.

[David Loeffler]

What's the reason to use

scoped notation:1024 "↑ₘ" A:1024 =>
  (((A : GL(2, ℝ)⁺) : GL (Fin 2) ℝ) : Matrix (Fin 2) (Fin 2) _)

The UpperHalfPlane stuff was originally written (long ago in mathlib3 days, and not by me, mostly by @Chris Birkbeck I think) with an action of GL(2, ℝ)⁺. This was kind of annoying because of constantly having to manage coercions between GL(2, ℝ)⁺ and GL(2, ℝ) (and a host of other related types as well). I think this ↑ₘ notation was introduced to ease that process slightly.

Subsequently I rewrote a bunch of this code to make the whole of GL(2, ℝ) act (by letting ![-1, 0; 0, 1] act as reflection in the real imaginary axis). Probably I overlooked that this notation should have been weeded out at the same time.

Also, does it make sense to have an action of GL, not GLPos? [...] Answering myself: yes, if we want to have orientation-reversing isometries too.

I hope it does, since I invested a nontrivial amount of work in doing so.

[Yury G. Kudryashov]

I'm going to add a PGL action too.

[David Loeffler]

Yury G. Kudryashov said:

Also, @David Loeffler , could you please expand the docstrings in file#LinearAlgebra/Matrix/GeneralLinearGroup/FinTwo ? E.g.,

• write a module docstring;
• explain the motivation behind the names IsParabolic etc, both in the module docstring and in the individual docstrings.

With all due respect, Yury: what is the role of the mathlib maintainers? Is it to manage the growth of mathlib, or to direct it? I have many projects and a lot of demands on my time, and I'm not accustomed to being told what to do.

[Yury G. Kudryashov]

I just saw a file with no docs, and asked the author of the file. It's OK to say that you have no time for this.

[David Loeffler]

Quite frankly don't know what the etymology of the term "parabolic element" is, for certain classes of 2x2 matrices; and I've managed to get by working in, and teaching, modular form theory for ~20 years without particularly needing to know the motivation behind this name. That's just the name that's conventionally used; that's enough.

[Yury G. Kudryashov]

Currently, the definitions are in the Matrix namespace, and the definition don't say that they have something to do with the action on the upper half-plane.

[David Loeffler]

The definition isn't specific to the upper half-plane, that's just one place that the distinction is relevant.

[Yury G. Kudryashov]

My main concern is that someone may expect Matrix.IsElliptic to be about matrices representing elliptic operators or something like that.

[David Loeffler]

More widely: Yury, in this thread and #maths > Shifts (translations?) of the hyperbolic plane you have twice tried to start a debate about how best to implement X in mathlib when X is actually already there (and clearly documented as such in the mathlib manuals).

We have an entire channel devoted to novices asking how to find stuff; but when a mathlib maintainer doesn't bother to check if something already exists before asking how to build it, that seems (to put it mildly) a little disrespectful to those who have invested vast amounts of work in doing so.

[Yury G. Kudryashov]

In this thread I'm asking what led to design choices that aren't documented in the code. Refactoring existing code is a part of maintainance.
In the other thread I took a shortcut by defining one specific type of Möbius transformations of the unit disc instead of transfering the structure from the upper half-plane. Indeed, this was a bad decision motivated by a rush towards formalizing RMT, so I'm working on a proper implementation now.

[David Loeffler]

The existence of an action of GL (as opposed to GLPos) is documented in the code – indeed, in the module docstring of a file you have already quoted from in this thread.

[Yury G. Kudryashov]

I'm sorry I've badly formulated my question. The actual question was whether the action of $GL$ is mathematically meaningful, or just a "junk" extension of the action of GLPos. This is not documented at the moment, and I've answered myself a few minutes later.

[Yury G. Kudryashov]

Indeed, I could've thought a bit more to avoid the question in the first place, sorry about that.

[Yury G. Kudryashov]

Back to "what can we do about it", will you have time to review PRs adding docs to MoebiusAction and GeneralLinearGroup/FinTwo, if I prepare them?

[David Loeffler]

I guess there is a cultural chasm here, becuase the UpperHalfPlane code was all written by number theorists (not analysts) who naturally have their own ideas what is important, what names are natural, etc. (E.g. elliptic operators are something the vast majority of number theorists don't ever think about, while you can't talk about modular forms for long without dealing with elliptic points.)

[Yury G. Kudryashov]

The metric was written by me, I'm not a number theorist ;-)

[David Loeffler]

Yury G. Kudryashov said:

Back to "what can we do about it", will you have time to review PRs adding docs to MoebiusAction and GeneralLinearGroup/FinTwo, if I prepare them?

Sure, can do.

[Yury G. Kudryashov]

I'll try to prepare them tomorrow then.

[David Loeffler]

I have some code written but not PR'ed which shows that the action of SL2Z is measure-preserving. I'll swap you one PR review for another if you like :-)

[Yury G. Kudryashov]

ack

[Yury G. Kudryashov]

Do you mean the action of GL2R?

[David Loeffler]

Need to look at code (might be some abs(det) factor preventing GL from acting measure-preservingly)

[Yury G. Kudryashov]

Since it's actually the action of PGL2R, the determinant shouldn't play any role.

[David Loeffler]

You're right, it's all of GL, code is here https://github.com/loefflerd/ModularFormDimensions/blob/856a596b38b4aab9a246d3f096e5486e21993b39/ModularFormDimensions/Measure.lean#L44C1-L44C57

[David Loeffler]

instance : SMulInvariantMeasure (GL (Fin 2) ℝ) ℍ volume := by

(here volume is Lebesgue measure weigthed by 1 / im z ^ 2)

[Yury G. Kudryashov]

BTW, do you know why the notation for GL takes a type while notations for GL^+, SL etc take a natural number?

[Yury G. Kudryashov]

I'm trying to decide which convention to follow for PGL.

[David Loeffler]

Not sure. Both are shorthands for more general notations that take a fintype; probably they were just independently implemented by different people. I had spotted that inconsistency but shied away from fixing it, because it is not easy to search-and-replace.

IMHO the abbreviations should both take a nat, for maximal simplicity when writing GL2R, and anyone who wants GL indexed by a more general fintype can live with writing Matrix.GeneralLinearGroup foo.

[David Loeffler]

(PS: I also think the special-case notations (& coercion instances etc) for GL^+ should be retired, that type is now very little used in the library.)

[Yaël Dillies]

My personal opinion is that we can have notation that disambiguates between both, since a natural number is never a type

[Chris Birkbeck]

Sorry I am a bit late to this, but it's as David says. The GL^+ stuff was added by me back in the lean 3 days since originally we only had an action by SL2Z. I thought for modular forms this is all we would ever need, but the coercions were a pain (hence we had this ↑ₘ notation). So more recently David extended this to GL. As for the notations taking in a type or a number, I honestly don't remember (it was likely me who added both of these), it was probably just me being inconsistent and reviewers not catching me.

Lastly, I also don't really know the origin of calling these points elliptic or parabolic, but there is some discussion about this on the Wikipedia page here

[David Loeffler]

Thanks Chris for explaining the origin of this! I think your link got a bit scrambled, I suspect you may have meant this one: https://en.wikipedia.org/wiki/SL2(R)#Classification_of_elements

[Chris Birkbeck]

Ah yes thanks, I was doing this on my phone and got the link wrong!

[Chris Birkbeck]

Oh thats a slightly different link, I meant to send this

[David Loeffler]

Here is a PR which adds the MeasurePreserving stuff, improves the docstring of FinTwo.lean, and removes the no-longer-needed coercion notation: #34402

[Yury G. Kudryashov]

Thanks! I'll review it after the breakfast.

[Yury G. Kudryashov]

I want to make minor adjustments (move some usage of defeq to Subtype to lemmas), otherwise LGTM. BTW, do you think it makes sense to add a lemma about mfderiv of the action?

[David Loeffler]

Thanks! I wasn't sure how best to handle the subtype defeq so very grateful for a second opinion on that.

Regarding mfderiv: I wrote a TODO in the code about this. I guess ultimately we want to have all the options in parallel – the abstract manifold deriv valued in the tangent space, the concrete deriv obtained by extending the function to C, and the link between the two via the canonical trivialization of the tangent space. But my experience is that if you ever want to actually do anything with these definitions, you end up falling back to functions on C anyway, so I wanted to get that in first.

[Yury G. Kudryashov]

I made a pass locally, but I got carried away and fixed some Subtype defeq abuses that are out of scope for this PR. I'll clean up the code and split these fixes into a separate PR tomorrow or on Friday.

[Yury G. Kudryashov]

(then I'll push the rest to your branch)

[David Loeffler]

Thanks for doing this, there is definitely a lot of sub-optimal code (of mine mostly!) in this part of the library so having an expert look it over is really highly appreciated.

[Yury G. Kudryashov]

I've opened #34597 and pushed to your branch. Feel free to revert changes that you don't like.