[Merged by Bors] - feat: Invertible matrices

Mathlib/Data/Matrix/Basic.lean

@@ -1708,6 +1708,11 @@ def mulVec.addMonoidHomLeft [Fintype n] (v : n → α) : Matrix m n α →+ m 
     apply add_dotProduct
 #align matrix.mul_vec.add_monoid_hom_left Matrix.mulVec.addMonoidHomLeft
 
+/-- The `i`th row of the multiplication is the same as the `vecMul` with the `i`th row of `A`. -/
+theorem mul_apply_eq_vecMul [Fintype n] (A : Matrix m n α) (B : Matrix n o α) (i : m) :
+    (A * B) i = vecMul (A i) B :=
+  rfl
+
 theorem mulVec_diagonal [Fintype m] [DecidableEq m] (v w : m → α) (x : m) :
     mulVec (diagonal v) w x = v x * w x :=
   diagonal_dotProduct v w x

Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean

@@ -5,6 +5,7 @@ Authors: Anne Baanen, Lu-Ming Zhang
 -/
 import Mathlib.Data.Matrix.Invertible
 import Mathlib.LinearAlgebra.Matrix.Adjugate
+import Mathlib.LinearAlgebra.FiniteDimensional
 
 #align_import linear_algebra.matrix.nonsingular_inverse from "leanprover-community/mathlib"@"722b3b152ddd5e0cf21c0a29787c76596cb6b422"
 
@@ -165,10 +166,16 @@ theorem isUnit_of_left_inverse (h : B * A = 1) : IsUnit A :=
   ⟨⟨A, B, mul_eq_one_comm.mp h, h⟩, rfl⟩
 #align matrix.is_unit_of_left_inverse Matrix.isUnit_of_left_inverse
 
+theorem exists_left_inverse_iff_isUnit : (∃ B, B * A = 1) ↔ IsUnit A :=
+  ⟨fun ⟨_, h⟩ ↦ isUnit_of_left_inverse h, fun h ↦ have := h.invertible; ⟨⅟A, invOf_mul_self' A⟩⟩
+
 theorem isUnit_of_right_inverse (h : A * B = 1) : IsUnit A :=
   ⟨⟨A, B, h, mul_eq_one_comm.mp h⟩, rfl⟩
 #align matrix.is_unit_of_right_inverse Matrix.isUnit_of_right_inverse
 
+theorem exists_right_inverse_iff_isUnit : (∃ B, A * B = 1) ↔ IsUnit A :=
+  ⟨fun ⟨_, h⟩ ↦ isUnit_of_right_inverse h, fun h ↦ have := h.invertible; ⟨⅟A, mul_invOf_self' A⟩⟩
+
 theorem isUnit_det_of_left_inverse (h : B * A = 1) : IsUnit A.det :=
   @isUnit_of_invertible _ _ _ (detInvertibleOfLeftInverse _ _ h)
 #align matrix.is_unit_det_of_left_inverse Matrix.isUnit_det_of_left_inverse
@@ -361,6 +368,86 @@ lemma mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A
 
 end InjectiveMul
 
