From 9b464299dbb3a31f0afbca1f1496768a4a413489 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Wed, 20 Mar 2024 23:48:33 -0500 Subject: [PATCH 1/2] chore(Determinant): fix `Fintype`/`Finite` assumptions `equivOfPiLEquivPi` only needs `Finite`, not `Fintype` --- Mathlib/LinearAlgebra/Determinant.lean | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/Mathlib/LinearAlgebra/Determinant.lean b/Mathlib/LinearAlgebra/Determinant.lean index 172877c760af8..ccfa638e3b585 100644 --- a/Mathlib/LinearAlgebra/Determinant.lean +++ b/Mathlib/LinearAlgebra/Determinant.lean @@ -55,15 +55,18 @@ variable (e : Basis ι R M) section Conjugate variable {A : Type*} [CommRing A] -variable {m n : Type*} [Fintype m] [Fintype n] +variable {m n : Type*} /-- If `R^m` and `R^n` are linearly equivalent, then `m` and `n` are also equivalent. -/ -def equivOfPiLEquivPi {R : Type*} [CommRing R] [Nontrivial R] (e : (m → R) ≃ₗ[R] n → R) : m ≃ n := +def equivOfPiLEquivPi {R : Type*} [Finite m] [Finite n] [CommRing R] [Nontrivial R] + (e : (m → R) ≃ₗ[R] n → R) : m ≃ n := Basis.indexEquiv (Basis.ofEquivFun e.symm) (Pi.basisFun _ _) #align equiv_of_pi_lequiv_pi equivOfPiLEquivPi namespace Matrix +variable [Fintype m] [Fintype n] + /-- If `M` and `M'` are each other's inverse matrices, they are square matrices up to equivalence of types. -/ def indexEquivOfInv [Nontrivial A] [DecidableEq m] [DecidableEq n] {M : Matrix m n A} From 03d13470740d6c67ac3dfba371b9e745de6f0315 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Thu, 21 Mar 2024 00:42:41 -0500 Subject: [PATCH 2/2] +2 files --- Mathlib/LinearAlgebra/Matrix/Basis.lean | 2 +- .../Matrix/NonsingularInverse.lean | 39 +++++++++++++------ 2 files changed, 29 insertions(+), 12 deletions(-) diff --git a/Mathlib/LinearAlgebra/Matrix/Basis.lean b/Mathlib/LinearAlgebra/Matrix/Basis.lean index 4a9bf8bbbc762..eb2e9a38facad 100644 --- a/Mathlib/LinearAlgebra/Matrix/Basis.lean +++ b/Mathlib/LinearAlgebra/Matrix/Basis.lean @@ -72,7 +72,7 @@ theorem toMatrix_eq_toMatrix_constr [Fintype ι] [DecidableEq ι] (v : ι → M) #align basis.to_matrix_eq_to_matrix_constr Basis.toMatrix_eq_toMatrix_constr -- TODO (maybe) Adjust the definition of `Basis.toMatrix` to eliminate the transpose. -theorem coePiBasisFun.toMatrix_eq_transpose [Fintype ι] : +theorem coePiBasisFun.toMatrix_eq_transpose [Finite ι] : ((Pi.basisFun R ι).toMatrix : Matrix ι ι R → Matrix ι ι R) = Matrix.transpose := by ext M i j rfl diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 7b7fb53579a2b..7a94a6c4c1017 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -193,6 +193,8 @@ theorem det_ne_zero_of_right_inverse [Nontrivial α] (h : A * B = 1) : A.det ≠ end Invertible +section Inv + variable [Fintype n] [DecidableEq n] [CommRing α] variable (A : Matrix n n α) (B : Matrix n n α) @@ -352,13 +354,15 @@ lemma mul_right_inj_of_invertible [Invertible A] {x y : Matrix n m α} : A * x = lemma mul_left_inj_of_invertible [Invertible A] {x y : Matrix m n α} : x * A = y * A ↔ x = y := (mul_left_injective_of_invertible A).eq_iff +end Inv + section InjectiveMul -variable [Fintype m] [DecidableEq m] +variable [Fintype n] [Fintype m] [DecidableEq m] [CommRing α] variable [Fintype l] [DecidableEq l] lemma mul_left_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) : - Function.Injective (fun x : Matrix l m α => x * A) := - fun _ _ g => by simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g + Function.Injective (fun x : Matrix l m α => x * A) := fun _ _ g => by + simpa only [Matrix.mul_assoc, Matrix.mul_one, h] using congr_arg (· * B) g lemma mul_right_injective_of_inv (A : Matrix m n α) (B : Matrix n m α) (h : A * B = 1) : Function.Injective (fun x : Matrix m l α => B * x) := @@ -368,29 +372,39 @@ end InjectiveMul section vecMul -variable [Fintype m] [DecidableEq m] {K R : Type*} [Field K] +variable [DecidableEq m] [DecidableEq n] + +section Semiring -theorem vecMul_surjective_iff_exists_left_inverse [Semiring R] {A : Matrix m n R} : +variable {R : Type*} [Semiring R] + +theorem vecMul_surjective_iff_exists_left_inverse [Fintype m] [Finite n] {A : Matrix m n R} : Function.Surjective A.vecMul ↔ ∃ B : Matrix n m R, B * A = 1 := by + cases nonempty_fintype n refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨y ᵥ* B, 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} : +theorem mulVec_surjective_iff_exists_right_inverse [Finite m] [Fintype n] {A : Matrix m n R} : Function.Surjective A.mulVec ↔ ∃ B : Matrix n m R, A * B = 1 := by + cases nonempty_fintype m refine ⟨fun h ↦ ?_, fun ⟨B, hBA⟩ y ↦ ⟨B *ᵥ 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 α} : +end Semiring + +variable {R K : Type*} [CommRing R] [Field K] [Fintype m] + +theorem vecMul_surjective_iff_isUnit {A : Matrix m m R} : 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 α} : +theorem mulVec_surjective_iff_isUnit {A : Matrix m m R} : Function.Surjective A.mulVec ↔ IsUnit A := by rw [mulVec_surjective_iff_exists_right_inverse, exists_right_inverse_iff_isUnit] @@ -420,11 +434,11 @@ theorem linearIndependent_cols_iff_isUnit {A : Matrix m m K} : rw [← transpose_transpose A, isUnit_transpose, linearIndependent_rows_iff_isUnit, transpose_transpose] -theorem vecMul_surjective_of_invertible (A : Matrix m m α) [Invertible A] : +theorem vecMul_surjective_of_invertible (A : Matrix m m R) [Invertible A] : Function.Surjective A.vecMul := vecMul_surjective_iff_isUnit.2 <| isUnit_of_invertible A -theorem mulVec_surjective_of_invertible (A : Matrix m m α) [Invertible A] : +theorem mulVec_surjective_of_invertible (A : Matrix m m R) [Invertible A] : Function.Surjective A.mulVec := mulVec_surjective_iff_isUnit.2 <| isUnit_of_invertible A @@ -446,6 +460,9 @@ theorem linearIndependent_cols_of_invertible (A : Matrix m m K) [Invertible A] : end vecMul +variable [Fintype n] [DecidableEq n] [CommRing α] +variable (A : Matrix n n α) (B : Matrix n n α) + 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⟩ @@ -760,7 +777,7 @@ end Submatrix section Det -variable [Fintype m] [DecidableEq m] +variable [Fintype m] [DecidableEq m] [CommRing α] /-- A variant of `Matrix.det_units_conj`. -/ theorem det_conj {M : Matrix m m α} (h : IsUnit M) (N : Matrix m m α) : det (M * N * M⁻¹) = det N :=