Algebraic compact-preimage ideal

MathlibAnnex.CStarAlgebra.compactPreimageIdeal

def

Collects the elements represented by compact operators into a two-sided algebraic ideal.

Statement

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and ρ a representation of A on H. compactPreimageIdeal ρ is the two-sided algebraic ideal of elements whose represented bounded operator is compact. Norm-closedness is a separate theorem and is not a field of this returned TwoSidedIdeal.

Definition

(compactPreimageIdeal ρ : Set A) = {a : A | IsCompactOperator (ρ a)}.

Assumptions

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and ρ a representation of A on H.

Conclusion

compactPreimageIdeal ρ is the two-sided algebraic ideal of elements whose represented bounded operator is compact. Norm-closedness is a separate theorem and is not a field of this returned TwoSidedIdeal.

Main citations

Lean source signature (exact)

def compactPreimageIdeal [NonUnitalCStarAlgebra A]
    (rho : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : TwoSidedIdeal A

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Card JSON