The state space of a C⋆-algebra

A state of a possibly nonunital C⋆-algebra A is a positive linear functional of norm one. This file defines the state space TauCeti.stateSpace A as a subset of the weak-* dual WeakDual ℂ A, so that convexity, closedness and compactness refer to the weak-* topology.

• TauCeti.mem_stateSpace_iff_exists_positiveLinearMap: the states are exactly the positive linear maps A →ₚ[ℂ] ℂ of norm one, through the automatic continuity of positive maps.
• TauCeti.convex_stateSpace: the state space is convex. No unit is needed, because the norm of a positive functional is its limit along an approximate unit.
• TauCeti.pullbackFunctional: precomposition with a star homomorphism, as a continuous complex-linear map of weak-* duals. By TauCeti.mapsTo_pullbackFunctional_stateSpace_of_surjective and TauCeti.mapsTo_pullbackFunctional_stateSpace it restricts to an affine map of state spaces along surjective star homomorphisms and along unital star homomorphisms.

For unital A:

• TauCeti.mem_stateSpace_iff_map_one: a positive functional is a state exactly when φ 1 = 1, and TauCeti.mem_stateSpace_iff_norm_eq_one_and_map_one: a functional is a state exactly when ‖φ‖ = φ 1 = 1, with positivity then automatic.
• TauCeti.isCompact_stateSpace: the state space is weak-* compact, by Banach–Alaoglu.
• TauCeti.stateSpace_nonempty: if A is nonzero it has a state, by Hahn–Banach. The state space of ℂ is the single functional z ↦ z, TauCeti.stateSpace_complex.
• TauCeti.closure_convexHull_extremePoints_stateSpace: the state space is the weak-* closed convex hull of its extreme points, the pure states, by the Krein–Milman theorem; in particular a nonzero unital C⋆-algebra has a pure state, TauCeti.extremePoints_stateSpace_nonempty.

Without a unit the state space is still closed in the norm topology of the dual, TauCeti.isClosed_preimage_toWeakDual_stateSpace, but in general it is not weak-* closed: on c₀ the point evaluations are states that converge weak-* to 0.

References

Jesse Peterson, Notes on operator algebras, Section 4.1.

def TauCeti.stateSpace (A : Type u_1) [NonUnitalCStarAlgebra A] [PartialOrder A] : Set (WeakDual ℂ A)

The state space of a C⋆-algebra A: the functionals in the weak-* dual of A that are nonnegative on nonnegative elements and have norm one. The results about it take the order on A to be the C⋆-algebra order, through StarOrderedRing A.

