generators

Stream: kbb

[Patrick Massot]

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

[Patrick Massot]

But I wonder how to properly generalize it.

[Kenny Lau]

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

thanks!

[Patrick Massot]

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]

Is this counter-intuitive order related to constructivity?

[Kenny Lau]

not constructivity

[Kenny Lau]

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

[Patrick Massot]

?

[Kenny Lau]

it's easier to use

[Patrick Massot]

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

[Kenny Lau]

I don't know about tactics

[Patrick Massot]

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]

@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]

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]

everything is letters

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

there is an SL2Z attribute?

[Patrick Massot]

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

[Mario Carneiro]

seems like a fine induction statement

[Patrick Massot]

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

[Mario Carneiro]

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]

I guess it's usually called closure in groups?

[Patrick Massot]

I did spans for group a very long time ago

[Mario Carneiro]

in mathlib?

[Patrick Massot]

no

[Mario Carneiro]

I think I recall

[Chris Hughes]

I think closure is in mathlib

[Patrick Massot]

It's the first thing I did

[Mario Carneiro]

you were doing something with norms in groups

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

given what is currently available, this theorem is fine

[Patrick Massot]

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

[Mario Carneiro]

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

[Kenny Lau]

guys, it's just closure

[Mario Carneiro]

?

[Chris Hughes]

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]

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]

the proofs will be the same

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Mario Carneiro]

ah, so it does

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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]

there is no mention of inverses in the induction theorem

[Mario Carneiro]

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

[Mario Carneiro]

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

[Patrick Massot]

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

[Patrick Massot]

Would that be a tactic?

[Mario Carneiro]

no, a theorem

[Mario Carneiro]

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

[Mario Carneiro]

and its eliminator is basically exactly that theorem

[Mario Carneiro]

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

[Patrick Massot]

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

[Mario Carneiro]

the general theorem is the eliminator for in_closure

[Mario Carneiro]

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]

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

[Patrick Massot]

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]

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

[Mario Carneiro]

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)

[Patrick Massot]

Ok, thanks

[Patrick Massot]

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]

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]

which looks like it could admit a general version

[Patrick Massot]

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

[Patrick Massot]

Thanks again!

[Johan Commelin]

@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]

In particular, the set of orbits is finite.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I think that would be a really cool move.

[Johan Commelin]

@Kenny Lau What do you think of this?

[Kenny Lau]

great!

[Johan Commelin]

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

[Kenny Lau]

maybe 30% hard!

[Kenny Lau]

can't wait to see someone implement it!

[Johan Commelin]

Lol

[Johan Commelin]

Do we have notation for group actions?

[Kenny Lau]

I used \ci a long time ago

[Johan Commelin]

But it is not in mathlib?

[Kenny Lau]

it isn't

[Johan Commelin]

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

[Johan Commelin]

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

[Kenny Lau]

sure

[Johan Commelin]

@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]

what if m is negative?

[Kenny Lau]

or 0?

[Johan Commelin]

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

[Johan Commelin]

Let me think it through...

[Johan Commelin]

For m = 0 the statement might be false.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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]

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

[Patrick Massot]

Did you try convert H ?

[Kenny Lau]

cases B; exact H

[Patrick Massot]

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]

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

[Kenny Lau]

I disagree

[Kenny Lau]

congr can go uncontrollable

[Kenny Lau]

(convert is just a kind of congr)

[Patrick Massot]

I'm not saying this will always work

[Kenny Lau]

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

[Kenny Lau]

for lack of a better word

[Johan Commelin]

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]

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

[Johan Commelin]

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

[Patrick Massot]

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]

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

[Johan Commelin]

No, I just cooked up a proof this morning.

[Johan Commelin]

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

[Patrick Massot]

Do you need help here?

[Johan Commelin]

I'm learning :lol:

[Johan Commelin]

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

[Johan Commelin]

I still need to learn how to juggle around hypotheses.

[Johan Commelin]

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]

