Zulip Chat Archive

Stream: kbb

Topic: SL2Z action


view this post on Zulip Johan Commelin (Sep 14 2018 at 09:54):

I'm trying to continue Patrick's work on finiteness of the quotient SL2Z \ (Mat m).
This is one (approximate) step that would be useful:

def reps := {A : Mat m | A.c = 0  0  A.a  0  A.b  int.nat_abs A.b  int.nat_abs A.d }

def ι : reps m  fin m :=
λ A, _

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:54):

I get a deterministic timeout just for parsing the type of ι

view this post on Zulip Kenny Lau (Sep 14 2018 at 09:54):

is that MWE?

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:55):

Proof strategy: we need to prove that reps is finite. Do this by injecting into fin m × fin m × fin m.

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:55):

It is not exactly a MWE. You can find it by pulling the latest commits from kbb

view this post on Zulip Kenny Lau (Sep 14 2018 at 09:55):

I don't think that's a good strategy

view this post on Zulip Johan Commelin (Sep 14 2018 at 09:55):

Ok, so how do you prove that reps is a finset?

view this post on Zulip Kenny Lau (Sep 14 2018 at 09:58):

equiv it with finset.filter (finset.univ : (finset (fin m × fin m × fin m))) sorry

view this post on Zulip Kenny Lau (Sep 14 2018 at 09:59):

also why int.nat_abs?

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:00):

Because I don't know better?

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:00):

that's not what I mean

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:00):

That's what you were using in your inductive proof

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:00):

alright

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:01):

I think I'll prove that it's a fintype

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:05):

ah

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:05):

of course it times out

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:05):

m is an integer

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:05):

fin m makes no sense

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:07):

Why did it time out? Why didn't it slap me in the face?

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:08):

It should just have errored immediately saying that m is not a nat.

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:09):

I think it's searching for a coercion from int to nat

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:13):

also it still isn't a fintype

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:16):

What isn't?

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:17):

if m=0 I don't think it's a fintype

view this post on Zulip Kenny Lau (Sep 14 2018 at 10:17):

the repr

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:17):

True. But you need m ≠ 0

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:18):

Otherwise the orbits are parameterised by pairs (a,b) with 0 ≤ a and a,b coprime.

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:18):

Inparticularinfinitelymanyorbits

view this post on Zulip Johan Commelin (Sep 14 2018 at 10:21):

Maybe we should have assumed m : ℕ from the beginning.

view this post on Zulip Kenny Lau (Sep 14 2018 at 11:11):

why on earth is there classical.prop_decidable in the beginning of the file?

view this post on Zulip Patrick Massot (Sep 14 2018 at 11:13):

Because it's a math file

view this post on Zulip Kenny Lau (Sep 14 2018 at 11:13):

about integers

view this post on Zulip Patrick Massot (Sep 14 2018 at 11:14):

The last lemma requires it

view this post on Zulip Patrick Massot (Sep 14 2018 at 11:15):

it needs decidable_eq (quotient (action_rel (SL2Z_M_ m)))

view this post on Zulip Kenny Lau (Sep 14 2018 at 11:15):

I'll prove it

view this post on Zulip Kenny Lau (Sep 14 2018 at 11:15):

after dinner

view this post on Zulip Patrick Massot (Sep 14 2018 at 11:16):

I guess we can't really avoid that

view this post on Zulip Kenny Lau (Sep 14 2018 at 11:17):

you're welcome to prove it if you want

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:17):

@Patrick Massot Oo.ooo you released Kenny's inner wrath.

view this post on Zulip Johan Commelin (Sep 14 2018 at 11:17):

I guess in this case you can prove that decidable_eq if you want to.

view this post on Zulip Patrick Massot (Sep 14 2018 at 11:18):

I already proved it: https://github.com/semorrison/kbb/blob/757806ec7f9848a5eb405ca26f5a12d94932a197/src/SL2Z_generators.lean#L4

view this post on Zulip Kenny Lau (Sep 14 2018 at 11:18):

no you haven't

view this post on Zulip Johan Commelin (Sep 14 2018 at 16:25):

Cool! So now we have established finiteness of the orbit set!

view this post on Zulip Patrick Massot (Sep 14 2018 at 18:42):

