The trace of a continuous endomorphism as a continuous linear functional

On a finite-dimensional Hausdorff topological vector 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[𝕜] 𝕜, where V →L[𝕜] V carries its usual topology of uniform convergence on bounded sets (the operator-norm topology when V is normed). Continuity is not something the algebraic LinearMap.trace can see: it holds because V →L[𝕜] V is again a finite-dimensional Hausdorff topological vector space over the complete field 𝕜, and every linear map out of such a space is continuous.

This bundled form is what lets the trace commute with limits, continuity and integrals: it is used, for instance, for the continuity of the character of a continuous representation, to move the trace through a Bochner integral of operators, and to define the divergence of a vector field as the trace of its derivative.

noncomputable def TauCeti.traceCLM (𝕜 : Type u_1) (V : Type u_2) [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] : (V →L[𝕜] V) →L[𝕜] 𝕜

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

@[simp]

theorem TauCeti.traceCLM_apply {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space 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.

theorem ContinuousLinearMap.traceCLM_comp_comm {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] (S T : V →L[𝕜] V) : (TauCeti.traceCLM 𝕜 V) (S ∘SL T) = (TauCeti.traceCLM 𝕜 V) (T ∘SL S)

The trace of a composition does not depend on the order of the factors: tr (S ∘ T) = tr (T ∘ S).

theorem ContinuousLinearEquiv.traceCLM_comp_comp_symm {𝕜 : Type u_1} {V : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [AddCommGroup V] [Module 𝕜 V] [TopologicalSpace V] [IsTopologicalAddGroup V] [ContinuousSMul 𝕜 V] [T2Space V] [FiniteDimensional 𝕜 V] {W : Type u_3} [AddCommGroup W] [Module 𝕜 W] [TopologicalSpace W] [IsTopologicalAddGroup W] [ContinuousSMul 𝕜 W] [T2Space W] [FiniteDimensional 𝕜 W] (e : V ≃L[𝕜] W) (T : V →L[𝕜] V) : (TauCeti.traceCLM 𝕜 W) (↑e ∘SL T ∘SL ↑e.symm) = (TauCeti.traceCLM 𝕜 V) T

The trace is invariant under conjugation by a continuous linear equivalence: tr (e ∘ T ∘ e⁻¹) = tr T.