Zulip Chat Archive

Stream: kbb

Topic: generators


view this post on Zulip Patrick Massot (Sep 12 2018 at 19:20):

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:21):

But I wonder how to properly generalize it.

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:21):

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

thanks!

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:22):

Is this counter-intuitive order related to constructivity?

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:23):

not constructivity

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:25):

?

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:26):

it's easier to use

view this post on Zulip 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?

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:36):

I don't know about tactics

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:50):

everything is letters

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:51):

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:51):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:51):

there is an SL2Z attribute?

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:52):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:52):

seems like a fine induction statement

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:54):

I guess it's usually called closure in groups?

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:54):

I did spans for group a very long time ago

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:54):

in mathlib?

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:54):

no

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:54):

I think I recall

view this post on Zulip Chris Hughes (Sep 12 2018 at 19:54):

I think closure is in mathlib

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:54):

It's the first thing I did

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:54):

you were doing something with norms in groups

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:55):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:55):

given what is currently available, this theorem is fine

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:56):

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

view this post on Zulip 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

view this post on Zulip Kenny Lau (Sep 12 2018 at 19:56):

guys, it's just closure

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:57):

?

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:57):

the proofs will be the same

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:58):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:59):

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 19:59):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 19:59):

ah, so it does

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:00):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:00):

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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:01):

there is no mention of inverses in the induction theorem

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:01):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:01):

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:02):

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

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:02):

Would that be a tactic?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:02):

no, a theorem

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:03):

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

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:03):

and its eliminator is basically exactly that theorem

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Sep 12 2018 at 20:04):

the general theorem is the eliminator for in_closure

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:27):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:52):

Ok, thanks

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:53):

which looks like it could admit a general version

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 12 2018 at 20:54):

Thanks again!

view this post on Zulip 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 (ab0d)\begin{pmatrix} a & b \\ 0 & d \end{pmatrix}, where ad=m,a>0,d>0a \cdot d = m,\quad a > 0,\quad d > 0, and 0b<d0 \le b < d.

view this post on Zulip Johan Commelin (Sep 13 2018 at 03:57):

In particular, the set of orbits is finite.

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Johan Commelin (Sep 13 2018 at 03:59):

I think that would be a really cool move.

view this post on Zulip Johan Commelin (Sep 13 2018 at 06:31):

@Kenny Lau What do you think of this?

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:32):

great!

view this post on Zulip Johan Commelin (Sep 13 2018 at 06:32):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:34):

maybe 30% hard!

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:34):

can't wait to see someone implement it!

view this post on Zulip Johan Commelin (Sep 13 2018 at 06:34):

Lol

view this post on Zulip Johan Commelin (Sep 13 2018 at 06:37):

Do we have notation for group actions?

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:41):

I used \ci a long time ago

view this post on Zulip Johan Commelin (Sep 13 2018 at 06:43):

But it is not in mathlib?

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:45):

it isn't

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 13 2018 at 06:46):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:53):

sure

view this post on Zulip 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 :=

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:59):

what if m is negative?

view this post on Zulip Kenny Lau (Sep 13 2018 at 06:59):

or 0?

view this post on Zulip Johan Commelin (Sep 13 2018 at 07:00):

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 07:00):

Let me think it through...

view this post on Zulip Johan Commelin (Sep 13 2018 at 07:02):

For m = 0 the statement might be false.

view this post on Zulip 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?

view this post on Zulip Johan Commelin (Sep 13 2018 at 07:04):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 13 2018 at 07:20):

Did you try convert H ?

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:21):

cases B; exact H

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 13 2018 at 07:44):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:44):

I disagree

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:44):

congr can go uncontrollable

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:45):

(convert is just a kind of congr)

view this post on Zulip Patrick Massot (Sep 13 2018 at 07:45):

I'm not saying this will always work

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:45):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 07:46):

for lack of a better word

view this post on Zulip 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),

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:06):

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

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

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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:16):

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:28):

No, I just cooked up a proof this morning.

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:28):

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

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:30):

Do you need help here?

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:39):

I'm learning :lol:

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:51):

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:51):

I still need to learn how to juggle around hypotheses.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:53):

@Kenny Lau Do you want to teach me?

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:53):

