## Stream: kbb

### Topic: SL2Z action

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


#### Johan Commelin (Sep 14 2018 at 09:54):

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

is that MWE?

#### 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.

#### 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

#### Kenny Lau (Sep 14 2018 at 09:55):

I don't think that's a good strategy

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

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

#### Kenny Lau (Sep 14 2018 at 09:58):

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

#### Kenny Lau (Sep 14 2018 at 09:59):

also why int.nat_abs?

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

Because I don't know better?

#### Kenny Lau (Sep 14 2018 at 10:00):

that's not what I mean

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

That's what you were using in your inductive proof

alright

#### Kenny Lau (Sep 14 2018 at 10:01):

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

ah

#### Kenny Lau (Sep 14 2018 at 10:05):

of course it times out

#### Kenny Lau (Sep 14 2018 at 10:05):

m is an integer

#### Kenny Lau (Sep 14 2018 at 10:05):

fin m makes no sense

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

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

#### Johan Commelin (Sep 14 2018 at 10:08):

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

#### Kenny Lau (Sep 14 2018 at 10:09):

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

#### Kenny Lau (Sep 14 2018 at 10:13):

also it still isn't a fintype

What isn't?

#### Kenny Lau (Sep 14 2018 at 10:17):

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

the repr

#### Johan Commelin (Sep 14 2018 at 10:17):

True. But you need m ≠ 0

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

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

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

Inparticularinfinitelymanyorbits

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

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

#### Kenny Lau (Sep 14 2018 at 11:11):

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

#### Patrick Massot (Sep 14 2018 at 11:13):

Because it's a math file

#### Patrick Massot (Sep 14 2018 at 11:14):

The last lemma requires it

#### Patrick Massot (Sep 14 2018 at 11:15):

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

I'll prove it

after dinner

#### Patrick Massot (Sep 14 2018 at 11:16):

I guess we can't really avoid that

#### Kenny Lau (Sep 14 2018 at 11:17):

you're welcome to prove it if you want

#### Johan Commelin (Sep 14 2018 at 11:17):

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

#### Johan Commelin (Sep 14 2018 at 11:17):

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

no you haven't

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

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

#### 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.

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

eh... I'm editing SL2Z_generators.lean

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

Done: no more sorry in SL2Z_generators.lean

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

ah I see what you did

done

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


#### Kenny Lau (Sep 14 2018 at 21:16):

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


#### Kenny Lau (Sep 14 2018 at 21:16):

@Patrick Massot @Johan Commelin

#### Johan Commelin (Sep 15 2018 at 04:28):

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

#### 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.

lol

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

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

#### Johan Commelin (Sep 15 2018 at 04:39):

Anyway, thanks a lot!

#### Johan Commelin (Sep 15 2018 at 04:39):

@Mario Carneiro Have you seen what happened?

what is this?

#### 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.

#### Johan Commelin (Sep 15 2018 at 04:40):

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

#### 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.

#### Mario Carneiro (Sep 15 2018 at 04:41):

This makes me vaguely uncomfortable

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

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

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

Would you mind scrolling through the repo a bit?

#### Mario Carneiro (Sep 15 2018 at 04:42):

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

#### Kenny Lau (Sep 15 2018 at 04:42):

SL2Z is generated by two matrices

Right.

#### Mario Carneiro (Sep 15 2018 at 04:42):

induction_on is frightening

#### Johan Commelin (Sep 15 2018 at 04:43):

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

#### 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

#### Johan Commelin (Sep 15 2018 at 04:44):

So certain things are really specific, others are not.

#### Kenny Lau (Sep 15 2018 at 04:44):

which is the restriction of GL2R acting on CP1

#### Mario Carneiro (Sep 15 2018 at 04:45):

where should I be looking?

#### Mario Carneiro (Sep 15 2018 at 04:45):

the frightening proof linked above appears to have been removed

#### Kenny Lau (Sep 15 2018 at 04:45):

I made a function called reduce

#### Johan Commelin (Sep 15 2018 at 04:45):

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

on master?

#### Johan Commelin (Sep 15 2018 at 04:46):

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

Yes

#### Johan Commelin (Sep 15 2018 at 04:46):

We don't really use branches

#### 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.

#### 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