## Stream: kbb

### Topic: generators

#### Patrick Massot (Sep 12 2018 at 19:20):

I just saw Kenny's work on generating SL2Z. It looks impressive

#### Patrick Massot (Sep 12 2018 at 19:21):

But I wonder how to properly generalize it.

#### Kenny Lau (Sep 12 2018 at 19:21):

I just saw Kenny's work on generating SL2Z. It looks impressive

thanks!

#### Patrick Massot (Sep 12 2018 at 19:22):

I would have expected to see a predicate saying: this set generate this group. And then a mechanism constructor the eliminator from this

#### Patrick Massot (Sep 12 2018 at 19:22):

Is this counter-intuitive order related to constructivity?

#### Kenny Lau (Sep 12 2018 at 19:23):

not constructivity

#### Kenny Lau (Sep 12 2018 at 19:23):

it's just the same reason we don't take quot.exists_rep as an axiom, but rather quot.ind

?

#### Kenny Lau (Sep 12 2018 at 19:26):

it's easier to use

#### Patrick Massot (Sep 12 2018 at 19:34):

Do you think there could be some tactic consuming a proof of generation and building the eliminator?

#### Kenny Lau (Sep 12 2018 at 19:36):

I don't know about tactics

#### Patrick Massot (Sep 12 2018 at 19:37):

Maybe a tactic is not needed, I'm only trying to understand whether there could be an interface which looks more natural (to me at least)

#### Patrick Massot (Sep 12 2018 at 19:38):

@Mario Carneiro Do you have any insight? We are discussing https://github.com/semorrison/kbb/blob/master/src/SL2Z_generators.lean#L49 and https://github.com/semorrison/kbb/blob/master/src/SL2Z_generators.lean#L97

#### Mario Carneiro (Sep 12 2018 at 19:50):

protected theorem induction_on {C : SL2Z → Prop} (A : SL2Z)
(H1 : C 1) (HS : ∀ B, C B → C (S * B))
(HT : ∀ B, C B → C (T * B)) : C A :=


It's amazing how little this tells me

#### Mario Carneiro (Sep 12 2018 at 19:50):

everything is letters

#### Patrick Massot (Sep 12 2018 at 19:51):

S and T are explicit elements of SL2Z defined a few lines earlier

#### Patrick Massot (Sep 12 2018 at 19:51):

So this theorem is a really weird way to state those elements generate SL2Z

#### Mario Carneiro (Sep 12 2018 at 19:51):

there is an SL2Z attribute?

#### Patrick Massot (Sep 12 2018 at 19:52):

https://github.com/semorrison/kbb/blob/master/src/modular_group.lean#L6

#### Mario Carneiro (Sep 12 2018 at 19:52):

seems like a fine induction statement

#### Patrick Massot (Sep 12 2018 at 19:53):

Sure. But the question is: what is the proper general context and interface? Dealing with generating sets for groups

#### Mario Carneiro (Sep 12 2018 at 19:53):

I don't think we have span for groups yet, I'm working on improving span for modules and we can do something similar in groups

#### Mario Carneiro (Sep 12 2018 at 19:54):

I guess it's usually called closure in groups?

#### Patrick Massot (Sep 12 2018 at 19:54):

I did spans for group a very long time ago

in mathlib?

no

I think I recall

#### Chris Hughes (Sep 12 2018 at 19:54):

I think closure is in mathlib

#### Patrick Massot (Sep 12 2018 at 19:54):

It's the first thing I did

#### Mario Carneiro (Sep 12 2018 at 19:54):

you were doing something with norms in groups

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

https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/invariant_norms.lean#L107

#### Mario Carneiro (Sep 12 2018 at 19:55):

But we don't need the general theory for this theorem, and it won't make the proof any easier

#### Mario Carneiro (Sep 12 2018 at 19:55):

given what is currently available, this theorem is fine

#### Patrick Massot (Sep 12 2018 at 19:56):

