The trace of a continuous endomorphism as a continuous linear functional

On a finite-dimensional normed space V over a complete nontrivially normed field 𝕜, the trace T ↦ trace T of a continuous endomorphism is itself a continuous linear functional TauCeti.traceCLM 𝕜 V : (V →L[𝕜] V) →L[𝕜] 𝕜. Continuity is not something the algebraic LinearMap.trace can see: it holds because V →L[𝕜] V is finite-dimensional over the complete field 𝕜, and every linear map out of such a space is continuous.

This bundled form is what lets the trace pass through the continuity of a representation (TauCeti/RepresentationTheory/Continuous/Character.lean) and commute with a Bochner integral (TauCeti/RepresentationTheory/Compact/Intertwiner/Basic.lean); both need the trace as a continuous linear map rather than as a bare linear map.

noncomputable def TauCeti.traceCLM (𝕜 : Type u_1) (V : Type u_2) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] : (V →L[𝕜] V) →L[𝕜] 𝕜

The trace of a continuous endomorphism of a finite-dimensional space, as a continuous linear functional. Continuity is automatic: V →L[𝕜] V is finite-dimensional over the complete field 𝕜, and every linear map out of such a space is continuous.

Equations

• TauCeti.traceCLM 𝕜 V = LinearMap.toContinuousLinearMap (LinearMap.trace 𝕜 V ∘ₗ ContinuousLinearMap.coeLM 𝕜)

@[simp]

theorem TauCeti.traceCLM_apply {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [NormedAddCommGroup V] [NormedSpace 𝕜 V] [FiniteDimensional 𝕜 V] (T : V →L[𝕜] V) : (traceCLM 𝕜 V) T = (LinearMap.trace 𝕜 V) ↑T

TauCeti.traceCLM evaluates to the trace of the underlying linear map.