begginer matrix question

Stream: new members

[Chris Birkbeck]

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

[Johan Commelin]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Chris Birkbeck]

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

[Johan Commelin]

I guess the following also works:

def my_matrix : SL2Z :=
_

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

[Johan Commelin]

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

[Johan Commelin]

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

[Chris Birkbeck]

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?).

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Then the ext tactic will help you further.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

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