Trace-free self-adjoint endomorphisms

For a finite-dimensional inner product space E over 𝕜 = ℝ or ℂ, the trace of the adjoint of an endomorphism is the conjugate of its trace (LinearMap.trace_adjoint), so the trace pairing tr (T U) of two self-adjoint endomorphisms is real. Consequently the trace-free part T - (tr T / n) Id, n = dim E, of an endomorphism T (TauCeti.traceFreePart) is again self-adjoint when T is. It is the projection of T onto the trace-free endomorphisms along the scalars: it is idempotent, kills Id and fixes every trace-free T, and it is orthogonal for the trace pairing (T, U) ↦ tr (T U).

Over ℂ, the trace-free self-adjoint endomorphisms form a real subspace TauCeti.traceFreeSelfAdjoint E of dimension n² - 1: the self-adjoint endomorphisms are a real form of all endomorphisms, so they have real dimension n², and the real trace is a nonzero real functional on them. In complex dimension two this is the three-dimensional real space {T : T* = T, tr T = 0}, the target of Clifford multiplication by imaginary self-dual two-forms on the positive half-spinors of a four-dimensional Spinᶜ structure, on which the Hilbert–Schmidt pairing tr (T* U) = tr (T U) is real.

Main definitions

• TauCeti.traceFreePart 𝕜 E: the linear projection T ↦ T - (tr T / n) Id onto the trace-free endomorphisms.
• TauCeti.traceFreeSelfAdjoint E: the real subspace of trace-free self-adjoint endomorphisms of a complex inner product space.

Main results

• LinearMap.trace_adjoint, ContinuousLinearMap.trace_adjoint: tr T* = conj (tr T).
• LinearMap.trace_eq_zero_of_inner_left_eq_neg: a skew-adjoint endomorphism of a real inner product space has trace zero.
• IsSelfAdjoint.conj_trace, IsSelfAdjoint.conj_trace_mul: the trace of a self-adjoint endomorphism, and the trace pairing tr (T U) of two of them, are real.
• ContinuousLinearMap.traceCLM_symmPart_comp: over ℝ, only the symmetric part of A enters the trace pairing tr (A M) with a self-adjoint M.
• InnerProductSpace.trace_rankOne_mul, InnerProductSpace.trace_mul_rankOne: the trace pairing of T with a rank-one endomorphism, tr (x y* T) = tr (T x y*) = ⟪y, T x⟫.
• TauCeti.trace_traceFreePart, TauCeti.traceFreePart_of_trace_eq_zero, TauCeti.traceFreePart_id: traceFreePart projects onto the trace-free endomorphisms along the scalars.
• TauCeti.trace_traceFreePart_mul: the projection is orthogonal for the trace pairing.
• TauCeti.finrank_traceFreeSelfAdjoint: the trace-free self-adjoint endomorphisms of a complex inner product space of dimension n have real dimension n² - 1.

@[simp]

theorem LinearMap.trace_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →ₗ[𝕜] E) : (trace 𝕜 E) (adjoint T) = (starRingEnd 𝕜) ((trace 𝕜 E) T)

The trace of the adjoint of an endomorphism is the conjugate of its trace.

theorem LinearMap.trace_eq_zero_of_inner_left_eq_neg {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] {A : V →ₗ[ℝ] V} (hA : ∀ (u w : V), inner ℝ (A u) w = -inner ℝ u (A w)) : (trace ℝ V) A = 0

A skew-adjoint endomorphism of a finite-dimensional real inner product space, one with ⟪A u, w⟫ = -⟪u, A w⟫, has trace zero.

@[simp]

theorem ContinuousLinearMap.trace_adjoint {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] (T : E →L[𝕜] E) : (LinearMap.trace 𝕜 E) ↑(adjoint T) = (starRingEnd 𝕜) ((LinearMap.trace 𝕜 E) ↑T)

The trace of the adjoint of an endomorphism is the conjugate of its trace.

theorem IsSelfAdjoint.conj_trace {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) : (starRingEnd 𝕜) ((LinearMap.trace 𝕜 E) ↑T) = (LinearMap.trace 𝕜 E) ↑T

The trace of a self-adjoint endomorphism is real.

theorem IsSelfAdjoint.conj_trace_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] {T U : E →L[𝕜] E} (hT : IsSelfAdjoint T) (hU : IsSelfAdjoint U) : (starRingEnd 𝕜) ((LinearMap.trace 𝕜 E) (↑T * ↑U)) = (LinearMap.trace 𝕜 E) (↑T * ↑U)

The trace pairing tr (T U) of two self-adjoint endomorphisms is real.

theorem ContinuousLinearMap.traceCLM_symmPart_comp {V : Type u_3} [NormedAddCommGroup V] [InnerProductSpace ℝ V] [FiniteDimensional ℝ V] (A M : V →L[ℝ] V) (hM : adjoint M = M) : (TauCeti.traceCLM ℝ V) ((2⁻¹ • (A + adjoint A)) ∘SL M) = (TauCeti.traceCLM ℝ V) (A ∘SL M)

