The specified equivalence from a dense orthogonal ideal sum

MathlibAnnex.Analysis.CStarAlgebra.ClosedStarIdeal.c0SumEquivOfDense

def

Identifies an algebra with the c₀-sum of a dense orthogonal family of closed ideals.

Statement

Let be a family of closed -ideals in a complex C*-algebra . Assume whenever , and , and that the set of finite sums of elements of these ideals is norm dense in . The ideal-sum map defines a -isomorphism from the dependent -sum of these ideals onto .

Definition

Give each ideal its inherited algebra structure, with inclusion . Use the dependent -sum of these ideals. The forward map is the continuous ideal-sum map

S_J:\bigoplus_i^{c_0}I_i\longrightarrow A.

The single-coordinate and finite-truncation formulas are

S_J(\operatorname{single}_i x)=\iota_i(x),\qquad S_J(\operatorname{truncate}_F x)=\sum_{i\in F}\iota_i(x_i).

Here truncation sets coordinates outside the finite set to zero. On a general family, is the continuous extension of finite ideal summation. Its injectivity and surjectivity under density make this same map a bijection. It preserves addition, multiplication, complex scalars and involution.

Assumptions

The family consists of closed -ideals satisfying the stated ordered zero-product condition. Density concerns all finite sums in , not density of each individual ideal. No countability or nonempty-index assumption is imposed.

Conclusion

The output is directed from the ideal -sum to . Its inverse gives the ideal coordinates used in the subsequent compact-operator decomposition.

Main citations

Lean source signature (exact)

Complete contiguous definition from the fixed source:

def c0SumEquivOfDense (hJ : PairwiseOrthogonal J)
    (hdense : Dense (finiteSums J)) :
    C0DirectSum (Fiber J) ≃⋆ₐ[ℂ] A :=
  { Equiv.ofBijective (c0SumHom J hJ)
      ⟨c0SumHom_injective J hJ, c0SumHom_surjective J hJ hdense⟩ with
    map_add' := map_add (c0SumHom J hJ)
    map_mul' := map_mul (c0SumHom J hJ)
    map_smul' := map_smul (c0SumHom J hJ)
    map_star' := map_star (c0SumHom J hJ) }

In the source	Mathematical meaning
Exact declaration`J : ι → ClosedStarIdeal A` and `Fiber J`	The family ; `Fiber J i` is the same ideal , regarded as an algebra with its inherited operations.
Exact declaration`hJ` and `hdense`	The displayed zero-product and finite-sum density assumptions.
Exact declaration`Equiv.ofBijective (c0SumHom J hJ) ...`	A bijection with exactly the existing ideal-sum map as its forward function; named results supply the two properties.
Exact declaration`map_add'`, `map_mul'`, `map_smul'`, `map_star'`	These fields equip that same equivalence with its complex -algebra structure.
Exact declaration`C0DirectSum (Fiber J) ≃⋆ₐ[ℂ] A`	The direction is from the coordinate family to the ambient algebra.

Exact surrounding source context (separate excerpts)

Source lines 44–48:

universe uι uA

variable {ι : Type uι} {A : Type uA} [NonUnitalCStarAlgebra A]

namespace ClosedStarIdeal

Source lines 63–63:

variable (J : ι → ClosedStarIdeal A)

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

Technical documentation