feat(algebra/lie/classical): Use computable matrix inverses where pos…

…sible (#10218)

src/algebra/lie/classical.lean

@@ -171,8 +171,9 @@ begin
     by_cases h : x = y; simp [Pso, indefinite_diagonal, h, hi], },
 end
 
-lemma is_unit_Pso {i : R} (hi : i*i = -1) : is_unit (Pso p q R i) :=
-@is_unit_of_invertible _ _ _ (invertible_of_right_inverse _ _ (Pso_inv p q R hi))
+/-- There is a constructive inverse of `Pso p q R i`. -/
+def invertible_Pso {i : R} (hi : i*i = -1) : invertible (Pso p q R i) :=
+invertible_of_right_inverse _ _ (Pso_inv p q R hi)
 
 lemma indefinite_diagonal_transform {i : R} (hi : i*i = -1) :
   (Pso p q R i)ᵀ ⬝ (indefinite_diagonal p q R) ⬝ (Pso p q R i) = 1 :=
@@ -190,10 +191,10 @@ end
 
 /-- An equivalence between the indefinite and definite orthogonal Lie algebras, over a ring
 containing a square root of -1. -/
-noncomputable def so_indefinite_equiv {i : R} (hi : i*i = -1) : so' p q R ≃ₗ⁅R⁆ so (p ⊕ q) R :=
+def so_indefinite_equiv {i : R} (hi : i*i = -1) : so' p q R ≃ₗ⁅R⁆ so (p ⊕ q) R :=
 begin
   apply (skew_adjoint_matrices_lie_subalgebra_equiv
-    (indefinite_diagonal p q R) (Pso p q R i) (is_unit_Pso p q R hi)).trans,
+    (indefinite_diagonal p q R) (Pso p q R i) (invertible_Pso p q R hi)).trans,
   apply lie_equiv.of_eq,
   ext A, rw indefinite_diagonal_transform p q R hi, refl,
 end
@@ -253,14 +254,14 @@ begin
   simp [h],
 end
 
-lemma is_unit_PD [fintype l] [invertible (2 : R)] : is_unit (PD l R) :=
-@is_unit_of_invertible _ _ _ (invertible_of_right_inverse _ _ (PD_inv l R))
+instance invertible_PD [fintype l] [invertible (2 : R)] : invertible (PD l R) :=
+invertible_of_right_inverse _ _ (PD_inv l R)
 
 /-- An equivalence between two possible definitions of the classical Lie algebra of type D. -/
-noncomputable def type_D_equiv_so' [fintype l] [invertible (2 : R)] :
+def type_D_equiv_so' [fintype l] [invertible (2 : R)] :
   type_D l R ≃ₗ⁅R⁆ so' l l R :=
 begin