Yes. I was trying to formalize the trivial part of https://arxiv.org/abs/1803.07997

#### Mario Carneiro (Sep 12 2018 at 19:56):

if and when we get spans in groups it would be natural to state span {S, T} = top

#### Kenny Lau (Sep 12 2018 at 19:56):

guys, it's just closure

?

#### Chris Hughes (Sep 12 2018 at 19:57):

From subgroup.lean

inductive in_closure (s : set α) : α → Prop
| basic {a : α} : a ∈ s → in_closure a
| one : in_closure 1
| inv {a : α} : in_closure a → in_closure a⁻¹
| mul {a b : α} : in_closure a → in_closure b → in_closure (a * b)


#### Patrick Massot (Sep 12 2018 at 19:57):

It's not my question though: I would like to first prove the span is everything, and then deduce the eliminator, not the other way around

#### Mario Carneiro (Sep 12 2018 at 19:57):

the proofs will be the same

#### Patrick Massot (Sep 12 2018 at 19:58):

Even better then. We can write things like we do in maths and have the same proofs

#### Mario Carneiro (Sep 12 2018 at 19:58):

ah, okay so you can write closure {S, T} = univ

#### Mario Carneiro (Sep 12 2018 at 19:59):

and the proof is to prove in_closure {S, T} by exactly the same induction argument as used in that big proof

#### Patrick Massot (Sep 12 2018 at 19:59):

Mario, did you follow both links of the messages when I pinged you?

#### Patrick Massot (Sep 12 2018 at 19:59):

The second linked line contains closure {S, T} = univ

ah, so it does

#### Mario Carneiro (Sep 12 2018 at 20:00):

However, the induction statement is a bit stronger than what you get from closure

#### Mario Carneiro (Sep 12 2018 at 20:00):

it says that S and T generate the group as a monoid

#### Patrick Massot (Sep 12 2018 at 20:00):

My questions were: 1) could we directly prove closure {S, T} = univ without more pain (you seem to say yes) 2) could you generate the induction statement automatically from there?

#### Mario Carneiro (Sep 12 2018 at 20:01):

there is no mention of inverses in the induction theorem

#### Mario Carneiro (Sep 12 2018 at 20:01):

but in the closure of a group you need to also assume closure by inverses

#### Mario Carneiro (Sep 12 2018 at 20:01):

so the real equivalent statement would be monoid.closure {S, T} = univ

#### Patrick Massot (Sep 12 2018 at 20:02):

Ok, let's assume we also define monoid.closure. How do we generate the eliminator?

#### Patrick Massot (Sep 12 2018 at 20:02):

Would that be a tactic?

no, a theorem

#### Mario Carneiro (Sep 12 2018 at 20:03):

monoid.closure would be defined by an inductive type just like in_closure is

#### Mario Carneiro (Sep 12 2018 at 20:03):

and its eliminator is basically exactly that theorem

#### Mario Carneiro (Sep 12 2018 at 20:03):

You would prove that {x | C x} is a monoid containing {S, T} and so deduce it is univ

#### Patrick Massot (Sep 12 2018 at 20:04):

Would you need to redo that for every generating set of every group, or would you have a general theorem?

#### Mario Carneiro (Sep 12 2018 at 20:04):

the general theorem is the eliminator for in_closure

#### Mario Carneiro (Sep 12 2018 at 20:05):

the part that needs to be redone is the unfolding of the set {S, T} into two induction hypotheses about multiplying by S and T

#### Patrick Massot (Sep 12 2018 at 20:27):

I tried to do the exercise, but clearly I missed something because it looks very complicated

#### Patrick Massot (Sep 12 2018 at 20:33):

I wrote, at the end of that file:

section
variables {α : Type*} [group α]
inductive monoid.in_closure (s : set α) : α → Prop
| basic {a : α} : a ∈ s → monoid.in_closure a
| one : monoid.in_closure 1
| mul {a b : α} : monoid.in_closure a → monoid.in_closure b → monoid.in_closure (a * b)

