The GNS (Gelfand-Naimark-Segal) construction

This file contains the constructions and definitions that produce a ⋆-homomorphism from an arbitrary C⋆-algebra into the algebra of bounded linear operators on an appropriately constructed Hilbert space.

Main results

• f.PreGNS : a type synonym of A that bundles in a fixed positive linear functional f so that we can construct an inner product and inner product-induced norm.
• f.GNS : the Hilbert space completion of f.preGNS.
• f.gnsNonUnitalStarAlgHom : The non-unital ⋆-homomorphism from a non-unital A into the bounded linear operators on f.GNS.
• f.gnsStarAlgHom : The unital ⋆-homomorphism from a unital A into the bounded linear operators on f.GNS.

TODO

• Explicitly construct a unit norm cyclic vector ζ such that a ↦ ⟨(f.gns(NonUnital)StarAlgHom a) * ζ, ,ζ⟩ is a state on A for both unital and non-unital cases.

def PositiveLinearMap.PreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) : Type u_1

The Gelfand─Naimark─Segal (GNS) space constructed from a positive linear functional on a non-unital C⋆-algebra. This is a type synonym of A.

This space is only a pre-inner product space. Its Hilbert space completion is PositiveLinearMap.GNS.

Equations

• f.PreGNS = A

instance PositiveLinearMap.instAddCommGroupPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) : AddCommGroup f.PreGNS

Equations

• f.instAddCommGroupPreGNS = inferInstanceAs (AddCommGroup A)

instance PositiveLinearMap.instModuleComplexPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) : Module ℂ f.PreGNS

Equations

• f.instModuleComplexPreGNS = inferInstanceAs (Module ℂ A)

def PositiveLinearMap.toPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) : A ≃ₗ[ℂ] f.PreGNS

The map from the C⋆-algebra to the GNS space, as a linear equivalence.

Equations

• f.toPreGNS = LinearEquiv.refl ℂ A

def PositiveLinearMap.ofPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) : f.PreGNS ≃ₗ[ℂ] A

The map from the GNS space to the C⋆-algebra, as a linear equivalence.

Equations

• f.ofPreGNS = f.toPreGNS.symm

@[simp]

theorem PositiveLinearMap.toPreGNS_ofPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) (a : f.PreGNS) : f.toPreGNS (f.ofPreGNS a) = a

@[simp]

theorem PositiveLinearMap.ofPreGNS_toPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) (a : A) : f.ofPreGNS (f.toPreGNS a) = a

@[reducible, inline]

abbrev PositiveLinearMap.preGNSpreInnerProdSpace {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] : PreInnerProductSpace.Core ℂ f.PreGNS

The (semi-)inner product space whose elements are the elements of A, but which has an inner product-induced norm that is different from the norm on A and which is induced by f.

Equations

• f.preGNSpreInnerProdSpace = { inner := fun (a b : f.PreGNS) => f (star (f.ofPreGNS a) * f.ofPreGNS b), conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯ }

noncomputable instance PositiveLinearMap.instSeminormedAddCommGroupPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] : SeminormedAddCommGroup f.PreGNS

Equations

• f.instSeminormedAddCommGroupPreGNS = InnerProductSpace.Core.toSeminormedAddCommGroup

noncomputable instance PositiveLinearMap.instInnerProductSpaceComplexPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] : InnerProductSpace ℂ f.PreGNS

Equations

• f.instInnerProductSpaceComplexPreGNS = InnerProductSpace.ofCore f.preGNSpreInnerProdSpace

theorem PositiveLinearMap.preGNS_inner_def {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] (a b : f.PreGNS) : inner ℂ a b = f (star (f.ofPreGNS a) * f.ofPreGNS b)

theorem PositiveLinearMap.preGNS_norm_def {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] (a : f.PreGNS) : ‖a‖ = √(f (star (f.ofPreGNS a) * f.ofPreGNS a)).re

