# mathlibdocumentation

linear_algebra.general_linear_group

# The General Linear group $GL(n, R)$ #

This file defines the elements of the General Linear group general_linear_group n R, consisting of all invertible n by n R-matrices.

## Main definitions #

• matrix.general_linear_group is the type of matrices over R which are units in the matrix ring.
• matrix.GL_pos gives the subgroup of matrices with positive determinant (over a linear ordered ring).

## Tags #

matrix group, group, matrix inverse

@[reducible]
def matrix.general_linear_group (n : Type u) (R : Type v) [decidable_eq n] [fintype n] [comm_ring R] :
Type (max u v)

GL n R is the group of n by n R-matrices with unit determinant. Defined as a subtype of matrices

@[simp]
theorem matrix.general_linear_group.coe_inv_det_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : GL n R) :
def matrix.general_linear_group.det {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
GL n R →* Rˣ

The determinant of a unit matrix is itself a unit.

Equations
@[simp]
theorem matrix.general_linear_group.coe_det_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : GL n R) :
def matrix.general_linear_group.to_lin {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
GL n R ≃* (n → R)

The GL n R and general_linear_group R n groups are multiplicatively equivalent

Equations
def matrix.general_linear_group.mk' {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : n R) (h : invertible A.det) :
GL n R

Given a matrix with invertible determinant we get an element of GL n R

Equations
noncomputable def matrix.general_linear_group.mk'' {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : n R) (h : is_unit A.det) :
GL n R

Given a matrix with unit determinant we get an element of GL n R

Equations
def matrix.general_linear_group.mk_of_det_ne_zero {n : Type u} [decidable_eq n] [fintype n] {K : Type u_1} [field K] (A : n K) (h : A.det 0) :
GL n K

Given a matrix with non-zero determinant over a field, we get an element of GL n K

Equations
theorem matrix.general_linear_group.ext_iff {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : GL n R) :
A = B ∀ (i j : n), A i j = B i j
theorem matrix.general_linear_group.ext {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] ⦃A B : GL n R⦄ (h : ∀ (i j : n), A i j = B i j) :
A = B

Not marked @[ext] as the ext tactic already solves this.

@[simp]
theorem matrix.general_linear_group.coe_mul {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A B : GL n R) :
(A * B) = A.mul B
@[simp]
theorem matrix.general_linear_group.coe_one {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
1 = 1
theorem matrix.general_linear_group.coe_inv {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : GL n R) :
def matrix.general_linear_group.to_linear {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
GL n R ≃* (n → R)

An element of the matrix general linear group on (n) [fintype n] can be considered as an element of the endomorphism general linear group on n → R.

Equations
@[simp]
theorem matrix.general_linear_group.coe_to_linear {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : GL n R) :
@[simp]
theorem matrix.general_linear_group.to_linear_apply {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : GL n R) (v : n → R) :
@[protected, instance]
Equations
@[simp]
theorem matrix.special_linear_group.coe_to_GL_det {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (g : R) :
def matrix.GL_pos (n : Type u) (R : Type v) [decidable_eq n] [fintype n]  :
subgroup (GL n R)

This is the subgroup of nxn matrices with entries over a linear ordered ring and positive determinant.

Equations
Instances for ↥matrix.GL_pos
@[simp]
theorem matrix.mem_GL_pos {n : Type u} {R : Type v} [decidable_eq n] [fintype n] (A : GL n R) :
A
@[protected, instance]
def matrix.GL_pos.has_neg {n : Type u} {R : Type v} [decidable_eq n] [fintype n] [fact (even (fintype.card n))] :

Formal operation of negation on general linear group on even cardinality n given by negating each element.

Equations
@[simp]
theorem matrix.GL_pos.coe_neg_GL {n : Type u} {R : Type v} [decidable_eq n] [fintype n] [fact (even (fintype.card n))] (g : R)) :
@[simp]
theorem matrix.GL_pos.coe_neg {n : Type u} {R : Type v} [decidable_eq n] [fintype n] [fact (even (fintype.card n))] (g : R)) :
@[simp]
theorem matrix.GL_pos.coe_neg_apply {n : Type u} {R : Type v} [decidable_eq n] [fintype n] [fact (even (fintype.card n))] (g : R)) (i j : n) :
(-g) i j = -g i j
@[protected, instance]
def matrix.GL_pos.has_distrib_neg {n : Type u} {R : Type v} [decidable_eq n] [fintype n] [fact (even (fintype.card n))] :
Equations
• matrix.GL_pos.has_distrib_neg = matrix.GL_pos.has_distrib_neg._proof_1 matrix.GL_pos.has_distrib_neg._proof_2 matrix.GL_pos.has_distrib_neg._proof_3
def matrix.special_linear_group.to_GL_pos {n : Type u} [decidable_eq n] [fintype n] {R : Type v}  :

special_linear_group n R embeds into GL_pos n R

Equations
@[protected, instance]
def matrix.special_linear_group.matrix.GL_pos.has_coe {n : Type u} [decidable_eq n] [fintype n] {R : Type v}  :
R)
Equations
theorem matrix.special_linear_group.coe_eq_to_GL_pos {n : Type u} [decidable_eq n] [fintype n] {R : Type v}  :
theorem matrix.special_linear_group.to_GL_pos_injective {n : Type u} [decidable_eq n] [fintype n] {R : Type v}  :
@[simp]
theorem matrix.special_linear_group.coe_GL_pos_coe_GL_coe_matrix {n : Type u} [decidable_eq n] [fintype n] {R : Type v} (g : R) :

Coercing a special_linear_group via GL_pos and GL is the same as coercing striaght to a matrix.

@[simp]
theorem matrix.special_linear_group.coe_to_GL_pos_to_GL_det {n : Type u} [decidable_eq n] [fintype n] {R : Type v} (g : R) :
@[norm_cast]
theorem matrix.special_linear_group.coe_GL_pos_neg {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [fact (even (fintype.card n))] (g : R) :
@[simp]
theorem matrix.coe_plane_conformal_matrix {R : Type u_1} [field R] (a b : R) (hab : a ^ 2 + b ^ 2 0) :
hab) = matrix.of ![![a, -b], ![b, a]]
def matrix.plane_conformal_matrix {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
@[protected, instance]
def matrix.general_linear_group.has_coe_to_fun {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] :
has_coe_to_fun (GL n R) (λ (_x : GL n R), n → n → R)

This instance is here for convenience, but is not the simp-normal form.

Equations
@[simp]
theorem matrix.general_linear_group.coe_fn_eq_coe {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R] (A : GL n R) :