+section vecMul
+
+variable [Fintype m] [DecidableEq m] {K R : Type*} [Field K]
+
+theorem vecMul_surjective_iff_exists_left_inverse [Semiring R] {A : Matrix m n R} :
+    Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by
+  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B.vecMul y, by simp [hBA]⟩⟩
+  choose rows hrows using (h <| Pi.single · 1)
+  refine ⟨Matrix.of rows, Matrix.ext fun i j => ?_⟩
+  rw [mul_apply_eq_vecMul, one_eq_pi_single, ←hrows]
+  rfl
+
+theorem mulVec_surjective_iff_exists_right_inverse [Semiring R] {A : Matrix m n R} :
+    Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by
+  refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B.mulVec y, by simp [hBA]⟩⟩
+  choose cols hcols using (h <| Pi.single · 1)
+  refine ⟨(Matrix.of cols)ᵀ, Matrix.ext fun i j ↦ ?_⟩
+  rw [one_eq_pi_single, Pi.single_comm, ← hcols j]
+  rfl
+
+theorem vecMul_surjective_iff_isUnit {A : Matrix m m α} :
+    Function.Surjective A.vecMul ↔ IsUnit A := by
+  rw [vecMul_surjective_iff_exists_left_inverse, exists_left_inverse_iff_isUnit]
+
+theorem mulVec_surjective_iff_isUnit {A : Matrix m m α} :
+    Function.Surjective A.mulVec ↔ IsUnit A := by
+  rw [mulVec_surjective_iff_exists_right_inverse, exists_right_inverse_iff_isUnit]
+
+theorem vecMul_injective_iff_isUnit {A : Matrix m m K} :
+    Function.Injective A.vecMul ↔ IsUnit A := by
+  refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
+  · rw [← vecMul_surjective_iff_isUnit]
+    exact LinearMap.surjective_of_injective (f := A.vecMulLinear) h
+  change Function.Injective A.vecMulLinear
+  rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
+  intro c hc
+  replace h := h.invertible
+  simpa using congr_arg A⁻¹.vecMulLinear hc
+
+theorem mulVec_injective_iff_isUnit {A : Matrix m m K} :
+    Function.Injective A.mulVec ↔ IsUnit A := by
+  rw [← isUnit_transpose, ← vecMul_injective_iff_isUnit]
+  simp_rw [vecMul_transpose]
+
+theorem linearIndependent_rows_iff_isUnit {A : Matrix m m K} :
+    LinearIndependent K (fun i ↦ A i) ↔ IsUnit A := by
+  rw [← transpose_transpose A, ← mulVecLin_injective_iff, mulVecLin_transpose,
+    transpose_transpose, ←vecMul_injective_iff_isUnit, coe_vecMulLinear]
+
+theorem linearIndependent_cols_iff_isUnit {A : Matrix m m K} :
+    LinearIndependent K (fun i ↦ Aᵀ i) ↔ IsUnit A := by
+  rw [← transpose_transpose A, isUnit_transpose, linearIndependent_rows_iff_isUnit,
+    transpose_transpose]
+
+theorem vecMul_surjective_of_invertible (A : Matrix m m α) [Invertible A] :
+    Function.Surjective A.vecMul :=
+  fun y ↦ ⟨A⁻¹.vecMul y, by simp⟩
+
+theorem mulVec_surjective_of_invertible (A : Matrix m m α) [Invertible A] :
+    Function.Surjective A.mulVec :=
+  fun y ↦ ⟨A⁻¹.mulVec y, by simp⟩
+
+theorem vecMul_injective_of_invertible (A : Matrix m m K) [Invertible A] :
+    Function.Injective A.vecMul :=
+  vecMul_injective_iff_isUnit.2 <| isUnit_of_invertible A
+
+theorem mulVec_injective_of_invertible (A : Matrix m m K) [Invertible A] :
+    Function.Injective A.mulVec :=
+  mulVec_injective_iff_isUnit.2 <| isUnit_of_invertible A
+
+theorem linearIndependent_rows_of_invertible (A : Matrix m m K) [Invertible A] :
+    LinearIndependent K (fun i ↦ A i) :=
+  linearIndependent_rows_iff_isUnit.2 <| isUnit_of_invertible A
+
+theorem linearIndependent_cols_of_invertible (A : Matrix m m K) [Invertible A] :
+    LinearIndependent K (fun i ↦ Aᵀ i) :=
+  linearIndependent_cols_iff_isUnit.2 <| isUnit_of_invertible A
+
+end vecMul
+
 theorem nonsing_inv_cancel_or_zero : A⁻¹ * A = 1 ∧ A * A⁻¹ = 1 ∨ A⁻¹ = 0 := by
   by_cases h : IsUnit A.det
   · exact Or.inl ⟨nonsing_inv_mul _ h, mul_nonsing_inv _ h⟩

Mathlib/LinearAlgebra/Matrix/ToLin.lean

@@ -84,13 +84,18 @@ variable {R : Type*} [Semiring R]
 variable {l m n : Type*}
 
 /-- `Matrix.vecMul M` is a linear map. -/
-@[simps]
 def Matrix.vecMulLinear [Fintype m] (M : Matrix m n R) : (m → R) →ₗ[R] n → R where
   toFun x := M.vecMul x
   map_add' _ _ := funext fun _ => add_dotProduct _ _ _
   map_smul' _ _ := funext fun _ => smul_dotProduct _ _ _
 #align matrix.vec_mul_linear Matrix.vecMulLinear
 
+@[simp] theorem Matrix.vecMulLinear_apply [Fintype m] (M : Matrix m n R) (x : m → R) :
+    M.vecMulLinear x = M.vecMul x := rfl
+
+theorem Matrix.coe_vecMulLinear [Fintype m] (M : Matrix m n R) :
+    (M.vecMulLinear : _ → _) = M.vecMul := rfl
+
 variable [Fintype m] [DecidableEq m]
 
 @[simp]
@@ -105,6 +110,28 @@ theorem Matrix.vecMul_stdBasis (M : Matrix m n R) (i j) :
   · rw [Function.update_noteq (Ne.symm h), Pi.zero_apply]
 #align matrix.vec_mul_std_basis Matrix.vecMul_stdBasis
 
+theorem range_vecMulLinear (M : Matrix m n R) :
+    LinearMap.range M.vecMulLinear = span R (range M) := by
+  letI := Classical.decEq m
+  simp_rw [range_eq_map, ← iSup_range_stdBasis, Submodule.map_iSup, range_eq_map, ←
+    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
+    Matrix.vecMulLinear_apply, iSup_span, range_eq_iUnion, vecMul, iUnion_singleton_eq_range,
+    dotProduct, stdBasis_apply', ite_mul, one_mul, zero_mul, Finset.sum_ite_eq,
+    Finset.mem_univ, ite_true]
+
+theorem Matrix.vecMulLinear_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R} :
+    Function.Injective M.vecMulLinear ↔ LinearIndependent R (fun i ↦ M i) := by
+  simp only [← LinearMap.ker_eq_bot, Fintype.linearIndependent_iff, Submodule.eq_bot_iff,
+     LinearMap.mem_ker, vecMulLinear_apply, vecMul, dotProduct]
+  refine ⟨fun h c h0 i ↦ ?_, fun h c h0 ↦ funext fun i ↦ ?_⟩
+  · rw [h c, Pi.zero_apply]
+    rw [←h0]
+    ext; simp [mul_comm]
+  rw [h c, Pi.zero_apply]
+  rw [←h0]
+  ext j
+  simp [mul_comm]
+
 /-- Linear maps `(m → R) →ₗ[R] (n → R)` are linearly equivalent over `Rᵐᵒᵖ` to `Matrix m n R`,
 by having matrices act by right multiplication.
  -/
