hello

Stream: kbb

[Welcome Bot]

Welcome to #kbb.

[Patrick Massot]

This is a test: can anyone hear me?

[Reid Barton]

Yes

[Patrick Massot]

Does anyone has another Zulip account and could check what is visible?

[Reid Barton]

I thought about this, but I'm not sure whether the stream would be visible to external people. Yeah

[Reid Barton]

Or, just remove me temporarily.

[Patrick Massot]

Funnily, I don't seem to be allowed to do that

[Simon Hudon]

I see you

[Patrick Massot]

I'm creating another account

[Simon Hudon]

Also: this is a great idea

[Simon Hudon]

Did you need the help of an administrator to create this stream?

[Patrick Massot]

No

[Patrick Massot]

I think this stream is safe

[Patrick Massot]

The point is that group PM is not suitable for what we were doing. That generates too many notifications

[Simon Hudon]

Amen

[Patrick Massot]

Reid, do you see things here?

[Patrick Massot]

Reid should be back in

[Reid Barton]

Yep, I am now.

[Patrick Massot]

And should see the full history, which is another advantage compared to group PM

[Reid Barton]

Indeed I can

[Patrick Massot]

(this was an option when creating the stream)

[Patrick Massot]

Ok, let's stop using the group PM and its endless series of emails and notification popups

[Patrick Massot]

Did you need the help of an administrator to create this stream?

No

[Patrick Massot]

What's the story of fast_matrix? Is it fast to compute because it uses vector? Or is it only fast to type because of the notation?

[Johan Commelin]

What's the story of fast_matrix? Is it fast to compute because it uses vector? Or is it only fast to type because of the notation?

Shouldn't this go into a new thread :rolling_on_the_floor_laughing:

[Johan Commelin]

To answer your question: fast_matrix is now obsolete, since @Jack Crawford pushed an implementation that is a lot more fleshed out. His implementation is both supposed to be faster to compute with and easier to type. You can use the equation compiler to grab the a b c d out of a 2x2 matrix, which makes for readable definitions.

[Johan Commelin]

Also: very good idea to create a private stream. I didn't know this was possible. We should have done that 1 week ago.

[Johan Commelin]

The cool side effect is that we can give Kevin access, and he can read through the history of all of our discussions :lol:

[Kenny Lau]

ok so we have 4 days left

[Kenny Lau]

can we come up with a realistic list of goals

[Kenny Lau]

or a list of realistic goals?

[Patrick Massot]

Mario, do you see anything in this repo that could hope to get into mathlib?

[Johan Commelin]

Like I said, I'll be gone on Wednesday, so I can only contribute today and tomorrow.

[Johan Commelin]

