A common root vector realizes every selected state through the generators

MathlibAnnex.CStarAlgebra.CAR.exists_targetDefectVectorFamily

theorem

Builds a compatible family of unit vectors from a surviving residual space and identifies their CAR vector states.

Statement

For the supplied shell family and nonzero irreducible representation described below, there exist a unit vector and unit vectors , one for each , with the following properties for every and :

For every they satisfy

Here , and inner products are linear in the second argument.

Assumptions

Let be the completed CAR algebra, obtained by completing the matrix stages with embeddings . Let be the image of the first diagonal matrix unit. Thus and the form a decreasing sequence of projections. The root state has value on a matrix in any stage.

Choose a pure state in each unitary-equivalence class of pure-state GNS representations, with at the root index . Denote its complete complex GNS space, unital star representation and unit cyclic vector by . Set and . The index set need not be countable.

A supplied shell family consists of unital complex star automorphisms with and elements . Put . Their support identities are and . At the root, is the identity and .

Let be unitaries on satisfying for every . Let be the norm-closed unital star algebra generated by and all . Write for and for the element represented by . For a unital complex star representation on a complete complex Hilbert space, put and . Each is unitary because preserves the unit, products and adjoints. Write for the common fixed space of the -th transported flag. The representation is nonzero and irreducible, in the sense that its only closed reducing subspaces are and . No root normalization and no prescribed action of on the atomic cyclic vectors is required.

Conclusion

All chosen vector states share one root vector: the family can be defined by . These pointed state realizations supply the vector data for the cyclic-sum capture theorem. The present result does not assert that an individual is cyclic for all of , or that the limiting fixed spaces are one-dimensional.

Proof route

Choose a unit vector in one nonzero limiting fixed space and apply its represented generator to obtain in the root fixed space. The CAR norm-compression estimates identify both vector states. For every other index, pull this same back by the corresponding unitary. The fixed-space equivalence in shell reconstruction places the pulled-back vector in the correct fixed space, and compression again identifies its state.

Proof steps

The nonvanishing theorem gives and . Normalize to and put . Unitarity preserves norm one. Reconstruction maps onto the root common range, so all fix .
For every , the source estimates are and . Apply the contractive representation and take a matrix coefficient at a unit vector fixed by the corresponding projections. Self-adjointness and fixedness make that coefficient equal to the constant difference between its vector state and the indicated source state. Norm convergence forces the difference to be zero. In particular this identifies the state of as .
Define for each . The same reconstruction equivalence, used in the reverse direction, gives . Unitarity gives and ; membership in the ranges of projections gives their fixedness.
Apply the transported compression estimate to this unit fixed vector. It yields for every and every . The construction uses one root vector throughout rather than separately choosing unrelated vector-state realizations.

Main citations

Lean source signature (exact)

theorem exists_targetDefectVectorFamily
    (family : RepresentativeShellFamily)
    (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →
      MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)
    (hLunit : ∀ i, L i ∈ unitary
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))
    (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation
      (transportedFlag family i n - transportedFlag family i (n + 1))) =
        representedShellLink family i n)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] (rho : Representation (AtomicTarget L) K)
    (hrho : rho.IsIrreducible) :
    ∃ (eta_o : K) (eta : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit → K),
      ‖eta_o‖ = 1 ∧
      (∀ n, (restrictedRepresentation L rho) (rootFlag n) eta_o = eta_o) ∧
      Representation.vectorFunctional (restrictedRepresentation L rho) eta_o =
        rootState ∧
      ∀ i,
        ‖eta i‖ = 1 ∧
        (∀ n, (restrictedRepresentation L rho)
          (transportedFlag family i n) (eta i) = eta i) ∧
        (Unitary.linearIsometryEquiv
          (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) (eta i) =
            eta_o ∧
        Representation.vectorFunctional (restrictedRepresentation L rho) (eta i) =
          (MathlibAnnex.CStarAlgebra.PureState.representative completedRootPureState i).1

Here Limit is , completedRootPureState is the root state bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is the atomic Hilbert space . eta_o is the common root vector , while eta i is the vector at the source index i corresponding to the mathematical index ; eta_o does not mean eta evaluated at the root index. vectorFunctional sigma eta sends to . representative completedRootPureState i is the selected state at that same index, and rootState is . The same eta_o occurs in the generator equation for every index.

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

Lean realization notes

The common root vector and the member indexed by the root class have the same root state, but their equality is not imposed here. The additional normalization , used in that cyclic-sum capture theorem, would give and hence . No orthogonality or surjectivity conclusion is included in this declaration.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:4888d88a4c7efeb37acd75ea32c5fe01cbce3d3cac678038c63b5954797902df

Card revision: 1 · SHA-256: 2c6fbf8ce3493850aea7596ff64198f7a7e816217b2b62eeb16fe4850c824ce8

Exposition revision: 1 · SHA-256: d1de79eac694b1605b00d082f1e28e79c934d815c630d7c8d4a7f5e0771e5342

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 673dd05a893665da3ada59f6ef7f2a9ba6c16b178d2fe7a4887e61c3ea072110