Only the symmetric part (A + A†) / 2 of A enters the trace pairing tr (A M) with a self-adjoint endomorphism M of a real inner product space.

theorem InnerProductSpace.trace_mul_rankOne {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) (x y : E) : (LinearMap.trace 𝕜 E) (↑T * ↑(((rankOne 𝕜) x) y)) = inner 𝕜 y (T x)

The trace pairing of T with a rank-one endomorphism: tr (T x y*) = ⟪y, T x⟫.

theorem InnerProductSpace.trace_rankOne_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (x y : E) (T : E →L[𝕜] E) : (LinearMap.trace 𝕜 E) (↑(((rankOne 𝕜) x) y) * ↑T) = inner 𝕜 y (T x)

The trace pairing of a rank-one endomorphism with T: tr (x y* T) = ⟪y, T x⟫.

noncomputable def TauCeti.traceFreePart (𝕜 : Type u_1) (E : Type u_2) [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] : (E →L[𝕜] E) →ₗ[𝕜] E →L[𝕜] E

The trace-free part T - (tr T / n) Id of an endomorphism T of an n-dimensional space, as a linear projection onto the trace-free endomorphisms.

theorem TauCeti.traceFreePart_apply {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] (T : E →L[𝕜] E) : (traceFreePart 𝕜 E) T = T - ((LinearMap.trace 𝕜 E) ↑T / ↑(Module.finrank 𝕜 E)) • ContinuousLinearMap.id 𝕜 E

traceFreePart T = T - (tr T / n) Id.

@[simp]

theorem TauCeti.trace_traceFreePart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) : (LinearMap.trace 𝕜 E) ↑((traceFreePart 𝕜 E) T) = 0

The trace-free part of an endomorphism is trace free.

theorem TauCeti.traceFreePart_of_trace_eq_zero {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {T : E →L[𝕜] E} (hT : (LinearMap.trace 𝕜 E) ↑T = 0) : (traceFreePart 𝕜 E) T = T

traceFreePart fixes every trace-free endomorphism.

@[simp]

theorem TauCeti.traceFreePart_id {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] : (traceFreePart 𝕜 E) (ContinuousLinearMap.id 𝕜 E) = 0

traceFreePart kills the scalars.

@[simp]

theorem TauCeti.traceFreePart_traceFreePart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] (T : E →L[𝕜] E) : (traceFreePart 𝕜 E) ((traceFreePart 𝕜 E) T) = (traceFreePart 𝕜 E) T

traceFreePart is idempotent.

theorem TauCeti.trace_traceFreePart_mul {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] {U : E →L[𝕜] E} (hU : (LinearMap.trace 𝕜 E) ↑U = 0) (T : E →L[𝕜] E) : (LinearMap.trace 𝕜 E) (↑((traceFreePart 𝕜 E) T) * ↑U) = (LinearMap.trace 𝕜 E) (↑T * ↑U)

traceFreePart is orthogonal for the trace pairing: against a trace-free U, the trace-free part of T pairs as T does.

theorem IsSelfAdjoint.traceFreePart {𝕜 : Type u_1} {E : Type u_2} [RCLike 𝕜] [NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [CompleteSpace E] {T : E →L[𝕜] E} (hT : IsSelfAdjoint T) : IsSelfAdjoint ((TauCeti.traceFreePart 𝕜 E) T)

The trace-free part of a self-adjoint endomorphism is self-adjoint.

def TauCeti.traceFreeSelfAdjoint (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] : Submodule ℝ (E →L[ℂ] E)

The real subspace {T : T* = T, tr T = 0} of trace-free self-adjoint endomorphisms of a complex inner product space.

@[simp]

theorem TauCeti.mem_traceFreeSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] {T : E →L[ℂ] E} : T ∈ traceFreeSelfAdjoint E ↔ IsSelfAdjoint T ∧ (LinearMap.trace ℂ E) ↑T = 0

An endomorphism lies in traceFreeSelfAdjoint E exactly when it is self-adjoint and trace free.

theorem IsSelfAdjoint.traceFreePart_mem {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [FiniteDimensional ℂ E] {T : E →L[ℂ] E} (hT : IsSelfAdjoint T) : (TauCeti.traceFreePart ℂ E) T ∈ TauCeti.traceFreeSelfAdjoint E

The trace-free part of a self-adjoint endomorphism is a trace-free self-adjoint endomorphism.

theorem TauCeti.finrank_traceFreeSelfAdjoint {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℂ E] [CompleteSpace E] [FiniteDimensional ℂ E] : Module.finrank ℝ ↥(traceFreeSelfAdjoint E) = Module.finrank ℂ E ^ 2 - 1

The trace-free self-adjoint endomorphisms of an n-dimensional complex inner product space form a real vector space of dimension n² - 1.