An irreducible target representation has a surviving fixed space

MathlibAnnex.CStarAlgebra.CAR.exists_nonzero_targetFixedSpace

theorem

Rules out simultaneous disappearance of all limiting CAR flags by passing reduction through the reconstructed generators.

Statement

For the shell family and generated algebra described below, let be a nonzero irreducible unital star representation and put . Then there is an index such that is nonzero.

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. Here irreducibility includes nonzero representation and means that the only closed subspaces invariant under every represented operator and its adjoint are and . No root normalization or prescribed transport of the atomic cyclic vectors is assumed.

Conclusion

At least one transported flag retains a nonzero common fixed vector. This supplies the initial vector for the residual-corner construction of vector states. The assertion concerns existence of some ; it neither chooses a distinguished index nor says that this common range is one-dimensional.

The temporary assertion that is irreducible occurs inside the contradiction argument under the all-zero hypothesis. It is not asserted for every source restriction. Strong limits are taken on , while extension from source and generators to uses norm-closed generation.

Proof route

Suppose all vanish, and write for the orthogonal projection onto . Let be the strong sum of the represented shell links. By the shell reconstruction theorem, in each reconstructed generator , the initial residual projection is zero, so . Every closed reducing subspace for therefore reduces every , and hence the entire target representation. Thus would be irreducible. Coverage by selected pure-state GNS representations then transports a selected cyclic vector back to a nonzero vector fixed by one of the flags, contradicting the assumption.

theorem exists_nonzero_targetFixedSpace
    (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) :
    ∃ i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit,
      (⨅ n, ((restrictedRepresentation L rho)
        (transportedFlag family i n)).range) ≠ ⊥

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

Earlier published Card and PDF