The same reduced atomic representation and its exact diagonal range

MathlibAnnex.Analysis.CStarAlgebra.PrimitiveSpectrum.reducedAtomicRepresentation_spec_of_isCompactlyRepresented

theorem

Collects the simultaneous properties and exact diagonal range of the same reduced atomic representation.

Statement

Let be a complex C*-algebra, let be a complex Hilbert space, and let be a faithful -representation with . Here denotes the algebra of compact operators on a complex Hilbert space . Write for the primitive ideal spectrum, whose points are the kernels of pure-state GNS representations. For each , fix the pure state selected by the primitive-point representative. Its GNS representation satisfies by the kernel-identification theorem. Write for its GNS Hilbert space and . On , the reduced atomic representation is specified by the coordinate-action theorem:

(R(a)\xi)_P=\rho_P(a)\xi_P\qquad(a\in A,\ \xi\in\mathcal H).

For a bounded family of compact operators with , let act diagonally on :

(\Delta_b(T)\xi)_P=T_P\xi_P,\qquad \sup_P\lVert T_P\rVert<\infty.

Write for the restriction to the -sum: for every , the set is finite. These bounded diagonal and c0-diagonal action formulas refer to the same Hilbert sum. Then, simultaneously:

is injective and compact-valued;
, where is the diagonal action of ;
, where is the diagonal action of the bounded product of compact blocks;
is an isometry and for every ;
for the coordinate projection and embedding , ;
for every .

Assumptions

The given acts on the complete complex Hilbert space . Only its injectivity and pointwise compactness are assumed. No irreducibility, nonzero algebra, nonempty index, countability, or separability is imposed. The Hilbert sum and its selected fibers are the already defined ones.

Conclusion

All outputs concern this one , not a replacement action. Its range is block diagonal; the theorem does not assert that it is all of or that arbitrary off-diagonal compact operators are present. It also does not claim unitary equivalence between and the original .

Main citations

The simultaneous reduced-atomic specification concerns the already defined reduced-atomic map. Its range as a compact c0-diagonal action and range as the compact part of the bounded diagonal action are exact equalities for that same map, not the whole compact-operator algebra.

Lean source signature (exact)

Exact source and declaration. Only the literal signature is displayed here; the linked source retains the proof.

