Every irreducible representation is unitarily equivalent to the inclusion

MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent

theorem

Extends the unitary equivalence from the CAR source to all additional generators and the norm-closed target.

Statement

For the data and assumptions below, there is a complex-linear unitary such that for every and . Equivalently, the inclusion representation is unitarily equivalent to .

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.

Let be unitaries on satisfying for all , and assume . Let be the norm-closed unital star algebra they generate. Write as an element of , and for the element represented by . Let be a unital complex star representation on a complete complex Hilbert space, put , and put . Assume is nonzero and irreducible: its only closed reducing subspaces are and . In addition, require for every . These are prescribed links between the selected cyclic vectors. The theorem applies to every complete complex target Hilbert space and every nonzero irreducible on it; no separability or fixed dimension is assumed.

Conclusion

A single unitary intertwines the whole target algebra, including its added generators. This identifies the irreducible representation with the concrete inclusion. Combining it with the construction of the faithful irreducible inclusion gives the fixed-family structural theorem. The family supplying the shell data remains a hypothesis.

The proof forms shell limits independently on and and compares them through a bounded unitary. It does not assume that an arbitrary representation preserves strong-operator limits, and it does not replace strong convergence by operator-norm convergence. The prescribed cyclic-vector action is used for the residual corner; source intertwining alone does not identify the added generators.

Proof route

Use the same surjective isometry supplied by surjective cyclic-sum assembly, now viewed as a unitary. For each generator, shell reconstruction gives a strong shell part and a residual corner on both Hilbert spaces. The source intertwiner compares the finite shell sums and hence their strong limits. The atomic common-range theorem identifies the source residual line, and the cyclic-vector transport identifies the remaining corner. Norm-closed generation extends the resulting generator identities to every element of the target.

theorem ambientInclusion_unitaryEquivalent
    (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))
    (hLmap : ∀ i, L i
      (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =
      MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState
        completedRootPureState.classOf
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState
          completedRootPureState.classOf))
    (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation
      (transportedFlag family i n - transportedFlag family i (n + 1))) =
        representedShellLink family i n)
    (hLroot : L completedRootPureState.classOf = 1)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] (rho : Representation (AtomicTarget L) K)
    (hrho : rho.IsIrreducible) :
    (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L).UnitaryEquivalent
      rho

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

Earlier published Card and PDF