Documentation

Mathlib.LinearAlgebra.Matrix.Adjugate

Cramer's rule and adjugate matrices #

The adjugate matrix is the transpose of the cofactor matrix. It is calculated with Cramer's rule, which we introduce first. The vectors returned by Cramer's rule are given by the linear map cramer, which sends a matrix A and vector b to the vector consisting of the determinant of replacing the ith column of A with b at index i (written as (A.update_column i b).det). Using Cramer's rule, we can compute for each matrix A the matrix adjugate A. The entries of the adjugate are the minors of A. Instead of defining a minor by deleting row i and column j of A, we replace the ith row of A with the jth basis vector; the resulting matrix has the same determinant but more importantly equals Cramer's rule applied to A and the jth basis vector, simplifying the subsequent proofs. We prove the adjugate behaves like det A • A⁻¹.

Main definitions #

References #

Tags #

cramer, cramer's rule, adjugate

cramer section #

Introduce the linear map cramer with values defined by cramerMap. After defining cramerMap and showing it is linear, we will restrict our proofs to using cramer.

def Matrix.cramerMap {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : nα) (i : n) :
α

cramerMap A b i is the determinant of the matrix A with column i replaced with b, and thus cramerMap A b is the vector output by Cramer's rule on A and b.

If A * x = b has a unique solution in x, cramerMap A sends the vector b to A.det • x. Otherwise, the outcome of cramerMap is well-defined but not necessarily useful.

Equations
  • A.cramerMap b i = (A.updateColumn i b).det
