Trace of Hermitian Matrices

While the trace of a Hermitian matrix is, in informal math, typically just "the same as" a trace of a matrix that happens to be Hermitian - it is a real number, not a complex number. Or more generally, it is a self-adjoint element of the base StarAddMonoid.

Working directly with Matrix.trace then means that there would be constant casts between rings, chasing imaginary parts and inequalities and so on. By defining HermitianMat.trace as its own operation, we encapsulate the mess and give a clean interface.

The IsMaximalSelfAdjoint class is used so that (for example) for matrices over ℤ or ℝ, HermitianMat.trace works as well and is in fact defeq to Matrix.trace. For ℂ or RCLike, it uses the real part.

def HermitianMat.trace {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [AddGroup α] [StarAddMonoid α] [CommSemiring R] [Semiring α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : R

The trace of the matrix. This requires a IsMaximalSelfAdjoint R α instance, and then maps from HermitianMat n α to R. This means that the trace of (say) a HermitianMat n ℤ gives values in ℤ, but that the trace of a HermitianMat n ℂ gives values in ℝ. The fact that traces are "automatically" real reduces coercions down the line.

Equations

• A.trace = IsMaximalSelfAdjoint.selfadjMap (↑A).trace

theorem HermitianMat.trace_eq_trace {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [AddGroup α] [StarAddMonoid α] [CommSemiring R] [Semiring α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : (algebraMap R α) A.trace = (↑A).trace

HermitianMat.trace reduces to Matrix.trace in the algebra.

@[simp]

theorem HermitianMat.trace_smul {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [AddGroup α] [StarAddMonoid α] [CommSemiring R] [Semiring α] [Algebra R α] [IsMaximalSelfAdjoint R α] [StarModule R α] (A : HermitianMat n α) (r : R) : (r • A).trace = r * A.trace

@[simp]

theorem HermitianMat.trace_zero {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [CommSemiring R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] : trace 0 = 0

@[simp]

theorem HermitianMat.trace_add {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [CommSemiring R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : (A + B).trace = A.trace + B.trace

@[simp]

theorem HermitianMat.trace_neg {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat n α) : (-A).trace = -A.trace

@[simp]

theorem HermitianMat.trace_sub {R : Type u_1} {n : Type u_2} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [CommRing R] [Ring α] [StarAddMonoid α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A B : HermitianMat n α) : (A - B).trace = A.trace - B.trace

theorem Matrix.IsHermitian.isSelfAdjoint_trace {n : Type u_2} {α : Type u_4} [Fintype n] [CommRing α] [StarRing α] {A : Matrix n n α} (hA : A.IsHermitian) : IsSelfAdjoint A.trace

@[simp]

theorem HermitianMat.trace_kronecker {R : Type u_1} {n : Type u_2} {m : Type u_3} {α : Type u_4} [Star R] [TrivialStar R] [Fintype n] [Fintype m] [CommRing R] [CommRing α] [StarRing α] [Algebra R α] [IsMaximalSelfAdjoint R α] (A : HermitianMat m α) (B : HermitianMat n α) [FaithfulSMul R α] : (A.kronecker B).trace = A.trace * B.trace

@[simp]

theorem HermitianMat.trace_eq_trace_trivial {n : Type u_2} [Fintype n] (A : HermitianMat n ℝ) : A.trace = (↑A).trace

HermitianMat.trace reduces to Matrix.trace when the elements are a TrivialStar.

instance HermitianMat.FiniteDimensional {n : Type u_5} {𝕜 : Type u_7} [Fintype n] [RCLike 𝕜] : _root_.FiniteDimensional ℝ (HermitianMat n 𝕜)

theorem HermitianMat.trace_eq_re_trace {n : Type u_5} {𝕜 : Type u_7} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.trace = RCLike.re (↑A).trace

@[simp]

theorem HermitianMat.trace_eq_trace_rc {n : Type u_5} {𝕜 : Type u_7} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : ↑A.trace = (↑A).trace

HermitianMat.trace reduces to Matrix.trace when the elements are RCLike.

theorem HermitianMat.trace_diagonal {T : Type u_8} [Fintype T] [DecidableEq T] (f : T → ℝ) : (diagonal f).trace = ∑ i : T, f i

theorem HermitianMat.sum_eigenvalues_eq_trace {n : Type u_5} {𝕜 : Type u_7} [Fintype n] [RCLike 𝕜] [DecidableEq n] (A : HermitianMat n 𝕜) : ∑ i : n, ⋯.eigenvalues i = A.trace

theorem HermitianMat.trace_eq_zero_iff {n : Type u_5} {𝕜 : Type u_7} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.trace = 0 ↔ (↑A).trace = 0

theorem HermitianMat.trace_eq_one_iff {n : Type u_5} {𝕜 : Type u_7} [Fintype n] [RCLike 𝕜] (A : HermitianMat n 𝕜) : A.trace = 1 ↔ (↑A).trace = 1

@[simp]

theorem HermitianMat.trace_reindex {n : Type u_5} {m : Type u_6} [Fintype n] [Fintype m] (A : HermitianMat n ℂ) (e : n ≃ m) : (A.reindex e).trace = A.trace