Cool! So now we have established finiteness of the orbit set!

Not quite, there has been some regression, let me fix that.

view this post on Zulip Kenny Lau (Sep 14 2018 at 18:42):

eh... I'm editing SL2Z_generators.lean

view this post on Zulip Patrick Massot (Sep 14 2018 at 18:42):

Done: no more sorry in SL2Z_generators.lean

view this post on Zulip Kenny Lau (Sep 14 2018 at 18:43):

ah I see what you did

view this post on Zulip Kenny Lau (Sep 14 2018 at 21:15):

done

view this post on Zulip Kenny Lau (Sep 14 2018 at 21:15):

/-- correct if m ≠ 0 -/
def reduce (m : ) (A : Mat m) : Mat m :=
(λ n, nat.strong_rec_on n $ λ n ih A H,
if H1 : n = 0
then if H2 : A.a > 0
  then SL2Z_M_ m (T^(-(A.b/A.d))) A
  else SL2Z_M_ m (T^(-(-A.b/ -A.d))) (SL2Z_M_ m S (SL2Z_M_ m S A))
else ih _ (by subst H; from reduce_aux _ _ H1)
  (SL2Z_M_ m S (SL2Z_M_ m (T^(-(A.a/A.c))) A)) rfl
: Π n (A:Mat m), n = int.nat_abs A.c  Mat m) _ A rfl

--#reduce reduce (-1) ⟨1, 3, 1, 2, by norm_num⟩

view this post on Zulip Kenny Lau (Sep 14 2018 at 21:16):

def reps_equiv (hm : m  0) : quotient (action_rel (SL2Z_M_ m))  reps m :=

view this post on Zulip Kenny Lau (Sep 14 2018 at 21:16):

@Patrick Massot @Johan Commelin

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:28):

Ah, that looks like a smart way to approach this!

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:35):

@Kenny Lau The linecount in that file really exploded! You write Lean several orders of magnitude faster than I can read it.

view this post on Zulip Kenny Lau (Sep 15 2018 at 04:37):

lol

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:38):

Also you seem to like refactoring code, whereas for me there is some nasty psychological barrier...

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:39):

Anyway, thanks a lot!

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:39):

@Mario Carneiro Have you seen what happened?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:39):

what is this?

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:39):

We now have several hundreds of lines of code about a silly type called SL2Z, and it doesn't tie in to the matrix code at all.

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:40):

Well, that is not strictly true, Kenny proved that SL2Z is equiv to SL 2 int.

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:41):

But now this SL2Z is acting on different sets, etc... and all this extra structure has not been tied to regular matrices.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:41):

This makes me vaguely uncomfortable

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:41):

I think this was a great experiment, but I'm somewhat worried.

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:41):

Would you mind scrolling through the repo a bit?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:42):

unless the properties are not shared by other dimensions or rings?

view this post on Zulip Kenny Lau (Sep 15 2018 at 04:42):

SL2Z is generated by two matrices

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:42):

Right.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:42):

induction_on is frightening

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:43):

But the action of SL2Z on other 2x2-matrices is generic

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:43):

And the action of SL2Z on the upper-half plane is a restriction of the action of (GL 2 real)_+ on the upper half plane

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:44):

So certain things are really specific, others are not.

view this post on Zulip Kenny Lau (Sep 15 2018 at 04:44):

which is the restriction of GL2R acting on CP1

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:45):

where should I be looking?

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:45):

the frightening proof linked above appears to have been removed

view this post on Zulip Kenny Lau (Sep 15 2018 at 04:45):

I made a function called reduce

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:45):

You could start with modular_forms.lean and then drill down.

view this post on Zulip Mario Carneiro (Sep 15 2018 at 04:46):

on master?

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:46):

Most of the hard stuff is happening in SL2Z_generators and some in modular_group.lean

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:46):

Yes

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:46):

We don't really use branches

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:50):

In the end, I would like Hecke_operator in hecke_operators.lean to have a somewhat readable definition.

view this post on Zulip Johan Commelin (Sep 15 2018 at 04:50):

It feels to me like all the ingredients are now there... but as you can see, my attempt at writing the definition is :poop:


Last updated: May 18 2021 at 10:14 UTC