The General Linear group $GL(n, R)$ #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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_groupis the type of matrices over R which are units in the matrix ring.matrix.GL_posgives 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
def
matrix.general_linear_group.det
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
The determinant of a unit matrix is itself a unit.
@[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 ≃* linear_map.general_linear_group R (n → R)
The GL n R and general_linear_group R n groups are multiplicatively equivalent
def
matrix.general_linear_group.mk'
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R]
(A : matrix n 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 : matrix n 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 : matrix n 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
@[simp]
theorem
matrix.general_linear_group.coe_one
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring 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 ≃* linear_map.general_linear_group 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.
@[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) :
⇑(⇑matrix.general_linear_group.to_linear A) v = ⇑(↑A.mul_vec_lin) v
@[protected, instance]
def
matrix.special_linear_group.has_coe_to_general_linear_group
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[comm_ring R] :
has_coe (matrix.special_linear_group n R) (GL n R)
@[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 : matrix.special_linear_group n R) :
def
matrix.GL_pos
(n : Type u)
(R : Type v)
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring 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]
[linear_ordered_comm_ring R]
(A : GL n R) :
A ∈ matrix.GL_pos n R ↔ 0 < ↑(⇑matrix.general_linear_group.det A)
theorem
matrix.GL_pos.det_ne_zero
{n : Type u}
{R : Type v}
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring R]
(A : ↥(matrix.GL_pos n R)) :
@[protected, instance]
def
matrix.GL_pos.has_neg
{n : Type u}
{R : Type v}
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring R]
[fact (even (fintype.card n))] :
has_neg ↥(matrix.GL_pos n R)
Formal operation of negation on general linear group on even cardinality n given by negating
each element.
Equations
- matrix.GL_pos.has_neg = {neg := λ (g : ↥(matrix.GL_pos n R)), ⟨-↑g, _⟩}
@[simp]
theorem
matrix.GL_pos.coe_neg_GL
{n : Type u}
{R : Type v}
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring R]
[fact (even (fintype.card n))]
(g : ↥(matrix.GL_pos n R)) :
@[simp]
theorem
matrix.GL_pos.coe_neg
{n : Type u}
{R : Type v}
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring R]
[fact (even (fintype.card n))]
(g : ↥(matrix.GL_pos n R)) :
@[simp]
theorem
matrix.GL_pos.coe_neg_apply
{n : Type u}
{R : Type v}
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring R]
[fact (even (fintype.card n))]
(g : ↥(matrix.GL_pos n R))
(i j : n) :
@[protected, instance]
def
matrix.GL_pos.has_distrib_neg
{n : Type u}
{R : Type v}
[decidable_eq n]
[fintype n]
[linear_ordered_comm_ring R]
[fact (even (fintype.card n))] :
Equations
- matrix.GL_pos.has_distrib_neg = function.injective.has_distrib_neg coe 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}
[linear_ordered_comm_ring R] :
matrix.special_linear_group n R →* ↥(matrix.GL_pos n R)
special_linear_group n R embeds into GL_pos n R
Equations
- matrix.special_linear_group.to_GL_pos = {to_fun := λ (A : matrix.special_linear_group n R), ⟨↑A, _⟩, map_one' := _, map_mul' := _}
@[protected, instance]
def
matrix.special_linear_group.matrix.GL_pos.has_coe
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[linear_ordered_comm_ring R] :
has_coe (matrix.special_linear_group n R) ↥(matrix.GL_pos n R)
theorem
matrix.special_linear_group.coe_eq_to_GL_pos
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[linear_ordered_comm_ring R] :
theorem
matrix.special_linear_group.to_GL_pos_injective
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[linear_ordered_comm_ring R] :
@[simp]
theorem
matrix.special_linear_group.coe_GL_pos_coe_GL_coe_matrix
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[linear_ordered_comm_ring R]
(g : matrix.special_linear_group n 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}
[linear_ordered_comm_ring R]
(g : matrix.special_linear_group n R) :
@[norm_cast]
theorem
matrix.special_linear_group.coe_GL_pos_neg
{n : Type u}
[decidable_eq n]
[fintype n]
{R : Type v}
[linear_ordered_comm_ring R]
[fact (even (fintype.card n))]
(g : matrix.special_linear_group n 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.plane_conformal_matrix a b hab = matrix.general_linear_group.mk_of_det_ne_zero (⇑matrix.of ![![a, -b], ![b, a]]) _
@[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.