transvection matrix is instance of GL(n, R)

Stream: new members

[Alex Brodbelt]

Hi!

I want to register the transvection as an element of the general linear group for later use.

Am I meant to to do this by creating an instance or by a theorem (like the one I tried to state below which does not compile)?

I want to use GeneralLinearGroup.mk' alongside with det_transvection_of_nebut I don't know how to set up the statement.

Thanks in advance (:

import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
import Mathlib.LinearAlgebra.Matrix.Transvection

open Matrix

variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

theorem tranvsvection_in_general_linear_group {i j : n} (i_neq_j : i ≠ j) : (((transvection i j (1 : R)) : Matrix n n R) : GL n R) = transvection i j (1 : R) := by sorry

[Etienne Marion]

There are different ways, I guess the easiest is this one:

import Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Basic
import Mathlib.LinearAlgebra.Matrix.Transvection

open Matrix

variable (n : Type u) [DecidableEq n] [Fintype n] (R : Type v) [CommRing R]

def transvection' {i j : n} (i_neq_j : i ≠ j) : GL n R :=
  GeneralLinearGroup.mk' (transvection i j (1 : R))
    ((det_transvection_of_ne i j i_neq_j (1 : R)).symm ▸ invertibleOne)

[Etienne Marion]

This is maybe clearer for last line:

(by rw [det_transvection_of_ne _ _ i_neq_j]; exact invertibleOne)

[Alex Brodbelt]

How do you choose between defining a coercion or when making a definition like the one above?

[Eric Wieser]

Usually you always make the definition, and if it's super convenient you register that definition as a coercion

[Alex Brodbelt]

Eric Wieser said:

Usually you always make the definition, and if it's super convenient you register that definition as a coercion

aha I see - thank you both of you

[Eric Wieser]

Would docs#Matrix.SpecialLinearGroup be more appropriate here?

[Alex Brodbelt]

Eric Wieser said:

Would docs#Matrix.SpecialLinearGroup be more appropriate here?

I want to prove properties about the general linear group - hm but I suppose I should register this for the special linear group and then use the coercion...