MathlibAnnex.Analysis.CStarAlgebra.C0DirectSum
abbrev
Names the algebra of bounded families that vanish at infinity.
Statement
Let be any index set and let be a complex C*-algebra for each , with no identity required. The dependent -direct sum is the algebra of families in the bounded product satisfying the vanishing condition below.
Definition
The ambient bounded product consists of families with , equipped with its supremum norm. Write
inside that bounded product. Operations are coordinatewise, and the norm is inherited. This subalgebra is norm closed, with the inherited C*-algebra structure.
Assumptions
Each fiber has its given complex C*-algebra structure. No identity, countability, separability, nonzero-fiber or nonempty-index assumption is imposed.
Conclusion
The abbreviation denotes this subalgebra, with the vanishing condition imposed for every positive threshold.
Main citations
Lean source signature (exact)
The following is the complete defining right-hand side, copied from the fixed source.
abbrev C0DirectSum {ι : Type uι} (A : ι → Type uA)
[∀ i, NonUnitalCStarAlgebra (A i)] :=
C0DirectSum.starSubalgebra A
| In the source | Mathematical meaning |
|---|---|
Exact declaration{ι : Type uι} (A : ι → Type uA) |
An arbitrary index set and its family of algebras . |
Exact declaration[∀ i, NonUnitalCStarAlgebra (A i)] |
Each fiber carries the specified complex C*-structure. |
Exact declarationC0DirectSum.starSubalgebra A |
The subalgebra of bounded families: is finite for every . Its operations are coordinatewise and its norm is the supremum norm. |
Exact surrounding source context (separate excerpts)
Source lines 34–36:
namespace MathlibAnnex.Analysis.CStarAlgebra
universe uι uA uH
Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·