The atomic-shell construction on selected pure-GNS fibers

MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel

theorem

Pure-state GNS data supplies the irreducible and inequivalent fibers required by the generic shell construction.

Statement

Let be a unital complex C*-algebra, with the positive order used for its states, and fix a pure state . A pure state is an extreme point of the normalized positive continuous linear functionals. Let be the set of pure-state GNS representations modulo unitary equivalence. For each , choose a pure state in that class, retaining literally at . Write for its GNS space, representation and canonical cyclic vector. Write for the Hilbert direct sum, for coordinate inclusion, and . Here the sum consists of square-summable families and has no countability restriction on . Put . Given the shell data specified below, there exist unitaries with and . The inclusion of into is irreducible.

Assumptions

For each , let and be decreasing subspaces of , with . All these subspaces and both intersections admit orthogonal projections. Write , , and , . The given bounded shell maps satisfy and . Their limiting defects are prescribed: and . Here , with the inner product linear in its second variable. In these formulas the generic index ranges over the GNS classes and the vectors are the selected GNS vectors just defined. The two flags, shell maps, support equations and limiting rank-one equations remain hypotheses; purity alone does not supply them.

Conclusion

One family of unitary links realizes all prescribed shell actions and joins every selected cyclic vector to the root vector, with irreducible concrete target action. This is the specialization of the generic atomic-shell result to the chosen pure-GNS family.

Proof route

Use the selected GNS representations as the fibers of the generic atomic-shell theorem, with root class and the same selected vectors . Three proved pure-GNS facts discharge its representation hypotheses; all shell hypotheses pass through unchanged.

Proof steps

The selected-vector normalization theorem gives , so each is nonzero. The selected-vector functional equals the pure state , and the selected GNS orbit is dense. The separate pure-GNS irreducibility theorem uses these facts to show that each is irreducible.
For , the selected-class non-intertwining theorem rules out a unitary intertwiner between and . The GNS classes, not merely the state functionals, are required to be distinct. Thus the pairwise-unitary-inequivalence hypothesis of the generic theorem is satisfied.
Apply the generic atomic-shell theorem with these fibers, the distinguished index , the already fixed vectors , and the given . The displayed support and rank-one intersection equations are the remaining inputs. Coordinate inclusion here is exactly , so its output vector-link and shell equations are the required ones, with no new choice of GNS representatives.

Main citations

Lean source signature (exact)

theorem exists_irreducible_pureAtomicShellModel
    (root : PureState A)
    (W : PureState.GNSClass A → ℕ →
      PureState.SelectedAtomicHilbert root →L[ℂ]
        PureState.SelectedAtomicHilbert root)
    (U V : PureState.GNSClass A → ℕ →
      Submodule ℂ (PureState.SelectedAtomicHilbert root))
    [∀ i n, (U i n).HasOrthogonalProjection]
    [∀ i n, (V i n).HasOrthogonalProjection]
    [∀ i, (⨅ n, U i n).HasOrthogonalProjection]
    [∀ i, (⨅ n, V i n).HasOrthogonalProjection]
    (hU : ∀ i, Antitone (U i)) (hV : ∀ i, Antitone (V i))
    (hU0 : ∀ i, U i 0 = ⊤) (hV0 : ∀ i, V i 0 = ⊤)
    (hInitial : ∀ i n, ((W i n)†).comp (W i n) =
      Submodule.projectionShell (U i) n)
    (hFinal : ∀ i n, (W i n).comp ((W i n)†) =
      Submodule.projectionShell (V i) n)
    (hUinf : ∀ i, (⨅ n, U i n).starProjection =
      InnerProductSpace.rankOne ℂ
        (PureState.selectedEmbedding root i (PureState.selectedVector root i))
        (PureState.selectedEmbedding root i (PureState.selectedVector root i)))
    (hVinf : ∀ i, (⨅ n, V i n).starProjection =
      InnerProductSpace.rankOne ℂ
        (PureState.selectedEmbedding root root.classOf
          (PureState.selectedVector root root.classOf))
        (PureState.selectedEmbedding root root.classOf
          (PureState.selectedVector root root.classOf))) :
    ∃ L : PureState.GNSClass A →
        PureState.SelectedAtomicHilbert root →L[ℂ]
          PureState.SelectedAtomicHilbert root,
      (∀ i, L i ∈ unitary
        (PureState.SelectedAtomicHilbert root →L[ℂ]
          PureState.SelectedAtomicHilbert root)) ∧
      (∀ i, L i (PureState.selectedEmbedding root i
          (PureState.selectedVector root i)) =
        PureState.selectedEmbedding root root.classOf
          (PureState.selectedVector root root.classOf)) ∧
      (∀ i n, (L i).comp (Submodule.projectionShell (U i) n) = W i n) ∧
      Representation.IsIrreducible
        (ambientInclusion
          (atomicRepresentation (PureState.selectedRepresentation root)) L)

Here root is , PureState.GNSClass A is , and SelectedAtomicHilbert root is . selectedEmbedding root i (selectedVector root i) is ; the root expression is . The signature retains hInitial,hFinal,hUinf,hVinf as shell hypotheses. The linked proof supplies isIrreducible_selectedRepresentation, no_unitaryIntertwiner_selectedRepresentation and norm_selectedVector to the generic theorem; those are separately cited, rather than assumed to follow from the names of the types.

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

Lean realization notes

The selected vectors are fixed before applying the construction and are not replaced by arbitrary unit vectors. No target capture or simplicity conclusion is part of this result, and the selected representations are not assumed faithful. No countability or separability of or is required.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:39c92e26710d4fb48d5d04f63b9e645279916a2fd6073c40e022f9ddece88d6a

Card revision: 1 · SHA-256: e244b62ef37cd89bb88e21906ffcf366d76ae4d38f5c2da2ce82cef0f7bb177b

Exposition revision: 1 · SHA-256: 288200e633113b2bc2910843475ce4e856c0194e110cb265f09f595f2a058355

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 4e5979432498f1696fc1be57d174785e46f80105b40a19fd5e85d373b9949e7d