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.

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.

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

The stated existence or structural result — MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel
Generic atomic-shell construction with its full input hypotheses — MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_atomicShellModel
Irreducibility of each selected GNS fiber — MathlibAnnex.CStarAlgebra.PureState.isIrreducible_selectedRepresentation
Inequivalence of distinct selected classes — MathlibAnnex.CStarAlgebra.PureState.no_unitaryIntertwiner_selectedRepresentation
Norm one of the selected cyclic vectors — MathlibAnnex.CStarAlgebra.PureState.norm_selectedVector
Selected coordinate inclusions — MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding

Supporting route explanation

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)

In the source	Mathematical meaning
`A; root : PureState A; PureState.GNSClass A`	A unital ordered complex C*-algebra , a fixed pure root state , and the arbitrary set of pure-GNS unitary-equivalence classes, with root .
`PureState.SelectedAtomicHilbert root`	The square-summable Hilbert sum of the selected GNS spaces of states , with .
`PureState.selectedEmbedding root i (PureState.selectedVector root i)`	The fixed coordinate vector ; is the selected unit GNS cyclic vector, not an arbitrary replacement.
`PureState.selectedEmbedding root root.classOf (PureState.selectedVector root root.classOf)`	The same distinguished vector at the root class.
`W : PureState.GNSClass A → ℕ → ... →L[ℂ] ...`	The supplied bounded complex-linear shell operators on , for all GNS classes and all natural .
`U V; Submodule ℂ (...)`	For each index and natural , subspaces of . Write and for their orthogonal projections.
`[∀ i n, (U i n).HasOrthogonalProjection]; [∀ i n, (V i n).HasOrthogonalProjection]`	Every subspace in both flags admits an orthogonal projection, as required separately for each .
`[∀ i, (⨅ n, U i n).HasOrthogonalProjection]; [∀ i, (⨅ n, V i n).HasOrthogonalProjection]`	The two intersections and also admit orthogonal projections, written .
`hU : ∀ i, Antitone (U i)`	For every the initial flag decreases: implies .
`hV : ∀ i, Antitone (V i)`	For every the final flag decreases: implies .
`hU0 : ∀ i, U i 0 = ⊤`	The initial flag begins with .
`hV0 : ∀ i, V i 0 = ⊤`	The final flag begins with .
`hInitial : ∀ i n, ((W i n)†).comp (W i n) = Submodule.projectionShell (U i) n`	For every , . Postfix `†` is the Hilbert adjoint and `.comp` composes operators rightmost first.
`hFinal : ∀ i n, (W i n).comp ((W i n)†) = Submodule.projectionShell (V i) n`	For every , , the final support of the same shell map.
`hUinf : ∀ i, (⨅ n, U i n).starProjection = InnerProductSpace.rankOne ℂ ... ...`	The initial intersection projection is , with and inner product linear in its second entry.
`hVinf : ∀ i, (⨅ n, V i n).starProjection = InnerProductSpace.rankOne ℂ ... ...`	The final intersection projection is , with the same root vector for every . Both rank-one identities are given hypotheses, not automatic properties of arbitrary flags.
`∃ L : PureState.GNSClass A → ... →L[ℂ] ...`	One family on the same satisfies all the following conclusions.
`∀ i, L i ∈ unitary (...)`	Every is unitary on .
`∀ i, L i (PureState.selectedEmbedding ... i ...) = PureState.selectedEmbedding ... root.classOf ...`	Every sends the fixed selected vector to .
`∀ i n, (L i).comp (Submodule.projectionShell (U i) n) = W i n`	Every prescribed initial shell has the operator action .
`Representation.IsIrreducible (ambientInclusion (atomicRepresentation (PureState.selectedRepresentation root)) L)`	The inclusion of acts irreducibly, where is the selected pure-GNS direct sum. All flags and shell identities remain supplied hypotheses; purity supplies the fiber representation properties only.
Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.AtomicConstruction.exists_irreducible_pureAtomicShellModel

Accepted content SHA-256: 5acad45a19c66110cd95c932be07fe6a64add6bc7ce462833711250280361b1e

Accepted source guide SHA-256: 87a720265f59825ab35a32440dfc635ffad95e2677e25e4028a380dd87e78465

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73