The GNS construction: from a state on a ⋆-algebra to a commuting-operator strategy

The Gelfand–Naimark–Segal construction, in the form the Tsirelson campaign needs (planning/tsirelson-campaign.md, §3.2): a state L on a complex ⋆-algebra P, together with elements e x a, f y b of P satisfying the defining relations of a pair of commuting POVM families under L, yields a MIPRE.CommutingOperatorStrategy whose correlation is Re L (e x a * f y b). The module is generic in P; it is instantiated at the free ⋆-algebra on the generators of a game elsewhere.

The construction has three layers.

Abstract GNS. A positive semidefinite Hermitian sesquilinear form β on a complex vector space V (PSDForm) makes the type synonym Pre β of V a pre-inner-product space (PreInnerProductSpace.Core, InnerProductSpace.ofCore). Its null vectors have norm zero but need not vanish, so Pre β is not T0; its completion H β is a Hilbert space, into which ι : V → H β maps with dense range, killing every null vector (ι_eq_zero_of_null). A linear map T of V that is bounded for the seminorm of β (Bdd) lifts to a continuous operator lift β T on H β, with lift β T (ι v) = ι (T v) (lift_ι). Identities between lifts are checked on the dense image of ι, where it suffices that they hold up to null vectors: sum_lift_eq_one, commute_lift. A lift is positive as soon as T is symmetric and positive for β (lift_isPositive).

States. A state on P (State) is a ℂ-linear L : P → ℂ with L 1 = 1, L (a⋆) = conj (L a) and 0 ≤ Re L (a⋆ a). Its GNS form is ⟨a, b⟩ = L (a⋆ b) (State.form). Left multiplication by g is a contraction as soon as Re L (s⋆ (1 - g⋆ g) s) ≥ 0 for every s (State.bdd_mulLeft), and for an effect g of a family that is positive under L and sums to one under L, this holds by 1 - g² = (1 - g) + g (1 - g) g + (1 - g) g (1 - g) (State.contraction_of_povm). A relation ρ with L (u ρ v) = 0 for all u, v makes every ρ s null (State.null_of_ideal), which turns the POVM and commutation relations in P into the corresponding operator identities on H (State.sum_lift_mulLeft, State.commute_lift_mulLeft). The cyclic vector ι 1 is a unit vector (State.norm_ι_one).

The strategy. GenData records the families e, f and the conditions on them; GenData.strategy is the resulting commuting-operator strategy on H, with state ι 1 and operators the lifts of left multiplication by e x a and f y b, and GenData.strategy_correlation computes its correlation to be Re L (e x a * f y b).

All carriers live in Type, since the Hilbert space of a CommutingOperatorStrategy does.

Main declarations

• PSDForm, Pre, H, ι, ι_eq_zero_of_null;
• Bdd, lift, lift_ι, sum_lift_eq_one, commute_lift, lift_isPositive;
• State, State.form, State.bdd_mulLeft, State.contraction_of_povm, State.null_of_ideal, State.sum_lift_mulLeft, State.commute_lift_mulLeft, State.norm_ι_one;
• GenData, GenData.strategy, GenData.strategy_correlation.

Abstract GNS on a positive semidefinite form

structure MIPRE.GNS.PSDForm (V : Type) [AddCommGroup V] [Module ℂ V] : Type

A positive semidefinite Hermitian sesquilinear form on a complex vector space V, conjugate-linear in the first argument.

• B : V →ₗ⋆[ℂ] V →ₗ[ℂ] ℂ

  The form.

• conj_symm (u v : V) : (starRingEnd ℂ) ((self.B v) u) = (self.B u) v

  The form is Hermitian.

• re_nonneg (v : V) : 0 ≤ ((self.B v) v).re

  The form is positive semidefinite.

def MIPRE.GNS.Pre {V : Type} [AddCommGroup V] [Module ℂ V] (_β : PSDForm V) : Type

The type synonym of V carrying the pre-inner product and the seminorm of β.

Equations

• MIPRE.GNS.Pre _β = V

@[instance_reducible]

instance MIPRE.GNS.instAddCommGroupPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : AddCommGroup (Pre β)

The additive group of V.

Equations

• One or more equations did not get rendered due to their size.

@[instance_reducible]