Instances For
    theorem Matrix.cramerMap_is_linear {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) :
    IsLinearMap α fun (b : nα) => A.cramerMap b i
    theorem Matrix.cramer_is_linear {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
    IsLinearMap α A.cramerMap
    def Matrix.cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
    (nα) →ₗ[α] nα

    cramer A b i is the determinant of the matrix A with column i replaced with b, and thus cramer A b is the vector output by Cramer's rule on A and b.

    If A * x = b has a unique solution in x, cramer A sends the vector b to A.det • x. Otherwise, the outcome of cramer is well-defined but not necessarily useful.

    Equations
    Instances For
      theorem Matrix.cramer_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : nα) (i : n) :
      A.cramer b i = (A.updateColumn i b).det
      theorem Matrix.cramer_transpose_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : nα) (i : n) :
      A.transpose.cramer b i = (A.updateRow i b).det
      theorem Matrix.cramer_transpose_row_self {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) :
      A.transpose.cramer (A i) = Pi.single i A.det
      theorem Matrix.cramer_row_self {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : nα) (i : n) (h : ∀ (j : n), b j = A j i) :
      A.cramer b = Pi.single i A.det
      @[simp]
      theorem Matrix.cramer_one {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] :
      theorem Matrix.cramer_smul {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (r : α) (A : Matrix n n α) :
      (r A).cramer = r ^ (Fintype.card n - 1) A.cramer
      @[simp]
      theorem Matrix.cramer_subsingleton_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Subsingleton n] (A : Matrix n n α) (b : nα) (i : n) :
      A.cramer b i = b i
      theorem Matrix.cramer_zero {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Nontrivial n] :
      theorem Matrix.sum_cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) {β : Type u_1} (s : Finset β) (f : βnα) :
      xs, A.cramer (f x) = A.cramer (∑ xs, f x)

      Use linearity of cramer to take it out of a summation.

      theorem Matrix.sum_cramer_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) {β : Type u_1} (s : Finset β) (f : nβα) (i : n) :
      xs, A.cramer (fun (j : n) => f j x) i = A.cramer (fun (j : n) => xs, f j x) i

      Use linearity of cramer and vector evaluation to take cramer A _ i out of a summation.

      theorem Matrix.cramer_submatrix_equiv {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (A : Matrix m m α) (e : n m) (b : nα) :
      (A.submatrix e e).cramer b = A.cramer (b e.symm) e
      theorem Matrix.cramer_reindex {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (e : m n) (A : Matrix m m α) (b : nα) :
      ((Matrix.reindex e e) A).cramer b = A.cramer (b e) e.symm

      adjugate section #

      Define the adjugate matrix and a few equations. These will hold for any matrix over a commutative ring.

      def Matrix.adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
      Matrix n n α

      The adjugate matrix is the transpose of the cofactor matrix.

      Typically, the cofactor matrix is defined by taking minors, i.e. the determinant of the matrix with a row and column removed. However, the proof of mul_adjugate becomes a lot easier if we use the matrix replacing a column with a basis vector, since it allows us to use facts about the cramer map.

      Equations
      • A.adjugate = Matrix.of fun (i : n) => A.transpose.cramer (Pi.single i 1)
      Instances For
        theorem Matrix.adjugate_def {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
        A.adjugate = Matrix.of fun (i : n) => A.transpose.cramer (Pi.single i 1)
        theorem Matrix.adjugate_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) (j : n) :
        A.adjugate i j = (A.updateRow j (Pi.single i 1)).det
        theorem Matrix.adjugate_transpose {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
        A.adjugate.transpose = A.transpose.adjugate
        @[simp]
        theorem Matrix.adjugate_submatrix_equiv_self {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (e : n m) (A : Matrix m m α) :
        (A.submatrix e e).adjugate = A.adjugate.submatrix e e
        theorem Matrix.adjugate_reindex {m : Type u} {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [DecidableEq m] [Fintype m] [CommRing α] (e : m n) (A : Matrix m m α) :
        ((Matrix.reindex e e) A).adjugate = (Matrix.reindex e e) A.adjugate
        theorem Matrix.cramer_eq_adjugate_mulVec {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : nα) :
        A.cramer b = A.adjugate.mulVec b

        Since the map b ↦ cramer A b is linear in b, it must be multiplication by some matrix. This matrix is A.adjugate.

        theorem Matrix.mul_adjugate_apply {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) (j : n) (k : n) :
        A i k * A.adjugate k j = A.transpose.cramer (Pi.single k (A i k)) j
        theorem Matrix.mul_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
        A * A.adjugate = A.det 1
        theorem Matrix.adjugate_mul {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
        A.adjugate * A = A.det 1
        theorem Matrix.adjugate_smul {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (r : α) (A : Matrix n n α) :
        (r A).adjugate = r ^ (Fintype.card n - 1) A.adjugate
        @[simp]
        theorem Matrix.mulVec_cramer {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (b : nα) :
        A.mulVec (A.cramer b) = A.det b

        A stronger form of Cramer's rule that allows us to solve some instances of A * x = b even if the determinant is not a unit. A sufficient (but still not necessary) condition is that A.det divides b.

        theorem Matrix.adjugate_subsingleton {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Subsingleton n] (A : Matrix n n α) :
        A.adjugate = 1
        theorem Matrix.adjugate_eq_one_of_card_eq_one {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] {A : Matrix n n α} (h : Fintype.card n = 1) :
        A.adjugate = 1
        @[simp]
        theorem Matrix.adjugate_zero {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [Nontrivial n] :
        @[simp]
        theorem Matrix.adjugate_one {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] :
        @[simp]
        theorem Matrix.adjugate_diagonal {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (v : nα) :
        (Matrix.diagonal v).adjugate = Matrix.diagonal fun (i : n) => jFinset.univ.erase i, v j
        theorem RingHom.map_adjugate {n : Type v} [DecidableEq n] [Fintype n] {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] (f : R →+* S) (M : Matrix n n R) :
        f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate
        theorem AlgHom.map_adjugate {n : Type v} [DecidableEq n] [Fintype n] {R : Type u_1} {A : Type u_2} {B : Type u_3} [CommSemiring R] [CommRing A] [CommRing B] [Algebra R A] [Algebra R B] (f : A →ₐ[R] B) (M : Matrix n n A) :
        f.mapMatrix M.adjugate = (f.mapMatrix M).adjugate
        theorem Matrix.det_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
        A.adjugate.det = A.det ^ (Fintype.card n - 1)
        @[simp]
        theorem Matrix.adjugate_fin_zero {α : Type w} [CommRing α] (A : Matrix (Fin 0) (Fin 0) α) :
        A.adjugate = 0
        @[simp]
        theorem Matrix.adjugate_fin_one {α : Type w} [CommRing α] (A : Matrix (Fin 1) (Fin 1) α) :
        A.adjugate = 1
        theorem Matrix.adjugate_fin_succ_eq_det_submatrix {α : Type w} [CommRing α] {n : } (A : Matrix (Fin n.succ) (Fin n.succ) α) (i : Fin n.succ) (j : Fin n.succ) :
        A.adjugate i j = (-1) ^ (j + i) * (A.submatrix j.succAbove i.succAbove).det
        theorem Matrix.adjugate_fin_two {α : Type w} [CommRing α] (A : Matrix (Fin 2) (Fin 2) α) :
        A.adjugate = !![A 1 1, -A 0 1; -A 1 0, A 0 0]
        @[simp]
        theorem Matrix.adjugate_fin_two_of {α : Type w} [CommRing α] (a : α) (b : α) (c : α) (d : α) :
        !![a, b; c, d].adjugate = !![d, -b; -c, a]
        theorem Matrix.adjugate_fin_three {α : Type w} [CommRing α] (A : Matrix (Fin 3) (Fin 3) α) :
        A.adjugate = !![A 1 1 * A 2 2 - A 1 2 * A 2 1, -(A 0 1 * A 2 2) + A 0 2 * A 2 1, A 0 1 * A 1 2 - A 0 2 * A 1 1; -(A 1 0 * A 2 2) + A 1 2 * A 2 0, A 0 0 * A 2 2 - A 0 2 * A 2 0, -(A 0 0 * A 1 2) + A 0 2 * A 1 0; A 1 0 * A 2 1 - A 1 1 * A 2 0, -(A 0 0 * A 2 1) + A 0 1 * A 2 0, A 0 0 * A 1 1 - A 0 1 * A 1 0]
        @[simp]
        theorem Matrix.adjugate_fin_three_of {α : Type w} [CommRing α] (a : α) (b : α) (c : α) (d : α) (e : α) (f : α) (g : α) (h : α) (i : α) :
        !![a, b, c; d, e, f; g, h, i].adjugate = !![e * i - f * h, -(b * i) + c * h, b * f - c * e; -(d * i) + f * g, a * i - c * g, -(a * f) + c * d; d * h - e * g, -(a * h) + b * g, a * e - b * d]
        theorem Matrix.det_eq_sum_mul_adjugate_row {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (i : n) :
        A.det = j : n, A i j * A.adjugate j i
        theorem Matrix.det_eq_sum_mul_adjugate_col {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (j : n) :
        A.det = i : n, A i j * A.adjugate j i
        theorem Matrix.adjugate_conjTranspose {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] [StarRing α] (A : Matrix n n α) :
        A.adjugate.conjTranspose = A.conjTranspose.adjugate
        theorem Matrix.isRegular_of_isLeftRegular_det {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] {A : Matrix n n α} (hA : IsLeftRegular A.det) :
        theorem Matrix.adjugate_mul_distrib_aux {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) (hA : IsLeftRegular A.det) (hB : IsLeftRegular B.det) :
        (A * B).adjugate = B.adjugate * A.adjugate
        theorem Matrix.adjugate_mul_distrib {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (B : Matrix n n α) :
        (A * B).adjugate = B.adjugate * A.adjugate

        Proof follows from "The trace Cayley-Hamilton theorem" by Darij Grinberg, Section 5.3

        @[simp]
        theorem Matrix.adjugate_pow {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (k : ) :
        (A ^ k).adjugate = A.adjugate ^ k
        theorem Matrix.det_smul_adjugate_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) :
        A.det A.adjugate.adjugate = A.det ^ (Fintype.card n - 1) A
        theorem Matrix.adjugate_adjugate {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) (h : Fintype.card n 1) :
        A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) A

        Note that this is not true for Fintype.card n = 1 since 1 - 2 = 0 and not -1.

        theorem Matrix.adjugate_adjugate' {n : Type v} {α : Type w} [DecidableEq n] [Fintype n] [CommRing α] (A : Matrix n n α) [Nontrivial n] :
        A.adjugate.adjugate = A.det ^ (Fintype.card n - 2) A

        A weaker version of Matrix.adjugate_adjugate that uses Nontrivial.