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.

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.

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.

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

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

Earlier published Card and PDF