@@ -195,7 +222,8 @@ This should eventually be remedied.
 -/
 
 
-section ToMatrix'
+
+section mulVec
 
 variable {R : Type*} [CommSemiring R]
 
@@ -208,6 +236,9 @@ def Matrix.mulVecLin [Fintype n] (M : Matrix m n R) : (n → R) →ₗ[R] m →
   map_smul' _ _ := funext fun _ => dotProduct_smul _ _ _
 #align matrix.mul_vec_lin Matrix.mulVecLin
 
+theorem Matrix.coe_mulVecLin [Fintype n] (M : Matrix m n R) :
+    (M.mulVecLin : _ → _) = M.mulVec := rfl
+
 @[simp]
 theorem Matrix.mulVecLin_apply [Fintype n] (M : Matrix m n R) (v : n → R) :
     M.mulVecLin v = M.mulVec v :=
@@ -225,6 +256,14 @@ theorem Matrix.mulVecLin_add [Fintype n] (M N : Matrix m n R) :
   LinearMap.ext fun _ => add_mulVec _ _ _
 #align matrix.mul_vec_lin_add Matrix.mulVecLin_add
 
+@[simp] theorem Matrix.mulVecLin_transpose [Fintype m] (M : Matrix m n R) :
+    Mᵀ.mulVecLin = M.vecMulLinear := by
+  ext; simp [mulVec_transpose]
+
+@[simp] theorem Matrix.vecMulLinear_transpose [Fintype n] (M : Matrix m n R) :
+    Mᵀ.vecMulLinear = M.mulVecLin := by
+  ext; simp [vecMul_transpose]
+
 theorem Matrix.mulVecLin_submatrix [Fintype n] [Fintype l] (f₁ : m → k) (e₂ : n ≃ l)
     (M : Matrix k l R) :
     (M.submatrix f₁ e₂).mulVecLin = funLeft R R f₁ ∘ₗ M.mulVecLin ∘ₗ funLeft _ _ e₂.symm :=
@@ -254,7 +293,7 @@ theorem Matrix.mulVecLin_mul [Fintype m] (M : Matrix l m R) (N : Matrix m n R) :
   LinearMap.ext fun _ => (mulVec_mulVec _ _ _).symm
 #align matrix.mul_vec_lin_mul Matrix.mulVecLin_mul
 
-theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix n n R} :
+theorem Matrix.ker_mulVecLin_eq_bot_iff {M : Matrix m n R} :
     (LinearMap.ker M.mulVecLin) = ⊥ ↔ ∀ v, M.mulVec v = 0 → v = 0 := by
   simp only [Submodule.eq_bot_iff, LinearMap.mem_ker, Matrix.mulVecLin_apply]
 #align matrix.ker_mul_vec_lin_eq_bot_iff Matrix.ker_mulVecLin_eq_bot_iff
@@ -272,13 +311,20 @@ theorem Matrix.mulVec_stdBasis_apply [DecidableEq n] (M : Matrix m n R) (j) :
 
 theorem Matrix.range_mulVecLin (M : Matrix m n R) :
     LinearMap.range M.mulVecLin = span R (range Mᵀ) := by
-  letI := Classical.decEq n
-  simp_rw [range_eq_map, ← iSup_range_stdBasis, Submodule.map_iSup, range_eq_map, ←
-    Ideal.span_singleton_one, Ideal.span, Submodule.map_span, image_image, image_singleton,
-    Matrix.mulVecLin_apply, M.mulVec_stdBasis_apply, iSup_span, range_eq_iUnion]
+  rw [← vecMulLinear_transpose, range_vecMulLinear]
 #align matrix.range_mul_vec_lin Matrix.range_mulVecLin
 
-variable [DecidableEq n]
+theorem Matrix.mulVecLin_injective_iff {R : Type*} [CommRing R] {M : Matrix m n R} :
+    Function.Injective M.mulVecLin ↔ LinearIndependent R (fun i ↦ Mᵀ i) := by
+  rw [← vecMulLinear_transpose, vecMulLinear_injective_iff]
+
+end mulVec
+
+section ToMatrix'
+
+variable {R : Type*} [CommSemiring R]
+
+variable {k l m n : Type*} [DecidableEq n] [Fintype n]
 
 /-- Linear maps `(n → R) →ₗ[R] (m → R)` are linearly equivalent to `Matrix m n R`. -/
 def LinearMap.toMatrix' : ((n → R) →ₗ[R] m → R) ≃ₗ[R] Matrix m n R where