MATHLIBANNEX / CANONICAL DECLARATION CARD

Assembling selected GNS cyclic subspaces into an isometric source representation

MathlibAnnex.CStarAlgebra.CAR.exists_selectedAtomicCyclicIsometry

theorem

Joins mutually orthogonal pure-state cyclic copies and controls the limiting flag projections on their sum.

Statement

For the shell family and selected GNS spaces below, let be a unital complex star representation on a complete complex Hilbert space. Suppose unit vectors satisfy for every and . Put and let be the orthogonal projection onto .

There is a complex-linear isometry such that , and for every and . For every , it satisfies .

Assumptions

Let be the completed CAR algebra, the completion of the matrix stages under . Let be the image of the first diagonal matrix unit, so and decreases through projections. The root state takes the value on each matrix stage.

Choose one pure state from each unitary-equivalence class of pure-state Gelfand-Naimark-Segal (GNS) representations, with root index and . Write for its complete complex GNS space, unital star representation and unit cyclic vector. Set , , and let be the coordinate embedding. No countability of is assumed. Inner products are linear in the second argument.

A supplied shell family consists of unital complex star automorphisms and elements . Put . The identities are , and . At the root, is the identity and . The family is an input, not an existence conclusion. The vectors are given simultaneously, one for each chosen class. No irreducibility of and no density of any individual orbit in all of is assumed. The algebra and the representations are unital, so each belongs to .

Conclusion

The isometry identifies the atomic Hilbert sum with a closed subspace reducing . Each ambient limiting flag projection sends this range into the indicated cyclic line. This is control on the isometry range; it is not a claim that the entire ambient fixed space has dimension one.

Surjectivity is not part of this theorem. The surjective cyclic-sum theorem proves it in the generated-target setting with additional hypotheses. The present hypotheses already supply the vector states; they do not assert that every representation of the CAR algebra contains all selected classes.

Proof route

Identify each cyclic restriction with its selected GNS representation by pointed cyclic transport. Orthogonality of inequivalent cyclic pieces allows these identifications to extend to the arbitrary-index Hilbert sum. The own-piece compression identity and vanishing on other cyclic pieces give the projection assertion; continuity passes the source intertwining law through the convergent sum.

Proof steps

  1. On , the restricted representation has the unit cyclic vector with pure state , and is irreducible. Equality of vector states gives a unitary sending to and intertwining with the restriction of . It extends the orbit map .

  2. For , the orthogonal projection from to intertwines their restrictions, since the cyclic subspaces reduce . A nonzero such intertwiner between irreducible representations would give a unitary equivalence by Schur’s lemma, contradicting the distinct selected GNS classes. Thus . The maps , followed by inclusion into , form an orthogonal family of isometries.

  3. For a fixed , the state identity gives , hence . Norm compression implies , so . Density of the orbit and closedness of the line give . If with and , normalizing yields a vector with state . Its cyclic space is orthogonal to . Then , a contradiction. Hence .

  4. For , define , with each summand viewed in . Orthogonality makes this an unconditionally norm-convergent Hilbert sum and gives . The coordinate formulas give . Applying the bounded operator kills every summand except the -th, whose image lies in . Applying the bounded operator termwise gives .

Main citations

Lean source signature (exact)

theorem exists_selectedAtomicCyclicIsometry
    (family : RepresentativeShellFamily)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] (sigma : Representation Limit K)
    (eta : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → K)
    (heta : ∀ i, ‖eta i‖ = 1)
    (hstate : ∀ i, Representation.vectorFunctional sigma (eta i) =
      (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1) :
    ∃ W : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K,
      (∀ i x, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i x) ∈
        Representation.cyclicSubspace sigma (eta i)) ∧
      (∀ i, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧
      (∀ i x, commonFixedProjection
        (fun n ↦ sigma (transportedFlag family i n)) (W x) ∈
          ℂ ∙ eta i) ∧
      ∀ a,
        W.toContinuousLinearMap.comp
            (selectedAtomicRepresentation a) =
          (sigma a).comp
            W.toContinuousLinearMap
In the source Mathematical meaning
family : RepresentativeShellFamily The given CAR shell family with transported flags and selected pure-GNS data , indexed by arbitrary . Write , .
sigma : Representation Limit K; [CompleteSpace K] The given unital star representation on a complete complex Hilbert space; it need not be irreducible.
eta : GNSClass Limit → K; heta : ∀ i, ‖eta i‖ = 1 A simultaneously given family of unit vectors , one for each selected class. Source i denotes the mathematical index .
hstate : ∀ i, Representation.vectorFunctional sigma (eta i) = (PureState.representative completedRootPureState i).1 For every and every , . Equality is of whole functionals; it is not just one matrix coefficient. Inner products are linear in the second entry.
∃ W : SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K One complex-linear isometry satisfies all four following properties. The arrow does not assert surjectivity.
∀ i x, W (selectedEmbedding ... i x) ∈ Representation.cyclicSubspace sigma (eta i) For every and , . The orbit is a linear subspace because and the representation are unital and linear. is not assumed to be all of .
∀ i, W (selectedEmbedding ... i (selectedVector ... i)) = eta i The same sends each embedded unit cyclic vector to its supplied vector: .
∀ i x, commonFixedProjection (fun n ↦ sigma (transportedFlag family i n)) (W x) ∈ ℂ ∙ eta i For every and , , where projects onto . This controls the projection only on the range of , not the dimension of the entire ambient fixed space.
∀ a, W.toContinuousLinearMap.comp (selectedAtomicRepresentation a) = (sigma a).comp W.toContinuousLinearMap For every , . W.toContinuousLinearMap is the same isometry viewed as a bounded map, and composition acts rightmost first.

Further source notes: Here Limit is , completedRootPureState is the root state bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is . The arrow →ₗᵢ[ℂ] asserts a complex-linear isometry; it does not assert surjectivity.

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_selectedAtomicCyclicIsometry

Accepted content SHA-256: c0bfb055058f001ab432d17e0bc4b3ab89842a3c706cc3c84461900b266c4de2

Accepted source guide SHA-256: 1c48447e5b17bc9705fe5825ec82ab86d1e4d2f976caaa5c5493095357f80b69

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