Unbundled compact-operator model

MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

def

Packages injectivity, compact-valuedness, and surjectivity onto all compact operators into one unbundled predicate.

Statement

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and e a nonunital complex star-algebra homomorphism from A to the bounded operators on H. The model predicate consists of all three clauses: e is injective; every represented e(a) is compact; and each compact bounded operator T on H equals e(a) for some a in A.

Definition

IsCompactOperatorModel e ↔ Injective e ∧ (∀ a, IsCompactOperator (e a)) ∧ ∀ T, IsCompactOperator T → ∃ a, e a = T.

Assumptions

Let A be a complex C*-algebra, not assumed unital, H a complex Hilbert space, and e a nonunital complex star-algebra homomorphism from A to the bounded operators on H.

Conclusion

The model predicate consists of all three clauses: e is injective; every represented e(a) is compact; and each compact bounded operator T on H equals e(a) for some a in A.

Main citations

Lean source signature (exact)

def IsCompactOperatorModel [NonUnitalCStarAlgebra A]
    (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Prop

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