The weak-* topology and convexity of the set of KMS states

For a real action α on a C⋆-algebra A and an inverse temperature β, kmsStates α β is the set K_β of β-KMS states of α, viewed in the weak-* dual WeakDual ℂ A.

Membership is characterised by the analytic KMS identity on entire analytic elements, mem_kmsStates_iff_forall_isEntireAnalytic. Since this identity is linear in the functional and is preserved under pointwise limits, it gives the following.

• IsKMSState.of_tendsto: a pointwise limit of β-KMS states is a β-KMS state as soon as it has norm one. The norm condition cannot be dropped for nonunital A, where states may converge weak-* to 0. In set form this is closure_kmsStates_inter_subset.
• kmsStates_subset_stateSpace: β-KMS states are states, so convex_kmsStates, the convexity of K_β, follows from that of the state space, with no identity element needed.
• For unital A, K_β is weak-* closed, isClosed_kmsStates, and weak-* compact, isCompact_kmsStates, as a closed subset of the weak-* compact state space.

References

Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 2, second edition, Theorem 5.3.30.

theorem TauCeti.CStarAction.IsKMSState.of_tendsto {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {ω : A →P[ℂ] ℂ} {ι : Type u_2} {l : Filter ι} [l.NeBot] {ω' : ι → A →P[ℂ] ℂ} (hω' : ∀ᶠ (i : ι) in l, α.IsKMSState β (ω' i)) (hlim : ∀ (a : A), Filter.Tendsto (fun (i : ι) => (ω' i) a) l (nhds (ω a))) (hnorm : ‖ω.toContinuousLinearMap‖ = 1) : α.IsKMSState β ω

Pointwise limits of KMS states. If β-KMS states converge pointwise to a positive functional of norm one, then the limit is a β-KMS state.

noncomputable def TauCeti.CStarAction.kmsStates {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (α : CStarAction (Multiplicative ℝ) A) (β : ℝ) : Set (WeakDual ℂ A)

The set K_β of β-KMS states of the real action α, as a subset of the weak-* dual of A.

theorem TauCeti.CStarAction.mem_kmsStates_iff {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : WeakDual ℂ A} : φ ∈ α.kmsStates β ↔ ∃ (ω : A →P[ℂ] ℂ), α.IsKMSState β ω ∧ StrongDual.toWeakDual ω.toContinuousLinearMap = φ

The elements of K_β are the images in the weak-* dual of the β-KMS states.

@[simp]

theorem TauCeti.CStarAction.toWeakDual_mem_kmsStates_iff {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {ω : A →P[ℂ] ℂ} : StrongDual.toWeakDual ω.toContinuousLinearMap ∈ α.kmsStates β ↔ α.IsKMSState β ω

A positive functional lies in K_β exactly when it is a β-KMS state.

theorem TauCeti.CStarAction.mem_kmsStates_iff_forall_isEntireAnalytic {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : WeakDual ℂ A} : φ ∈ α.kmsStates β ↔ (∀ (a : A), 0 ≤ a → 0 ≤ φ a) ∧ ‖WeakDual.toStrongDual φ‖ = 1 ∧ ∀ (a : A), α.IsEntireAnalytic a → ∀ (b : A), α.IsEntireAnalytic b → φ (a * α.entireExtension b (↑β * Complex.I)) = φ (b * a)

Analytic description of K_β. A functional lies in K_β exactly when it is positive, has norm one, and satisfies the analytic KMS identity φ (a α_{iβ}(b)) = φ (b a) for all entire analytic a and b.

theorem TauCeti.CStarAction.kmsStates_subset_stateSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} : α.kmsStates β ⊆ stateSpace A

β-KMS states are states.

theorem TauCeti.CStarAction.closure_kmsStates_inter_subset {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} : closure (α.kmsStates β) ∩ {φ : WeakDual ℂ A | ‖WeakDual.toStrongDual φ‖ = 1} ⊆ α.kmsStates β

Weak- limits of KMS states.* A weak-* limit point of β-KMS states which has norm one is a β-KMS state.

theorem TauCeti.CStarAction.convex_kmsStates {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} : Convex ℝ (α.kmsStates β)

Convexity of K_β. Convex combinations of β-KMS states are β-KMS states.

theorem TauCeti.CStarAction.isClosed_kmsStates {B : Type u_2} [CStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {α : CStarAction (Multiplicative ℝ) B} {β : ℝ} : IsClosed (α.kmsStates β)

For unital B, the set K_β of β-KMS states is weak-* closed.

theorem TauCeti.CStarAction.isCompact_kmsStates {B : Type u_2} [CStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {α : CStarAction (Multiplicative ℝ) B} {β : ℝ} : IsCompact (α.kmsStates β)

Weak- compactness of K_β.* For unital B, the set of β-KMS states is weak-* compact.