theorem TauCeti.mem_stateSpace_iff {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {φ : WeakDual ℂ A} : φ ∈ stateSpace A ↔ (∀ (a : A), 0 ≤ a → 0 ≤ φ a) ∧ ‖WeakDual.toStrongDual φ‖ = 1

Membership in the state space unfolds to positivity and norm one.

theorem TauCeti.map_nonneg_of_mem_stateSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {φ : WeakDual ℂ A} (hφ : φ ∈ stateSpace A) {a : A} (ha : 0 ≤ a) : 0 ≤ φ a

A state is nonnegative on nonnegative elements.

theorem TauCeti.norm_toStrongDual_of_mem_stateSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {φ : WeakDual ℂ A} (hφ : φ ∈ stateSpace A) : ‖WeakDual.toStrongDual φ‖ = 1

A state has norm one.

theorem TauCeti.norm_apply_le_of_mem_stateSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {φ : WeakDual ℂ A} (hφ : φ ∈ stateSpace A) (a : A) : ‖φ a‖ ≤ ‖a‖

A state is contractive.

theorem TauCeti.isClosed_preimage_toWeakDual_stateSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] : IsClosed (⇑StrongDual.toWeakDual ⁻¹' stateSpace A)

In the norm topology of the continuous dual, the state space is closed.

@[simp]

theorem PositiveContinuousLinearMap.toWeakDual_mem_stateSpace_iff {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (ω : A →P[ℂ] ℂ) : StrongDual.toWeakDual ω.toContinuousLinearMap ∈ TauCeti.stateSpace A ↔ ‖ω.toContinuousLinearMap‖ = 1

A positive continuous linear functional is a state exactly when its norm is one.

theorem TauCeti.mem_stateSpace_iff_exists_positiveLinearMap {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] {φ : WeakDual ℂ A} [StarOrderedRing A] : φ ∈ stateSpace A ↔ ∃ (ω : A →ₚ[ℂ] ℂ), ‖(PositiveContinuousLinearMap.ofClass ω).toContinuousLinearMap‖ = 1 ∧ StrongDual.toWeakDual (PositiveContinuousLinearMap.ofClass ω).toContinuousLinearMap = φ

The states of A are exactly the positive linear maps A →ₚ[ℂ] ℂ of norm one, viewed in the weak-* dual.

theorem TauCeti.convex_stateSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : Convex ℝ (stateSpace A)

Convexity of the state space. Real convex combinations of states are states.

noncomputable def TauCeti.pullbackFunctional (A : Type u_1) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {B : Type u_2} {F : Type u_3} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) : WeakDual ℂ B →L[ℂ] WeakDual ℂ A

Precomposition of functionals with a star homomorphism f : A → B, as a weak-* continuous complex-linear map WeakDual ℂ B →L[ℂ] WeakDual ℂ A; it is continuous because each evaluation φ ↦ φ (f a) is. On states it is the pullback of states along f, which is affine when f is surjective or unital.

@[simp]

theorem TauCeti.pullbackFunctional_apply {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {B : Type u_2} {F : Type u_3} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) (φ : WeakDual ℂ B) (a : A) : ((pullbackFunctional A f) φ) a = φ (f a)

The pullback of a functional along f evaluates as φ ∘ f.

theorem TauCeti.mapsTo_pullbackFunctional_stateSpace_of_surjective {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {B : Type u_2} {F : Type u_3} [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) (hf : Function.Surjective ⇑f) : Set.MapsTo (⇑(pullbackFunctional A f)) (stateSpace B) (stateSpace A)

Pullback of states along a surjective star homomorphism. Composing a state of B with a surjective star homomorphism A → B gives a state of A. Without surjectivity the norm of the composite can drop, for instance to 0.

theorem TauCeti.mem_stateSpace_iff_map_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : WeakDual ℂ A} : φ ∈ stateSpace A ↔ (∀ (a : A), 0 ≤ a → 0 ≤ φ a) ∧ φ 1 = 1

On a unital C⋆-algebra, a functional that is nonnegative on nonnegative elements is a state exactly when it takes the value 1 at 1.

theorem TauCeti.map_one_of_mem_stateSpace {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : WeakDual ℂ A} (hφ : φ ∈ stateSpace A) : φ 1 = 1

A state of a unital C⋆-algebra takes the value 1 at 1.

theorem TauCeti.mem_stateSpace_iff_norm_eq_one_and_map_one {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : WeakDual ℂ A} : φ ∈ stateSpace A ↔ ‖WeakDual.toStrongDual φ‖ = 1 ∧ φ 1 = 1

On a unital C⋆-algebra, a functional is a state exactly when ‖φ‖ = φ 1 = 1. Positivity is then automatic: it follows from φ 1 = ‖φ‖ = 1.

theorem TauCeti.isClosed_stateSpace {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : IsClosed (stateSpace A)

For unital A, the state space is weak-* closed.

theorem TauCeti.isCompact_stateSpace {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : IsCompact (stateSpace A)

Weak- compactness of the state space.* For unital A, the state space is weak-* compact, by the Banach–Alaoglu theorem.

theorem TauCeti.stateSpace_nonempty {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] : (stateSpace A).Nonempty

Existence of states. A nonzero unital C⋆-algebra has a state.

theorem TauCeti.closure_convexHull_extremePoints_stateSpace {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] : closure ((convexHull ℝ) (Set.extremePoints ℝ (stateSpace A))) = stateSpace A

Krein–Milman for states. For unital A, the state space is the weak-* closed convex hull of its extreme points, the pure states.

theorem TauCeti.extremePoints_stateSpace_nonempty {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [Nontrivial A] : (Set.extremePoints ℝ (stateSpace A)).Nonempty

Existence of pure states. A nonzero unital C⋆-algebra has an extreme state.

theorem TauCeti.stateSpace_complex : stateSpace ℂ = {StrongDual.toWeakDual (ContinuousLinearMap.id ℂ ℂ)}

The only state of ℂ is the identity functional.

theorem TauCeti.mapsTo_pullbackFunctional_stateSpace {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {B : Type u_2} {F : Type u_3} [CStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [AlgHomClass F ℂ A B] [StarHomClass F A B] (f : F) : Set.MapsTo (⇑(pullbackFunctional A f)) (stateSpace B) (stateSpace A)

Pullback of states along a unital star homomorphism. Composing a state of B with a unital star homomorphism A → B gives a state of A.