-
Notifications
You must be signed in to change notification settings - Fork 307
/
Invertible.lean
124 lines (90 loc) · 4.91 KB
/
Invertible.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
/-
Copyright (c) 2023 Eric Wieser. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Eric Wieser
-/
import Mathlib.Data.Matrix.Basic
#align_import data.matrix.invertible from "leanprover-community/mathlib"@"722b3b152ddd5e0cf21c0a29787c76596cb6b422"
/-! # Extra lemmas about invertible matrices
A few of the `Invertible` lemmas generalize to multiplication of rectangular matrices.
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`
-/
open scoped Matrix
variable {m n : Type*} {α : Type*}
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
/-- A copy of `invOf_mul_self_assoc` for rectangular matrices. -/
protected theorem invOf_mul_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
⅟ A * (A * B) = B := by rw [← Matrix.mul_assoc, invOf_mul_self, Matrix.one_mul]
#align matrix.inv_of_mul_self_assoc Matrix.invOf_mul_self_assoc
/-- A copy of `mul_invOf_self_assoc` for rectangular matrices. -/
protected theorem mul_invOf_self_assoc (A : Matrix n n α) (B : Matrix n m α) [Invertible A] :
A * (⅟ A * B) = B := by rw [← Matrix.mul_assoc, mul_invOf_self, Matrix.one_mul]
#align matrix.mul_inv_of_self_assoc Matrix.mul_invOf_self_assoc
/-- A copy of `mul_invOf_mul_self_cancel` for rectangular matrices. -/
protected theorem mul_invOf_mul_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
A * ⅟ B * B = A := by rw [Matrix.mul_assoc, invOf_mul_self, Matrix.mul_one]
#align matrix.mul_inv_of_mul_self_cancel Matrix.mul_invOf_mul_self_cancel
/-- A copy of `mul_mul_invOf_self_cancel` for rectangular matrices. -/
protected theorem mul_mul_invOf_self_cancel (A : Matrix m n α) (B : Matrix n n α) [Invertible B] :
A * B * ⅟ B = A := by rw [Matrix.mul_assoc, mul_invOf_self, Matrix.mul_one]
#align matrix.mul_mul_inv_of_self_cancel Matrix.mul_mul_invOf_self_cancel
#align matrix.invertible_mul invertibleMul
#align matrix.inv_of_mul invOf_mul
#align matrix.invertible_of_invertible_mul invertibleOfInvertibleMul
#align matrix.invertible_of_mul_invertible invertibleOfMulInvertible
section ConjTranspose
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 ConjTranspose
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
#align invertible.matrix_mul_right Invertible.mulRight