theorem PositiveLinearMap.preGNS_norm_sq {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] (a : f.PreGNS) : ↑‖a‖ ^ 2 = f (star (f.ofPreGNS a) * f.ofPreGNS a)

@[reducible, inline]

abbrev PositiveLinearMap.GNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] : Type u_1

The Hilbert space constructed from a positive linear functional on a C⋆-algebra.

Equations

• f.GNS = UniformSpace.Completion f.PreGNS

noncomputable def PositiveLinearMap.leftMulMapPreGNS {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] (a : A) : f.PreGNS →L[ℂ] f.PreGNS

The continuous linear map from a C⋆-algebra A to the PositiveLinearMap.preGNS space induced by a positive linear functional f : A →ₚ[ℂ] ℂ. This map is given by left-multiplication by a: x ↦ f.toPreGNS (a * f.ofPreGNS x).

This is the map that is lifted to the completion of f.PreGNS (i.e. f.GNS) in order to define gnsNonUnitalStarAlgHom.

Equations

• f.leftMulMapPreGNS a = (↑f.toPreGNS ∘ₗ ↑((ContinuousLinearMap.mul ℂ A) a) ∘ₗ ↑f.ofPreGNS).mkContinuous ‖a‖ ⋯

@[simp]

theorem PositiveLinearMap.leftMulMapPreGNS_apply {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] (a : A) (a✝ : f.PreGNS) : (f.leftMulMapPreGNS a) a✝ = f.toPreGNS (a * f.ofPreGNS a✝)

@[simp]

theorem PositiveLinearMap.leftMulMapPreGNS_mul_eq_comp {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] (a b : A) : f.leftMulMapPreGNS (a * b) = (f.leftMulMapPreGNS a).comp (f.leftMulMapPreGNS b)

noncomputable def PositiveLinearMap.gnsNonUnitalStarAlgHom {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] : A →⋆ₙₐ[ℂ] f.GNS →L[ℂ] f.GNS

The non-unital ⋆-homomorphism/⋆-representation of A into the algebra of bounded operators on a Hilbert space that is constructed from a positive linear functional f on a possibly non-unital C⋆-algebra.

Equations

• f.gnsNonUnitalStarAlgHom = { toFun := fun (a : A) => (f.leftMulMapPreGNS a).completion, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

theorem PositiveLinearMap.gnsNonUnitalStarAlgHom_apply {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] {a : A} : f.gnsNonUnitalStarAlgHom a = (f.leftMulMapPreGNS a).completion

@[simp]

theorem PositiveLinearMap.gnsNonUnitalStarAlgHom_apply_coe {A : Type u_1} [NonUnitalCStarAlgebra A] [PartialOrder A] (f : A →ₚ[ℂ] ℂ) [StarOrderedRing A] {a : A} {b : f.PreGNS} : (f.gnsNonUnitalStarAlgHom a) ↑b = ↑((f.leftMulMapPreGNS a) b)

noncomputable def PositiveLinearMap.gnsStarAlgHom {A : Type u_2} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →ₚ[ℂ] ℂ) : A →⋆ₐ[ℂ] f.GNS →L[ℂ] f.GNS

The unital ⋆-homomorphism/⋆-representation of A into the algebra of bounded operators on a Hilbert space that is constructed from a positive linear functional f on a unital C⋆-algebra.

This is the unital version of gnsNonUnitalStarAlgHom.

Equations

• f.gnsStarAlgHom = { toFun := f.gnsNonUnitalStarAlgHom.toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯, map_star' := ⋯ }

@[simp]

theorem PositiveLinearMap.gnsStarAlgHom_apply {A : Type u_2} [CStarAlgebra A] [PartialOrder A] [StarOrderedRing A] (f : A →ₚ[ℂ] ℂ) (a✝ : A) : f.gnsStarAlgHom a✝ = f.gnsNonUnitalStarAlgHom.toFun a✝