where did you push?

view this post on Zulip Kenny Lau (Sep 13 2018 at 08:53):

well S*S*A = -A

view this post on Zulip Kenny Lau (Sep 13 2018 at 08:53):

so you prove it for S*S*A first

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:53):

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

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:55):

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 08:58):

That is because of the strong_induction

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Sep 13 2018 at 08:59):

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

view this post on Zulip Patrick Massot (Sep 13 2018 at 09:00):

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 09:04):

Never mind. I might have found a way out.

view this post on Zulip 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.)

view this post on Zulip Johan Commelin (Sep 13 2018 at 11:03):

@Kenny Lau Would you want to take over?

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

I’m not free now

view this post on Zulip 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,

view this post on Zulip Johan Commelin (Sep 13 2018 at 12:04):

they should all be by schoolkid.

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

Let's say I try the first one

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

Ooh, I was just trying that one.

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

I'm almost there!

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

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

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

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

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

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:15):

Right, same place (-;

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:15):

I'll move to sorry₂

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

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

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

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

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

Done!

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

Should I move to the third one?

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:27):

Yes please.

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:27):

Did you push?

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

Do you want me to push?

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

I pushed

view this post on Zulip 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...

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

What is this /? Euclidean quotient?

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

seems so

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:34):

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

view this post on Zulip Rob Lewis (Sep 13 2018 at 14:36):

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

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

bingo!

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

@Johan Commelin Are you sure this sorry is true?

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

It actually looks really weird

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:46):

I'm done with 2

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:46):

You're worried about 3?

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

yes

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:51):

By the way, I pushed my fix of sorry₂

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

hold on

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

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

view this post on Zulip 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.

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

And now you set me a deadline!

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:59):

And I haven't made any progress on sorry₃

view this post on Zulip Johan Commelin (Sep 13 2018 at 14:59):

@Kenny Lau is online :time_ticking:

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

hi

view this post on Zulip Patrick Massot (Sep 13 2018 at 15:39):

done

view this post on Zulip Patrick Massot (Sep 13 2018 at 15:39):

so much suffering...

view this post on Zulip Johan Commelin (Sep 13 2018 at 16:52):

@Patrick Massot Thank you so much!

view this post on Zulip Patrick Massot (Sep 13 2018 at 16:59):

The stupid lemma in the middle is now in mathlib

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Sep 13 2018 at 17:05):

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

view this post on Zulip Johan Commelin (Sep 13 2018 at 18:59):

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

view this post on Zulip Kenny Lau (Sep 13 2018 at 18:59):

after I finish with my PR

view this post on Zulip Patrick Massot (Sep 13 2018 at 19:01):

Which PR?

view this post on Zulip Kenny Lau (Sep 13 2018 at 19:03):

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

view this post on Zulip Patrick Massot (Sep 13 2018 at 19:10):

Nice!

view this post on Zulip 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

view this post on Zulip Patrick Massot (Sep 13 2018 at 20:41):

But what is stated may be false

view this post on Zulip Patrick Massot (Sep 13 2018 at 20:41):

and the names are stupid too

view this post on Zulip 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.

view this post on Zulip 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).

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

Done

view this post on Zulip 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

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

Cool!

view this post on Zulip 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.

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

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

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

also, it doesn't compile because someone deleted mul_self_pos

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

It does compile

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

mul_self_pos is now in mathlib

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

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

view this post on Zulip 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

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

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

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

mul_self_pos is now in mathlib

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

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

leanpkg will do that for you

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

Use leanpkg build

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

And restart Lean in VScode afterwards...

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

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

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

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

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

@Kenny Lau Please assume m > 0

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

what do you mean

view this post on Zulip 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

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

Not in this project.

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

oh well

view this post on Zulip 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

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

right

view this post on Zulip 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

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

your whole induction_on proof

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

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

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

oh, @Johan Commelin then

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

@Kenny Lau Sure, go ahead!

view this post on Zulip 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)

view this post on Zulip 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)

view this post on Zulip 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?

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

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

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

I changed two le to lt

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

it restricted things

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

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

view this post on Zulip 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.

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

I thought things would get harder.

view this post on Zulip 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