Physlib

PhyslibAlpha.ProbabilisticTheory.StarAlgebra.Traciality

Tracial states and weights

i. Overview

A state `ω` is tracial when `ω (a⋆ a) = ω (a a⋆)`. For a complex-linear functional this is equivalent to `f (a b) = f (b a)`. A finite tracial weight gives a tracial state.

ii. Key results

- `UnitalPositiveLinearMap.IsTracial` : tracial states. - `Weight.IsTracial` : tracial weights. - `LinearMap.isTracial_iff_star_mul_self_eq_mul_star_self` : a complex functional is tracial iff `f (a⋆ a) = f (a a⋆)`.

4 declarations

definition

ww is a tracial weight (w(x∗x)=w(xx∗)w(x^* x) = w(x x^*))

Let AA be a ∗*-algebra and ww be a weight on AA. The property that ww is tracial signifies that for any x∈Ax \in A, the value assigned by the weight's finite positive-linear extension to x∗xx^* x is equal to the value assigned to xx∗x x^*. That is, w(x∗x)=w(xx∗)w(x^* x) = w(x x^*).

theorem

A finite tracial weight ww satisfies ϕw(x∗x)=ϕw(xx∗)\phi_w(x^* x) = \phi_w(x x^*)

Let ww be a finite and tracial weight on a ∗*-algebra AA. Let ϕw\phi_w denote the real positive-linear extension of ww (given by `toPositiveLinearMap`). For any element x∈Ax \in A, the extension satisfies the tracial property: ϕw(x∗x)=ϕw(xx∗)\phi_w(x^* x) = \phi_w(x x^*) where x∗x^* denotes the adjoint (or star) of xx.

definition

Tracial property of a state ss

A state ss, which is a unital positive linear map on a ∗*-algebra AA, is tracial if for every element x∈Ax \in A, the equality s(xx∗)=s(x∗x)s(x x^*) = s(x^* x) holds.

theorem

The state of a tracial weight satisfies s(x∗x)=s(xx∗)s(x^* x) = s(x x^*)

Let ww be a weight on a ∗*-algebra AA. If ww is a state and is tracial, then for any x∈Ax \in A, the induced state ss satisfies s(x∗x)=s(xx∗)s(x^* x) = s(x x^*).