I think either: we start cleaning up; or we focus on the Hecke operator (on the complex vector space (=module :lol:) of modular forms.

[Johan Commelin]

This second option will probably force us to clean up other stuff as well.

[Johan Commelin]

Otoh, we could also leave the modular form part of the repo as it is.

[Johan Commelin]

And then we could focus all our time on exp and friends.

[Johan Commelin]

:bell: We have 99 commits in the kbb repository! Well done to everyone who contributed!

[Patrick Massot]

What's the status of the Hecke operator file? I don't even understand the maths here. What is the meaning of the first displayed formula at https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula? Is each term in the sum meant to be well defined? Or only the sum? If I naively try to change (a b c d) by multiplication by a element of SL2Z and use the weight formula for f, I don't seem to get the same term.

[Johan Commelin]

You should get the same term, right? Or did I mess something up. I was quite convinced that every term in the sum was well-defined.

[Johan Commelin]

But maybe we should just delete this file... I think I aimed to high.

[Patrick Massot]

I don't understand the wikipedia page, so you don't need to mess up anything

[Patrick Massot]

What is the pen and paper proof that each term in the sum is well-defined?

[Patrick Massot]

I must be missing something obvious

[Johan Commelin]

$(cz + d)^{-k} f(\frac{az + b}{cz + d}) = (cz + d)^{-k} f(\begin{pmatrix} a & b \\ c & d \end{pmatrix}z)$, is that right?

[Patrick Massot]

yes

[Johan Commelin]

So now we take another representative: $M\begin{pmatrix}a & b \\ c & d \end{pmatrix}$

[Patrick Massot]

The trouble is that $a, b, c, d \mapsto (cz+d)$ is not a group morphism

[Johan Commelin]

Hmm, I'm also getting myself confused.

[Patrick Massot]

If that were a group morphism then everything would be obviously ok

[Patrick Massot]

Too bad we can't ask Kevin

[Reid Barton]

It shouldn't be a group morphism, it should be a 1-cocycle, or something. Right? Because $z$ is changing too

[Patrick Massot]

oh yes, z is changing

[Patrick Massot]

I think it's not changing enough on my paper

[Patrick Massot]

Ok, it works now

[Patrick Massot]

You can continue to do number theory, it's alright

[Patrick Massot]

It was only a stupid copy-paste mistake

[Johan Commelin]

It also works on my paper

[Johan Commelin]

So, we've proven it! Let's move on to the next maths theorem (-;

[Patrick Massot]

It shouldn't be that hard to Lean (modulo those f***ing cast and coes)

[Johan Commelin]

Right, Kenny did a lot of useful stuff (-;

[Johan Commelin]

But all those actions of matrices on each other, and on the upper half plane...

[Johan Commelin]

That's going to be quite a pain.

[Johan Commelin]

@Patrick Massot Are you willing to take a shot at it?

[Patrick Massot]

I may try in the afternoon

[Patrick Massot]

I cleaned up a tiny bit but several things are weird. First I cannot sorry the proof. Lean complains there are remaining meta-variables, but I don't see where. And I have an hypothesis H: A ≈ B that I found no way to destruct into the existence of P in SL2 such that B = PA. This is not such a suprise because the beginning of the proof is really a mess

[Patrick Massot]

I think this is a very bad start. @Johannes Hölzl could you have a look?

[Johan Commelin]

Right... my brain stopped working after I wrote the start of that file. Guess why...

[Johannes Hölzl]

@Patrick Massot where should I look? I have no idea what a Hecke operator is. Did you push your commits, I don't see anything in kbb.

[Johan Commelin]

There is a file called Hecke_operator or something

[Johan Commelin]

The mathy definition is here: https://en.wikipedia.org/wiki/Hecke_operator#Explicit_formula

[Johan Commelin]

To prove that the sum is over a finite set, we need to use the stuff that you cleaned up.

[Johannes Hölzl]

Hm, the statements shouldn't change, besides reduce_def which is now reduce_eq1, reduce_eq2, reduce_eq3`.

[Johan Commelin]

Right, line 12 should be

  haveI := SL2Z_M.finiteness m (ne_of_gt h),

[Patrick Massot]

Crap. I forgot to push

[Patrick Massot]

And I left my computer

[Patrick Massot]

Fixed

[Patrick Massot]

@Johannes Hölzl Now you can have a look, sorry about the false start

[Johan Commelin]

I'm a bit scared about the fact that we only know that SL2Z_H is a group action.

[Johan Commelin]

It seems like we would want to know that MAT2_H is a monoid action.

[Patrick Massot]

Oh yes, we need that

[Johan Commelin]

But refactoring SL2Z into a subtype of MAT2 give me a headache

[Patrick Massot]

I thought this was the reason you put det > 0 everywhere instead of det = 1

[Johan Commelin]

Because that means we have to go through all of Kenny's code again

[Patrick Massot]

And this is why I don't understand how term mode code could be easier to maintain

[Johan Commelin]

They set things up in the correct way the first time.

[Patrick Massot]

No, that's not what refactoring means

[Johan Commelin]

Instead of me: I only get it right after 42 attemts.

[Johan Commelin]

You're right.

[Johan Commelin]

But I agree that it is really confusing that we can not unfold that equivalence between A and B

[Johan Commelin]

After we have that, we could try to just battle on.

[Johan Commelin]

Although it might be nicer to have the monoid action do some work for us

[Johan Commelin]

Oh my goodness. If we want to generalise stuff to monoid actions there I'm so scared that everything breaks. I've learned a lesson: first try to think out some good API's.

[Johan Commelin]

@Johannes Hölzl So we have two problems: (1) how do we unfold the equivalence in hecke_operator.lean.

[Johan Commelin]

By definition A and B are equivalent if there is an M : SL2Z such that A = MB.

[Johan Commelin]

We want to get that M out.

[Johan Commelin]

And (2), to get a readable (and workable) version of the Hecke operator, it would be good to have A • z where A is any 2x2-matrix with integer coefficients, and z : ℍ.

[Johan Commelin]

In the end we will get (M • B) • z, and then we want to know that this is the same thing as M • (B • z)

[Johannes Hölzl]

So, first I fixed the basic definition. We currently had some missing goals (the anonymous constructor was outside tactic mode, so some type class instances where missing)

[Johan Commelin]

Ok, I guess that helps a bit (-;

[Patrick Massot]

I suspected something like this

[Johan Commelin]

@Johannes Hölzl Do you think it would be better if Möbius_transform turned into • notation?

[Johannes Hölzl]

Uh, overloading • could be problematic, at least annoying...

[Johannes Hölzl]

Why do we know that A an B are representatives?

[Johannes Hölzl]

so inreps?

[Johan Commelin]

No, we don't know that

[Patrick Massot]

We don't need that

[Johan Commelin]

They are merely "any representative"

[Patrick Massot]

This reps story is all used up in the finiteness fact

[Patrick Massot]

We won't use it again

[Patrick Massot]

in this proof

[Johan Commelin]

We won't use it again

We promise.

[Johannes Hölzl]

but we could use them to define the Hecke operator? Then we don't need to lift the quotients...

[Johannes Hölzl]

of course, later we need the proof anyway

[Johan Commelin]

Hmm, I suppose so.

[Patrick Massot]

That would be cheating

[Johan Commelin]

And "later" will be after the birthday party.

[Johan Commelin]

@Johannes Hölzl Why would we be overloading •? The monoid action MAT2 → ℍ → ℍ can be an instance of has_scalar right?

[Johan Commelin]

We don't have MAT2, but I think every monoid action should be an instance of has_scalar.

[Johannes Hölzl]

ah, okay. I thought you wanted to add another notation...

[Patrick Massot]

It's interesting to know how far one should be allowed to go into definition cheating. Say I want to prove RH in Lean. I define the usual zeta, call it zeta', and then define zeta(z) to be zeta'(z) if z is not a surprising zero of zeta', and one otherwise. Then I prove RH, and all is left is proving my definition of zeta is equivalent to the usual one...

[Johannes Hölzl]

what do you mean you want t get the M out? Like rintros A B ⟨M, eq⟩, works...

[Johan Commelin]

I guess so

[Patrick Massot]

I think it works because of your previous fix

[Patrick Massot]

It definitely didn't work this morning

[Johan Commelin]

Good!

[Johan Commelin]

Because now we can rw along eq, and then the fight begins!

[Johannes Hölzl]

The current state is

...
A B : Mat m,
M : SL2Z,
eq : SL2Z_M m M A = B,
weight_f :
  ∀ (M : SL2Z) (z : {x // x ∈ ℍ}),
    f ⟨«Möbius_transform» ↑(M.a) ↑(M.b) ↑(M.c) ↑(M.d) ↑z, _⟩ =
      (↑(M.c) * ↑z + ↑(M.d)) ^ (k + 1) * f z
⊢ 1 / (↑(A.c) * ↑z + ↑(A.d)) ^ (k + 1) *
      f ⟨«Möbius_transform» ↑(A.a) ↑(A.b) ↑(A.c) ↑(A.d) ↑z, _⟩ =
    1 / (↑(B.c) * ↑z + ↑(B.d)) ^ (k + 1) *
      f ⟨«Möbius_transform» ↑(B.a) ↑(B.b) ↑(B.c) ↑(B.d) ↑z, _⟩

Is this what you want?

[Patrick Massot]

Yep

[Johannes Hölzl]

ah, okay. Its in kbb now

[Johannes Hölzl]

by the way: it is surely good style to define Möbius_transform on Mat m instead fof integer tuples.

[Patrick Massot]

I hate this integer tuples thing. I don't understand why we don't use matrices everywhere

[Johan Commelin]

Right, so why don't we define it on matrix (fin 2) (fin 2) R where R is a subring of ℝ?

[Johan Commelin]

Also, can we have a coercion from ℕ to fintype, that sends n to fin n?

[Johan Commelin]

Then stuff becomes even more readable (-;

[Johan Commelin]

@Patrick Massot I think we should. But with an old version of matrices it was hard to actually write down examples.

[Johannes Hölzl]

Hm, having a coerion from ℕ to Type would be nice!

[Johannes Hölzl]

Ah, I see there is SL2Z_H. So maybe we want a similar form for Mat m?

[Johan Commelin]

It is in the repo, but I haven't pushed yet.

[Johan Commelin]

Well, MAT2 really. And afterwards we can restrict to subtypes.

[Johan Commelin]

Mat m is a bad algebraic structure

[Johan Commelin]

It isn't a monoid

[Johan Commelin]

So, we have

@[simp] theorem one_val_ne {i j} (h : i ≠ j) : (1 : matrix n n α) i j = 0 :=
by simp [one_val, h]

in the matrices file. I would like Lean to try and figure out on its own if h is satisfied. In fin 2 it should know that 0 ≠ 1.

[Johan Commelin]

Is this something that an auto_param like dec_trivial could do?

[Johannes Hölzl]

Okay, I added M_trans anyway.

[Johan Commelin]

How do I need to change the statement?

[Johannes Hölzl]

Either add a tactic: dec_tac := ``[exact dec_trivial] and use this: (h : i ≠ j . dec_tac)

[Johannes Hölzl]

or use default parameter (h : i ≠ j := dec_trivial)

[Johannes Hölzl]

I don't know if the default parameter work. If dec_trivial gets evaluated too early it might not work

[Johan Commelin]

I'll try.

[Johan Commelin]

Ok, the M_trans is nice. So now we need to plug that into the definition of the Hecke operator.

[Johan Commelin]

It isn't happy about meta def dec_tac : tactic unit := ``[exact dec_trivial]

[Johannes Hölzl]

meta def dec_tac : tactic unit := `[exact dec_trivial]

maybe?

[Johan Commelin]

That worked

[Johan Commelin]

So now my goal is:

z : ℂ
⊢ (z + ↑0) / (1 + ↑0 * z) = z

If Kevin saw that goal...

[Johan Commelin]

simp didn't kill it.

[Johannes Hölzl]

Does unfold_coes help?

[Johan Commelin]

Is that a tactic?

[Johannes Hölzl]

yes

[Johan Commelin]

It doesn't help enough...

[Johan Commelin]

I'll go back to the Hecke operator for a moment.

[Johan Commelin]

Ok guys... I'm gone for a week. I might be able to check Zulip now and then, but I won't be able to do any serious Leaning until next week on Thursday.

[Johan Commelin]

I'm looking forward to Kevin's reaction on Friday

[Johan Commelin]

Thanks for all your help so far! I really enjoyed it!

[Patrick Massot]

Thanks for all your efforts

[Patrick Massot]

But we still haven't decided what will happen on Friday

[Patrick Massot]

Seriously, what are we doing tomorrow? @Chris Hughes will you see Kevin tomorrow?

[Johan Commelin]

Tomorrow is Thursday. I guess any cleaning up that we want to do should be done today or tomorrow. On Friday we give Kevin access to kbb and we PR the determinants file and the remainder of matrices.lean

[Johan Commelin]

I don't think there is much in the modular form files that is ready to merge.

[Chris Hughes]

What about sin and cos? We don't have pi yet, but we do have sin and cos.

[Patrick Massot]

I would veto the current definition of sin

[Patrick Massot]

unless it changed recently

[Chris Hughes]

How come?

[Johan Commelin]

What was wrong with it?

[Patrick Massot]

Would you write this on a blackboard?

[Patrick Massot]

def sin (z : ℂ) : ℂ := ((exp (-z * I) - exp (z * I)) * I) / 2

[Patrick Massot]

come on

[Kenny Lau]

I don't see what's wrong with it

[Patrick Massot]

Is it the definition in the UK?

[Johan Commelin]

I think a PR on exp would be nice. Possibly including cos und sin. Hopefully that will induce a rampage by some Lean-fu experts to prove continuity.

[Johan Commelin]

I don't even know what definition of sin I saw. My training in analysis was terrible.

[Johan Commelin]

Possibly it was the analytic continuation of real.sin

[Johan Commelin]

I don't know how real.sin was defined. Probably using angles etc...

[Chris Hughes]

I'm going to have a serious bash on continuity today. The definition I saw was ((exp (z * I) - exp (-z * I))) / (2 * I)

[Patrick Massot]

In France, sin z = (exp (z * I) - exp (-z * I)) * I) / (2*I)

[Kenny Lau]

is there any difference?

[Patrick Massot]

Yes. One is the definition people expect to see, the other one could be a useful lemma if Chris needs it

[Chris Hughes]

I multiplied by $-i$, Patrick divided by $i$.

[Patrick Massot]

Chris, why did you do that?

[Chris Hughes]

It's easier to prove sin (x + y) because I have less division to deal with.

[Patrick Massot]

Then you could use a lemma

[Patrick Massot]

Actually I don't understand why you use these proofs for sin(x+y) etc.

[Chris Hughes]

Which proofs should I use?

[Patrick Massot]

Why not taking real and imaginary parts of the equation exp(i(x+y)) = exp(ix)exp(iy)?

[Patrick Massot]

That's the real life proof

[Patrick Massot]

But I guess you should rather prove continuity and try to get pi

[Patrick Massot]

And also answer my question: will you see Kevin tomorrow?

[Chris Hughes]

Yes.

[Johan Commelin]

@Patrick Massot Why tomorrow? Don't you mean Friday? Or do you have some plan in mind?

[Chris Hughes]

I won't see him on Friday.

[Johan Commelin]

@Scott Morrison Could you give Kevin access when it is Friday 09:00 your time? Because then it is 00:00 his time, I think.

[Scott Morrison]

Sure.

[Johan Commelin]

Nice :lol:

[Patrick Massot]

I meant Friday, sorry

[Johan Commelin]

And @Kenny Lau isn't back in the UK at that point, I guess?

[Kenny Lau]

i'm not

[Johan Commelin]

Patrick, were you thinking of physically giving him some gift? A print-out of the files :lol: ?

[Patrick Massot]

I wanted someone who could see his face and tell us.

[Johan Commelin]

Agreed, that would be nice.

[Mario Carneiro]

Why not taking real and imaginary parts of the equation exp(i(x+y)) = exp(ix)exp(iy)?

That only proves the addition formulas for sin and cos when the arguments are real

[Patrick Massot]

oh yes

[Mario Carneiro]

I don't think there is any substitute for just doing the algebra in the complex case

[Patrick Massot]

I never thought about the complex case here

[Patrick Massot]

crazy

[Reid Barton]

no problem. then just show that two holomorphic functions which agree on the real line are equal :upside_down:

[Patrick Massot]

Great !

[Johan Commelin]

This is so amazing! Awesome! That was an immense tour de force, Chris. Well done!

[Johan Commelin]

I am about to go to bed. I'm sorry I won't be able to be online when Kevin gets his birthday present. I am sure that you guys will be able to break the surprise! I'll read up on it afterwards (-;

[Scott Morrison]

I think the plan is that in 24 minutes I will add Kevin to the kbb repository.

[Johan Commelin]

@Scott Morrison Yes, that's a good plan!

[Johan Commelin]

You can also add him to this stream on Zulip, and you can write a happy birthday post in the general stream.

[Johan Commelin]

I should really go to bed now. Tomorrow I'll have 4 hard math-talks waiting for me...

[Johan Commelin]

Happy PR'ing (-;

[Kevin Buzzard]

wtf?

[Johan Commelin]

@Kevin Buzzard We hope you will enjoy reading back through all our crazy conversations of the last 10 days. :stuck_out_tongue_wink:

[Simon Hudon]

Did we bash Kevin in any of it?

[Patrick Massot]

I don't remember doing it more than on the regular streams

[Patrick Massot]

Kevin: the conversation about this project started in group PM but then it was generating a huge mess of notification for everybody, and I eventually found out anybody could create private streams. So the story of this stream starts in the middle.

[Patrick Massot]

I think it's fair to point out that Johan came with this idea, on September 4th.

[Patrick Massot]

In order to understand the mess in the repository, it may be relevant to know that, beyond Johan's idea of a birthday pi, the unrealistic idea that I proposed was to formal abstract https://www.sciencedirect.com/science/article/pii/S0022314X96900396?via%3Dihub

[Kevin Buzzard]

ROFL

[Kevin Buzzard]

That is so funny. That is a fine abstract to formalise. It would be trivial if there was a half-decent API for modular forms, and Lean is perfect for that sort of thing.

[Kevin Buzzard]

You could formalise a mathematically equivalent statement more easily -- the eigenvalues of a Hecke operator on a space of modular forms are the same as the eigenvalues of a corresponding Hecke operator on a certain group cohomology group, by a theorem of Eichler and Shimura. Formalising group cohomology would perhaps be easier than formalising modular forms -- I'm not really sure but it sounds easier to me. Group cohomology is just there waiting to be done.

[Kevin Buzzard]

I wrote that paper after hearing a talk of Dinakar Ramakrishnan, when he mentioned that he had never seen a modular eigenform whose Hecke eigenvalues generated a non-solvable extension of the rationals. Talking to him afterwards it became clear that this was only because there were no computer programs to compute modular forms, and that we all knew exactly where to look. I took the trouble to look and there they were. Dinakar urged me to write it up.

[Patrick Massot]

We are not so far away from having Hecke operators (they almost act on functions of a fixed weight, and it shouldn't be so hard to show they act on holomorphic functions and preserve boundedness at infinity). We also have characteristic polynomial, and Johannes has been working towards Galois groups. But we mostly gave up when Johan pointed out that we would need that modular forms of a fixed weight form a finite dimensional subspace of holomorphic functions (we do have a vector space structure on holomorphic functions on the upper half plane).

[Kevin Buzzard]

aie, yes, finite-dimensionality is needed. A trivial consequence of the fact that the global sections of a line bundle on a compact Riemann surface are finite-dimensional, so by maths_undergraduate should do it. I'm going to try and build that tactic at Imperial.

Finite-dimensionality for the group cohomology would be a trivial consequence of the fact that a finite index subgroup of a finitely-generated group is finitely-generated, and the fact that SL(2,Z) is finitely-generated. I don't know how easy it is to prove the finite index result just by group theory, I am no algebraist. The proofs I know are topological. The group cohomology variant would be provably equal once we had something like Stokes' theorem.

[Johan Commelin]

We have the fact that S and T generate SL2Z in your birthday repo :lol:

[Kevin Buzzard]

Right. But for finite-dimensionality of the cohomology group for general levels we'll need that a finite index subgroup of a f.g. group is f.g. But I see what you're saying -- this is enough to prove that level 1 modular forms are finite-dimensional.

[Kevin Buzzard]

There is some kind of subtlety which I have only recently become aware of, and again it was a comment of @Reid Barton which clarified things for me. Without some general theory of global sections of line bundles on compact Riemann surfaces it's kind of a pain to prove that the space of modular forms is finite-dimensional. But it is finite-dimensional, so one can define the char poly of a Hecke operator to be "if the space is infinite-dimensional then 37, and if it's finite-dimensional then the char poly". This gives a sorry-free way of defining the char poly which is human-provably equivalent to the right thing. What one cannot do is to get away without defining the Hecke operator at all and just sorrying it -- because then the char poly has a sorry in too.

One of the things I realise I want now is for a bunch of mathematicians to come along and say "can you formalise theorem X or definition Y in Lean?" because questions such as that are ways of discovering what kind of an API a normal mathematician (perhaps with no Lean training) wants. Who cares about proofs, they are too hard. I know that Mario feels that a definition is pointless without an application. How about if the application is some statements of theorems or conjectures?