def monoid.closure (s : set α) : set α := {a | monoid.in_closure s a }
end

@[elab_as_eliminator]
protected theorem induction_on' {C : SL2Z → Prop} (A : SL2Z)
(H1 : C 1) (HS : ∀ B, C B → C (S * B))
(HT : ∀ B, C B → C (T * B)) : C A :=
begin

have : monoid.in_closure ({S, T} : set SL2Z) A := sorry,
apply monoid.in_closure.rec_on this _ H1,
sorry
end


The first sorry is irrelevant. But the tactic state after the first sorry is not what I was hoping for. I tried to move on but it looked too complicated to be what you suggested

#### Mario Carneiro (Sep 12 2018 at 20:45):

There is a theorem that in_closure can be generated by only left multiplication by the generators

#### Mario Carneiro (Sep 12 2018 at 20:46):

If you want it to be by definition, you will need the following definition for monoid.in_closure

inductive monoid.in_closure (s : set α) : α → Prop
| one : monoid.in_closure 1
| mul_basic {a b : α} : a ∈ s → monoid.in_closure b → monoid.in_closure (a * b)


Ok, thanks

#### Patrick Massot (Sep 12 2018 at 20:52):

That theorem is indeed what I saw I needed to prove, and I was confused because it seemed to contradict the announced triviality

#### Patrick Massot (Sep 12 2018 at 20:53):

With the stronger definition of monoid.in_closure, the new proof is

@[elab_as_eliminator]
protected theorem induction_on' {C : SL2Z → Prop} (A : SL2Z)
(H1 : C 1) (HS : ∀ B, C B → C (S * B))
(HT : ∀ B, C B → C (T * B)) : C A :=
begin
have : monoid.in_closure ({S, T} : set SL2Z) A := sorry,
apply monoid.in_closure.rec_on this H1,
intros A B H,
cases H ; intro h ; finish
end


#### Patrick Massot (Sep 12 2018 at 20:53):

which looks like it could admit a general version

#### Patrick Massot (Sep 12 2018 at 20:54):

Now, I need to go to bed, but I'll probably come back to all this tomorrow

Thanks again!

#### Johan Commelin (Sep 13 2018 at 03:57):

@Kenny Lau A really cool way to generalise this is to apply this strategy to the action of SL2Z on matrices with determinant m. You get the same sort of "Euclidean algorithm"-like induction steps. The end result is that you prove that every matrix is equivalent to $\begin{pmatrix} a & b \\ 0 & d \end{pmatrix}$, where $a \cdot d = m,\quad a > 0,\quad d > 0$, and $0 \le b < d$.

#### Johan Commelin (Sep 13 2018 at 03:57):

In particular, the set of orbits is finite.

#### Johan Commelin (Sep 13 2018 at 03:57):

If you apply this to the case m = 1 you recover the result that S and T generate SL2Z.

#### Johan Commelin (Sep 13 2018 at 03:58):

Once we know this set is finite for arbitrary m : int, then we can define Hecke operators!

#### Johan Commelin (Sep 13 2018 at 03:59):

I think that would be a really cool move.

#### Johan Commelin (Sep 13 2018 at 06:31):

@Kenny Lau What do you think of this?

great!

#### Johan Commelin (Sep 13 2018 at 06:32):

How hard do you think it is to adapt your proof?

maybe 30% hard!

#### Kenny Lau (Sep 13 2018 at 06:34):

can't wait to see someone implement it!

Lol

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

Do we have notation for group actions?

#### Kenny Lau (Sep 13 2018 at 06:41):

I used \ci a long time ago

#### Johan Commelin (Sep 13 2018 at 06:43):

But it is not in mathlib?

it isn't

#### Johan Commelin (Sep 13 2018 at 06:46):