theorem reducedAtomicRepresentation_spec_of_isCompactlyRepresented
    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :
    (reducedAtomicRepresentation (A := A)).IsCompactlyRepresented ∧
    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) =
      (NonUnitalStarAlgHom.range (CompactOperatorC0Sum.diagonalRepresentation
        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ∧
    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) =
      (NonUnitalStarAlgHom.range (CompactOperatorBoundedProduct.diagonalRepresentation
        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ⊓
        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ
          (ReducedAtomicHilbertSpace A) ∧
    Isometry (reducedAtomicRepresentation (A := A)) ∧
    (∀ a : A, ‖reducedAtomicRepresentation (A := A) a‖ = ‖a‖) ∧
    (∀ (a : A) (P : PrimitiveSpectrum A),
      (coordinateProjection P).comp
        ((reducedAtomicRepresentation (A := A) a).comp (coordinateEmbedding P)) =
          P.pureStateRepresentative.gnsRepresentation a) ∧
    (∀ a : A, ContinuousLinearMap.adjoint (reducedAtomicRepresentation (A := A) a) =
      reducedAtomicRepresentation (star a))

Back to the reading-guide item

In the source	Mathematical meaning
Algebra, Hilbert space and positivity`universe u v variable {A : Type u} [NonUnitalCStarAlgebra A] variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]`Fixed source	The complex C*-algebra and complex Hilbert space are independent inputs. Completeness is part of the Hilbert structure. The local spectral-order instances displayed separately provide the positivity used for pure states.
Given faithful compact action`(pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :`Fixed source	The input is the given , faithful with . This hypothesis places no irreducibility or nonzero requirement on .
Meaning of compact representability`def NonUnitalCStarRepresentation.IsCompactlyRepresented (pi : NonUnitalCStarRepresentation A H) : Prop := Function.Injective pi ∧ ∀ a : A, IsCompactOperator (pi a)`Fixed source	Injectivity is faithfulness, and the universal compactness condition says that every is compact. The same definition is applied to in the first conclusion.
Fixed pure-state representatives`def pureStateRepresentative (P : PrimitiveSpectrum A) : NonUnitalPureState A := P.property.choose`Fixed source	For each this selects the fixed pure state . The separately cited kernel theorem identifies , where on . These are the same representatives in every conclusion.
Hilbert sum`abbrev ReducedAtomicHilbertSpace (A : Type u) [NonUnitalCStarAlgebra A] [PartialOrder A] [StarOrderedRing A] := HilbertSum (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS)`Fixed source	The representation space is $\mathcal H=\bigoplus_{P\in\operatorname{Prim}(A)}^2 H_P.$ This is the Hilbert direct sum of the selected GNS spaces, not the algebra of bounded operator families.
Reduced atomic action`theorem reducedAtomicRepresentation_apply (a : A) (x : ReducedAtomicHilbertSpace A) (P : PrimitiveSpectrum A) : reducedAtomicRepresentation a x P = P.pureStateRepresentative.gnsRepresentation a (x P) := by`Fixed source	The coordinate formula specifies the same : $(R(a)\xi)_P=\rho_P(a)\xi_P.$ It holds for every , and .
Faithfulness and compact values of R`(reducedAtomicRepresentation (A := A)).IsCompactlyRepresented ∧`Fixed source	The first conclusion is that this is injective and that is compact for every .
Range as c0 diagonal operators`(NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) = (NonUnitalStarAlgHom.range (CompactOperatorC0Sum.diagonalRepresentation (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ∧`Fixed source	The family argument assigns the same to each primitive ideal. The equality is $\operatorname{ran}R=\operatorname{ran}\Delta_0,$ where acts on the -family of compact blocks defined in the Statement, on the same .
Range as compact bounded-diagonal operators`(NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) = (NonUnitalStarAlgHom.range (CompactOperatorBoundedProduct.diagonalRepresentation (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ⊓ ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (ReducedAtomicHilbertSpace A) ∧`Fixed source	The meet `⊓` is intersection of subalgebras of . Thus $\operatorname{ran}R=\operatorname{ran}\Delta_b\cap\mathcal K(\mathcal H).$ The bounded family and the compact-operator algebra use the same selected Hilbert sum; no off-diagonal operators are added.
Isometry and norm equality`Isometry (reducedAtomicRepresentation (A := A)) ∧ (∀ a : A, ‖reducedAtomicRepresentation (A := A) a‖ = ‖a‖) ∧`Fixed source	The same preserves distances and satisfies $\lVert R(a)\rVert=\lVert a\rVert\qquad(a\in A).$ Both assertions occur explicitly as conjuncts.
Coordinate compression`(∀ (a : A) (P : PrimitiveSpectrum A), (coordinateProjection P).comp ((reducedAtomicRepresentation (A := A) a).comp (coordinateEmbedding P)) = P.pureStateRepresentative.gnsRepresentation a) ∧`Fixed source	The projection and inclusion give $p_PR(a)j_P=\rho_P(a)\qquad(a\in A,\ P\in\operatorname{Prim}(A)).$ The order of the two `comp` operations is exactly this composition.
Adjoint identity`(∀ a : A, ContinuousLinearMap.adjoint (reducedAtomicRepresentation (A := A) a) = reducedAtomicRepresentation (star a)) := by`Fixed source	The last conjunct is $R(a)^=R(a^)\qquad(a\in A).$ The left side is the Hilbert adjoint on and the right side uses the involution of . It concerns the same as all preceding conjuncts.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

attribute [local instance] _root_.CStarAlgebra.spectralOrder
  _root_.CStarAlgebra.spectralOrderedRing

Back to the reading-guide item

Exact surrounding source:

universe u v

variable {A : Type u} [NonUnitalCStarAlgebra A]
variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

Back to the reading-guide item

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation