The cyclic sum fills every irreducible target representation

MathlibAnnex.CStarAlgebra.CAR.exists_surjective_selectedAtomicCyclicIsometry

theorem

Uses shell reconstruction and residual lines to turn an isometric CAR intertwiner into a unitary equivalence on the source.

Statement

Under the shell-family, generator and irreducibility assumptions below, there exist unit vectors , for , and a surjective complex-linear isometry such that

for every , and for every . In particular, is unitarily equivalent to the selected atomic source representation .

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 . This theorem does not assume the additional identity . The root normalization is required.

Conclusion

The selected cyclic pieces exhaust the target Hilbert space. The source-restriction equivalence is the direct consequence obtained by viewing the surjective isometry as a unitary. The representation being assumed irreducible is on , not its generally reducible restriction on .

The conclusion displayed here intertwines the CAR source. To obtain intertwining for every element of , the full capture theorem also uses the prescribed action . No multiplicity assertion for arbitrary reducible target representations and no unconditional existence of a shell family is claimed.

Proof route

The common-root vector-state theorem supplies compatible unit vectors. Cyclic-sum assembly gives an isometry with closed source-reducing range . Shell reconstruction splits each represented generator into a strong shell sum and a residual corner. Both parts and their adjoints preserve . Norm-closed generation then makes a nonzero reducing subspace for , so irreducibility forces .

theorem exists_surjective_selectedAtomicCyclicIsometry
    (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)
    (hLroot : L completedRootPureState.classOf = 1)
    {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)
      (W : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →ₗᵢ[ℂ] K),
      Function.Surjective W ∧
      ‖eta_o‖ = 1 ∧
      (∀ i, ‖eta i‖ = 1) ∧
      (∀ i, W (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) = eta i) ∧
      (∀ i, (Unitary.linearIsometryEquiv
        (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K)
          (eta i) = eta_o) ∧
      ∀ a,
        W.toContinuousLinearMap.comp (selectedAtomicRepresentation a) =
          ((restrictedRepresentation L rho) a).comp
            W.toContinuousLinearMap

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

Earlier published Card and PDF