Exact source: Mathlib/LinearAlgebra/Matrix/Adjugate.lean
Pinned GitHub source · Raw UTF-8 source
Back to Cramer’s rule for coordinates of a row
1/-2Copyright (c) 2019 Anne Baanen. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Anne Baanen5-/6module78public import Mathlib.Algebra.Regular.Basic9public import Mathlib.LinearAlgebra.Matrix.Symmetric10public import Mathlib.LinearAlgebra.Matrix.MvPolynomial11public import Mathlib.LinearAlgebra.Matrix.Polynomial12public import Mathlib.GroupTheory.GroupAction.Ring1314/-!15# Cramer's rule and adjugate matrices1617The adjugate matrix is the transpose of the cofactor matrix.18It is calculated with Cramer's rule, which we introduce first.19The vectors returned by Cramer's rule are given by the linear map `cramer`,20which sends a matrix `A` and vector `b` to the vector consisting of the21determinant of replacing the `i`th column of `A` with `b` at index `i`22(written as `(A.updateCol i b).det`).23Using Cramer's rule, we can compute for each matrix `A` the matrix `adjugate A`.24The entries of the adjugate are the minors of `A`.25Instead of defining a minor by deleting row `i` and column `j` of `A`, we26replace the `i`th row of `A` with the `j`th basis vector; the resulting matrix27has the same determinant but more importantly equals Cramer's rule applied28to `A` and the `j`th basis vector, simplifying the subsequent proofs.29We prove the adjugate behaves like `det A • A⁻¹`.3031## Main definitions3233* `Matrix.cramer A b`: the vector output by Cramer's rule on `A` and `b`.34* `Matrix.adjugate A`: the adjugate (or classical adjoint) of the matrix `A`.3536## References3738 * https://en.wikipedia.org/wiki/Cramer's_rule#Finding_inverse_matrix3940## Tags4142cramer, cramer's rule, adjugate43-/4445@[expose] public section464748namespace Matrix4950universe u v w5152variable {m : Type u} {n : Type v} {α : Type w}53variable [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α]5455open Matrix Polynomial Equiv Equiv.Perm Finset5657section Cramer5859/-!60 ### `cramer` section6162 Introduce the linear map `cramer` with values defined by `cramerMap`.63 After defining `cramerMap` and showing it is linear,64 we will restrict our proofs to using `cramer`.65-/666768variable (A : Matrix n n α) (b : n → α)6970/-- `cramerMap A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,71 and thus `cramerMap A b` is the vector output by Cramer's rule on `A` and `b`.7273 If `A * x = b` has a unique solution in `x`, `cramerMap A` sends the vector `b` to `A.det • x`.74 Otherwise, the outcome of `cramerMap` is well-defined but not necessarily useful.75-/76def cramerMap (i : n) : α :=77 (A.updateCol i b).det7879theorem cramerMap_is_linear (i : n) : IsLinearMap α fun b => cramerMap A b i :=80 { map_add := det_updateCol_add _ _81 map_smul := det_updateCol_smul _ _ }8283theorem cramer_is_linear : IsLinearMap α (cramerMap A) := by84 constructor <;> intros <;> ext i85 · apply (cramerMap_is_linear A i).186 · apply (cramerMap_is_linear A i).28788/-- `cramer A b i` is the determinant of the matrix `A` with column `i` replaced with `b`,89 and thus `cramer A b` is the vector output by Cramer's rule on `A` and `b`.9091 If `A * x = b` has a unique solution in `x`, `cramer A` sends the vector `b` to `A.det • x`.92 Otherwise, the outcome of `cramer` is well-defined but not necessarily useful.93-/94def cramer (A : Matrix n n α) : (n → α) →ₗ[α] (n → α) :=95 IsLinearMap.mk' (cramerMap A) (cramer_is_linear A)9697theorem cramer_apply (i : n) : cramer A b i = (A.updateCol i b).det :=98 rfl99100theorem cramer_transpose_apply (i : n) : cramer Aᵀ b i = (A.updateRow i b).det := by101 rw [cramer_apply, updateCol_transpose, det_transpose]102103theorem cramer_transpose_row_self (i : n) : Aᵀ.cramer (A i) = Pi.single i A.det := by104 ext j105 rw [cramer_apply, Pi.single_apply]106 split_ifs with h107 · -- i = j: this entry should be `A.det`108 subst h109 simp only [updateCol_transpose, det_transpose, updateRow_eq_self]110 · -- i ≠ j: this entry should be 0111 rw [updateCol_transpose, det_transpose]112 apply det_zero_of_row_eq h113 rw [updateRow_self, updateRow_ne (Ne.symm h)]114115theorem cramer_row_self (i : n) (h : ∀ j, b j = A j i) : A.cramer b = Pi.single i A.det := by116 rw [← transpose_transpose A, det_transpose]117 convert! cramer_transpose_row_self Aᵀ i118 exact funext h119120@[simp]121theorem cramer_one : cramer (1 : Matrix n n α) = 1 := by122 ext i j123 convert! congr_fun (cramer_row_self (1 : Matrix n n α) (Pi.single i 1) i _) j124 · simp125 · intro j126 rw [Matrix.one_eq_pi_single, Pi.single_comm]127128theorem cramer_smul (r : α) (A : Matrix n n α) :129 cramer (r • A) = r ^ (Fintype.card n - 1) • cramer A :=130 LinearMap.ext fun _ => funext fun _ => det_updateCol_smul_left _ _ _ _131132@[simp]133theorem cramer_subsingleton_apply [Subsingleton n] (A : Matrix n n α) (b : n → α) (i : n) :134 cramer A b i = b i := by rw [cramer_apply, det_eq_elem_of_subsingleton _ i, updateCol_self]135136theorem cramer_zero [Nontrivial n] : cramer (0 : Matrix n n α) = 0 := by137 ext i j138 obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j139 apply det_eq_zero_of_column_eq_zero j'140 simp [updateCol_ne hj']141142/-- Use linearity of `cramer` to take it out of a summation. -/143theorem sum_cramer {β} (s : Finset β) (f : β → n → α) :144 (∑ x ∈ s, cramer A (f x)) = cramer A (∑ x ∈ s, f x) :=145 (map_sum (cramer A) ..).symm146147/-- Use linearity of `cramer` and vector evaluation to take `cramer A _ i` out of a summation. -/148theorem sum_cramer_apply {β} (s : Finset β) (f : n → β → α) (i : n) :149 (∑ x ∈ s, cramer A (fun j => f j x) i) = cramer A (fun j : n => ∑ x ∈ s, f j x) i :=150 calc151 (∑ x ∈ s, cramer A (fun j => f j x) i) = (∑ x ∈ s, cramer A fun j => f j x) i :=152 (Finset.sum_apply i s _).symm153 _ = cramer A (fun j : n => ∑ x ∈ s, f j x) i := by154 rw [sum_cramer, cramer_apply]155 congr with j156 apply Finset.sum_apply157158theorem cramer_submatrix_equiv (A : Matrix m m α) (e : n ≃ m) (b : n → α) :159 cramer (A.submatrix e e) b = cramer A (b ∘ e.symm) ∘ e := by160 ext i161 simp_rw [Function.comp_apply, cramer_apply, updateCol_submatrix_equiv,162 det_submatrix_equiv_self e, Function.comp_def]163164theorem cramer_reindex (e : m ≃ n) (A : Matrix m m α) (b : n → α) :165 cramer (reindex e e A) b = cramer A (b ∘ e) ∘ e.symm :=166 cramer_submatrix_equiv _ _ _167168end Cramer169170section Adjugate171172/-!173### `adjugate` section174175Define the `adjugate` matrix and a few equations.176These will hold for any matrix over a commutative ring.177-/178179180/-- The adjugate matrix is the transpose of the cofactor matrix.181182 Typically, the cofactor matrix is defined by taking minors,183 i.e. the determinant of the matrix with a row and column removed.184 However, the proof of `mul_adjugate` becomes a lot easier if we use the185 matrix replacing a column with a basis vector, since it allows us to use186 facts about the `cramer` map.187-/188def adjugate (A : Matrix n n α) : Matrix n n α :=189 of fun i => cramer Aᵀ (Pi.single i 1)190191theorem adjugate_def (A : Matrix n n α) : adjugate A = of fun i => cramer Aᵀ (Pi.single i 1) :=192 rfl193194theorem adjugate_apply (A : Matrix n n α) (i j : n) :195 adjugate A i j = (A.updateRow j (Pi.single i 1)).det := by196 rw [adjugate_def, of_apply, cramer_apply, updateCol_transpose, det_transpose]197198theorem adjugate_transpose (A : Matrix n n α) : (adjugate A)ᵀ = adjugate Aᵀ := by199 ext i j200 rw [transpose_apply, adjugate_apply, adjugate_apply, updateRow_transpose, det_transpose]201 rw [det_apply', det_apply']202 apply Finset.sum_congr rfl203 intro σ _204 congr 1205 by_cases h : i = σ j206 · -- Everything except `(i, j)` (= `(σ j, j)`) is given by A, and the rest is a single `1`.207 congr208 ext j'209 subst h210 have : σ j' = σ j ↔ j' = j := σ.injective.eq_iff211 rw [updateRow_apply, updateCol_apply]212 simp_rw [this]213 rw [← dite_eq_ite, ← dite_eq_ite]214 congr 1 with rfl215 rw [Pi.single_eq_same, Pi.single_eq_same]216 · -- Otherwise, we need to show that there is a `0` somewhere in the product.217 have : (∏ j' : n, updateCol A j (Pi.single i 1) (σ j') j') = 0 := by218 apply prod_eq_zero (mem_univ j)219 rw [updateCol_self, Pi.single_eq_of_ne' h]220 rw [this]221 apply prod_eq_zero (mem_univ (σ⁻¹ i))222 simp only [Perm.coe_inv, apply_symm_apply, updateRow_self]223 apply Pi.single_eq_of_ne224 intro h'225 exact h ((symm_apply_eq σ).mp h')226227theorem IsSymm.adjugate {A : Matrix n n α} (hA : A.IsSymm) : A.adjugate.IsSymm := by228 rw [IsSymm, Matrix.adjugate_transpose, hA.eq]229230@[simp]231theorem adjugate_submatrix_equiv_self (e : n ≃ m) (A : Matrix m m α) :232 adjugate (A.submatrix e e) = (adjugate A).submatrix e e := by233 ext i j234 have : (fun j ↦ Pi.single i 1 <| e.symm j) = Pi.single (e i) 1 :=235 Function.update_comp_equiv (0 : n → α) e.symm i 1236 rw [adjugate_apply, submatrix_apply, adjugate_apply, ← det_submatrix_equiv_self e,237 updateRow_submatrix_equiv, this]238239theorem adjugate_reindex (e : m ≃ n) (A : Matrix m m α) :240 adjugate (reindex e e A) = reindex e e (adjugate A) :=241 adjugate_submatrix_equiv_self _ _242243/-- Since the map `b ↦ cramer A b` is linear in `b`, it must be multiplication by some matrix. This244matrix is `A.adjugate`. -/245theorem cramer_eq_adjugate_mulVec (A : Matrix n n α) (b : n → α) :246 cramer A b = A.adjugate *ᵥ b := by247 nth_rw 2 [← A.transpose_transpose]248 rw [← adjugate_transpose, adjugate_def]249 have : b = ∑ i, b i • (Pi.single i 1 : n → α) := by250 refine (pi_eq_sum_univ b).trans ?_251 congr with j252 simp [Pi.single_apply, eq_comm]253 conv_lhs =>254 rw [this]255 ext k256 simp [mulVec, dotProduct, mul_comm]257258theorem mul_adjugate_apply (A : Matrix n n α) (i j k) :259 A i k * adjugate A k j = cramer Aᵀ (Pi.single k (A i k)) j := by260 rw [← smul_eq_mul, adjugate, of_apply, ← Pi.smul_apply, ← map_smul, ← Pi.single_smul',261 smul_eq_mul, mul_one]262263set_option backward.isDefEq.respectTransparency false in264theorem mul_adjugate (A : Matrix n n α) : A * adjugate A = A.det • (1 : Matrix n n α) := by265 ext i j266 rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]267 simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]268269theorem adjugate_mul (A : Matrix n n α) : adjugate A * A = A.det • (1 : Matrix n n α) :=270 calc271 adjugate A * A = (Aᵀ * adjugate Aᵀ)ᵀ := by272 rw [← adjugate_transpose, ← transpose_mul, transpose_transpose]273 _ = _ := by rw [mul_adjugate Aᵀ, det_transpose, transpose_smul, transpose_one]274275theorem adjugate_smul (r : α) (A : Matrix n n α) :276 adjugate (r • A) = r ^ (Fintype.card n - 1) • adjugate A := by277 rw [adjugate, adjugate, transpose_smul, cramer_smul]278 rfl279280/-- A stronger form of **Cramer's rule** that allows us to solve some instances of `A * x = b` even281if the determinant is not a unit. A sufficient (but still not necessary) condition is that `A.det`282divides `b`. -/283@[simp]284theorem mulVec_cramer (A : Matrix n n α) (b : n → α) : A *ᵥ cramer A b = A.det • b := by285 rw [cramer_eq_adjugate_mulVec, mulVec_mulVec, mul_adjugate, smul_mulVec, one_mulVec]286287theorem det_eq_zero_of_mulVec_eq_zero_of_mem_nonZeroDivisors {M : Matrix n n α} {v : n → α}288 (h : M *ᵥ v = 0) {i : n} (hi : v i ∈ nonZeroDivisors α) : M.det = 0 := by289 apply mul_right_mem_nonZeroDivisors_eq_zero_iff hi |>.mp290 simpa [adjugate_mul, smul_mulVec] using congr((M.adjugate *ᵥ $h) i)291292theorem adjugate_subsingleton [Subsingleton n] (A : Matrix n n α) : adjugate A = 1 := by293 ext i j294 simp [Subsingleton.elim i j, adjugate_apply, det_eq_elem_of_subsingleton _ i, one_apply]295296theorem adjugate_eq_one_of_card_eq_one {A : Matrix n n α} (h : Fintype.card n = 1) :297 adjugate A = 1 :=298 haveI : Subsingleton n := Fintype.card_le_one_iff_subsingleton.mp h.le299 adjugate_subsingleton _300301@[simp]302theorem adjugate_zero [Nontrivial n] : adjugate (0 : Matrix n n α) = 0 := by303 ext i j304 obtain ⟨j', hj'⟩ : ∃ j', j' ≠ j := exists_ne j305 apply det_eq_zero_of_column_eq_zero j'306 simp [updateCol_ne hj']307308@[simp]309theorem adjugate_one : adjugate (1 : Matrix n n α) = 1 := by310 ext311 simp [adjugate_def, Matrix.one_apply, Pi.single_apply, eq_comm]312313@[simp]314theorem adjugate_diagonal (v : n → α) :315 adjugate (diagonal v) = diagonal fun i => ∏ j ∈ Finset.univ.erase i, v j := by316 ext i j317 simp only [adjugate_def, cramer_apply, diagonal_transpose, of_apply]318 obtain rfl | hij := eq_or_ne i j319 · rw [diagonal_apply_eq, diagonal_updateCol_single, det_diagonal,320 prod_update_of_mem (Finset.mem_univ _), sdiff_singleton_eq_erase, one_mul]321 · rw [diagonal_apply_ne _ hij]322 refine det_eq_zero_of_row_eq_zero j fun k => ?_323 obtain rfl | hjk := eq_or_ne k j324 · rw [updateCol_self, Pi.single_eq_of_ne' hij]325 · rw [updateCol_ne hjk, diagonal_apply_ne' _ hjk]326327theorem _root_.RingHom.map_adjugate {R S : Type*} [CommRing R] [CommRing S] (f : R →+* S)328 (M : Matrix n n R) : f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) := by329 ext i k330 have : Pi.single i (1 : S) = f ∘ Pi.single i 1 := by331 rw [← f.map_one]332 exact Pi.single_op (fun _ => f) (fun _ => f.map_zero) i (1 : R)333 rw [adjugate_apply, RingHom.mapMatrix_apply, map_apply, RingHom.mapMatrix_apply, this, ←334 map_updateRow, ← RingHom.mapMatrix_apply, ← RingHom.map_det, ← adjugate_apply]335336theorem _root_.AlgHom.map_adjugate {R A B : Type*} [CommSemiring R] [CommRing A] [CommRing B]337 [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (M : Matrix n n A) :338 f.mapMatrix M.adjugate = Matrix.adjugate (f.mapMatrix M) :=339 f.toRingHom.map_adjugate _340341theorem det_adjugate (A : Matrix n n α) : (adjugate A).det = A.det ^ (Fintype.card n - 1) := by342 -- get rid of the `- 1`343 rcases (Fintype.card n).eq_zero_or_pos with h_card | h_card344 · haveI : IsEmpty n := Fintype.card_eq_zero_iff.mp h_card345 rw [h_card, Nat.zero_sub, pow_zero, adjugate_subsingleton, det_one]346 replace h_card := tsub_add_cancel_of_le h_card.nat_succ_le347 -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring348 -- where `A'.det` is non-zero.349 let A' := mvPolynomialX n n ℤ350 suffices A'.adjugate.det = A'.det ^ (Fintype.card n - 1) by351 rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_det, ←352 AlgHom.map_det, ← map_pow, this]353 apply mul_left_cancel₀ (show A'.det ≠ 0 from det_mvPolynomialX_ne_zero n ℤ)354 calc355 A'.det * A'.adjugate.det = (A' * adjugate A').det := (det_mul _ _).symm356 _ = A'.det ^ Fintype.card n := by rw [mul_adjugate A', det_smul, det_one, mul_one]357 _ = A'.det * A'.det ^ (Fintype.card n - 1) := by rw [← pow_succ', h_card]358359@[simp]360theorem adjugate_fin_zero (A : Matrix (Fin 0) (Fin 0) α) : adjugate A = 0 :=361 Subsingleton.elim _ _362363@[simp]364theorem adjugate_fin_one (A : Matrix (Fin 1) (Fin 1) α) : adjugate A = 1 :=365 adjugate_subsingleton A366367theorem adjugate_fin_succ_eq_det_submatrix {n : ℕ} (A : Matrix (Fin n.succ) (Fin n.succ) α) (i j) :368 adjugate A i j = (-1) ^ (j + i : ℕ) * det (A.submatrix j.succAbove i.succAbove) := by369 simp_rw [adjugate_apply, det_succ_row _ j, updateRow_self, submatrix_updateRow_succAbove]370 rw [Fintype.sum_eq_single i fun h hjk => ?_, Pi.single_eq_same, mul_one]371 rw [Pi.single_eq_of_ne hjk, mul_zero, zero_mul]372373theorem adjugate_fin_two (A : Matrix (Fin 2) (Fin 2) α) :374 adjugate A = !![A 1 1, -A 0 1; -A 1 0, A 0 0] := by375 ext i j376 rw [adjugate_fin_succ_eq_det_submatrix]377 fin_cases i <;> fin_cases j <;> simp378379@[simp]380theorem adjugate_fin_two_of (a b c d : α) : adjugate !![a, b; c, d] = !![d, -b; -c, a] :=381 adjugate_fin_two _382383theorem adjugate_fin_three (A : Matrix (Fin 3) (Fin 3) α) :384 adjugate A =385 !![A 1 1 * A 2 2 - A 1 2 * A 2 1,386 -(A 0 1 * A 2 2) + A 0 2 * A 2 1,387 A 0 1 * A 1 2 - A 0 2 * A 1 1;388 -(A 1 0 * A 2 2) + A 1 2 * A 2 0,389 A 0 0 * A 2 2 - A 0 2 * A 2 0,390 -(A 0 0 * A 1 2) + A 0 2 * A 1 0;391 A 1 0 * A 2 1 - A 1 1 * A 2 0,392 -(A 0 0 * A 2 1) + A 0 1 * A 2 0,393 A 0 0 * A 1 1 - A 0 1 * A 1 0] := by394 ext i j395 rw [adjugate_fin_succ_eq_det_submatrix, det_fin_two]396 fin_cases i <;> fin_cases j <;> simp [Fin.succAbove, Fin.lt_def] <;> ring397398set_option linter.style.whitespace false in -- Use spaces to format a matrix.399@[simp]400theorem adjugate_fin_three_of (a b c d e f g h i : α) :401 adjugate !![a, b, c; d, e, f; g, h, i] =402 !![ e * i - f * h, -(b * i) + c * h, b * f - c * e;403 -(d * i) + f * g, a * i - c * g, -(a * f) + c * d;404 d * h - e * g, -(a * h) + b * g, a * e - b * d] :=405 adjugate_fin_three _406407theorem det_eq_sum_mul_adjugate_row (A : Matrix n n α) (i : n) :408 det A = ∑ j : n, A i j * adjugate A j i := by409 haveI : Nonempty n := ⟨i⟩410 obtain ⟨n', hn'⟩ := Nat.exists_eq_succ_of_ne_zero (Fintype.card_ne_zero : Fintype.card n ≠ 0)411 obtain ⟨e⟩ := Fintype.truncEquivFinOfCardEq hn'412 let A' := reindex e e A413 suffices det A' = ∑ j : Fin n'.succ, A' (e i) j * adjugate A' j (e i) by414 simp_rw [A', det_reindex_self, adjugate_reindex, reindex_apply, submatrix_apply, ← e.sum_comp,415 Equiv.symm_apply_apply] at this416 exact this417 rw [det_succ_row A' (e i)]418 simp_rw [mul_assoc, mul_left_comm _ (A' _ _), ← adjugate_fin_succ_eq_det_submatrix]419420theorem det_eq_sum_mul_adjugate_col (A : Matrix n n α) (j : n) :421 det A = ∑ i : n, A i j * adjugate A j i := by422 simpa only [det_transpose, ← adjugate_transpose] using! det_eq_sum_mul_adjugate_row Aᵀ j423424theorem adjugate_conjTranspose [StarRing α] (A : Matrix n n α) : A.adjugateᴴ = adjugate Aᴴ := by425 dsimp only [conjTranspose]426 have : Aᵀ.adjugate.map star = adjugate (Aᵀ.map star) := (starRingEnd α).map_adjugate Aᵀ427 rw [A.adjugate_transpose, this]428429theorem isRegular_of_isLeftRegular_det {A : Matrix n n α} (hA : IsLeftRegular A.det) :430 IsRegular A := by431 constructor432 · intro B C h433 refine hA.matrix ?_434 simp only at h ⊢435 rw [← Matrix.one_mul B, ← Matrix.one_mul C, ← Matrix.smul_mul, ← Matrix.smul_mul, ←436 adjugate_mul, Matrix.mul_assoc, Matrix.mul_assoc, h]437 · intro B C (h : B * A = C * A)438 refine hA.matrix ?_439 simp only440 rw [← Matrix.mul_one B, ← Matrix.mul_one C, ← Matrix.mul_smul, ← Matrix.mul_smul, ←441 mul_adjugate, ← Matrix.mul_assoc, ← Matrix.mul_assoc, h]442443theorem adjugate_mul_distrib_aux (A B : Matrix n n α) (hA : IsLeftRegular A.det)444 (hB : IsLeftRegular B.det) : adjugate (A * B) = adjugate B * adjugate A := by445 have hAB : IsLeftRegular (A * B).det := by446 rw [det_mul]447 exact hA.mul hB448 refine (isRegular_of_isLeftRegular_det hAB).left ?_449 simp only450 rw [mul_adjugate, Matrix.mul_assoc, ← Matrix.mul_assoc B, mul_adjugate,451 smul_mul, Matrix.one_mul, Matrix.mul_smul, mul_adjugate, smul_smul, mul_comm, ← det_mul]452453/-- Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3454-/455theorem adjugate_mul_distrib (A B : Matrix n n α) : adjugate (A * B) = adjugate B * adjugate A := by456 let g : Matrix n n α → Matrix n n α[X] := fun M =>457 M.map Polynomial.C + (Polynomial.X : α[X]) • (1 : Matrix n n α[X])458 let f' : Matrix n n α[X] →+* Matrix n n α := (Polynomial.evalRingHom 0).mapMatrix459 have f'_inv : ∀ M, f' (g M) = M := by460 intro461 ext462 simp [f', g]463 have f'_adj : ∀ M : Matrix n n α, f' (adjugate (g M)) = adjugate M := by464 intro465 rw [RingHom.map_adjugate, f'_inv]466 have f'_g_mul : ∀ M N : Matrix n n α, f' (g M * g N) = M * N := by467 intro M N468 rw [map_mul, f'_inv, f'_inv]469 have hu : ∀ M : Matrix n n α, IsRegular (g M).det := by470 intro M471 refine Polynomial.Monic.isRegular ?_472 simp only [g, Polynomial.Monic.def, ← Polynomial.leadingCoeff_det_X_one_add_C M, add_comm]473 rw [← f'_adj, ← f'_adj, ← f'_adj, ← f'.map_mul, ←474 adjugate_mul_distrib_aux _ _ (hu A).left (hu B).left, RingHom.map_adjugate,475 RingHom.map_adjugate, f'_inv, f'_g_mul]476477@[simp]478theorem adjugate_pow (A : Matrix n n α) (k : ℕ) : adjugate (A ^ k) = adjugate A ^ k := by479 induction k with480 | zero => simp481 | succ k IH => rw [pow_succ', adjugate_mul_distrib, IH, pow_succ]482483theorem det_smul_adjugate_adjugate (A : Matrix n n α) :484 det A • adjugate (adjugate A) = det A ^ (Fintype.card n - 1) • A := by485 have : A * (A.adjugate * A.adjugate.adjugate) =486 A * (A.det ^ (Fintype.card n - 1) • (1 : Matrix n n α)) := by487 rw [← adjugate_mul_distrib, adjugate_mul, adjugate_smul, adjugate_one]488 rwa [← Matrix.mul_assoc, mul_adjugate, Matrix.mul_smul, Matrix.mul_one, Matrix.smul_mul,489 Matrix.one_mul] at this490491/-- Note that this is not true for `Fintype.card n = 1` since `1 - 2 = 0` and not `-1`. -/492theorem adjugate_adjugate (A : Matrix n n α) (h : Fintype.card n ≠ 1) :493 adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A := by494 -- get rid of the `- 2`495 rcases h_card : Fintype.card n with _ | n'496 · subsingleton [Fintype.card_eq_zero_iff.mp h_card]497 cases n'498 · exact (h h_card).elim499 rw [← h_card]500 -- express `A` as an evaluation of a polynomial in n^2 variables, and solve in the polynomial ring501 -- where `A'.det` is non-zero.502 let A' := mvPolynomialX n n ℤ503 suffices adjugate (adjugate A') = det A' ^ (Fintype.card n - 2) • A' by504 rw [← mvPolynomialX_mapMatrix_aeval ℤ A, ← AlgHom.map_adjugate, ← AlgHom.map_adjugate, this,505 ← AlgHom.map_det, ← map_pow (MvPolynomial.aeval fun p : n × n ↦ A p.1 p.2),506 AlgHom.mapMatrix_apply, AlgHom.mapMatrix_apply, Matrix.map_smul' _ _ _ (map_mul _)]507 have h_card' : Fintype.card n - 2 + 1 = Fintype.card n - 1 := by simp [h_card]508 have is_reg : IsSMulRegular (MvPolynomial (n × n) ℤ) (det A') := fun x y =>509 mul_left_cancel₀ (det_mvPolynomialX_ne_zero n ℤ)510 apply is_reg.matrix511 simp only512 rw [smul_smul, ← pow_succ', h_card', det_smul_adjugate_adjugate]513514/-- A weaker version of `Matrix.adjugate_adjugate` that uses `Nontrivial`. -/515theorem adjugate_adjugate' (A : Matrix n n α) [Nontrivial n] :516 adjugate (adjugate A) = det A ^ (Fintype.card n - 2) • A :=517 adjugate_adjugate _ <| Fintype.one_lt_card.ne'518519end Adjugate520521end Matrix