MathlibAnnex.Analysis.CStarAlgebra.CompactOperatorC0Sum
abbrev
Names the c₀-sum of a family of compact-operator algebras.
Statement
Let be any family of complete complex Hilbert spaces. This abbreviation denotes the -sum of the compact-operator algebras .
Definition
Use the dependent -sum with fiber , the compact operators on the given . Its elements are bounded families , , such that for every only finitely many have . Its norm is and its algebra operations are coordinatewise. The RHS specifies precisely this family of subalgebras of bounded operators.
Assumptions
Every has its own normed additive group, complex inner product and completeness. Zero and infinite-dimensional Hilbert spaces are allowed. There is no restriction on the size of the index set.
Conclusion
The output is an abbreviation for this dependent algebra. It does not denote all compact operators on a Hilbert-space sum and does not include additional off-diagonal operator entries.
Main citations
Lean source signature (exact)
The following is the complete defining right-hand side, copied from the fixed source.
abbrev CompactOperatorC0Sum {ι : Type uι} (H : ι → Type uH)
[∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)]
[∀ i, CompleteSpace (H i)] :=
C0DirectSum
(fun i => ContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i))
| In the source | Mathematical meaning |
|---|---|
Exact declarationH : ι → Type uH |
The family of Hilbert spaces ; the spaces may vary with . |
The three Exact declaration∀ i instances |
Each has the stated norm and complex inner product and is complete. |
Exact declarationContinuousLinearMap.compactOperatorStarSubalgebra ℂ (H i) |
The subalgebra of compact complex-linear endomorphisms of this same fiber. |
Exact declarationC0DirectSum (fun i => ...) |
The preceding dependent vanishing-at-infinity construction applied to exactly those algebras. |
Exact surrounding source context (separate excerpts)
Source lines 23–25:
namespace MathlibAnnex.Analysis.CStarAlgebra
universe uι uA uH
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·