Reconstructing a represented unitary from its shells and residual corner

MathlibAnnex.CStarAlgebra.CAR.exists_targetShellReconstruction

theorem

Separates a represented generator into a strong shell sum and the exact operator between its limiting fixed spaces.

Statement

In the setting below, fix . Put , and , and let and . There are contractions such that, for every ,

.

If are the orthogonal projections onto , then and . The remaining operator satisfies

.

Moreover, if and only if , for every .

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. The index is arbitrary and fixed for this assertion. No irreducibility of , root normalization , or prescribed action on the selected cyclic vectors is assumed.

Conclusion

The shell sum is a partial isometry from onto , and the residual corner is a partial isometry from onto . Together they recover the actual represented generator. The bounds are and ; all displayed limits are norm limits for each fixed vector.

The strong sums are formed on . No continuity of for the strong-operator topology is used, and operator-norm convergence is not asserted. The spaces are not claimed to be one-dimensional in an arbitrary representation. This theorem reconstructs a generator for a supplied family; it does not prove existence of that family.

Proof route

The finite shell identities pass through the star homomorphism and give . Orthogonality of the initial and final difference projections yields the strong sums of the and their adjoints. Finite telescoping identifies the sum with the complementary part of . Strong convergence of decreasing projections then identifies the remaining corner and its two support projections.

theorem exists_targetShellReconstruction
    (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)
    (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :
    let sigma := restrictedRepresentation L rho
    let p := transportedFlag family i
    let q := rootFlag
    let w := (representativeShellData family i).link
    let U : ℕ → Submodule ℂ K := fun n ↦ (sigma (p n)).range
    let V : ℕ → Submodule ℂ K := fun n ↦ (sigma (q n)).range
    ∃ S T P Q R : K →L[ℂ] K,
      ContinuousLinearMap.StronglyConverges
        (ContinuousLinearMap.partialSum (fun n ↦ sigma (w n))) atTop S ∧
      ContinuousLinearMap.StronglyConverges
        (ContinuousLinearMap.partialSum (fun n ↦ (sigma (w n))†)) atTop T ∧
      ‖S‖ ≤ 1 ∧ ‖T‖ ≤ 1 ∧ T = S† ∧
      IsStarProjection P ∧ P.range = ⨅ n, U n ∧
      IsStarProjection Q ∧ Q.range = ⨅ n, V n ∧
      (S†).comp S = 1 - P ∧ S.comp (S†) = 1 - Q ∧
      (Unitary.linearIsometryEquiv
        (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) =
          S + R ∧
      R = ((Unitary.linearIsometryEquiv
        (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) :
          K →L[ℂ] K).comp P ∧
      (R†).comp R = P ∧ R.comp (R†) = Q ∧
      R = (Q.comp R).comp P ∧
      (∀ x, x ∈ ⨅ n, U n ↔
        (Unitary.linearIsometryEquiv
          (representedGeneratorUnitary L hLunit rho i) : K ≃ₗᵢ[ℂ] K) x ∈
            ⨅ n, V n)

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

Earlier published Card and PDF