SL2Z action

Stream: kbb

[Johan Commelin]

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, _

[Johan Commelin]

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

[Kenny Lau]

is that MWE?

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

I don't think that's a good strategy

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

also why int.nat_abs?

[Johan Commelin]

Because I don't know better?

[Kenny Lau]

that's not what I mean

[Johan Commelin]

That's what you were using in your inductive proof

[Kenny Lau]

alright

[Kenny Lau]

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

[Kenny Lau]

ah

[Kenny Lau]

of course it times out

[Kenny Lau]

m is an integer

[Kenny Lau]

fin m makes no sense

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

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

[Kenny Lau]

also it still isn't a fintype

[Johan Commelin]

What isn't?

[Kenny Lau]

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

[Kenny Lau]

the repr

[Johan Commelin]

True. But you need m ≠ 0

[Johan Commelin]

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

[Johan Commelin]

Inparticularinfinitelymanyorbits

[Johan Commelin]

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

[Kenny Lau]

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

[Patrick Massot]

Because it's a math file

[Kenny Lau]

about integers

[Patrick Massot]

The last lemma requires it

[Patrick Massot]

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

[Kenny Lau]

I'll prove it

[Kenny Lau]

after dinner

[Patrick Massot]

I guess we can't really avoid that

[Kenny Lau]

you're welcome to prove it if you want

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Kenny Lau]

no you haven't

[Johan Commelin]

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

[Patrick Massot]

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

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

[Kenny Lau]

eh... I'm editing SL2Z_generators.lean

[Patrick Massot]

Done: no more sorry in SL2Z_generators.lean

[Kenny Lau]

ah I see what you did

[Kenny Lau]

done

[Kenny Lau]

/-- 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⟩

[Kenny Lau]

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

[Kenny Lau]

@Patrick Massot @Johan Commelin

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

lol

[Johan Commelin]

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

[Johan Commelin]

Anyway, thanks a lot!

[Johan Commelin]

@Mario Carneiro Have you seen what happened?

[Mario Carneiro]

what is this?

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

This makes me vaguely uncomfortable

[Johan Commelin]

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

[Johan Commelin]

Would you mind scrolling through the repo a bit?

[Mario Carneiro]

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

[Kenny Lau]

SL2Z is generated by two matrices

[Johan Commelin]

Right.

[Mario Carneiro]

induction_on is frightening

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

So certain things are really specific, others are not.

[Kenny Lau]

which is the restriction of GL2R acting on CP1

[Mario Carneiro]

where should I be looking?

[Mario Carneiro]

the frightening proof linked above appears to have been removed

[Kenny Lau]

I made a function called reduce

[Johan Commelin]

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

[Mario Carneiro]

on master?

[Johan Commelin]

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

[Johan Commelin]

Yes

[Johan Commelin]

We don't really use branches

[Johan Commelin]

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

[Johan Commelin]

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