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.

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

Here Limit is , completedRootPureState is the root state bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is . selectedEmbedding ... i is , selectedVector ... i is , and eta i is , with source index i corresponding to the mathematical index . cyclicSubspace sigma (eta i) is and commonFixedProjection is . The arrow →ₗᵢ[ℂ] asserts a complex-linear isometry; it does not assert surjectivity. W.toContinuousLinearMap is the same map used in the operator identity.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:67cdb16a93cf0accba9a49b2a23802225c8252938eb49ca5542397f7374dbc77

Card revision: 1 · SHA-256: 5b9f5d0a4cfb13095b600fce83d7654403ab06f9f73800276dece4ac88a2ba89

Exposition revision: 1 · SHA-256: 9a2fd2ad5c81a0200c831f362bc88b3039ffbaa404aa904a04216ef9baeaf083

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 736e588b0b6e9a21179bc5261a1be9e5f55db338cfcb540d971d7d109445740b

Back to top ↑