From e9d747efaf44790f92c3b259f01071f60961da97 Mon Sep 17 00:00:00 2001 From: Eric Wieser Date: Wed, 23 Aug 2023 12:46:03 +0000 Subject: [PATCH] chore(Data/Matrix/Invertible): generalize conjugate and transpose lemmas (#6618) The `conjTranspose` lemmas now work for non-commutative rings. --- Mathlib/Data/Matrix/Invertible.lean | 69 ++++++++++++++++++- .../Matrix/NonsingularInverse.lean | 23 ------- 2 files changed, 68 insertions(+), 24 deletions(-) diff --git a/Mathlib/Data/Matrix/Invertible.lean b/Mathlib/Data/Matrix/Invertible.lean index c3e53d6b11703..5c4caad2140f6 100644 --- a/Mathlib/Data/Matrix/Invertible.lean +++ b/Mathlib/Data/Matrix/Invertible.lean @@ -14,6 +14,13 @@ A few of the `Invertible` lemmas generalize to multiplication of rectangular mat For lemmas about the matrix inverse in terms of the determinant and adjugate, see `Matrix.inv` in `LinearAlgebra/Matrix/NonsingularInverse.lean`. + +## Main results + +* `Matrix.invertibleConjTranspose` +* `Matrix.invertibleTranspose` +* `Matrix.isUnit_conjTranpose` +* `Matrix.isUnit_tranpose` -/ @@ -21,10 +28,13 @@ open scoped Matrix variable {m n : Type*} {α : Type*} -variable [Fintype n] [DecidableEq n] [Semiring α] +variable [Fintype n] [DecidableEq n] namespace Matrix +section Semiring +variable [Semiring α] + #align matrix.inv_of_mul_self invOf_mul_self #align matrix.mul_inv_of_self mul_invOf_self @@ -53,6 +63,63 @@ protected theorem mul_mul_invOf_self_cancel (A : Matrix m n α) (B : Matrix n n #align matrix.invertible_of_invertible_mul invertibleOfInvertibleMul #align matrix.invertible_of_mul_invertible invertibleOfMulInvertible +section conj_transpose +variable [StarRing α] (A : Matrix n n α) + +/-- The conjugate transpose of an invertible matrix is invertible. -/ +instance invertibleConjTranspose [Invertible A] : Invertible Aᴴ := Invertible.star _ + +lemma conjTranspose_invOf [Invertible A] [Invertible Aᴴ] : (⅟A)ᴴ = ⅟(Aᴴ) := star_invOf _ + +/-- A matrix is invertible if the conjugate transpose is invertible. -/ +def invertibleOfInvertibleConjTranspose [Invertible Aᴴ] : Invertible A := by + rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose] + infer_instance +#align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose + +@[simp] lemma isUnit_conjTranspose : IsUnit Aᴴ ↔ IsUnit A := isUnit_star + +end conj_transpose + +end Semiring + +section CommSemiring + +variable [CommSemiring α] (A : Matrix n n α) + +/-- The transpose of an invertible matrix is invertible. -/ +instance invertibleTranspose [Invertible A] : Invertible Aᵀ where + invOf := (⅟A)ᵀ + invOf_mul_self := by rw [←transpose_mul, mul_invOf_self, transpose_one] + mul_invOf_self := by rw [←transpose_mul, invOf_mul_self, transpose_one] +#align matrix.invertible_transpose Matrix.invertibleTranspose + +lemma transpose_invOf [Invertible A] [Invertible Aᵀ] : (⅟A)ᵀ = ⅟(Aᵀ) := by + letI := invertibleTranspose A + convert (rfl : _ = ⅟(Aᵀ)) + +/-- `Aᵀ` is invertible when `A` is. -/ +def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A where + invOf := (⅟(Aᵀ))ᵀ + invOf_mul_self := by rw [←transpose_one, ← mul_invOf_self Aᵀ, transpose_mul, transpose_transpose] + mul_invOf_self := by rw [←transpose_one, ← invOf_mul_self Aᵀ, transpose_mul, transpose_transpose] +#align matrix.invertible__of_invertible_transpose Matrix.invertibleOfInvertibleTranspose + +/-- Together `Matrix.invertibleTranspose` and `Matrix.invertibleOfInvertibleTranspose` form an +equivalence, although both sides of the equiv are subsingleton anyway. -/ +@[simps] +def transposeInvertibleEquivInvertible : Invertible Aᵀ ≃ Invertible A where + toFun := @invertibleOfInvertibleTranspose _ _ _ _ _ _ + invFun := @invertibleTranspose _ _ _ _ _ _ + left_inv _ := Subsingleton.elim _ _ + right_inv _ := Subsingleton.elim _ _ + +@[simp] lemma isUnit_transpose : IsUnit Aᵀ ↔ IsUnit A := by + simp only [← nonempty_invertible_iff_isUnit, + (transposeInvertibleEquivInvertible A).nonempty_congr] + +end CommSemiring + end Matrix #align invertible.matrix_mul_left Invertible.mulLeft diff --git a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean index 1d55a78c3c41d..b13b739bde77e 100644 --- a/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean +++ b/Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean @@ -142,29 +142,6 @@ def invertibleOfRightInverse (h : A * B = 1) : Invertible A := ⟨B, mul_eq_one_comm.mp h, h⟩ #align matrix.invertible_of_right_inverse Matrix.invertibleOfRightInverse -/-- The transpose of an invertible matrix is invertible. -/ -instance invertibleTranspose [Invertible A] : Invertible Aᵀ := - haveI : Invertible Aᵀ.det := by simpa using detInvertibleOfInvertible A - invertibleOfDetInvertible Aᵀ -#align matrix.invertible_transpose Matrix.invertibleTranspose - --- porting note: added because Lean can no longer find this instance automatically -/-- The conjugate transpose of an invertible matrix is invertible. -/ -instance invertibleConjTranspose [StarRing α] [Invertible A] : Invertible Aᴴ := - Invertible.star A - -/-- A matrix is invertible if the transpose is invertible. -/ -def invertibleOfInvertibleTranspose [Invertible Aᵀ] : Invertible A := by - rw [← transpose_transpose A] - infer_instance -#align matrix.invertible__of_invertible_transpose Matrix.invertibleOfInvertibleTranspose - -/-- A matrix is invertible if the conjugate transpose is invertible. -/ -def invertibleOfInvertibleConjTranspose [StarRing α] [Invertible Aᴴ] : Invertible A := by - rw [← conjTranspose_conjTranspose A, ← star_eq_conjTranspose] - infer_instance -#align matrix.invertible_of_invertible_conj_transpose Matrix.invertibleOfInvertibleConjTranspose - /-- Given a proof that `A.det` has a constructive inverse, lift `A` to `(Matrix n n α)ˣ`-/ def unitOfDetInvertible [Invertible A.det] : (Matrix n n α)ˣ := @unitOfInvertible _ _ A (invertibleOfDetInvertible A)