feat(number_theory/modular_forms): Modular form definition

[CBirkbeck]

This contains the basic definitions of modular forms and cusp forms together with some lemmas about mdifferentiability that are needed.

---

• [x] depends on: #15009

[CBirkbeck]

• [ ] depends on: #12415

[CBirkbeck]

• [ ] depends on: #15007

[CBirkbeck]

• [ ] depends on: #15009

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15009~~ By Dependent Issues (🤖). Happy coding!

[Vierkantor]

bors d=@alexjbest

[bors[bot]]

:v: alexjbest can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

[riccardobrasca]

This looks good to me. @kbuzzard @AlexKontorovich can you have a look?

[kbuzzard]

Sorry, I only just saw this: I will take a look.

[hrmacbeth]

Can you set this up to be a graded ring? It seems like this is the mathematics of what you are doing, so you might as well do it explicitly. @eric-wieser @jjaassoonn can probably help with the formalism if you haven't used it before.

[CBirkbeck]

Can you set this up to be a graded ring? It seems like this is the mathematics of what you are doing, so you might as well do it explicitly. @eric-wieser @jjaassoonn can probably help with the formalism if you haven't used it before.

Oh I have it as a graded ring already, but the PR was already quite long, so I haven't included it here. I plan to PR that and some other things later

[kbuzzard]

This PR has failed to build because of an unrelated timeout. Junyan has fixed the problem with #16873 so after that has been merged to master someone should merge master to this branch and try again. Sorry I've not looked at this PR yet! But right now it doesn't compile for me :-(

[hrmacbeth]

Can you set this up to be a graded ring? It seems like this is the mathematics of what you are doing, so you might as well do it explicitly. @eric-wieser @jjaassoonn can probably help with the formalism if you haven't used it before.

Oh I have it as a graded ring already, but the PR was already quite long, so I haven't included it here. I plan to PR that and some other things later

OK great! Just wanted to check that your setup would be compatible with the graded ring formalism. What branch is that on?

[CBirkbeck]

Can you set this up to be a graded ring? It seems like this is the mathematics of what you are doing, so you might as well do it explicitly. @eric-wieser @jjaassoonn can probably help with the formalism if you haven't used it before.

Oh I have it as a graded ring already, but the PR was already quite long, so I haven't included it here. I plan to PR that and some other things later

OK great! Just wanted to check that your setup would be compatible with the graded ring formalism. What branch is that on?

So its not on a branch yet, but its here: https://github.com/CBirkbeck/ModularForms/blob/master/src/for_mathlib/mod_forms2.lean (line 306)

I essentially proved and instance of direct_sum.gcomm_ring for (λ k, M k Γ)

[CBirkbeck]

This PR has failed to build because of an unrelated timeout. Junyan has fixed the problem with #16873 so after that has been merged to master someone should merge master to this branch and try again. Sorry I've not looked at this PR yet! But right now it doesn't compile for me :-(

yeah I saw that. I've bumped to see if it works now!

[CBirkbeck]

• depends on: #17432

[CBirkbeck]

• depends on: #17675

[CBirkbeck]

• depends on: #17676

[CBirkbeck]

• depends on: #17677

[tb65536]

@CBirkbeck You should update the description of the PR to include the new dependencies.

[mathlib-dependent-issues-bot]

This PR/issue depends on:

• ~~leanprover-community/mathlib#15009~~
• ~~leanprover-community/mathlib#17677~~
• ~~leanprover-community/mathlib#17676~~ By Dependent Issues (🤖). Happy coding!

[tb65536]

@CBirkbeck Could you merge master?

[alreadydone]

