## Stream: kbb

### Topic: hecke operator

#### Johan Commelin (Sep 14 2018 at 16:32):

The next step would be to define https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula on the subspace of Petersson_weight k functions on the upper half plane.

#### Johan Commelin (Sep 14 2018 at 16:33):

Afterwards, we need to show that it preserves holomorphic, bounded_at_infinity and zero_at_infinity.

#### Johan Commelin (Sep 14 2018 at 16:33):

We also need to prove that it is linear.

#### Johan Commelin (Sep 14 2018 at 18:55):

Ok, this stuff is a mess. I just wanted to plug a matrix with determinant m into the Möbius transform action. Of course that doesn't work...

#### Kenny Lau (Sep 14 2018 at 19:04):

wow this is really a heck of an operator

#### Johan Commelin (Sep 14 2018 at 19:13):

Ok, I think we should forget about Hecke operators. We can define them if we want. But we won't even get close to formalising the abstract of Kevin's paper.

#### Johan Commelin (Sep 14 2018 at 19:13):

Until 5 minutes ago, I thought that the only thing missing was the fact that $S_k$ is finite-dimensional (which requires Riemann–Roch).

#### Johan Commelin (Sep 14 2018 at 19:15):

But of course, with the definition of the Hecke operator that we are now going after, we will get a linear operator on a complex vector space. This beast will have a characteristic polynomial defined over complex.

#### Johan Commelin (Sep 14 2018 at 19:15):

Such polynomials do not have very interesting splitting fields.

#### Patrick Massot (Sep 15 2018 at 13:30):

How do you prove this polynomial has interesting coefficients in the real world?

#### Reid Barton (Sep 15 2018 at 13:32):

are the coefficients actually rational?

#### Patrick Massot (Sep 15 2018 at 13:32):

I guess there are integers

#### Patrick Massot (Sep 15 2018 at 13:32):

But I know no number theory

#### Patrick Massot (Sep 15 2018 at 13:34):

And it probably also requires Fourier series for modular forms

#### Reid Barton (Sep 15 2018 at 13:35):

If they are actually integers, then can't we define the splitting field to be the smallest subfield of C which contains the roots?

#### Johan Commelin (Sep 15 2018 at 13:36):

The Hecke operator acts on the singular homology of the modular curve. This has Q coeffients

#### Reid Barton (Sep 15 2018 at 13:36):

Then we don't need either splitting fields or to prove that the coefficients are integers

#### Johan Commelin (Sep 15 2018 at 13:36):

By Hodge theory you recover the cusp forms in the complexification of this cohomology group.

#### Johan Commelin (Sep 15 2018 at 13:36):

But maybe I'm using a sledgehammer, there might be a more low-brow proof.

#### Reid Barton (Sep 15 2018 at 13:37):

Of course then we wouldn't know that the this field is a finite extension...

Right...

#### Johan Commelin (Sep 15 2018 at 13:38):

Somehow I don't mind sorrying finite-dimensionality of S_k, but sorrying this fact feels like a big cheat.

#### Patrick Massot (Sep 15 2018 at 13:39):

I guess Hecke's point of view was less sophisticated

#### Johan Commelin (Sep 15 2018 at 13:41):

Probably. I think using Fourier coefficients there is another approach.

#### Johan Commelin (Sep 15 2018 at 13:42):

But then, we didn't want to do Fourier coefficients either.

#### Johan Commelin (Sep 15 2018 at 13:42):

So maybe we just define the Hecke operator over complex, and then wrap up the project.

#### Johan Commelin (Sep 18 2018 at 12:35):

Let's put this discussion in the correct thread.

#### Johan Commelin (Sep 18 2018 at 12:35):

The following lemma is crucial:

theorem M_trans_SL2Z_H {m : ℤ} {h : m > 0} {M : SL2Z} {A : Mat m} :
M_trans h (SL2Z_M m M A) = SL2Z_H M ∘ (M_trans h A) :=
begin
funext z,
simp [M_trans, SL2Z_M, SL2Z_H, «Möbius_transform»],

