MATHLIBANNEX / CANONICAL DECLARATION CARD

A compact-operator model for a representation

MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

def

Packages faithfulness together with the equality .

Statement

Let be a complex -algebra, with no unit assumed, let be a complex Hilbert space, and let be a -representation. The predicate below asserts that identifies exactly with the compact operators on .

Definition

The three conditions are Equivalently, is faithful and ; hence is -isomorphic to through the specified representation.

Assumptions

No separability, irreducibility or singleton-spectrum hypothesis is part of this definition. A unit is not assumed.

Conclusion

The output is a property of the given representation , not merely an assertion that some abstract -isomorphism exists.

Main citations

Lean source signature (exact)

The complete declaration below is a separate exact source excerpt; the original header record is retained with the manuscript.

/-- A nonunital star representation that is injective and has precisely the
compact operators as its range.  This is the unbundled form of a star
isomorphism with `K(H)`. -/
def IsCompactOperatorModel [NonUnitalCStarAlgebra A]
    (e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) : Prop :=
  Function.Injective e ∧
    (∀ a : A, IsCompactOperator (e a)) ∧
    ∀ T : H →L[ℂ] H, IsCompactOperator T → ∃ a : A, e a = T
In the source Mathematical meaning
[NonUnitalCStarAlgebra A] The complex -algebra ; a unit is not required.
(e : A →⋆ₙₐ[ℂ] (H →L[ℂ] H)) The given -representation .
Function.Injective e Equal represented operators imply equal algebra elements.
(∀ a : A, IsCompactOperator (e a)) Every element of is sent to a compact operator; this is .
∀ T : H →L[ℂ] H, IsCompactOperator T → ∃ a : A, e a = T Choose any bounded operator ; if it is compact, choose an element of the original algebra whose image is exactly . This is the opposite inclusion.
: Prop The conjunction of injectivity and the two inclusions and .

Exact source and proof.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.Analysis.CStarAlgebra.IsCompactOperatorModel

Accepted content SHA-256: 2ccd05514cd6571908decd8a6e1d8a3991d3eeb9e9dcaf01b7070510bdeaeea8

Accepted source guide SHA-256: d640d0b8566257ea8525354777d4a81352e71a27795c169ca2acfe7a7c614066

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