MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

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.

Proof steps

  1. Applying to the finite identity gives the represented shell relation. Also and . The two projection sequences start at and decrease.

  2. The difference projections for different are orthogonal. The orthogonal-shell theorem therefore makes both partial-sum sequences converge strongly to contractions. Taking inner products of the two finite sums identifies their limits as adjoints; the theorem also gives and .

  3. For , telescoping gives . Its final support identity is , hence . Since and strongly, these finite identities yield and . Only multiplication by fixed bounded operators is used in these limit passages.

  4. Set . Unitarity and the projection identities give , , and . The equality gives the fixed-space equivalence, in both directions, by injectivity of .

Main citations

Lean source signature (exact)

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)

Here Limit is , completedRootPureState is the root state bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is the atomic Hilbert space . AtomicTarget L is , restrictedRepresentation L rho is , and representedGeneratorUnitary L hLunit rho i is . In the source, p, q, w are the algebra-valued sequences , , ; U n and V n are their represented ranges. The source witness T is the adjoint limit , not the algebra . P, Q, R are the projection and corner operators above; comp denotes composition and † the Hilbert-space adjoint.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 46468a9773e38db1c55d17a95e2a9bd0e48c1c2b8428b4a9f4dc8eb92af863a8

Exposition revision: 1 · SHA-256: 64fb2500bbff7edb7b7f6e92966fb3d3ded511e67e335fff122b9ef2c3c7e12f

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: cfa973b787ddc8ca8afcfc7e19820fb9530ac1f1b62662ad61e6716826d1b1a2

Back to top ↑