-- m : ℤ,
-- h : m > 0,
-- M : SL2Z,
-- A : Mat m,
-- z : ↥ℍ
-- ⊢ (↑(M.a) * ↑(A.b) + (↑(M.b) * ↑(A.d) + (↑(M.a) * ↑(A.a) + ↑(M.b) * ↑(A.c)) * ↑z)) /
--       (↑(M.c) * ↑(A.b) + (↑(M.d) * ↑(A.d) + (↑(M.c) * ↑(A.a) + ↑(M.d) * ↑(A.c)) * ↑z)) =
--     (↑(M.b) + ↑(M.a) * ((↑(A.b) + ↑(A.a) * ↑z) / (↑(A.d) + ↑(A.c) * ↑z))) /
--       (↑(M.d) + ↑(M.c) * ((↑(A.b) + ↑(A.a) * ↑z) / (↑(A.d) + ↑(A.c) * ↑z)))

-- ring, -- fails
end


#### Johan Commelin (Sep 18 2018 at 12:36):

I'm not surprised that ring fails, because there are divisions. But boy, I really don't want to prove this stuff by hand.

#### Patrick Massot (Sep 18 2018 at 12:36):

I could try since Johannes is working for me right now

#### Patrick Massot (Sep 18 2018 at 12:36):

Did you push everything?

#### Johannes Hölzl (Sep 18 2018 at 12:37):

Hm, isabelle has field_simps for these kind of things. field_simps is a collection which applies distributivity, and tries to remove the x / d. Sometimes it needs to introduces if to check if d = 0

#### Johan Commelin (Sep 18 2018 at 12:45):

I pushed some stuff

#### Johan Commelin (Sep 18 2018 at 12:45):

I've got M out of f, so now we need to do the cocycle computation

#### Johan Commelin (Sep 18 2018 at 12:46):

Which is just as ugly as the other thing I just posted.

#### Patrick Massot (Sep 18 2018 at 12:46):

Did you do the other ugly thing?

#### Johan Commelin (Sep 18 2018 at 12:55):

No, everything I did was pushed.

#### Johan Commelin (Sep 18 2018 at 12:55):

I went to the last sorry: proving that the result again has weight k

#### Johan Commelin (Sep 18 2018 at 12:55):

I now have the following goal

⊢ quotient.lift_on' o
(λ (A : Mat m), 1 / (↑(A.c) * ↑(SL2Z_H M z) + ↑(A.d)) ^ (k + 1) * f.val (M_trans h A (SL2Z_H M z)))
_ =
(↑(M.c) * ↑z + ↑(M.d)) ^ (k + 1) *
quotient.lift_on' o (λ (A : Mat m), 1 / (↑(A.c) * ↑z + ↑(A.d)) ^ (k + 1) * f.val (M_trans h A z)) _


#### Johan Commelin (Sep 18 2018 at 12:55):

How do I get past that quotient.lift_on'?

#### Patrick Massot (Sep 18 2018 at 12:55):

I'm working on M_trans_SL2Z_H

#### Johannes Hölzl (Sep 18 2018 at 13:04):

eliminate o. Easiest: rcases o with <x>.

#### Johan Commelin (Sep 18 2018 at 13:09):

Thanks, that worked!

#### Johan Commelin (Sep 18 2018 at 13:09):

@Patrick Massot The name is wrong. The final _H should be _M.

#### Johan Commelin (Sep 18 2018 at 13:09):

