Trace of a matrix

This file defines the trace of a matrix, the map sending a matrix to the sum of its diagonal entries.

See also LinearAlgebra.Trace for the trace of an endomorphism.

Tags

matrix, trace, diagonal

def Matrix.trace {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (A : Matrix n n R) : R

The trace of a square matrix. For more bundled versions, see:

• Matrix.traceAddMonoidHom
• Matrix.traceLinearMap

Equations

• Matrix.trace A = Finset.sum Finset.univ fun (i : n) => Matrix.diag A i

theorem Matrix.trace_diagonal {R : Type u_6} [AddCommMonoid R] {o : Type u_8} [Fintype o] [DecidableEq o] (d : o → R) : Matrix.trace (Matrix.diagonal d) = Finset.sum Finset.univ fun (i : o) => d i

@[simp]

theorem Matrix.trace_zero (n : Type u_3) (R : Type u_6) [Fintype n] [AddCommMonoid R] : Matrix.trace 0 = 0

@[simp]

theorem Matrix.trace_eq_zero_of_isEmpty {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] [IsEmpty n] (A : Matrix n n R) : Matrix.trace A = 0

@[simp]

theorem Matrix.trace_add {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (A : Matrix n n R) (B : Matrix n n R) : Matrix.trace (A + B) = Matrix.trace A + Matrix.trace B

@[simp]

theorem Matrix.trace_smul {n : Type u_3} {α : Type u_5} {R : Type u_6} [Fintype n] [AddCommMonoid R] [Monoid α] [DistribMulAction α R] (r : α) (A : Matrix n n R) : Matrix.trace (r • A) = r • Matrix.trace A

@[simp]

theorem Matrix.trace_transpose {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (A : Matrix n n R) : Matrix.trace (Matrix.transpose A) = Matrix.trace A

@[simp]

theorem Matrix.trace_conjTranspose {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] [StarAddMonoid R] (A : Matrix n n R) : Matrix.trace (Matrix.conjTranspose A) = star (Matrix.trace A)

@[simp]

theorem Matrix.traceAddMonoidHom_apply (n : Type u_3) (R : Type u_6) [Fintype n] [AddCommMonoid R] (A : Matrix n n R) : (Matrix.traceAddMonoidHom n R) A = Matrix.trace A

def Matrix.traceAddMonoidHom (n : Type u_3) (R : Type u_6) [Fintype n] [AddCommMonoid R] : Matrix n n R →+ R

Matrix.trace as an AddMonoidHom

Equations

• Matrix.traceAddMonoidHom n R = { toZeroHom := { toFun := Matrix.trace, map_zero' := ⋯ }, map_add' := ⋯ }

@[simp]

theorem Matrix.traceLinearMap_apply (n : Type u_3) (α : Type u_5) (R : Type u_6) [Fintype n] [AddCommMonoid R] [Semiring α] [Module α R] (A : Matrix n n R) : (Matrix.traceLinearMap n α R) A = Matrix.trace A

def Matrix.traceLinearMap (n : Type u_3) (α : Type u_5) (R : Type u_6) [Fintype n] [AddCommMonoid R] [Semiring α] [Module α R] : Matrix n n R →ₗ[α] R

Matrix.trace as a LinearMap

Equations

• Matrix.traceLinearMap n α R = { toAddHom := { toFun := Matrix.trace, map_add' := ⋯ }, map_smul' := ⋯ }

@[simp]

theorem Matrix.trace_list_sum {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (l : List (Matrix n n R)) : Matrix.trace (List.sum l) = List.sum (List.map Matrix.trace l)

@[simp]

theorem Matrix.trace_multiset_sum {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (s : Multiset (Matrix n n R)) : Matrix.trace (Multiset.sum s) = Multiset.sum (Multiset.map Matrix.trace s)

@[simp]

theorem Matrix.trace_sum {ι : Type u_1} {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommMonoid R] (s : Finset ι) (f : ι → Matrix n n R) : Matrix.trace (Finset.sum s fun (i : ι) => f i) = Finset.sum s fun (i : ι) => Matrix.trace (f i)

theorem AddMonoidHom.map_trace {n : Type u_3} {R : Type u_6} {S : Type u_7} [Fintype n] [AddCommMonoid R] [AddCommMonoid S] (f : R →+ S) (A : Matrix n n R) : f (Matrix.trace A) = Matrix.trace ((AddMonoidHom.mapMatrix f) A)

theorem Matrix.trace_blockDiagonal {n : Type u_3} {p : Type u_4} {R : Type u_6} [Fintype n] [Fintype p] [AddCommMonoid R] [DecidableEq p] (M : p → Matrix n n R) : Matrix.trace (Matrix.blockDiagonal M) = Finset.sum Finset.univ fun (i : p) => Matrix.trace (M i)

theorem Matrix.trace_blockDiagonal' {p : Type u_4} {R : Type u_6} [Fintype p] [AddCommMonoid R] [DecidableEq p] {m : p → Type u_8} [(i : p) → Fintype (m i)] (M : (i : p) → Matrix (m i) (m i) R) : Matrix.trace (Matrix.blockDiagonal' M) = Finset.sum Finset.univ fun (i : p) => Matrix.trace (M i)

@[simp]

theorem Matrix.trace_sub {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommGroup R] (A : Matrix n n R) (B : Matrix n n R) : Matrix.trace (A - B) = Matrix.trace A - Matrix.trace B

@[simp]

theorem Matrix.trace_neg {n : Type u_3} {R : Type u_6} [Fintype n] [AddCommGroup R] (A : Matrix n n R) : Matrix.trace (-A) = -Matrix.trace A

@[simp]

theorem Matrix.trace_one {n : Type u_3} {R : Type u_6} [Fintype n] [DecidableEq n] [AddCommMonoidWithOne R] : Matrix.trace 1 = ↑(Fintype.card n)

@[simp]

theorem Matrix.trace_transpose_mul {m : Type u_2} {n : Type u_3} {R : Type u_6} [Fintype m] [Fintype n] [AddCommMonoid R] [Mul R] (A : Matrix m n R) (B : Matrix n m R) : Matrix.trace (Matrix.transpose A * Matrix.transpose B) = Matrix.trace (A * B)

theorem Matrix.trace_mul_comm {m : Type u_2} {n : Type u_3} {R : Type u_6} [Fintype m] [Fintype n] [AddCommMonoid R] [CommSemigroup R] (A : Matrix m n R) (B : Matrix n m R) : Matrix.trace (A * B) = Matrix.trace (B * A)

theorem Matrix.trace_mul_cycle {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [Fintype m] [Fintype n] [Fintype p] [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) : Matrix.trace (A * B * C) = Matrix.trace (C * A * B)

theorem Matrix.trace_mul_cycle' {m : Type u_2} {n : Type u_3} {p : Type u_4} {R : Type u_6} [Fintype m] [Fintype n] [Fintype p] [NonUnitalCommSemiring R] (A : Matrix m n R) (B : Matrix n p R) (C : Matrix p m R) : Matrix.trace (A * (B * C)) = Matrix.trace (C * (A * B))

@[simp]

theorem Matrix.trace_col_mul_row {n : Type u_3} {R : Type u_6} [Fintype n] [NonUnitalNonAssocSemiring R] (a : n → R) (b : n → R) : Matrix.trace (Matrix.col a * Matrix.row b) = Matrix.dotProduct a b

theorem Matrix.trace_submatrix_succ {R : Type u_6} {n : ℕ} [NonUnitalNonAssocSemiring R] (M : Matrix (Fin (Nat.succ n)) (Fin (Nat.succ n)) R) : M 0 0 + Matrix.trace (Matrix.submatrix M Fin.succ Fin.succ) = Matrix.trace M

Special cases for Fin n

While simp [Fin.sum_univ_succ] can prove these, we include them for convenience and consistency with Matrix.det_fin_two etc.

theorem Matrix.trace_fin_zero {R : Type u_6} [AddCommMonoid R] (A : Matrix (Fin 0) (Fin 0) R) : Matrix.trace A = 0

theorem Matrix.trace_fin_one {R : Type u_6} [AddCommMonoid R] (A : Matrix (Fin 1) (Fin 1) R) : Matrix.trace A = A 0 0

theorem Matrix.trace_fin_two {R : Type u_6} [AddCommMonoid R] (A : Matrix (Fin 2) (Fin 2) R) : Matrix.trace A = A 0 0 + A 1 1

theorem Matrix.trace_fin_three {R : Type u_6} [AddCommMonoid R] (A : Matrix (Fin 3) (Fin 3) R) : Matrix.trace A = A 0 0 + A 1 1 + A 2 2