Hmm, so I generalised the simp lemmas a bit. Now I need to cook up a new induction statement.

#### Johan Commelin (Sep 13 2018 at 06:46):

Should C 1 be replaced by the explicit representatives that I described above?

sure

#### Johan Commelin (Sep 13 2018 at 06:58):

@Kenny Lau Does this look good?

protected theorem induction_on {C : (Mat m) → Prop} (A : Mat m)
(H0 : ∀ {a b d : ℤ} (h1 : a * d = m) (h2 : 0 < a) (h3 : 0 < d) (h4 : 0 ≤ b) (h5 : b < d), C ⟨a,b,0,d,by simp [h1]⟩)
(HS : ∀ B, C B → C (SL2Z_M_ m S B)) (HT : ∀ B, C B → C (SL2Z_M_ m T B)) : C A :=


#### Kenny Lau (Sep 13 2018 at 06:59):

what if m is negative?

or 0?

#### Johan Commelin (Sep 13 2018 at 07:00):

Hmm, good point, I guess I should drop my requirement on d.

#### Johan Commelin (Sep 13 2018 at 07:00):

Let me think it through...

#### Johan Commelin (Sep 13 2018 at 07:02):

For m = 0 the statement might be false.

#### Johan Commelin (Sep 13 2018 at 07:03):

You have matrices (a, 0, 0, 0). And I think they are not sharing orbits, are they?

#### Johan Commelin (Sep 13 2018 at 07:04):

So I drop h3, and h5 becomes b < (abs d).

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

What is the general strategy to kill this goal:

H : C {a := B.a, b := B.b, c := B.c, d := B.d, det := _}
⊢ C B


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

exact H doesn't work. Somehow I'dd like to prove it by some extensionality or something.

#### Patrick Massot (Sep 13 2018 at 07:20):

Did you try convert H ?

#### Kenny Lau (Sep 13 2018 at 07:21):

cases B; exact H

#### Patrick Massot (Sep 13 2018 at 07:43):

Kenny's solution is more efficient. But I think it's still good to keep in mind that convert H, cases B, congr works

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

Because convert H is a natural thing to try when exact H refuses to work

I disagree

#### Kenny Lau (Sep 13 2018 at 07:44):

congr can go uncontrollable

#### Kenny Lau (Sep 13 2018 at 07:45):

(convert is just a kind of congr)

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

I'm not saying this will always work

#### Kenny Lau (Sep 13 2018 at 07:45):

I'm saying we shouldn't make convert our "first resort"

#### Kenny Lau (Sep 13 2018 at 07:46):

for lack of a better word

#### Johan Commelin (Sep 13 2018 at 07:58):

Here is what I've got so far