instance MIPRE.GNS.instModuleComplexPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : Module ℂ (Pre β)

The complex vector space structure of V.

Equations

• MIPRE.GNS.instModuleComplexPre β = { toSMul := MIPRE.GNS.instModuleComplexPre._aux_1 β, mul_smul := ⋯, one_smul := ⋯, smul_zero := ⋯, smul_add := ⋯, add_smul := ⋯, zero_smul := ⋯ }

def MIPRE.GNS.toPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : V ≃ₗ[ℂ] Pre β

The identity V ≃ Pre β.

Equations

• MIPRE.GNS.toPre β = LinearEquiv.refl ℂ V

def MIPRE.GNS.ofPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : Pre β ≃ₗ[ℂ] V

The identity Pre β ≃ V.

Equations

• MIPRE.GNS.ofPre β = (MIPRE.GNS.toPre β).symm

@[simp]

theorem MIPRE.GNS.toPre_ofPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (a : Pre β) : (toPre β) ((ofPre β) a) = a

toPre inverts ofPre.

@[simp]

theorem MIPRE.GNS.ofPre_toPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (a : V) : (ofPre β) ((toPre β) a) = a

ofPre inverts toPre.

@[reducible, inline]

noncomputable abbrev MIPRE.GNS.core {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : PreInnerProductSpace.Core ℂ (Pre β)

The pre-inner-product core of β on Pre β.

Equations

• MIPRE.GNS.core β = { inner := fun (a b : MIPRE.GNS.Pre β) => (β.B ((MIPRE.GNS.ofPre β) a)) ((MIPRE.GNS.ofPre β) b), conj_inner_symm := ⋯, re_inner_nonneg := ⋯, add_left := ⋯, smul_left := ⋯ }

@[instance_reducible]

noncomputable instance MIPRE.GNS.instSeminormedAddCommGroupPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : SeminormedAddCommGroup (Pre β)

The seminorm of β, ‖a‖ = √(Re β a a).

Equations

• MIPRE.GNS.instSeminormedAddCommGroupPre β = InnerProductSpace.Core.toSeminormedAddCommGroup

@[instance_reducible]

noncomputable instance MIPRE.GNS.instInnerProductSpaceComplexPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : InnerProductSpace ℂ (Pre β)

The pre-inner product ⟪a, b⟫ = β a b.

Equations

• MIPRE.GNS.instInnerProductSpaceComplexPre β = InnerProductSpace.ofCore (MIPRE.GNS.core β)

theorem MIPRE.GNS.pre_inner_def {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (a b : Pre β) : inner ℂ a b = (β.B ((ofPre β) a)) ((ofPre β) b)

The inner product of Pre β is the form β.

theorem MIPRE.GNS.pre_norm_def {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (a : Pre β) : ‖a‖ = √((β.B ((ofPre β) a)) ((ofPre β) a)).re

The seminorm of Pre β is √(Re β a a).

@[reducible, inline]

abbrev MIPRE.GNS.H {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) : Type

The GNS Hilbert space of β: the completion of Pre β.

Equations

• MIPRE.GNS.H β = UniformSpace.Completion (MIPRE.GNS.Pre β)

noncomputable def MIPRE.GNS.ι {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (v : V) : H β

The canonical map V → H β.

Equations

• MIPRE.GNS.ι β v = ↑((MIPRE.GNS.toPre β) v)

theorem MIPRE.GNS.inner_ι {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (u v : V) : inner ℂ (ι β u) (ι β v) = (β.B u) v

The inner product of two images of ι is the form β.

theorem MIPRE.GNS.norm_ι {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (v : V) : ‖ι β v‖ = √((β.B v) v).re

The norm of an image of ι is √(Re β v v).

theorem MIPRE.GNS.ι_add {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (u v : V) : ι β (u + v) = ι β u + ι β v

ι is additive.

theorem MIPRE.GNS.ι_sub {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (u v : V) : ι β (u - v) = ι β u - ι β v

ι commutes with subtraction.

theorem MIPRE.GNS.ι_eq_zero_of_null {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {v : V} (hv : (β.B v) v = 0) : ι β v = 0

A null vector of β maps to 0.

theorem MIPRE.GNS.ι_induction {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {p : H β → Prop} (hp : IsClosed {x : H β | p x}) (h : ∀ (v : V), p (ι β v)) (x : H β) : p x

Density induction on H β: a closed property that holds on the image of ι holds everywhere.

Lifting operators

def MIPRE.GNS.Bdd {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (T : V →ₗ[ℂ] V) : Prop

A linear map of V bounded for the seminorm of β.

Equations

• MIPRE.GNS.Bdd β T = ∃ (C : ℝ), ∀ (v : V), ((β.B (T v)) (T v)).re ≤ C * ((β.B v) v).re

noncomputable def MIPRE.GNS.liftPre {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (T : V →ₗ[ℂ] V) (hT : Bdd β T) : Pre β →L[ℂ] Pre β

A bounded linear map of V, as a continuous operator on Pre β.

Equations

• MIPRE.GNS.liftPre β T hT = (↑(MIPRE.GNS.toPre β) ∘ₗ T ∘ₗ ↑(MIPRE.GNS.ofPre β)).mkContinuousOfExistsBound ⋯

noncomputable def MIPRE.GNS.lift {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (T : V →ₗ[ℂ] V) (hT : Bdd β T) : H β →L[ℂ] H β

A bounded linear map of V, as a continuous operator on the Hilbert space H β.

Equations

• MIPRE.GNS.lift β T hT = (MIPRE.GNS.liftPre β T hT).completion

@[simp]

theorem MIPRE.GNS.lift_ι {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (T : V →ₗ[ℂ] V) (hT : Bdd β T) (v : V) : (lift β T hT) (ι β v) = ι β (T v)

The lift of T extends T: lift β T (ι v) = ι (T v).

theorem MIPRE.GNS.bdd_of_contraction {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (T : V →ₗ[ℂ] V) (hT : ∀ (v : V), ((β.B (T v)) (T v)).re ≤ ((β.B v) v).re) : Bdd β T

Contractions for β are bounded.

theorem MIPRE.GNS.ext_ι {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {S S' : H β →L[ℂ] H β} (h : ∀ (v : V), S (ι β v) = S' (ι β v)) : S = S'

Two operators on H β that agree on the image of ι are equal.

theorem MIPRE.GNS.Bdd.comp {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {T T' : V →ₗ[ℂ] V} (hT : Bdd β T) (hT' : Bdd β T') : Bdd β (T ∘ₗ T')

Composites of bounded maps are bounded.

theorem MIPRE.GNS.sum_lift_ι {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {ι' : Type u_1} (s : Finset ι') (T : ι' → V →ₗ[ℂ] V) (hT : ∀ (i : ι'), Bdd β (T i)) (v : V) : (∑ i ∈ s, lift β (T i) ⋯) (ι β v) = ι β ((∑ i ∈ s, T i) v)

A finite sum of lifts, evaluated on the image of ι.

theorem MIPRE.GNS.sum_lift_eq_one {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {ι' : Type u_1} [Fintype ι'] (T : ι' → V →ₗ[ℂ] V) (hT : ∀ (i : ι'), Bdd β (T i)) (h : ∀ (v : V), (β.B ((∑ i : ι', T i) v - v)) ((∑ i : ι', T i) v - v) = 0) : ∑ i : ι', lift β (T i) ⋯ = 1

A family of bounded maps summing to the identity up to null vectors lifts to a family summing to 1.

theorem MIPRE.GNS.commute_lift {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {T T' : V →ₗ[ℂ] V} (hT : Bdd β T) (hT' : Bdd β T') (h : ∀ (v : V), (β.B (T (T' v) - T' (T v))) (T (T' v) - T' (T v)) = 0) : Commute (lift β T hT) (lift β T' hT')

Two bounded maps commuting up to null vectors have commuting lifts.

theorem MIPRE.GNS.lift_isPositive {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) (T : V →ₗ[ℂ] V) (hT : Bdd β T) (hsymm : ∀ (u v : V), (β.B (T u)) v = (β.B u) (T v)) (hpos : ∀ (v : V), 0 ≤ ((β.B v) (T v)).re) : (lift β T hT).IsPositive

The lift of a map that is symmetric and positive for β is a positive operator.

theorem MIPRE.GNS.norm_ι_eq_one {V : Type} [AddCommGroup V] [Module ℂ V] (β : PSDForm V) {v₀ : V} (h : (β.B v₀) v₀ = 1) : ‖ι β v₀‖ = 1

A vector of β-norm one maps to a unit vector.

States on a ⋆-algebra

structure MIPRE.GNS.State (P : Type) [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] : Type

A state on a complex ⋆-algebra: a normalized, Hermitian, positive linear functional. Positivity is required on the squares a⋆ a only; the positivity of the generators is a separate hypothesis (GenData).

• L : P →ₗ[ℂ] ℂ

  The functional.

• map_one : self.L 1 = 1

  L 1 = 1.

• map_star (a : P) : self.L (star a) = (starRingEnd ℂ) (self.L a)

  L is Hermitian.

• nonneg (a : P) : 0 ≤ (self.L (star a * a)).re

  L is positive on squares.

noncomputable def MIPRE.GNS.State.form {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) : PSDForm P

The GNS form ⟨a, b⟩ = L (a⋆ b) of a state.

Equations

• φ.form = { B := LinearMap.mk₂'ₛₗ (starRingEnd ℂ) (RingHom.id ℂ) (fun (a b : P) => φ.L (star a * b)) ⋯ ⋯ ⋯ ⋯, conj_symm := ⋯, re_nonneg := ⋯ }

@[simp]

theorem MIPRE.GNS.State.form_B {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) (a b : P) : (φ.form.B a) b = φ.L (star a * b)

The GNS form of a state, applied.

theorem MIPRE.GNS.State.bdd_mulLeft {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) (g : P) (hg : ∀ (s : P), 0 ≤ (φ.L (star s * (1 - star g * g) * s)).re) : Bdd φ.form (LinearMap.mulLeft ℂ g)

Left multiplication by g is bounded for the GNS form as soon as 1 - g⋆ g is positive under L after conjugation by every s.

theorem MIPRE.GNS.State.lift_mulLeft_isPositive {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) (g : P) (hg : Bdd φ.form (LinearMap.mulLeft ℂ g)) (hsa : star g = g) (hpos : ∀ (s : P), 0 ≤ (φ.L (star s * g * s)).re) : (lift φ.form (LinearMap.mulLeft ℂ g) hg).IsPositive

The lift of left multiplication by a self-adjoint g, positive under L after conjugation, is a positive operator.

theorem MIPRE.GNS.State.null_of_ideal {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) (ρ : P) (hρ : ∀ (u v : P), φ.L (u * ρ * v) = 0) (s : P) : (φ.form.B (ρ * s)) (ρ * s) = 0

If L (u ρ v) = 0 for all u, v, then every ρ s is a null vector of the GNS form.

theorem MIPRE.GNS.sum_mulLeft_apply {P : Type} [Ring P] [Algebra ℂ P] {ι' : Type u_1} (t : Finset ι') (g : ι' → P) (v : P) : (∑ i ∈ t, LinearMap.mulLeft ℂ (g i)) v = (∑ i ∈ t, g i) * v

A finite sum of left multiplications is left multiplication by the sum.

theorem MIPRE.GNS.State.sum_lift_mulLeft {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) {ι' : Type u_1} [Fintype ι'] (g : ι' → P) (hg : ∀ (i : ι'), Bdd φ.form (LinearMap.mulLeft ℂ (g i))) (hsum : ∀ (u v : P), φ.L (u * (∑ i : ι', g i - 1) * v) = 0) : ∑ i : ι', lift φ.form (LinearMap.mulLeft ℂ (g i)) ⋯ = 1

A family summing to one under L (L (u (Σ g - 1) v) = 0) lifts to operators summing to 1.

theorem MIPRE.GNS.State.commute_lift_mulLeft {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) (g g' : P) (hg : Bdd φ.form (LinearMap.mulLeft ℂ g)) (hg' : Bdd φ.form (LinearMap.mulLeft ℂ g')) (hc : ∀ (u v : P), φ.L (u * (g * g' - g' * g) * v) = 0) : Commute (lift φ.form (LinearMap.mulLeft ℂ g) hg) (lift φ.form (LinearMap.mulLeft ℂ g') hg')

Two elements commuting under L (L (u [g, g'] v) = 0) lift to commuting operators.

theorem MIPRE.GNS.State.inner_ι {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) (a b : P) : inner ℂ (ι φ.form a) (ι φ.form b) = φ.L (star a * b)

The inner product of the images of a and b in the GNS space is L (a⋆ b).

theorem MIPRE.GNS.State.norm_ι_one {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) : ‖ι φ.form 1‖ = 1

The cyclic vector ι 1 is a unit vector.

theorem MIPRE.GNS.State.contraction_of_povm {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (φ : State P) {ι' : Type u_1} [Fintype ι'] [DecidableEq ι'] (g : ι' → P) (hsa : ∀ (i : ι'), star (g i) = g i) (hpos : ∀ (i : ι') (s : P), 0 ≤ (φ.L (star s * g i * s)).re) (hsum : ∀ (u v : P), φ.L (u * (∑ i : ι', g i - 1) * v) = 0) (i : ι') (s : P) : 0 ≤ (φ.L (star s * (1 - star (g i) * g i) * s)).re

The contraction condition for one effect of a family that is positive under L and sums to one under L: 1 - g² = (1 - g) + g (1 - g) g + (1 - g) g (1 - g), and 1 - g_i = Σ_{j ≠ i} g_j - (Σ g - 1).

A commuting-operator strategy from a state

structure MIPRE.GNS.GenData (P : Type) [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] (X Y A B : Type) [Fintype A] [Fintype B] (φ : State P) : Type

Elements e x a, f y b of P satisfying, under the state φ, the relations of two commuting families of POVMs: self-adjoint, positive under φ after conjugation, summing to one and commuting inside φ (u · v).

• e : X → A → P

  The first player's effects.

• f : Y → B → P

  The second player's effects.

• e_sa (x : X) (a : A) : star (self.e x a) = self.e x a

  The first player's effects are self-adjoint.

• f_sa (y : Y) (b : B) : star (self.f y b) = self.f y b

  The second player's effects are self-adjoint.

• e_pos (x : X) (a : A) (s : P) : 0 ≤ (φ.L (star s * self.e x a * s)).re

  The first player's effects are positive under φ.

• f_pos (y : Y) (b : B) (s : P) : 0 ≤ (φ.L (star s * self.f y b * s)).re

  The second player's effects are positive under φ.

• e_sum (x : X) (u v : P) : φ.L (u * (∑ a : A, self.e x a - 1) * v) = 0

  The first player's effects sum to one under φ.

• f_sum (y : Y) (u v : P) : φ.L (u * (∑ b : B, self.f y b - 1) * v) = 0

  The second player's effects sum to one under φ.

• comm (x : X) (y : Y) (a : A) (b : B) (u v : P) : φ.L (u * (self.e x a * self.f y b - self.f y b * self.e x a) * v) = 0

  The two players' effects commute under φ.

theorem MIPRE.GNS.GenData.e_bdd {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] {X Y A B : Type} [Fintype A] [Fintype B] {φ : State P} (d : GenData P X Y A B φ) (x : X) (a : A) : Bdd φ.form (LinearMap.mulLeft ℂ (d.e x a))

Left multiplication by a first-player effect is bounded.

theorem MIPRE.GNS.GenData.f_bdd {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] {X Y A B : Type} [Fintype A] [Fintype B] {φ : State P} (d : GenData P X Y A B φ) (y : Y) (b : B) : Bdd φ.form (LinearMap.mulLeft ℂ (d.f y b))

Left multiplication by a second-player effect is bounded.

noncomputable def MIPRE.GNS.GenData.strategy {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] {X Y A B : Type} [Fintype A] [Fintype B] {φ : State P} (d : GenData P X Y A B φ) [Fintype X] [Fintype Y] : CommutingOperatorStrategy X Y A B

GNS: the commuting-operator strategy of a state, on the GNS space of φ, with state the cyclic vector ι 1 and operators the lifts of left multiplication by the effects.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.GNS.GenData.strategy_correlation {P : Type} [Ring P] [StarRing P] [Algebra ℂ P] [StarModule ℂ P] {X Y A B : Type} [Fintype A] [Fintype B] {φ : State P} (d : GenData P X Y A B φ) [Fintype X] [Fintype Y] (x : X) (y : Y) (a : A) (b : B) : d.strategy.correlation x y a b = (φ.L (d.e x a * d.f y b)).re

GNS: the correlation of the strategy of a state is Re L (e x a * f y b).