With _H it is another lemma, and I need that one now (-;

#### Patrick Massot (Sep 18 2018 at 13:10):

but do you still want  {m : ℤ} {h : m > 0} {M : SL2Z} {A : Mat m} : M_trans h (SL2Z_M m M A) = SL2Z_H M ∘ (M_trans h A)?

#### Patrick Massot (Sep 18 2018 at 13:10):

Or only the other one?

#### Johan Commelin (Sep 18 2018 at 13:12):

No, the one you are working on is used

#### Johan Commelin (Sep 18 2018 at 13:12):

I just realised that I had the wrong name.

#### Johan Commelin (Sep 18 2018 at 13:12):

You can already see it being used

#### Johan Commelin (Sep 18 2018 at 13:13):

In what I last pushed

#### Johan Commelin (Sep 18 2018 at 13:36):

Aaahrg, the final sorry is a real pain. I'm now even confused about the maths again.

#### Johan Commelin (Sep 18 2018 at 13:37):

OTOH, those are the better moments of theorem proving (-; I'm rather confused about the maths than that I'm fight silly ↑

#### Patrick Massot (Sep 18 2018 at 13:44):

I just pushed something

#### Patrick Massot (Sep 18 2018 at 13:45):

Things are reduced to many variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/hecke_operator.lean#L16 which itself is a variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/upper_half_space.lean#L37

#### Patrick Massot (Sep 18 2018 at 13:45):

But I'm tired of fighting this

#### Patrick Massot (Sep 18 2018 at 13:46):

One day we will think back and laugh. But right now it's only screaming: Lean is nowhere near ready!

#### Johan Commelin (Sep 18 2018 at 13:47):

Right, it's really annoying

#### Johan Commelin (Sep 18 2018 at 13:51):

I also pushed. I didn't really get very far.

#### Patrick Massot (Sep 18 2018 at 13:52):

Maybe we can switch sides

#### Johan Commelin (Sep 18 2018 at 13:53):

So, on my side that maths is confusing.

#### Johan Commelin (Sep 18 2018 at 13:53):

If you take an f of weight k. After you plug it into Hecke, you want to check that the result has weight k.

#### Johan Commelin (Sep 18 2018 at 13:54):

But this means that you get f(A • M z), where A : Mat m and M : SL2Z

#### Johan Commelin (Sep 18 2018 at 13:54):

Now you can't use the weight property of f.

#### Johan Commelin (Sep 18 2018 at 13:54):

Because the M is not on the left.

#### Johan Commelin (Sep 18 2018 at 13:55):

But A M A¯¹ doesn't have to be in SL2Z...

#### Johan Commelin (Sep 18 2018 at 13:55):

So now I'm confused.

#### Patrick Massot (Sep 18 2018 at 13:56):

M should be on the left

#### Patrick Massot (Sep 18 2018 at 13:56):

We are acting from the left

#### Patrick Massot (Sep 18 2018 at 13:56):

At least on my piece of paper

And on Wikipedia

#### Johan Commelin (Sep 18 2018 at 14:00):

Yes, but M acts before A does, right?

#### Johan Commelin (Sep 18 2018 at 14:01):

It is f (A • (M • z)). So M is in fact acting on the left.

#### Reid Barton (Sep 18 2018 at 14:02):

Yeah you want to write $AM = MA'$ for some other $A'$ of det m, I think. The action of M will permute the terms of the sum

#### Patrick Massot (Sep 18 2018 at 14:02):

It didn't seem necessary earlier today

#### Patrick Massot (Sep 18 2018 at 14:04):

I think using reflexivity of the equivalence relation is enough

#### Patrick Massot (Sep 18 2018 at 14:04):

or reflexivity of equality

#### Johan Commelin (Sep 18 2018 at 14:05):

Hmmm... Reid, that might be the trick

#### Johan Commelin (Sep 18 2018 at 14:05):

I tried writing AM = M'A, but then your M' is not in SL2Z

#### Johan Commelin (Sep 18 2018 at 14:05):

But maybe with your attack it works.

#### Patrick Massot (Sep 18 2018 at 14:06):

You need to prove to compute the term in the sum corresponding to AM until you get the one corresponding to M

#### Johan Commelin (Sep 18 2018 at 14:06):

Because $A' = M^{-1}AM$ and $M^{-1} \in \mathrm{SL2Z}$

#### Johan Commelin (Sep 18 2018 at 14:07):

@Patrick Massot I don't think that will work. You really need to use that f has weight k at some point. So you need to rewrite things.

#### Patrick Massot (Sep 18 2018 at 14:07):

of course you use that!

#### Reid Barton (Sep 18 2018 at 14:10):

The book I have writes the action of SL(2, Z) (or more generally GL+(2, R)) on functions on the upper half plane as a right action, which I think makes more sense

#### Reid Barton (Sep 18 2018 at 14:10):

$(f|_k \gamma)(z) = \frac{\det \gamma}{(cz + d)^k} f(\gamma z)$

#### Johan Commelin (Sep 18 2018 at 14:12):

True, but it acts on the left on the plane, right?

#### Reid Barton (Sep 18 2018 at 14:12):

and also the Hecke operators
$(f|_k T_p) = p^{k/2-1} \sum_\delta f|_k \delta$ "where $\delta$ runs over a set of representatives for the distinct right cosets of $\Gamma_1(N)$ in $\Delta_p$"

Yes

#### Johan Commelin (Sep 18 2018 at 14:13):

In Lean we only have the action on the plane, so far...

#### Johan Commelin (Sep 18 2018 at 14:13):

Well, and the action on other matrices.

#### Reid Barton (Sep 18 2018 at 14:14):

Then to check that the Hecke operator preserves modular forms of weight k you need to show that
$(\sum_\delta f|_k\delta)|_k \gamma = \sum_\delta f|_\delta$ and the strategy is going to be to move $\gamma$ past $\delta$ and reindex

#### Reid Barton (Sep 18 2018 at 14:17):

Yeah, I'm just trying to show how to isolate the step where you reindex the sum

#### Reid Barton (Sep 18 2018 at 14:19):

do we even know yet that the Hecke operator preserves holomorphic functions?

#### Johan Commelin (Sep 18 2018 at 14:20):

That statement does not make sense yet (-;

#### Johan Commelin (Sep 18 2018 at 14:20):

Hmmm, maybe we could turn it into a sensible statement.

#### Johan Commelin (Sep 18 2018 at 14:20):

At the moment the Hecke operators are being defined as operators on functions of weight k

#### Reid Barton (Sep 18 2018 at 14:21):

do we know that (az + b)/(cz + d) is itself a holomorphic function?

#### Johan Commelin (Sep 18 2018 at 14:21):

Afterwards we want to check that the preserve holomorphic functions and functions bound at infinity.

right

#### Johan Commelin (Sep 18 2018 at 14:21):

We do not know that

I see

#### Johan Commelin (Sep 18 2018 at 14:21):

It might be a nice example of a holomorphic function (-;

#### Kenny Lau (Sep 18 2018 at 14:24):

are there any sorry that I can fill in?

YES

#### Johan Commelin (Sep 18 2018 at 14:24):

@Kenny Lau It might be good to read the discussion of the last 20 minutes

#### Johan Commelin (Sep 18 2018 at 14:25):

There is some non-trivialish math going into this. (Nothing you don't understand in 30 secs) But still...

#### Kenny Lau (Sep 18 2018 at 14:26):

where is the sorry?

#### Johan Commelin (Sep 18 2018 at 14:27):

Look in the Hecke file

is it WIP?

#### Kenny Lau (Sep 18 2018 at 14:27):

I don't want to cause pull conflict

#### Patrick Massot (Sep 18 2018 at 14:29):

I stand by my claim we don't need any reordering

#### Johan Commelin (Sep 18 2018 at 14:29):

I'm not working on it right now

#### Johan Commelin (Sep 18 2018 at 14:29):

Need to do some emails

Hold on 10 sec

#### Patrick Massot (Sep 18 2018 at 14:31):

I claim there is no problem here

#### Patrick Massot (Sep 18 2018 at 14:31):

Except we miss a field tactic

#### Patrick Massot (Sep 18 2018 at 14:32):

Kenny: you can fill in all sorries in that file

#### Kenny Lau (Sep 18 2018 at 14:32):

well you just pulled

pushed*

yes

#### Patrick Massot (Sep 18 2018 at 14:32):

Don't forget what I wrote: Things are reduced to many variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/hecke_operator.lean#L16 which itself is a variation on https://github.com/semorrison/kbb/blob/42b4509e2d9ca5beaeb712a17fc0f5754f73854c/src/upper_half_space.lean#L37

#### Patrick Massot (Sep 18 2018 at 14:32):

About the other sorries in that file

#### Patrick Massot (Sep 18 2018 at 14:33):

And if you really feel like impressing us, you can get rid of all quadruples of integers and use matrices everywhere

#### Patrick Massot (Sep 18 2018 at 14:33):

I'm giving up on this.

#### Patrick Massot (Sep 18 2018 at 14:34):

Honestly I think the upshot of this story is that Lean is not yet ready for anything involving divisions

#### Kenny Lau (Sep 18 2018 at 14:35):

I don't feel like impressing anyone

#### Mario Carneiro (Sep 18 2018 at 14:35):

You could always just apply division cancellation theorems, it's not that hard...

#### Mario Carneiro (Sep 18 2018 at 14:35):

I'm not too keen on replacing these direct and logical proofs with arcane tactic-generated proofs

#### Patrick Massot (Sep 18 2018 at 14:36):

The trouble with division cancellations theorems is that terms must be next to each other

#### Johan Commelin (Sep 18 2018 at 14:36):

I am very keen on have a tactic that will write the direct and logical proof for me.

#### Patrick Massot (Sep 18 2018 at 14:36):

hence the endless conv

#### Patrick Massot (Sep 18 2018 at 14:36):

No, this is stupid

#### Patrick Massot (Sep 18 2018 at 14:36):

We don't want to see this proof

#### Patrick Massot (Sep 18 2018 at 14:37):

We want Lean to compute, as with ring

#### Mario Carneiro (Sep 18 2018 at 14:37):

I think it can be done better than that

#### Mario Carneiro (Sep 18 2018 at 14:37):

plus a little calc would go a long way in that proof

#### Mario Carneiro (Sep 18 2018 at 14:37):

what is all the uparrow stuff?

#### Johan Commelin (Sep 18 2018 at 14:38):

ℤ-matrices acting on ℂ

#### Johan Commelin (Sep 18 2018 at 14:39):

There is a boatload of stuff in this repo that could be generalised. But some thing's can't... for example this lemma could be about arbitrary matrices in GL2R+. But that would shift the arrows somewhere else.

#### Johan Commelin (Sep 18 2018 at 14:47):

I'm looking forward to Lean Forward... these things are the basic Lego blocks that Sander Dahmen works with.

#### Mario Carneiro (Sep 18 2018 at 14:48):

Okay, I've downloaded and set up kbb. What area needs my attention?

#### Johan Commelin (Sep 18 2018 at 14:48):

hecke_operator.lean

#### Johan Commelin (Sep 18 2018 at 14:48):

You'll get pulled into the other files by import

#### Johan Commelin (Sep 18 2018 at 14:48):

Beware, there are minor dragons in these files.

#### Johan Commelin (Sep 18 2018 at 14:49):

Every 10 lines will give you another opportunity for a major refactor (-;

#### Patrick Massot (Sep 18 2018 at 14:49):

The area where you write a field tactic

#### Johan Commelin (Sep 18 2018 at 14:49):

@Kenny Lau you might want to tell @Mario Carneiro which sorry you are working on.

all of them

#### Mario Carneiro (Sep 18 2018 at 14:50):

lol that's not happening before friday Patrick

#### Patrick Massot (Sep 18 2018 at 14:50):

I'm sure Kevin will understand

#### Patrick Massot (Sep 18 2018 at 14:51):

Do you think you could do it before he turns 60?

#### Johan Commelin (Sep 18 2018 at 14:51):

@Mario Carneiro Any improvements of the repo would be appreciated.

#### Johan Commelin (Sep 18 2018 at 14:51):

matrices and determinants seem to be almost ready to merge. And independent of the other files.

#### Kenny Lau (Sep 18 2018 at 15:19):

@Patrick Massot what's the math proof of the thing that Patrick claims to be true?

#### Kenny Lau (Sep 18 2018 at 15:20):

and what is the second thing?

#### Patrick Massot (Sep 18 2018 at 15:20):

The maths proof is to expand everythings and compute

#### Patrick Massot (Sep 18 2018 at 15:20):

But probably there is a better way to setup all this

#### Kenny Lau (Sep 18 2018 at 15:22):

I filled in two of the sorries

#### Kenny Lau (Sep 18 2018 at 15:22):

see if you can learn anything therefrom

#### Johan Commelin (Sep 19 2018 at 10:15):

Reid quoted some formulas containing the Petersson slash operator (of weight k). Would it make sense to mimic that notation, somehow? I think we should also wrap M_trans and SL2Z_H into notation (has_scalar). I hope it will make statements more readable. Maybe it will even improve proofs, I don't know.

#### Johan Commelin (Sep 19 2018 at 11:04):

@Kenny Lau I agree with Patrick's claim. I made some small rewrites. Maybe now it is easier to math-see why it is true. I still wish ring would kill this. But it doesn't... because there are divisions. I hate divisions in Lean.

#### Johan Commelin (Sep 19 2018 at 11:05):

(Oooh, I also pushed those small rewrites.)

Last updated: May 18 2021 at 09:14 UTC