@[elab_as_eliminator]
protected theorem induction_on {C : (Mat m) → Prop} (A : Mat m)
(H0 : ∀ {a b d : ℤ} (h1 : a * d = m) (h2 : 0 ≤ a) (h3 : 0 ≤ b) (h4 : b ≤ d ∨ b ≤ -d), C ⟨a,b,0,d,by simp [h1]⟩)
(HS : ∀ B, C B → C (SL2Z_M_ m S B)) (HT : ∀ B, C B → C (SL2Z_M_ m T B)) : C A :=
have hSid : ∀ B, (SL2Z_M_ m S (SL2Z_M_ m S (SL2Z_M_ m S (SL2Z_M_ m S B)))) = B, from λ B, by ext; simp [SL2Z_M_],
have HS' : ∀ B, C (SL2Z_M_ m S B) → C B,
from λ B ih, have H : _ := (HS _ $HS _$ HS _ ih), by rwa hSid B at H,
have hTinv : ∀ B, SL2Z_M_ m S (SL2Z_M_ m S (SL2Z_M_ m S (SL2Z_M_ m T (SL2Z_M_ m S (SL2Z_M_ m T (SL2Z_M_ m S B)))))) = SL2Z_M_ m T⁻¹ B,
from λ B, by repeat {rw [←is_monoid_action.mul (SL2Z_M_ m)]}; congr,
have HT' : ∀ B, C B → C (SL2Z_M_ m T⁻¹ B),
from λ B ih, by {have H := (HS _ $HS _$ HS _ $HT _$ HS _ $HT _$ HS _ ih), by rwa [hTinv] at H},
-- have HT2 : ∀ n : ℤ, C (T^n),
--   from λ n, int.induction_on n H1
--     (λ i ih, by rw [add_comm, gpow_add]; from HT _ ih)
--     (λ i ih, by rw [sub_eq_neg_add, gpow_add]; from HT1 _ ih),
have HT3 : ∀ B, C (SL2Z_M_ m T B) → C B, from λ B ih,
begin
have H := HT' (SL2Z_M_ m T B) ih,
rw [←is_monoid_action.mul (SL2Z_M_ m)] at H,
simp at H,
rw [is_monoid_action.one (SL2Z_M_ m)] at H,
exact H
end,
have HT4 : ∀ B, C (SL2Z_M_ m T⁻¹ B) → C B, from λ B ih,
begin
have H := HT (SL2Z_M_ m T⁻¹ B) ih,
rw [←is_monoid_action.mul (SL2Z_M_ m)] at H,
simp at H,
rw [is_monoid_action.one (SL2Z_M_ m)] at H,
exact H
end,
have HT5 : ∀ B (n:ℤ), C (SL2Z_M_ m (T^n) B) → C B, from λ B n,
int.induction_on n (by rw [gpow_zero, is_monoid_action.one (SL2Z_M_ m)]; from id)
(λ i ih1 ih2, ih1 $HT3 _$ begin
conv { congr, rw ←is_monoid_action.mul (SL2Z_M_ m) },
conv at ih2 { congr, rw [add_comm, gpow_add, gpow_one] },
assumption end)
(λ i ih1 ih2, ih1 $HT4 _$ begin
conv { congr, rw ←is_monoid_action.mul (SL2Z_M_ m) },
conv at ih2 { congr, rw [sub_eq_neg_add, gpow_add, gpow_neg_one] },
assumption end),


#### Patrick Massot (Sep 13 2018 at 08:06):

Isn't it even more contrived to prove first the induction lemma in that case?

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

I don't know. But if we want Hecke operators, we need it.

#### Patrick Massot (Sep 13 2018 at 08:12):

Why don't you want to state the result you need in the way you would state it on paper, and then deduce the induction statement?

#### Patrick Massot (Sep 13 2018 at 08:16):

Is there an available written proof you are trying to follow?

#### Johan Commelin (Sep 13 2018 at 08:28):

No, I just cooked up a proof this morning.

#### Johan Commelin (Sep 13 2018 at 08:28):

There are probably proofs around, but I haven't found one yet.

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

Do you need help here?

#### Johan Commelin (Sep 13 2018 at 08:39):

I'm learning :lol:

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

I've pushed a proof that has 1 sorry for the case A.c = 0.

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

I still need to learn how to juggle around hypotheses.

#### Johan Commelin (Sep 13 2018 at 08:52):

A mathematician says: Ooh, if A.a ≤ 0 then replace A by -A. I find it hard to make such a step in Lean.

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

@Kenny Lau Do you want to teach me?

#### Patrick Massot (Sep 13 2018 at 08:53):

where did you push?

#### Kenny Lau (Sep 13 2018 at 08:53):

well S*S*A = -A

#### Kenny Lau (Sep 13 2018 at 08:53):

so you prove it for S*S*A first

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

Fail... I only commited. Now I pushed.

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

I have hneg : ∀ (B : Mat m), SL2Z_M_ m S (SL2Z_M_ m S B) = -B in my context

#### Patrick Massot (Sep 13 2018 at 08:55):