@Kenny Lau Do you want to teach me?

[Patrick Massot]

where did you push?

[Kenny Lau]

well S*S*A = -A

[Kenny Lau]

so you prove it for S*S*A first

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

That is because of the strong_induction

[Johan Commelin]

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]

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

[Patrick Massot]

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

[Johan Commelin]

Never mind. I might have found a way out.

[Johan Commelin]

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]

@Kenny Lau Would you want to take over?

[Kenny Lau]

I’m not free now

[Johan Commelin]

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

[Johan Commelin]

they should all be by schoolkid.

[Patrick Massot]

Let's say I try the first one

[Johan Commelin]

Ooh, I was just trying that one.

[Patrick Massot]

I'm almost there!

[Johan Commelin]

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

[Johan Commelin]

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

[Patrick Massot]

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

[Johan Commelin]

Right, same place (-;

[Johan Commelin]

I'll move to sorry₂

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

Done!

[Patrick Massot]

Should I move to the third one?

[Johan Commelin]

Yes please.

[Johan Commelin]

Did you push?

[Patrick Massot]

Do you want me to push?

[Patrick Massot]

I pushed

[Johan Commelin]

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

[Patrick Massot]

What is this /? Euclidean quotient?

[Patrick Massot]

seems so

[Johan Commelin]

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

[Rob Lewis]

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

[Patrick Massot]

bingo!

[Patrick Massot]

@Johan Commelin Are you sure this sorry is true?

[Patrick Massot]

It actually looks really weird

[Johan Commelin]

I'm done with 2

[Johan Commelin]

You're worried about 3?

[Patrick Massot]

yes

[Johan Commelin]

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

[Johan Commelin]

By the way, I pushed my fix of sorry₂

[Patrick Massot]

hold on

[Patrick Massot]

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

[Johan Commelin]

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

[Patrick Massot]

And now you set me a deadline!

[Johan Commelin]

And I haven't made any progress on sorry₃

[Johan Commelin]

@Kenny Lau is online :time_ticking:

[Kenny Lau]

hi

[Patrick Massot]

done

[Patrick Massot]

so much suffering...

[Johan Commelin]

@Patrick Massot Thank you so much!

[Patrick Massot]

The stupid lemma in the middle is now in mathlib

[Patrick Massot]

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

[Johan Commelin]

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]

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]

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

[Johan Commelin]

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

[Kenny Lau]

after I finish with my PR

[Patrick Massot]

Which PR?

[Kenny Lau]

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

[Patrick Massot]

Nice!

[Patrick Massot]

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]

But what is stated may be false

[Patrick Massot]

and the names are stupid too

[Johan Commelin]

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]

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

[Patrick Massot]

Done

[Patrick Massot]

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

[Johan Commelin]

Cool!

[Johan Commelin]

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]

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

[Kenny Lau]

also, it doesn't compile because someone deleted mul_self_pos

[Patrick Massot]

It does compile

[Patrick Massot]

mul_self_pos is now in mathlib

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kenny Lau]

mul_self_pos is now in mathlib

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

[Patrick Massot]

leanpkg will do that for you

[Patrick Massot]

Use leanpkg build

[Johan Commelin]

And restart Lean in VScode afterwards...

[Kenny Lau]

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

[Johan Commelin]

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

[Johan Commelin]

@Kenny Lau Please assume m > 0

[Kenny Lau]

what do you mean

[Johan Commelin]

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

[Johan Commelin]

Not in this project.

[Kenny Lau]

oh well

[Johan Commelin]

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

[Kenny Lau]

right

[Patrick Massot]

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]

your whole induction_on proof

[Patrick Massot]

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

[Kenny Lau]

oh, @Johan Commelin then

[Johan Commelin]

@Kenny Lau Sure, go ahead!

[Kenny Lau]

@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]

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]

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]

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

[Kenny Lau]

I changed two le to lt

[Kenny Lau]

it restricted things

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

I thought things would get harder.

[Kenny Lau]

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