-  apply (skew_adjoint_matrices_lie_subalgebra_equiv (JD l R) (PD l R) (is_unit_PD l R)).trans,
+  apply (skew_adjoint_matrices_lie_subalgebra_equiv (JD l R) (PD l R) (by apply_instance)).trans,
   apply lie_equiv.of_eq,
   ext A,
   rw [JD_transform, ← coe_unit_of_invertible (2 : R), ←units.smul_def, lie_subalgebra.mem_coe,
@@ -307,14 +308,15 @@ def PB := matrix.from_blocks (1 : matrix unit unit R) 0 0 (PD l R)
 
 variable [fintype l]
 
-lemma PB_inv [invertible (2 : R)] : (PB l R) * (matrix.from_blocks 1 0 0 (PD l R)⁻¹) = 1 :=
+lemma PB_inv [invertible (2 : R)] : PB l R * matrix.from_blocks 1 0 0 (⅟(PD l R)) = 1 :=
 begin
-  simp [PB, matrix.from_blocks_multiply, (PD l R).mul_nonsing_inv, is_unit_PD,
-        ← (PD l R).is_unit_iff_is_unit_det]
+  rw [PB, matrix.mul_eq_mul, matrix.from_blocks_multiply, matrix.mul_inv_of_self],
+  simp only [matrix.mul_zero, matrix.mul_one, matrix.zero_mul, zero_add, add_zero,
+    matrix.from_blocks_one]
 end
 
-lemma is_unit_PB [invertible (2 : R)] : is_unit (PB l R) :=
-@is_unit_of_invertible _ _ _ (invertible_of_right_inverse _ _ (PB_inv l R))
+instance invertible_PB [invertible (2 : R)] : invertible (PB l R) :=
+invertible_of_right_inverse _ _ (PB_inv l R)
 
 lemma JB_transform : (PB l R)ᵀ ⬝ (JB l R) ⬝ (PB l R) = (2 : R) • matrix.from_blocks 1 0 0 (S l R) :=
 by simp [PB, JB, JD_transform, matrix.from_blocks_transpose, matrix.from_blocks_multiply,
@@ -338,10 +340,10 @@ begin
 end
 
 /-- An equivalence between two possible definitions of the classical Lie algebra of type B. -/
-noncomputable def type_B_equiv_so' [invertible (2 : R)] :
+def type_B_equiv_so' [invertible (2 : R)] :
   type_B l R ≃ₗ⁅R⁆ so' (unit ⊕ l) l R :=
 begin
-  apply (skew_adjoint_matrices_lie_subalgebra_equiv (JB l R) (PB l R) (is_unit_PB l R)).trans,
+  apply (skew_adjoint_matrices_lie_subalgebra_equiv (JB l R) (PB l R) (by apply_instance)).trans,
   symmetry,
   apply (skew_adjoint_matrices_lie_subalgebra_equiv_transpose
     (indefinite_diagonal (unit ⊕ l) l R)

src/algebra/lie/matrix.lean

@@ -52,16 +52,16 @@ def lie_equiv_matrix' : module.End R (n → R) ≃ₗ⁅R⁆ matrix n n R :=
   (@lie_equiv_matrix' R _ n _ _).symm A = A.to_lin' := rfl
 
 /-- An invertible matrix induces a Lie algebra equivalence from the space of matrices to itself. -/
-noncomputable def matrix.lie_conj (P : matrix n n R) (h : is_unit P) :
+def matrix.lie_conj (P : matrix n n R) (h : invertible P) :
   matrix n n R ≃ₗ⁅R⁆ matrix n n R :=
 ((@lie_equiv_matrix' R _ n _ _).symm.trans (P.to_linear_equiv' h).lie_conj).trans lie_equiv_matrix'
 
-@[simp] lemma matrix.lie_conj_apply (P A : matrix n n R) (h : is_unit P) :
+@[simp] lemma matrix.lie_conj_apply (P A : matrix n n R) (h : invertible P) :
   P.lie_conj h A = P ⬝ A ⬝ P⁻¹ :=
 by simp [linear_equiv.conj_apply, matrix.lie_conj, linear_map.to_matrix'_comp,
          linear_map.to_matrix'_to_lin']
 
-@[simp] lemma matrix.lie_conj_symm_apply (P A : matrix n n R) (h : is_unit P) :
+@[simp] lemma matrix.lie_conj_symm_apply (P A : matrix n n R) (h : invertible P) :
   (P.lie_conj h).symm A = P⁻¹ ⬝ A ⬝ P :=
 by simp [linear_equiv.symm_conj_apply, matrix.lie_conj, linear_map.to_matrix'_comp,
          linear_map.to_matrix'_to_lin']

src/algebra/lie/skew_adjoint.lean

@@ -110,7 +110,7 @@ iff.rfl
 
 /-- An invertible matrix `P` gives a Lie algebra equivalence between those endomorphisms that are
 skew-adjoint with respect to a square matrix `J` and those with respect to `PᵀJP`. -/
-noncomputable def skew_adjoint_matrices_lie_subalgebra_equiv (P : matrix n n R) (h : is_unit P) :
+def skew_adjoint_matrices_lie_subalgebra_equiv (P : matrix n n R) (h : invertible P) :
   skew_adjoint_matrices_lie_subalgebra J ≃ₗ⁅R⁆ skew_adjoint_matrices_lie_subalgebra (Pᵀ ⬝ J ⬝ P) :=
 lie_equiv.of_subalgebras _ _ (P.lie_conj h).symm
 begin
@@ -119,11 +119,11 @@ begin
     A ∈ skew_adjoint_matrices_submodule (Pᵀ ⬝ J ⬝ P),
   { simp only [lie_subalgebra.mem_coe, submodule.mem_map_equiv, lie_subalgebra.mem_map_submodule,
       coe_coe], exact this, },
-  simp [matrix.is_skew_adjoint, J.is_adjoint_pair_equiv _ _ P h],
+  simp [matrix.is_skew_adjoint, J.is_adjoint_pair_equiv _ _ P (is_unit_of_invertible P)],
 end
 
 lemma skew_adjoint_matrices_lie_subalgebra_equiv_apply
-  (P : matrix n n R) (h : is_unit P) (A : skew_adjoint_matrices_lie_subalgebra J) :
+  (P : matrix n n R) (h : invertible P) (A : skew_adjoint_matrices_lie_subalgebra J) :
   ↑(skew_adjoint_matrices_lie_subalgebra_equiv J P h A) = P⁻¹ ⬝ ↑A ⬝ P :=
 by simp [skew_adjoint_matrices_lie_subalgebra_equiv]
 

src/linear_algebra/matrix/to_linear_equiv.lean

@@ -43,22 +43,22 @@ variables [decidable_eq n]
 
 See `matrix.to_linear_equiv` for the same map on arbitrary modules.
 -/
-noncomputable def to_linear_equiv' (P : matrix n n R) (h : is_unit P) : (n → R) ≃ₗ[R] (n → R) :=
-have h' : is_unit P.det := P.is_unit_iff_is_unit_det.mp h,
-{ inv_fun   := P⁻¹.to_lin',
+def to_linear_equiv' (P : matrix n n R) (h : invertible P) : (n → R) ≃ₗ[R] (n → R) :=
+{ inv_fun   := (⅟P).to_lin',
   left_inv  := λ v,
-    show (P⁻¹.to_lin'.comp P.to_lin') v = v,
-    by rw [← matrix.to_lin'_mul, P.nonsing_inv_mul h', matrix.to_lin'_one, linear_map.id_apply],
+    show ((⅟P).to_lin'.comp P.to_lin') v = v,
+    by rw [← matrix.to_lin'_mul, P.inv_of_mul_self, matrix.to_lin'_one, linear_map.id_apply],
   right_inv := λ v,
-    show (P.to_lin'.comp P⁻¹.to_lin') v = v,
-    by rw [← matrix.to_lin'_mul, P.mul_nonsing_inv h', matrix.to_lin'_one, linear_map.id_apply],
+    show (P.to_lin'.comp (⅟P).to_lin') v = v,
+    by rw [← matrix.to_lin'_mul, P.mul_inv_of_self, matrix.to_lin'_one, linear_map.id_apply],
   ..P.to_lin' }
 
-@[simp] lemma to_linear_equiv'_apply (P : matrix n n R) (h : is_unit P) :
+@[simp] lemma to_linear_equiv'_apply (P : matrix n n R) (h : invertible P) :
   (↑(P.to_linear_equiv' h) : module.End R (n → R)) = P.to_lin' := rfl
 
-@[simp] lemma to_linear_equiv'_symm_apply (P : matrix n n R) (h : is_unit P) :
-  (↑(P.to_linear_equiv' h).symm : module.End R (n → R)) = P⁻¹.to_lin' := rfl
+@[simp] lemma to_linear_equiv'_symm_apply (P : matrix n n R) (h : invertible P) :
+  (↑(P.to_linear_equiv' h).symm : module.End R (n → R)) = P⁻¹.to_lin' :=
+show (⅟P).to_lin' = _, from congr_arg _ P.inv_of_eq_nonsing_inv
 
 end to_linear_equiv'