The canonical compact c₀-decomposition — Exact Mathematics with AI

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.compactC0Decomposition

def

Defines the compact-operator c₀-decomposition associated with a faithful compact-valued representation.

Statement

Let be an injective compact-valued representation of a complex C*-algebra on a complete complex Hilbert space , and write for the compact operators on a Hilbert space . Let be the set of minimal nonzero closed -ideals of , and write for the ideal indexed by . Set . For each , take the chosen cyclic Hilbert space and compact model produced from this same . The definition constructs one -isomorphism

D_\pi:A\longrightarrow\bigoplus_{i\in M(A)}^{c_0}\mathcal K(H_i).

Definition

The index set is the family of all minimal nonzero closed -ideals. The Hilbert space is the compact model space chosen from this same and ideal , with the corresponding compact-model isomorphism .

The target compact-operator -sum is the subalgebra of the bounded product given by

\bigoplus_{i\in M(A)}^{c_0}\mathcal K(H_i) =\left\{(T_i):\forall\varepsilon>0,\ \{i:\|T_i\|\geq\varepsilon\}\text{ is finite}\right\}.

Its algebra operations are coordinatewise and its norm is . See the dependent -sum for this same vanishing condition and inherited norm.

Let be the specified ideal-sum equivalence. Its forward map is the continuous ideal-sum map, whose finite-support values are the corresponding sums in . Let act by the same coordinate models . The RHS uses the compact-coordinate equivalence, namely

D_\pi=E_*\circ S_J^{-1}.

The coordinate-evaluation theorem gives

(D_\pi(a))_i=E_i\bigl((S_J^{-1}(a))_i\bigr).

The single-coordinate formula, finite-truncation formula, and inverse identification specify

D_\pi^{-1}(\operatorname{single}_i T)=\iota_i(E_i^{-1}(T)),\qquad D_\pi^{-1}(\operatorname{truncate}_F T)=\sum_{i\in F}\iota_i(E_i^{-1}(T_i)).

Here is the inclusion, is finite, and truncation retains on and is zero elsewhere. The cited evaluation theorems give these formulas for .

The defining expression uses the canonical ideal family, the orthogonality theorem for the minimal ideal family, the spaces and maps , and the density theorem for finite sums of these ideals. These theorems guarantee orthogonality and density for the specified ideal family; neither is an additional assumption.

Assumptions

Only and its faithfulness and pointwise compactness are inputs beyond the algebra and Hilbert structures. The cited theorems guarantee orthogonality, density, nonzero Hilbert spaces, and compact models for this family. The index can be empty. No unit, nonzero algebra, countability, separability, or finite-dimensionality is imposed.

Conclusion

The output is a -isomorphism using the same ideal family, representation and dependent model choices throughout. The definition permits an empty index family and does not assume a nonzero algebra. It does not identify the block algebra with all compact operators on a Hilbert sum.

Main citations

Lean source signature (exact)

Exact source and declaration. The complete defining right-hand side is included.

def compactC0Decomposition :
    letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A
    letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A
    A ≃⋆ₐ[ℂ] CompactOperatorC0Sum
      (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi) := by
  letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A
  letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A
  exact ClosedStarIdeal.compactC0SumEquivOfDense
    (minimalClosedStarIdealFamily (A := A))
    pairwiseOrthogonal_minimalClosedStarIdealFamily
    (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)
    (fun i => i.compactModelEquiv pi hpi)
    (dense_finiteSums_minimalClosedStarIdealFamily pi hpi)

In the source	Mathematical meaning
Exact declaration`pi`, `hpi` in the surrounding context	The fixed faithful compact-valued representation , used for all the models.
The result-type Exact declaration`letI` expressions	The compatible spectral order on used in this construction.
Exact declaration`minimalClosedStarIdealFamily (A := A)`	The family of all minimal nonzero closed -ideals of .
Exact declaration`pairwiseOrthogonal_minimalClosedStarIdealFamily`	The guarantee that for , and . It is not an extra hypothesis.
Exact declaration`i.CompactModelSpace pi hpi`	The chosen cyclic Hilbert space for the ideal and the same representation .
Exact declaration`i.compactModelEquiv pi hpi`	The -isomorphism using that ideal's chosen projection and cyclic vector.
Exact declaration`dense_finiteSums_minimalClosedStarIdealFamily pi hpi`	The guarantee that finite sums of elements of the ideals are norm dense in . This too follows from the cited result, rather than being an extra input.
Exact declaration`compactC0SumEquivOfDense`	The map : first take ideal coordinates using the inverse of the specified ideal-sum map, then apply the same in each coordinate.
Exact declaration`A ≃⋆ₐ[ℂ] CompactOperatorC0Sum ...`	A -isomorphism from onto the displayed -sum of compact-operator algebras.

Exact surrounding source context (separate excerpts)

Source lines 53-60:

universe u v

variable {A : Type u} [NonUnitalCStarAlgebra A]
variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)

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

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

Technical documentation