Basic lemmas about the general linear group $GL(n, R)$

This file lists various basic lemmas about the general linear group $GL(n, R)$. For the definitions, see LinearAlgebra/Matrix/GeneralLinearGroup/Defs.lean.

def Matrix.planeConformalMatrix {R : Type u_1} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) : GL (Fin 2) R

The matrix [a, -b; b, a] (inspired by multiplication by a complex number); it is an element of $GL_2(R)$ if a ^ 2 + b ^ 2 is nonzero.

Equations

• Matrix.planeConformalMatrix a b hab = Matrix.GeneralLinearGroup.mkOfDetNeZero !![a, -b; b, a] ⋯

@[simp]

theorem Matrix.val_planeConformalMatrix {R : Type u_1} [Field R] (a b : R) (hab : a ^ 2 + b ^ 2 ≠ 0) : ↑(planeConformalMatrix a b hab) = !![a, -b; b, a]

theorem Matrix.GeneralLinearGroup.mem_center_iff_val_eq_scalar {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {g : GL n R} : g ∈ Subgroup.center (GL n R) ↔ ↑g ∈ Set.range ⇑(scalar n)

The center of GL n R consists of scalar matrices.

theorem Matrix.GeneralLinearGroup.center_eq_range_units {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : Subgroup.center (GL n R) = (Units.map ↑(algebraMap R (Matrix n n R))).range

The center of GL n R is the image of Rˣ.