I also see n n : ℕ, which is a good recipe for confusion

#### Johan Commelin (Sep 13 2018 at 08:58):

That is because of the strong_induction

#### Johan Commelin (Sep 13 2018 at 08:59):

I don't understand why strong_induction does this, but we could safely forget about the first n. It has played it's role, and the new n took over.

#### Patrick Massot (Sep 13 2018 at 08:59):

Why don't you use another name for the new n?

#### Patrick Massot (Sep 13 2018 at 09:00):

Anyway, I can't help with this sorry without knowing what is the paper proof

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

Never mind. I might have found a way out.

#### Johan Commelin (Sep 13 2018 at 11:03):

I did find a way out, but it is becoming pretty crazy. (I also had lunch. Please don't be worried that I kept banging my head against this wall for 3 hours.)

#### Johan Commelin (Sep 13 2018 at 11:03):

@Kenny Lau Would you want to take over?

I’m not free now

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

There are 3 sorrys left in https://github.com/semorrison/kbb/blob/master/src/SL2Z_generators.lean#L118-L125,

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

they should all be by schoolkid.

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

Let's say I try the first one

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

Ooh, I was just trying that one.

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

I'm almost there!

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

I just finished a maths paper. So I am allowing myself some Lean time.

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

@Patrick Massot I only need 1 ≤ A.d * A.d

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

I'm at this : A.d * A.d > 0 ⊢ A.d * A.d - 1 ≥ 0

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

Right, same place (-;

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

I'll move to sorry₂

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

Oh no, for Lean it's not the same place

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

I'm soo close this : A.d * A.d > 0 ⊢ 1 ≤ A.d * A.d

Done!

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

Should I move to the third one?

Yes please.

Did you push?

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

Do you want me to push?

I pushed

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

This should be a standard lemma: A.b / A.d * A.d ≤ A.b But I can't find it...

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

What is this /? Euclidean quotient?

seems so

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

Right, so (11 / (-3)) = -3

#### Rob Lewis (Sep 13 2018 at 14:36):

int.div_mul_le? Are you working over int? I'm not really following the context.

bingo!

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

@Johan Commelin Are you sure this sorry is true?

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

It actually looks really weird

I'm done with 2

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

You're worried about 3?

yes

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

Hmm, I think it is fine. Proof by example: abs (101 - (101/13 * 13)) ≤ abs(13), which reduces to 10 ≤ 13.

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

By the way, I pushed my fix of sorry₂

hold on

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

You sent me on a wrong track to make sure you'll be done first!

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

Guess what, I have to catch a train. So I won't be Leaning for the next 90 minutes.

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

And now you set me a deadline!

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

And I haven't made any progress on sorry₃

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

@Kenny Lau is online :time_ticking:

hi

done

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

so much suffering...

#### Johan Commelin (Sep 13 2018 at 16:52):

@Patrick Massot Thank you so much!

#### Patrick Massot (Sep 13 2018 at 16:59):

The stupid lemma in the middle is now in mathlib

#### Patrick Massot (Sep 13 2018 at 17:00):

I also removed a couple of simp that were in the middle of the proof hence frowned upon

#### Johan Commelin (Sep 13 2018 at 17:04):

Ok, I realised that it might have been easier to assume m > 0. And then deduce the result for negative m via an SL2Z-equivariant isom between Mat m and Mat -m.

#### Johan Commelin (Sep 13 2018 at 17:05):

Anyway, the next step would be to use this horrible lemma to prove that for m ≠ 0 the set of orbits of SL2Z_M_ is finite.

#### Johan Commelin (Sep 13 2018 at 17:05):

Once we have that, we can define the Hecke operator.

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

@Kenny Lau Are you interested in golfing what we came up with?

#### Kenny Lau (Sep 13 2018 at 18:59):

after I finish with my PR

Which PR?

#### Kenny Lau (Sep 13 2018 at 19:03):

https://github.com/leanprover/mathlib/pull/345

Nice!

#### Patrick Massot (Sep 13 2018 at 20:40):

I made a small start on SL2Z\SL2ZM, simply telling Lean what this mean, and somehow stating what I think Johan told us we should prove in order to get finiteness

#### Patrick Massot (Sep 13 2018 at 20:41):

But what is stated may be false

#### Patrick Massot (Sep 13 2018 at 20:41):

and the names are stupid too

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

Thanks! That is exactly what I had in mind. (I do think we might need a bit more conditions in reps. I think we can/should just copy the condition from H0 in the induction lemma.

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

The set of orbits is only finite if m ≠ 0. Otherwise it is parameterised by pairs of coprime integers (up to ±1).

Done

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

Note that a small modification of the setup is required to recover the generation theorem for SL2. The relevant action is not the action of the full SL2 on Mat m, but only the monoid spanned by S and T. But otherwise the proof should be the same

Cool!

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

I guess for the finiteness result that is still sorried, we could do the dual thing. Build an injection into a product of fins.

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

are we going to restate the SL2Z theorem as a special case?

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

also, it doesn't compile because someone deleted mul_self_pos

It does compile

#### Patrick Massot (Sep 14 2018 at 08:19):

mul_self_pos is now in mathlib

#### Patrick Massot (Sep 14 2018 at 08:20):

Did you try to compile using leanpkg build? (hint: the correct answer is yes)

#### Patrick Massot (Sep 14 2018 at 08:20):

Yes, we could restate the SL2Z theorem as a special case. It should cost much and will be convenient

#### Patrick Massot (Sep 14 2018 at 08:21):

Feel free to do so, I need to do real work now

#### Kenny Lau (Sep 14 2018 at 08:22):

mul_self_pos is now in mathlib

well I haven't updated mathlib, that's why

#### Patrick Massot (Sep 14 2018 at 08:40):

leanpkg will do that for you

#### Patrick Massot (Sep 14 2018 at 08:40):

Use leanpkg build

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

And restart Lean in VScode afterwards...

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

@Patrick Massot you see... I might change your proof if you don't mind

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

I just pushed a first start on hecke operators...

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

@Kenny Lau Please assume m > 0

what do you mean

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

It will probably make your life easier. And I now realise that we won't ever use m < 0

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

Not in this project.

oh well

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

And outside the project, the can deduce the result by an SL2Z-equivariant map Mat m → Mat -m

right

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

Patrick Massot you see... I might change your proof if you don't mind

I have no idea what you are talking about

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

your whole induction_on proof

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

It's not my proof, I only contributed a handful of schoolkid lines

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

oh, @Johan Commelin then

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

@Kenny Lau Sure, go ahead!

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

@Johan Commelin this is the original base case:

(H0 : ∀ {A : Mat m} (h0 : A.c = 0) (h1 : A.a * A.d = m) (h2 : 0 ≤ A.a) (h3 : 0 ≤ A.b) (h4 : int.nat_abs A.b ≤ int.nat_abs A.d), C A)


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

it can be changed to:

(H0 : ∀ {A : Mat m} (h0 : A.c = 0) (h1 : A.a * A.d = m) (h2 : 0 < A.a) (h3 : 0 ≤ A.b) (h4 : int.nat_abs A.b < int.nat_abs A.d), C A)


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

1) h1 is redundant. It follows from h0 and A.det. (I realised this half-way writing my own proof.)
2) Now you have no upper-bound on A.b. So how will you prove finiteness of orbits?

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

what do you mean I have no upper-bound on A.b?

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

I changed two le to lt

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

it restricted things

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

Aah, sorry, I didn't see the h4.

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

Yes, I know you could make those restrictions, but I didn't know if it would make the proof easier.

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

I thought things would get harder.

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

I always do more work to ensure that the users do less work

Last updated: May 18 2021 at 09:14 UTC