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 Mathlib/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_mem_range_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 ⇑(Matrix.scalar n)

The center of GL n R consists of scalar matrices.

theorem Matrix.GeneralLinearGroup.center_eq_range_scalar {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] : Subgroup.center (GL n R) = (scalar n).range

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

theorem Matrix.GeneralLinearGroup.map_center_le {R : Type u_1} {n : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] {S : Type u_3} [CommRing S] (f : R →+* S) : Subgroup.center (GL n R) ≤ Subgroup.comap (map f) (Subgroup.center (GL n S))

theorem Matrix.SpecialLinearGroup.toGL_mem_center_iff {n : Type u_1} {R : Type u_2} [Fintype n] [DecidableEq n] [CommRing R] (g : SpecialLinearGroup n R) : toGL g ∈ Subgroup.center (GL n R) ↔ g ∈ Subgroup.center (SpecialLinearGroup n R)