MATHLIBANNEX / CANONICAL DECLARATION CARD

Approximating another vector state along a unitary path

MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx

theorem

A fixed irreducible CAR representation can approximate any vector state on finitely many elements by moving a given unit vector.

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. Let be irreducible with , let be any representation, and choose unit vectors and . For every finite and , there exist a unitary and a norm-continuous path from to such that for all .

Assumptions

The spaces and are complete complex Hilbert spaces. Both representations are unital; only must be irreducible. There are no initial stage-state tests and no protected finite set.

Conclusion

The approximating state is obtained from the specified starting vector by a unitary in the identity path component of . The approximation is on the prescribed finite set at the endpoint.

The conclusion supplies a path but makes no near-centrality claim and no uniform approximation claim along that path. It does not identify the two representations or give exact equality of their states on all elements.

Proof route

Keep the given vectors and fixed. Purification supplies a new unit vector that realizes the target state on a sufficiently large stage . To move to , use the fixed-stage transport lemma at stage , where its tests are automatic. These are two different stages: controls approximation, whereas stage supplies transport without any near-centrality requirement.

Proof steps

  1. Choose so that each has an approximant with . Apply finite-stage purification to the given , , and at stage . Its hypotheses hold because is nonzero and irreducible, both representations are unital, and . It gives with and for all . This is a new vector; the prescribed starting vector is not replaced.

  2. Use the fixed-stage exact-transport lemma, not the protected-finite-set theorem. For a prescribed stage and a positive commutator tolerance, it supplies a before the pair of unit vectors is chosen. Its hypothesis compares their vector functionals on the matrix units of that stage. Set and take the auxiliary commutator tolerance to be ; its commutator conclusion will not be needed.

  3. The inputs to this transport lemma are in the same representation , not and from different spaces. Since and , unitality and the two unit-vector norms give . This is the only matrix-unit test at stage . Thus the lemma supplies and a path from to with . No comparison between these states on the larger stage , and no norm closeness of and , is required.

  4. For each , the two states agree at and are contractive, so Substitute to obtain the asserted endpoint estimate.

Main citations

Lean source signature (exact)

theorem exists_unitary_crossRepresentation_path_approx
    {H K : Type*}
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
    [Nontrivial H]
    [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
    (rho : Representation Limit H) (hrho : StarAlgHom.IsIrreducible rho)
    (sigma : Representation Limit K) (xi : H) (eta : K)
    (hxi : ‖xi‖ = 1) (heta : ‖eta‖ = 1)
    (F : Finset Limit) {epsilon : ℝ} (hepsilon : 0 < epsilon) :
    ∃ u : unitary Limit, ∃ p : Path 1 u, ∀ a ∈ F,
      ‖Representation.vectorFunctional rho (rho (u : Limit) xi) a -
        Representation.vectorFunctional sigma eta a‖ < epsilon
In the source Mathematical meaning
H; K; rho; hrho; sigma Complete complex Hilbert spaces , with ; an irreducible unital representation named rho, and any unital representation .
xi : H; eta : K; hxi; heta The prescribed vectors , both have norm .
F : Finset Limit; hepsilon : 0 < epsilon The finite endpoint-test set and tolerance .
∃ u : unitary Limit, ∃ p : Path 1 u One unitary joined to by a norm-continuous unitary path . The path need not nearly centralize .
Representation.vectorFunctional rho (rho (u : Limit) xi) a Evaluate the state of the transported vector at : .
∀ a ∈ F, ‖... - Representation.vectorFunctional sigma eta a‖ < epsilon For every , . There are no initial stage-state tests and no assertion about intermediate state values along .

Further source notes: In the linked proof, zeta is the new finite-stage realization of the state of eta; htrans xi zeta applies the fixed-stage lemma inside rho at stage zero. The signature imposes no initial comparison of the states of xi and eta.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.exists_unitary_crossRepresentation_path_approx

Accepted content SHA-256: 8c5ef92d55e64650288d91be015773f79eee7e923d116ab71af6d83f17dc6bc8

Accepted source guide SHA-256: fb4ba07378b912ad5d3ba8146801a874b84e4f85596a55de27610d8d35499d62

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