general_linear_group

/-

The Genera Linear group $GL(n, R)$
-/
import linear_algebra.matrix
import linear_algebra.matrix.nonsingular_inverse
import linear_algebra.special_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 `n` by `n` `R`-matrices with unit determinant.


## Main definitions

 * `matrix.GL` is the type of matrices over R with unit determinant
 * `matrix.GL.group` gives the group structure (under multiplication)


## Implementation notes


## References


## Tags

matrix group, group, matrix inverse
-/

namespace matrix
universes u v
open_locale matrix
open linear_map


section

variables (n : Type u) [decidable_eq n] [fintype n] (R : Type v) [comm_ring R]

/-- `GL n R` is the group of `n` by `n` `R`-matrices with unit determinant.
-/
def GL := { A : matrix n n R // is_unit (A.det) }

end

namespace GL



variables {n : Type u} [decidable_eq n] [fintype n] {R : Type v} [comm_ring R]

instance coe_matrix : has_coe (GL n R) (matrix n n R) :=
⟨λ A, A.val⟩

instance coe_fun : has_coe_to_fun (GL n R) :=
{ F   := λ _, n → n → R,
  coe := λ A, A.val }


def to_lin' (A : GL n R) := matrix.to_lin' A

lemma ext_iff (A B : GL n R) : A = B ↔ (∀ i j, A i j = B i j) :=
iff.trans subtype.ext_iff_val ⟨(λ h i j, congr_fun (congr_fun h i) j), matrix.ext⟩

@[ext] lemma ext (A B : GL n R) : (∀ i j, A i j = B i j) → A = B :=
(GL.ext_iff A B).mpr




/-- Inverse of a matrix in `GL n R`-/
noncomputable def nonsing_inve (A : GL n R) := matrix.nonsing_inv A


lemma nonsing_inve_det (A: GL n R): (det (nonsing_inve A))* (det A.1)=1:=
begin
have h1:= nonsing_inv_det A.1 A.2, convert h1,
end



lemma inv_in_gl (A : GL n R): is_unit (det (nonsing_inve A)):=

begin
 have h1:=nonsing_inve_det A, rw is_unit_iff_exists_inv, use A.val.det, exact h1,
end


instance has_mul : has_mul (GL n R) :=
⟨λ A B, ⟨A.1 ⬝ B.1, by {erw [det_mul], apply is_unit.mul A.2 B.2}⟩⟩

instance has_one : has_one (GL n R) :=
⟨⟨1, by {simp only [det_one, is_unit_one]}⟩⟩



noncomputable instance has_inv : has_inv (GL n R) :=
⟨λ A, ⟨nonsing_inve A, inv_in_gl A⟩ ⟩



instance : inhabited (GL n R) := ⟨1⟩

section coe_lemmas

variables (A B : GL n R)

@[simp] lemma inv_val : ↑(A⁻¹) = nonsing_inve A := rfl

@[simp] lemma inv_apply : ⇑(A⁻¹) = nonsing_inve A := rfl


@[simp] lemma mul_val : ↑(A * B) = A ⬝ B := rfl

@[simp] lemma mul_apply : ⇑(A * B) = (A ⬝ B) := rfl


@[simp] lemma one_val : ↑(1 : GL n R) = (1 : matrix n n R) := rfl

@[simp] lemma one_apply : ⇑(1 : GL n R) = (1 : matrix n n R) := rfl



@[simp] lemma to_lin'_mul :
  to_lin' (A * B) = (to_lin' A).comp (to_lin' B) :=
matrix.to_lin'_mul A B

@[simp] lemma to_lin'_one :
  to_lin' (1 : GL n R) = linear_map.id :=
matrix.to_lin'_one

end coe_lemmas


lemma is_left_inv (A : GL n R): A⁻¹ *  A = 1:=

begin
have h1: is_unit (det A), by {have:=A.2, exact this,},
have:=nonsing_inv_mul A A.2, ext, dsimp, rw nonsing_inve, rw nonsing_inv, simp only [dif_pos, h1], rw nonsing_inv_apply at this, rw this,
end



lemma inv_is_inv (A : GL n R) : A.nonsing_inve= (↑A)⁻¹:=

begin
have h1: is_unit (det A), by {have:=A.2, exact this,},
have:=is_left_inv A, have:=nonsing_inv_mul A.1 h1, simp at this, have:=nonsing_inv_apply A h1,
ext, dsimp, rw nonsing_inve, rw nonsing_inv, refl,
end





noncomputable instance group : group (GL n R) :=
{ mul_assoc := λ A B C, by { ext, simp [matrix.mul_assoc] },
  one_mul := λ A, by { ext, simp },
  mul_one := λ A, by { ext, simp },
  mul_left_inv := λ A, by {apply  is_left_inv A },
  ..GL.has_mul,
  ..GL.has_one,
  ..GL.has_inv }


/-- `to_linear_equiv A` is matrix multiplication of vectors by `A`, as a linear equivalence. -/
noncomputable def to_linear_equiv (A : GL n R) : (n → R) ≃ₗ[R] (n → R) :=
{ inv_fun := A⁻¹.to_lin',
  left_inv := λ x, calc
    A⁻¹.to_lin'.comp A.to_lin' x
        = (A⁻¹ * A).to_lin' x : by rw [←to_lin'_mul]
    ... = x : by rw [mul_left_inv, to_lin'_one, id_apply],
  right_inv := λ x, calc
    A.to_lin'.comp A⁻¹.to_lin' x
        = (A * A⁻¹).to_lin' x : by rw [←to_lin'_mul]
    ... = x : by rw [mul_right_inv, to_lin'_one, id_apply],
  ..matrix.to_lin' A }


noncomputable def to_general_linear_group (A : GL n R) : general_linear_group R (n → R) :=
general_linear_group.of_linear_equiv (to_linear_equiv A)

lemma coe_to_general_linear_group (A : GL n R) :
  (@coe (units _) _ _ (to_general_linear_group A)) = A.to_lin' :=
rfl

variables (K : Type v)  [field K ] [nontrivial K]



lemma det_eq_val_det (A: GL n R ) : det A = A.1.det:=
begin
simp only [subtype.val_eq_coe], refl,
end


lemma det_inv' (A: GL n K) : A.1.det * (A.1.det)⁻¹=1:=

begin
simp only [subtype.val_eq_coe],
have h1: A.1.det ≠ 0, {have:=A.2, simp only [subtype.val_eq_coe] at this, rw is_unit_iff_exists_inv at this, simp, by_contra,
 rw h at this, simp only [zero_mul, exists_false, zero_ne_one] at this, exact this },
simp only [ne.def, subtype.val_eq_coe] at h1, apply mul_inv_cancel h1,
end


lemma det_inv'' (A B : GL n K ) (h: det A * det B =1) : det A= (det B)⁻¹ :=

begin
simp only [det_eq_val_det, subtype.val_eq_coe],simp only [det_eq_val_det, subtype.val_eq_coe] at h, have h1: A.1.det * B.1.det* (B.1.det)⁻¹ = 1 * (B.1.det)⁻¹,
simp, rw h, simp only [one_mul], simp only [one_mul, subtype.val_eq_coe] at h1, rw ←  h1, rw mul_assoc,
simp only, have:=det_inv' _ B,
simp only [subtype.val_eq_coe] at this, rw this, simp only [mul_one],
end

lemma det_inv (A: GL n K )  : (det A)⁻¹ = det (A⁻¹):=

begin
have h1: is_unit(det A), by {rw is_unit_iff_exists_inv, use (det A)⁻¹, rw mul_inv_cancel, simp only [ne.def],
intro hh,have:= A.2, unfold_coes at hh, rw hh at this, simp only [not_is_unit_zero] at this, exact this,},
have:= nonsing_inv_det A.1 h1,simp only [subtype.val_eq_coe] at this, rw det_eq_val_det,
have h5: A.nonsing_inve= (↑A)⁻¹, {apply GL.inv_is_inv,}, unfold_coes,
 {simp only [subtype.val_eq_coe], have:= det_inv'' _ A⁻¹ A this, simp only [det_eq_val_det, GL.inv_apply, subtype.val_eq_coe] at this,
rw ← this, dsimp, rw h5},

end

instance SL_to_GL: has_coe (special_linear_group n R) (GL n R):= ⟨λ A, ⟨ A.1, by {have:=A.2,  rw this, simp,}⟩ ⟩

end GL

namespace GL_pos


variables  (n : Type u) [decidable_eq n] [fintype n] (F : Type v)  [linear_ordered_field F ] [nontrivial F]


lemma one_in_GL_pos : 0 < det (1:GL n F ) :=
begin
simp only [det_one, gt_iff_lt, GL.one_apply,zero_lt_one],
end




lemma mul_in_GL_pos (A B :GL n F ) (h1: det A >0 ) (h2: det B >0): det (A*B)>0:=

begin
simp only [gt_iff_lt, det_mul, mul_eq_mul], apply mul_pos h1 h2,
end




lemma inv_det_pos  (A:GL n F ) (h: 0 < det A ):  0 < det A⁻¹ :=

begin
have h2: (det A)⁻¹ = det (A⁻¹), by {apply GL.det_inv _ A},
 rw ← h2, apply inv_pos.2 h,
end

/-- This is the subgroup of nxn matrices with  entries over a linear ordered field and positive determinant-/


noncomputable def GL_pos : subgroup (GL n F) :=
{carrier:={M  | 0 < det M},
 one_mem':= one_in_GL_pos _ _,
 mul_mem':=λ A B h1 h2, mul_in_GL_pos _ _ A B h1 h2,
 inv_mem':=λ A h1,inv_det_pos _ _ A h1,
}




@[simp] lemma mem_GL2R_pos (A: GL n F ) :
  A  ∈ (GL_pos n F)  ↔ 0 < A.1.det := iff.rfl


instance GL_pos_to_GL : has_coe (GL_pos n F)  (GL n F) := ⟨λ A, A.val⟩



lemma SL_det_pos' (A : special_linear_group n F): (A).1.det > 0:=

begin
have:=A.2, simp only [gt_iff_lt, subtype.val_eq_coe], simp only [subtype.val_eq_coe] at this,  rw this, simp,
end


instance SL_to_GL_pos: has_coe (special_linear_group n F) (GL_pos n F):= ⟨λ A, ⟨(A : GL n F), by {simp, have:=A.2,
simp at this, rw ← coe_coe, rw this, simp,} ⟩⟩



end GL_pos


end matrix