KMS states of C⋆-algebra dynamics

Let α be a point-norm continuous real action on a possibly nonunital C⋆-algebra A, and let β be a real number, the inverse temperature. For a continuous linear functional φ and a b : A, a KMS function is a bounded continuous function F on the closed strip between the real axis and the line im z = β, holomorphic on the open strip, with boundary values

F t = φ (a α_t(b)) and F (t + iβ) = φ (α_t(b) a).

A β-KMS state is a state, that is a positive continuous functional of norm one, admitting a KMS function for every pair a, b. Positivity refers to the C⋆-algebra order on A, the order making it a StarOrderedRing. The positivity of a state is used only for pullback along surjective equivariant homomorphisms, where it guarantees that the norm is preserved.

The strip lies above the real axis for β > 0 and below it for β < 0. For β = 0 it is the real axis itself, and the 0-KMS states are exactly the tracial states, isKMSState_zero_iff; at β = 0 the definition does not force invariance under α. On a commutative algebra every state is a 0-KMS state, isKMSState_zero_iff_of_comm.

The KMS function of a pair is unique, IsKMSFunction.eqOn, by Schwarz reflection across the real axis, and it is bounded on the strip by ‖φ‖ ‖a‖ ‖b‖, IsKMSFunction.norm_le, by the Phragmén–Lindelöf principle. When b is entire analytic, the KMS function is z ↦ φ (a α_z(b)); this gives the analytic form of the KMS condition, ω (a α_{iβ}(b)) = ω (b a), IsKMSState.apply_mul_entireExtension_mul_I. The converse analytic criterion and its specialization to the trivial action are proved in TauCeti.Analysis.CStarAlgebra.Action.KMS.Dense.

For β ≠ 0 every β-KMS state is invariant under the dynamics, IsKMSState.apply_action. Replacing a by an approximate unit in the analytic KMS identity gives ω (α_{iβ}(b)) = ω b for entire analytic b, so z ↦ ω (α_z(b)) is an entire function with period iβ. It is bounded on a strip, hence on ℂ, and therefore constant by Liouville's theorem, IsKMSState.apply_entireExtension. Invariance on all of A follows by density of the entire analytic elements. No identity element is needed.

KMS functions and KMS states pull back along an equivariant homomorphism π: a KMS function of the pair π a, π b for φ is one of the pair a, b for φ ∘ π, Hom.isKMSFunction_iff, so ω ∘ π is a β-KMS state whenever ω is and ω ∘ π has norm one, IsKMSState.comp. Along a surjective π, for instance a quotient map by an invariant ideal, the norm condition is automatic, and a positive functional ω of the quotient dynamics is a β-KMS state exactly when ω ∘ π is, isKMSState_comp_iff_of_surjective. For the inclusion of a closed invariant star subalgebra this gives restriction of KMS states, IsKMSState.restrict, which needs the norm condition: the restriction of a state need not be a state.

References

Bratteli--Robinson, Operator Algebras and Quantum Statistical Mechanics 2, second edition, Definition 5.3.1 and Proposition 5.3.7, for the strip and analytic forms of the KMS condition, and Proposition 5.3.3 for the invariance of KMS states.

structure TauCeti.CStarAction.IsKMSFunction {A : Type u_1} [NonUnitalCStarAlgebra A] (α : CStarAction (Multiplicative ℝ) A) (β : ℝ) (φ : A →L[ℂ] ℂ) (a b : A) (F : ℂ → ℂ) : Prop

F is a KMS function at inverse temperature β for the functional φ and the pair a, b: it is bounded and continuous on the closed strip between the real axis and the line im z = β, holomorphic on the open strip, and has the boundary values F t = φ (a α_t(b)) and F (t + iβ) = φ (α_t(b) a).

