matrix inverse

matrix inverse.lean

import tactic
import data.complex.basic
import linear_algebra.matrix.nonsingular_inverse

variables {α β I J K L M N: Type*}
variables [fintype I] [fintype J] [fintype K] [fintype L] [fintype M] [fintype N]

----------------------------------------------------------------------------
-- a missing lemma in invertible.lean
lemma inv_of_eq_left_inv [monoid α] {a b : α} [invertible a] (hac : b * a = 1) : ⅟a = b :=
(left_inv_eq_right_inv  hac (mul_inv_of_self _)).symm
----------------------------------------------------------------------------

namespace matrix
open_locale matrix
open_locale big_operators
open complex

/- ## inverse section -/
section inverse
variables [decidable_eq I] [comm_ring α]
variables (A B: matrix I I α)

lemma is_unit_det_of_invertible [invertible A] : is_unit A.det :=
by apply is_unit_det_of_left_inverse A (invertible.inv_of A) (inv_of_mul_self A)

@[simp,norm]
lemma inv_eq_nonsing_inv_of_invertible [invertible A] : ⅟ A = A⁻¹ :=
begin
  have ha:= is_unit_det_of_invertible A,
  have ha':= (is_unit_iff_is_unit_det A).2 ha,
  have h:= inv_of_mul_self A,
  have h':= nonsing_inv_mul A ha,
  rw ←h' at h,
  apply (is_unit.mul_left_inj ha').1 h,
end

variables {A} {B}

noncomputable
lemma invertible_of_is_unit_det  (h: is_unit A.det) : invertible A :=
⟨A⁻¹, nonsing_inv_mul A h, mul_nonsing_inv A h⟩

lemma inv_eq_right_inv (h : A ⬝ B = 1) : A⁻¹ = B :=
begin
  have h1 :=  (is_unit_det_of_right_inverse A B h),
  have h2 := invertible_of_is_unit_det h1,
  have := @inv_of_eq_right_inv (matrix I I α) (infer_instance) A B h2 h,
  simp* at *,
end

lemma inv_eq_left_inv (h : B ⬝ A = 1) : A⁻¹ = B :=
begin
  have h1 :=  (is_unit_det_of_left_inverse A B h),
  have h2 := invertible_of_is_unit_det h1,
  have := @inv_of_eq_left_inv (matrix I I α) (infer_instance) A B h2 h,
  simp* at *,
end

variables {C: matrix I I α}

lemma left_inv_eq_left_inv (h: B ⬝ A = 1) (g: C ⬝ A = 1) : B = C :=
by rw [←(inv_eq_left_inv h), ←(inv_eq_left_inv g)]

lemma right_inv_eq_right_inv (h: A ⬝ B = 1) (g: A ⬝ C = 1) : B = C :=
by rw [←(inv_eq_right_inv h), ←(inv_eq_right_inv g)]

lemma right_inv_eq_left_inv (h: A ⬝ B = 1) (g: C ⬝ A = 1) : B = C :=
by rw [←(inv_eq_right_inv h), ←(inv_eq_left_inv g)]

noncomputable
lemma invertible_of_left_inverse (h: B ⬝ A = 1) : invertible A :=
invertible_of_is_unit_det (is_unit_det_of_left_inverse A B h)

noncomputable
lemma invertible_of_right_inverse (h: A ⬝ B = 1) : invertible A :=
invertible_of_is_unit_det (is_unit_det_of_right_inverse A B h)

variable (A)

@[simp] lemma mul_inv_of_invertible [invertible A] : A ⬝ A⁻¹ = 1 :=
mul_nonsing_inv A (is_unit_det_of_invertible A)

@[simp] lemma inv_mul_of_invertible [invertible A] : A⁻¹ ⬝ A = 1 :=
nonsing_inv_mul A (is_unit_det_of_invertible A)

end inverse
/- ## end inverse -/

/- ## conjugate transpose section -/
/-- The conjugate transpose of a matrix. -/
def conj_transpose (M : matrix I J ℂ) : matrix J I ℂ
| x y := conj (M y x)
localized "postfix `ᴴ`:1500 := matrix.conj_transpose" in matrix
/- ## end conjugate transpose -/

end matrix