Norms of positive functionals on C⋆-algebras

Pullback along surjective homomorphisms

The norm of a positive functional on a possibly nonunital C⋆-algebra is its limit along any increasing approximate unit, Mathlib's PositiveContinuousLinearMap.tendsto_nhds_opNorm. A surjective star-algebra homomorphism carries increasing approximate units to increasing approximate units, so pulling a positive functional back along it does not change the norm, PositiveContinuousLinearMap.opNorm_comp_ofClass_of_surjective. In particular states pull back to states along quotient maps; without surjectivity the norm can drop, for instance to 0.

Positive functionals in the weak-* dual

For a functional φ : WeakDual ℂ A on a C⋆-algebra that is nonnegative on nonnegative elements, this file records the norm facts about positive functionals in the form used on the weak-* dual.

• WeakDual.monotone_toStrongDual_of_map_nonneg: φ is monotone.
• WeakDual.tendsto_approximateUnit_norm_of_map_nonneg: along the approximate unit, φ tends to its norm.
• WeakDual.norm_toStrongDual_eq_map_one_of_map_nonneg: if A is unital, the norm of φ is φ 1.

These are Mathlib's ContinuousLinearMap.monotone_iff_tendsto_nhds_opNorm and ContinuousLinearMap.monotone_iff_opNorm_eq_map_one, restated for WeakDual ℂ A.

Finally, WeakDual.ext_nonneg: a functional on a C⋆-algebra is determined by its values on nonnegative elements, since these span the algebra.

theorem PositiveContinuousLinearMap.opNorm_comp_ofClass_of_surjective {A : Type u_1} {B : Type u_2} {F : Type u_3} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] [NonUnitalCStarAlgebra B] [PartialOrder B] [StarOrderedRing B] [FunLike F A B] [NonUnitalAlgHomClass F ℂ A B] [StarHomClass F A B] (ω : B →P[ℂ] ℂ) (f : F) (hf : Function.Surjective ⇑f) : ‖(ω.comp (ofClass f)).toContinuousLinearMap‖ = ‖ω.toContinuousLinearMap‖

Pulling a positive functional back along a surjective star-algebra homomorphism of C⋆-algebras preserves its norm.

theorem WeakDual.ext_nonneg {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ ψ : WeakDual ℂ A} (h : ∀ (a : A), 0 ≤ a → φ a = ψ a) : φ = ψ

A functional on a C⋆-algebra is determined by its values on nonnegative elements, since these span the algebra. In particular two states that agree on nonnegative elements are equal.

theorem WeakDual.monotone_toStrongDual_of_map_nonneg {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : WeakDual ℂ A} (hφ : ∀ (a : A), 0 ≤ a → 0 ≤ φ a) : Monotone ⇑(toStrongDual φ)

A functional that is nonnegative on nonnegative elements is monotone.

theorem WeakDual.tendsto_approximateUnit_norm_of_map_nonneg {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : WeakDual ℂ A} (hφ : ∀ (a : A), 0 ≤ a → 0 ≤ φ a) : Filter.Tendsto (fun (e : A) => φ e) (CStarAlgebra.approximateUnit A) (nhds ↑‖toStrongDual φ‖)

Along the approximate unit, a functional that is nonnegative on nonnegative elements tends to its norm.

theorem WeakDual.norm_toStrongDual_eq_map_one_of_map_nonneg {A : Type u_1} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] {φ : WeakDual ℂ A} (hφ : ∀ (a : A), 0 ≤ a → 0 ≤ φ a) : ↑‖toStrongDual φ‖ = φ 1

On a unital C⋆-algebra, the norm of a functional that is nonnegative on nonnegative elements is its value at 1.