Purifying a vector state on a finite CAR stage

MathlibAnnex.CStarAlgebra.CAR.exists_unitVector_vectorFunctional_eq_on_stage

theorem

Every finite-stage restriction of a unit vector state can be realized by a unit vector in any irreducible CAR representation.

Statement

Let be the completed CAR algebra: the norm completion of the increasing union of under the unital embeddings (with the fixed coordinate reindexing). Write for the canonical isometric inclusion and for its matrix units. A representation is a unital complex star homomorphism into the bounded operators on a complex Hilbert space. Irreducibility means nonzero action and no proper nonzero closed reducing subspace. We use the inner product conjugate linear in its first argument and write for the vector functional. Fix an irreducible representation , any representation , and a unit vector . For every stage there is a unit vector such that for all .

Assumptions

Both and are complete complex Hilbert spaces. Only is required to be irreducible with nonzero action. The representation is unital but may be reducible. The target vector has norm .

Conclusion

The two vector states agree exactly on the whole chosen matrix stage, not merely approximately on a finite list. The unit vector may depend on the stage. No single vector realizing the target state on all of is asserted.

Finite-stage purification is compatible with mixed restrictions of the target state: no purity assumption on that restriction is needed. The extra room comes from the infinite-dimensional represented root corner.

Proof route

Encode the target stage restriction as a Gram matrix, realize that matrix in the root corner of , and reconstruct a vector by applying the first-column matrix units. Matrix-unit coefficients determine a linear functional on a full matrix algebra, and evaluation at the unit gives normalization.

theorem exists_unitVector_vectorFunctional_eq_on_stage
    {H K : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    (ρ : Representation Limit H) (hρ : ρ.IsIrreducible)
    (σ : Representation Limit K) (n : ℕ) (η : K) (hη : ‖η‖ = 1) :
    ∃ ξ : H, ‖ξ‖ = 1 ∧ ∀ c : Stage n,
      Representation.vectorFunctional ρ ξ (ofStage n c) =
        Representation.vectorFunctional σ η (ofStage n c)

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF