Zulip Chat Archive

Stream: new members

Topic: begginer matrix question


view this post on Zulip Chris Birkbeck (Apr 06 2021 at 09:56):

Hello, I'm new here and have been playing around with matrices in Lean. First of all, sorry if this is not the correct stream to ask this in.

My problems are essentially with matrix coercion. I’ve seen that we there is the following notation for matrices and I would like to know how to use it for special_linear_group. Specifically, how do I take

import linear_algebra.matrix
import data.matrix.notation
        def N : matrix  (fin 2) (fin 2 ) := ![![-1, 0], ![0, -1]]

and turn it into an element of

import linear_algebra.special_linear_group
        def SL2Z := special_linear_group (fin 2) 

I assume this wont be automatic as one has prove N has determinant 1, but I dont know how to get lean to take a 2x2 matrix of determinant 1 and think of it as an element of SL2Z.

Thank you

view this post on Zulip Johan Commelin (Apr 06 2021 at 10:00):

@Chris Birkbeck Welcome! This stream is fine (-;

view this post on Zulip Johan Commelin (Apr 06 2021 at 10:00):

You can turn a matrix into an element of SL2Z using \< _, _ \>. If you type that into VScode, the \< and \> will turn into funny unicode brackets.

view this post on Zulip Johan Commelin (Apr 06 2021 at 10:01):

The end result will be \<your_matrix, proof_that_det_eq_1\>

view this post on Zulip Chris Birkbeck (Apr 06 2021 at 10:10):

Ah that's what I needed. Thank you very much!

view this post on Zulip Johan Commelin (Apr 06 2021 at 10:13):

I guess the following also works:

def my_matrix : SL2Z :=
_

Now put your cursor on the _, and wait till a little :bulb: appears.

view this post on Zulip Johan Commelin (Apr 06 2021 at 10:13):

Then you can click it, or type Ctrl-..

view this post on Zulip Johan Commelin (Apr 06 2021 at 10:14):

Now choose generate skeleton (almost at the bottom of hte menu)

view this post on Zulip Chris Birkbeck (Apr 06 2021 at 13:25):

Thats really useful, thank you. Now, say I wanted to use this notation. I was trying to prove that N^2 is 1. I end up with something that looks like

⟨N, proof⟩ * ⟨N, proof⟩ = 1

Now, I can't seem to figure out how to simplify this. I guess I'm confused how one splits this into working with the matrices and proofs separetely (but maybe one doesnt want to do this and there is something better?).

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:26):

@Chris Birkbeck So now there is hopefully an ext-lemma for SL2Z that says that for proving equalities it suffices to check equality of the matrices.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:26):

If it doesn't exist apply subtype.coe_injective hopefully works. (I'm just guessing.)

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:28):

@Chris Birkbeck You might want to just work with special_linear_group, instead of making your SL2Z definition on top of it.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:29):

Then the ext tactic will help you further.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:29):

It will apply this lemma: https://leanprover-community.github.io/mathlib_docs/linear_algebra/special_linear_group.html#matrix.special_linear_group.ext

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:29):

Which says that if all coefficients are equal, then you are done.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:30):

After ext, you do intros i j, and then fin_cases i; fin_cases j should give you 4 goals, one for each coefficient.

view this post on Zulip Johan Commelin (Apr 06 2021 at 13:30):

With a bit of luck, each of them can be closed with simp.


Last updated: May 16 2021 at 21:11 UTC