PhyslibAlpha.AlgebraicFramework.WStarAlgebra.Concrete

Let $H$ be a complex Hilbert space. Let $\mathcal{L}(H)$ denote the space of bounded linear operators on $H$, and let $\mathcal{S}_1(H)$ denote the space of trace-class operators on $H$ equipped with the trace norm $\|\cdot\|_1$. The linear isometry from $\mathcal{L}(H)$ to the continuous dual space $\mathcal{S}_1(H)^*$ that maps each operator $A \in \mathcal{L}(H)$ to the continuous linear functional $T \mapsto \text{Tr}(AT)$ is surjective.

Let $H$ be a complex Hilbert space. This definition is the isometric linear isomorphism $\mathcal{L}(H) \cong \mathcal{S}_1(H)^*$ between the space of bounded linear operators $\mathcal{L}(H)$ and the strong dual of the space of trace-class operators $\mathcal{S}_1(H)$. The map identifies each operator $A \in \mathcal{L}(H)$ with the continuous linear functional on $\mathcal{S}_1(H)$ defined by the trace pairing $T \mapsto \text{Tr}(AT)$.

Let $H$ be a complex Hilbert space. For any bounded linear operator $A \in \mathcal{L}(H)$, the value of the isometric linear isomorphism $\mathcal{L}(H) \cong \mathcal{S}_1(H)^*$ (denoted as `tracePairingEquiv`) at $A$ is equal to the trace pairing functional (denoted as `tracePairing A`), which maps each trace-class operator $T \in \mathcal{S}_1(H)$ to the trace of the product $AT$, denoted as $\text{Tr}(AT)$.

Let $H$ be a complex Hilbert space. The space of bounded linear operators $\mathcal{L}(H)$ (denoted `H →L[ℂ] H`) is equipped with a $W^*$-algebra structure. This structure is defined by taking the predual to be the Banach space of trace-class operators $\mathcal{S}_1(H)$ (denoted `TraceClass H`). The canonical isometric isomorphism $\mathcal{L}(H) \cong \mathcal{S}_1(H)^*$ is given by the trace pairing $A \mapsto (T \mapsto \text{Tr}(AT))$, where $A \in \mathcal{L}(H)$ and $T \in \mathcal{S}_1(H)$.