MathlibAnnex.Analysis.CStarAlgebra.ClosedStarIdeal.compactC0SumEquivOfDense
def
Expresses an algebra in compact-operator coordinates through its orthogonal ideal decomposition.
Statement
Let be a pairwise orthogonal family of closed -ideals whose finite sums are norm dense in a complex C*-algebra . For each ideal , fix a -isomorphism , where is the specified complete complex Hilbert space. This definition gives a -isomorphism from to the compact-operator -sum.
Definition
Let be the specified ideal-sum equivalence. Let apply the given in every coordinate, with the same index retained. The definition is precisely
The target is the compact-operator -sum. The coordinate-evaluation theorem gives
The inverse identification, single-coordinate formula, and finite-truncation formula give
Here is the ideal inclusion; truncation retains precisely the finite coordinate set . The cited evaluation theorems give these formulas.
Assumptions
Orthogonality means that products from distinct ideals vanish. Density concerns their finite sums in the ambient algebra. The coordinate maps are given equivalences onto all compact operators on their respective , not merely faithful compact-valued actions. No countability or nontriviality is added.
Conclusion
Thus first resolves an element into its ideal coordinates and then applies in each coordinate. Its target contains no off-diagonal operator entries and is not asserted to be the full compact-operator algebra of a Hilbert sum.
Main citations
Lean source signature (exact)
Complete contiguous definition from the fixed source:
def compactC0SumEquivOfDense (hdense : Dense (finiteSums J)) :
A ≃⋆ₐ[ℂ] CompactOperatorC0Sum H :=
(c0SumEquivOfDense J hJ hdense).symm.trans
(C0DirectSum.equiv (Fiber J)
(fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))
(Equiv.refl ι) E)
| In the source | Mathematical meaning |
|---|---|
Exact declaration(c0SumEquivOfDense J hJ hdense).symm |
The inverse , directed from to the ideal-coordinate -sum. |
Exact declaration.trans (C0DirectSum.equiv ... (Equiv.refl ι) E) |
First use , then apply coordinatewise, retaining the same index . |
Exact declarationFiber J i and compactOperatorStarSubalgebra ℂ (H i) |
The ideal in the family and the full compact-operator algebra on , respectively. |
Exact declarationhdense : Dense (finiteSums J) |
The density assumption used by the ideal-sum equivalence, not a new conclusion of this definition. |
Exact surrounding source context (separate excerpts)
Source lines 51–58:
variable {ι : Type uι} {A : Type uA} [NonUnitalCStarAlgebra A]
variable (J : ι → ClosedStarIdeal A) (hJ : PairwiseOrthogonal J)
variable (H : ι → Type uH)
variable [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)]
variable [∀ i, CompleteSpace (H i)]
variable (E : ∀ i, Fiber J i ≃⋆ₐ[ℂ]
ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·