• continuousOn : ContinuousOn F (Complex.im ⁻¹' Set.uIcc 0 β)
• differentiableOn : DifferentiableOn ℂ F (Complex.im ⁻¹' Set.uIoo 0 β)
• isBounded_image : Bornology.IsBounded (F '' Complex.im ⁻¹' Set.uIcc 0 β)
• apply_ofReal (t : ℝ) : F ↑t = φ (a * (α (Multiplicative.ofAdd t)) b)
• apply_ofReal_add_mul_I (t : ℝ) : F (↑t + ↑β * Complex.I) = φ ((α (Multiplicative.ofAdd t)) b * a)

theorem TauCeti.CStarAction.IsKMSFunction.eqOn_of_apply_ofReal {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} {F G : ℂ → ℂ} (hF : α.IsKMSFunction β φ a b F) (hGc : ContinuousOn G (Complex.im ⁻¹' Set.uIcc 0 β)) (hGd : DifferentiableOn ℂ G (Complex.im ⁻¹' Set.uIoo 0 β)) (hG : ∀ (t : ℝ), G ↑t = φ (a * (α (Multiplicative.ofAdd t)) b)) : Set.EqOn F G (Complex.im ⁻¹' Set.uIcc 0 β)

A KMS function agrees on the strip with any function that is continuous on the closed strip, holomorphic on the open strip and has the same values on the real axis.

theorem TauCeti.CStarAction.IsKMSFunction.eqOn {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} {F G : ℂ → ℂ} (hF : α.IsKMSFunction β φ a b F) (hG : α.IsKMSFunction β φ a b G) : Set.EqOn F G (Complex.im ⁻¹' Set.uIcc 0 β)

Uniqueness of KMS functions. Two KMS functions of the same pair agree on the strip.

theorem TauCeti.CStarAction.IsKMSFunction.sub_right {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} {F G : ℂ → ℂ} {c : A} (hF : α.IsKMSFunction β φ a b F) (hG : α.IsKMSFunction β φ a c G) : α.IsKMSFunction β φ a (b - c) fun (z : ℂ) => F z - G z

Subtracting KMS functions with the same first coefficient subtracts the second coefficients.

theorem TauCeti.CStarAction.IsKMSFunction.norm_le {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} {F : ℂ → ℂ} (hF : α.IsKMSFunction β φ a b F) {z : ℂ} (hz : z ∈ Complex.im ⁻¹' Set.uIcc 0 β) : ‖F z‖ ≤ ‖φ‖ * ‖a‖ * ‖b‖

Norm bound. A KMS function is bounded on the strip by ‖φ‖ ‖a‖ ‖b‖.

theorem TauCeti.CStarAction.IsKMSFunction.apply_eq_apply_mul_entireExtension {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} {F : ℂ → ℂ} (hF : α.IsKMSFunction β φ a b F) (hb : α.IsEntireAnalytic b) {z : ℂ} (hz : z ∈ Complex.im ⁻¹' Set.uIcc 0 β) : F z = φ (a * α.entireExtension b z)

For an entire analytic b, the KMS function of the pair a, b is z ↦ φ (a α_z(b)).

theorem TauCeti.CStarAction.IsKMSFunction.apply_mul_entireExtension_ofReal_add_mul_I {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} {F : ℂ → ℂ} (hF : α.IsKMSFunction β φ a b F) (hb : α.IsEntireAnalytic b) (t : ℝ) : φ (a * α.entireExtension b (↑t + ↑β * Complex.I)) = φ ((α (Multiplicative.ofAdd t)) b * a)

Analytic KMS identity. If the pair a, b has a KMS function and b is entire analytic, then φ (a α_{t + iβ}(b)) = φ (α_t(b) a) for every real t.

theorem TauCeti.CStarAction.isKMSFunction_apply_mul_entireExtension_iff {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {φ : A →L[ℂ] ℂ} {a b : A} (hb : α.IsEntireAnalytic b) : (α.IsKMSFunction β φ a b fun (z : ℂ) => φ (a * α.entireExtension b z)) ↔ ∀ (t : ℝ), φ (a * α.entireExtension b (↑t + ↑β * Complex.I)) = φ ((α (Multiplicative.ofAdd t)) b * a)

For an entire analytic b, the function z ↦ φ (a α_z(b)) is a KMS function of the pair a, b exactly when it satisfies the analytic KMS identity on the line im z = β.

theorem TauCeti.CStarAction.Hom.isKMSFunction_iff {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {a b : A} {F : ℂ → ℂ} {B : Type u_2} [NonUnitalCStarAlgebra B] {γ : CStarAction (Multiplicative ℝ) B} (π : α.Hom γ) {φ : B →L[ℂ] ℂ} {ψ : A →L[ℂ] ℂ} (hψ : ∀ (x : A), ψ x = φ (π x)) : α.IsKMSFunction β ψ a b F ↔ γ.IsKMSFunction β φ (π a) (π b) F

Pullback of KMS functions. Let π be an equivariant homomorphism and let ψ be the pullback φ ∘ π of a functional φ. Then F is a KMS function of the pair a, b for ψ exactly when it is a KMS function of the pair π a, π b for φ.

structure TauCeti.CStarAction.IsKMSState {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (α : CStarAction (Multiplicative ℝ) A) (β : ℝ) (ω : A →P[ℂ] ℂ) : Prop

A β-KMS state of the real action α is a state ω, a positive continuous functional of norm one, such that every pair a, b has a KMS function at inverse temperature β: a bounded continuous function on the closed strip between the real axis and the line im z = β, holomorphic on the open strip, with boundary values ω (a α_t(b)) and ω (α_t(b) a). Positivity is for the C⋆-algebra order, so StarOrderedRing A is assumed although no field uses it.

• norm_eq_one : ‖ω.toContinuousLinearMap‖ = 1
• exists_isKMSFunction (a b : A) : ∃ (F : ℂ → ℂ), α.IsKMSFunction β ω.toContinuousLinearMap a b F

theorem TauCeti.CStarAction.IsKMSState.apply_mul_entireExtension_mul_I {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {b : A} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} (hω : α.IsKMSState β ω) (a : A) (hb : α.IsEntireAnalytic b) : ω (a * α.entireExtension b (↑β * Complex.I)) = ω (b * a)

Analytic form of the KMS condition. For a β-KMS state ω and an entire analytic b, ω (a α_{iβ}(b)) = ω (b a).

theorem TauCeti.CStarAction.isKMSState_zero_iff {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} : α.IsKMSState 0 ω ↔ ‖ω.toContinuousLinearMap‖ = 1 ∧ ∀ (a b : A), ω (a * b) = ω (b * a)

The 0-KMS states are exactly the tracial states.

theorem TauCeti.CStarAction.isKMSState_zero_iff_of_comm {B : Type u_2} [NonUnitalCommCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {γ : CStarAction (Multiplicative ℝ) B} {ψ : B →P[ℂ] ℂ} : γ.IsKMSState 0 ψ ↔ ‖ψ.toContinuousLinearMap‖ = 1

On a commutative C⋆-algebra every state is a 0-KMS state, for every dynamics.

Invariance of KMS states

theorem TauCeti.CStarAction.IsKMSState.apply_entireExtension {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} {b : A} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} (hω : α.IsKMSState β ω) (hβ : β ≠ 0) (hb : α.IsEntireAnalytic b) (z : ℂ) : ω (α.entireExtension b z) = ω b

KMS states are invariant on entire analytic elements. For β ≠ 0, a β-KMS state ω satisfies ω (α_z(b)) = ω b for every entire analytic b and every complex time z.

theorem TauCeti.CStarAction.IsKMSState.apply_action {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} (hω : α.IsKMSState β ω) (hβ : β ≠ 0) (t : Multiplicative ℝ) (a : A) : ω ((α t) a) = ω a

KMS states are invariant. For β ≠ 0, every β-KMS state ω is invariant under the dynamics: ω (α_t(a)) = ω a. At β = 0 the KMS states are the tracial states, which need not be invariant.

Pullback along equivariant homomorphisms

theorem TauCeti.CStarAction.IsKMSState.comp {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {B : Type u_2} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {γ : CStarAction (Multiplicative ℝ) B} {ω : B →P[ℂ] ℂ} (hω : γ.IsKMSState β ω) (π : α.Hom γ) (hnorm : ‖(ω.comp (PositiveContinuousLinearMap.ofClass π)).toContinuousLinearMap‖ = 1) : α.IsKMSState β (ω.comp (PositiveContinuousLinearMap.ofClass π))

Pullback of KMS states. If π is an equivariant homomorphism and ω is a β-KMS state, then ω ∘ π is a β-KMS state as soon as it has norm one.

theorem TauCeti.CStarAction.IsKMSState.comp_of_surjective {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {B : Type u_2} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {γ : CStarAction (Multiplicative ℝ) B} {ω : B →P[ℂ] ℂ} (hω : γ.IsKMSState β ω) (π : α.Hom γ) (hπ : Function.Surjective ⇑π) : α.IsKMSState β (ω.comp (PositiveContinuousLinearMap.ofClass π))

Pullback of KMS states along quotients. If π is a surjective equivariant homomorphism and ω is a β-KMS state, then ω ∘ π is a β-KMS state.

theorem TauCeti.CStarAction.isKMSState_comp_iff_of_surjective {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {B : Type u_2} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] {γ : CStarAction (Multiplicative ℝ) B} {ω : B →P[ℂ] ℂ} (π : α.Hom γ) (hπ : Function.Surjective ⇑π) : α.IsKMSState β (ω.comp (PositiveContinuousLinearMap.ofClass π)) ↔ γ.IsKMSState β ω

Along a surjective equivariant homomorphism π, the β-KMS states of the quotient dynamics are exactly the positive functionals ω whose pullback ω ∘ π is a β-KMS state.

theorem TauCeti.CStarAction.IsKMSState.restrict {A : Type u_1} [NonUnitalCStarAlgebra A] {α : CStarAction (Multiplicative ℝ) A} {β : ℝ} [PartialOrder A] [StarOrderedRing A] {ω : A →P[ℂ] ℂ} (hω : α.IsKMSState β ω) {S : NonUnitalStarSubalgebra ℂ A} (hS : IsInvariant (fun (t : Multiplicative ℝ) (a : A) => (α t) a) ↑S) [IsClosed ↑S] (hωS : ‖(ω.comp (PositiveContinuousLinearMap.ofClass hS.subtypeHom)).toContinuousLinearMap‖ = 1) : hS.restrict.IsKMSState β (ω.comp (PositiveContinuousLinearMap.ofClass hS.subtypeHom))

Restriction of KMS states. The restriction of a β-KMS state to a closed invariant star subalgebra S is a β-KMS state of the restricted dynamics as soon as it has norm one.