MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

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.

Proof steps

  1. Set . The matrix-unit relations and the star property give . Use the root-corner Gram realization theorem to choose with the same inner products.

  2. Define . Multiplication by a matrix unit gives . Taking the inner product with yields .

  3. The two vector functionals therefore agree on every matrix unit, and linearity extends equality to every element of . At its identity, the target value is and the reconstructed value is , so .

Main citations

Lean source signature (exact)

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)

Here ρ is , σ is , and Representation.vectorFunctional is . The input η is the target unit vector and the existential ξ is its finite-stage realization. ofStage n a denotes . The proof uses reconstructedStageVector for the finite sum in the second step.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:01114f6a304958dac0148625cc7265d07805d6e12fa9bd365d3804095d9c2fc1

Card revision: 1 · SHA-256: b68e61a55e1334abdc50b1e9cf528b04c1e40407e8ac766004918e72ddf9c01f

Exposition revision: 1 · SHA-256: 88c54360c0e0254051673cb7d6c1b17c24460ef5417b8103dd7ecf9591a57f43

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: aa6eb3909385750df351b67bc34b313eedb922e3776fc7fee3cdf0a4d2dab9a4

Back to top ↑