MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

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.

Proof steps

  1. Let be a closed subspace reducing . Every and its adjoint preserve , hence so do their finite sums. Closure of passes this invariance to the two strong limits and . Under , the formula gives , so reduces .

  2. The orthogonal projection onto commutes with the represented source and all added generators. Its commutation relation persists under algebraic star operations and norm limits. Consequently reduces every , , and irreducibility of forces or . The space is nonzero and is unital, so this proves nonzero irreducibility of under the supposition.

  3. Coverage by selected pure-state GNS representations supplies an index and a unitary with for every . The vector has norm one. Since , each projection fixes ; intertwining therefore gives for all .

  4. A fixed vector of a projection belongs to its range. Thus , contradicting and . This completes the exclusion of the all-zero case.

Main citations

Lean source signature (exact)

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) ≠ ⊥

Here Limit is , completedRootPureState is the root state bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is the atomic Hilbert space . hrho : rho.IsIrreducible includes nonzero irreducibility of . The expression ⨅ n, ... .range is , and ≠ ⊥ means that this subspace is not . restrictedRepresentation L rho is ; the source conclusion quantifies over an index i and does not claim irreducibility of without the temporary all-zero hypothesis used in the proof.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:a78c4de54da4fbe1ab39f1d488112128a74cc98680c7764d29e113cb74ba0efc

Card revision: 1 · SHA-256: 3013bebd0fa8135adbc19e340286b79e88fbfc0497c793aa18a17bdd139e5f0e

Exposition revision: 1 · SHA-256: 17a142f497c21610256d4f3f2cb3df7b8d046f032b3ee22b748339048333cb66

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: f0c0b33183fc841527bb2392df81b7ef2534000f45fa1754983256552fad45be

Back to top ↑