I just looked at the definition of slash_action and found that slash_action β G α γ is exactly same as β → representation γ Gᵐᵒᵖ α. slash_action has weaker assumptions, but working with α being a γ-module should be general enough. (I wonder why the unused_argument linter doesn't complain about the [has_one α] though.) We also have representation.invariants for slash_invariant_forms.

slash_action was added in #15007 and representation earlier in #13573, but maybe @CBirkbeck isn't aware of the work.

cc @antoinelab01

[riccardobrasca]

I just looked at the definition of slash_action and found that slash_action β G α γ is exactly same as β → representation γ Gᵐᵒᵖ α. slash_action has weaker assumptions, but working with α being a γ-module should be general enough. (I wonder why the unused_argument linter doesn't complain about the [has_one α] though.) We also have representation.invariants for slash_invariant_forms.

slash_action was added in #15007 and representation earlier in #13573, but maybe @CBirkbeck isn't aware of the work.

cc @antoinelab01

Is #17765 related to this?

[CBirkbeck]

I just looked at the definition of slash_action and found that slash_action β G α γ is exactly same as β → representation γ Gᵐᵒᵖ α. slash_action has weaker assumptions, but working with α being a γ-module should be general enough. (I wonder why the unused_argument linter doesn't complain about the [has_one α] though.) We also have representation.invariants for slash_invariant_forms.

slash_action was added in #15007 and representation earlier in #13573, but maybe @CBirkbeck isn't aware of the work.

cc @antoinelab01

No I wasn't aware of this and no one stopped me making this class :P . I'm not sure whats best here.

Edit: But you make a good point about the has_one I honestly don't remember why its there. I felt that everything I added was because I at one point needed it, but maybe this was a leftover from a previous version.

[hrmacbeth]

Edit: But you make a good point about the has_one I honestly don't remember why its there. I felt that everything I added was because I at one point needed it, but maybe this was a leftover from a previous version.

You probably need it for the graded algebra instance, right?

[CBirkbeck]

Edit: But you make a good point about the has_one I honestly don't remember why its there. I felt that everything I added was because I at one point needed it, but maybe this was a leftover from a previous version.

You probably need it for the graded algebra instance, right?

Hmm maybe, but its hard to check as the code is out of date now. That said, it now seems harder to prove a gcomm_ring instance for (λ k, modular_form Γ k). It wants me to show that 1.mul f == f which I don't know how to do. Has making things their own type made it so that now we need to deal with these things? Because with the previous iteration of the definition, I managed to get away with never worrying about k + 0 = k issues.

[riccardobrasca]

I am little bit lost because of the huge amount of comments, but unless there is something we're sure is wrong, I propose to merge this: it now only create a new file, so it cannot really do anything bad. If something is badly designed and can be improved, we can do it in another PR, and in any case the best way to test the actual design is to use it.

[hrmacbeth]

@riccardobrasca This does seem like a real issue to me. But the graded ring setup is rather complicated and I'm not sure that in my quick test just now I was using it correctly. Maybe @eric-wieser, who has written some of the few existing graded ring instances, can comment. If the fun_like setting is incompatible with the graded ring instance, then I think we should choose the graded ring instance (ping @mcdoll who advocated for fun_like).

[eric-wieser]

I will try to make time to look at this tomorrow. Please ping me if I forget!

[mcdoll]

Sorry, I haven't followed the discussion. Almost all of my Lean attention is at mathlib4 at the moment. When I originally suggested fun_like, I was completely ignorant of the graded ring instance, but it seems to me that fun_like should be the way to go (or else we have to rethink how to implement functions in mathlib again, but please not in this PR). I feel very bad for causing so much work for Chris and would really like to see modular forms in mathlib.

[CBirkbeck]

Yeah this graded ring thing it annoying. Before I could use sigma.subtype_ext but now I only have sigma.ext which involves these ==. I guess one could maybe define the space of modular forms (of any weight and level) and then have these spaces as subtypes of that(?) But this feels almost like going back to the non-fun_like definition. I should say I'm trying to prove an instance of direct_sum.gcomm_ring which is what I had managed to prove before. At somepoint someone suggested using set_like.graded_monoid and going from there. But I can't seem to get the correct set_like instance.