Graded ring of modular forms

Stream: maths

[Chris Birkbeck]

I seem to have run into a cliché when trying to define the graded ring of modular forms. In order to do this I need to check one_mul, i.e., that multiplying by the one in the ring (in this case given by the identity function (which is a weight zero modular form)) does nothing. The problem is that , how I've defined it, multiplying by 1 takes me from modular forms of weight k and level Γ to modular forms of weight k+0 and level Γ and these two spaces aren't definitionally equal (?).

I seem to remember something similar happening when people tried to define chain complexes (?) but I don't remember what the fix ended up being. So does anyone have a suggestion of how I should fix this?

[Kevin Buzzard]

Are you grading externally or internally? Is an abstraction of what you have the following: for each natural $k$ you have an abelian group $M_k$, and for each pair $i,j$ of naturals you have a map $M_i\times M_j\to M_{i+j}$ satisfying various axioms (because it's pointwise multiplication of functions) and you now want to put a ring structure on the external direct sum of the $M_k$?

[Chris Birkbeck]

Externally, so your abstraction is correct (if I understand internal vs external correctly!).

[Eric Wieser]

Are you aware of docs#direct_sum.gring?

[Eric Wieser]

Or possibly docs#set_like.graded_monoid?

[Andrew Yang]

I think docs#direct_sum.gring still causes quite some undesired dependent type issues. In particular there isn't a good ext lemma that does not involve heq's.
I think the solution here is to either introduce ext lemmas stating that pairs $(k_i, f_i)$ with $f_i$ of weight $k_i$ are equal iff $k_1 = k_2$ and the underlying functions of $f_i$ are equal.
Or, it might be possible to realize modular forms of weight $k$ and level $\Gamma$ as submodules of $H$, the ring of holomorphic functions, and consider the graded ring of modular forms as a graded subalgebra of $H[X]$.

[Kevin Buzzard]

The problem with that approach (the "internal" grading approach I mentioned earlier) is that you now have to go off on a tangent to prove that some random nonzero linear combination of modular forms of different weights can't ever be zero (to prove that the sum is direct) (which is true).

[Kevin Buzzard]

Oh -- maybe the X in Andrew's message some kind of dummy grading variable which avoids this problem?

[Andrew Yang]

Yes. This was the approach I took when I needed the graded module $\bigoplus_n I^n M$, by viewing it as a submodule of $M[X]$. It is the reason I made the PR about polynomial modules in the first place.

[Junyan Xu]

If the goal is to fill in docs#direct_sum.gring.one_mul, I think you can just use docs#sigma.subtype_ext.

[Eric Wieser]

If your types are subtypes then you should use docs#set_like.graded_monoid

[Eric Wieser]

Which generates the instance proved in the way @Junyan Xu describes as src#set_like.gring.

[Junyan Xu]

Yeah I think they are subtypes defined by the predicate here.

[Junyan Xu]

By the way in the original post it's 0+k that's not defeq to k right?

[Eric Wieser]

One way to handle equality of direct sums of subtypes is with docs#direct_sum.of_eq_of_graded_monoid_eq, then docs#sigma.subtype_ext

[Eric Wieser]

Unfortunately Lean doesn't let us write custom congr lemmas to make that type of thing easier to work with

[Andrew Yang]

Ah yes. I now remember that I did not use it as there wasn't a smul version of it. Should there be one?

[Eric Wieser]

There's an open PR about graded modules $R_i \times M_j \to M_{I+j}$ , I've been on vacation and short on time to finish reviewing it

[Chris Birkbeck]

Eric Wieser said:

Are you aware of docs#direct_sum.gring?

Yes I've been trying to prove an instance of direct_sum.gcomm_ring

[Chris Birkbeck]

Junyan Xu said:

If the goal is to fill in docs#direct_sum.gring.one_mul, I think you can just use docs#sigma.subtype_ext.

hmm ok let me try and see if I can get this to work

[Chris Birkbeck]

Ok that worked! thanks! It seems I was being a bit to dramatic about what the problem was :P

[Eric Wieser]

@Chris Birkbeck, to reiterate an above message, you should instead probably be providing an instance of docs#set_like.graded_monoid which will be easier and provide you the gring instance automatically

[Chris Birkbeck]

Ah I was a bit careless and didn't notice the set_like at the start of your link. I just continued and proved gcomm_ring directly. Other than it being easier to define, are they any other advantages to using this?

[Eric Wieser]

It's a stronger typeclass too, and therefore gives you access to lemmas that would otherwise not be available