Possibly nonunital representation

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation

abbrev

Names nonunital complex star-algebra homomorphisms into bounded operators as the representation type.

Statement

Let A be a complex C*-algebra, not assumed unital, and H a complex Hilbert space. A representation of A on H is a complex-linear nonunital star-algebra homomorphism into the bounded complex-linear operators on H. It preserves addition, multiplication, complex scalar multiplication and involution; neither preservation of a unit nor faithfulness is built in.

Definition

NonUnitalCStarRepresentation A H = A →⋆ₙₐ[ℂ] (H →L[ℂ] H).

Assumptions

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

Conclusion

A representation of A on H is a complex-linear nonunital star-algebra homomorphism into the bounded complex-linear operators on H. It preserves addition, multiplication, complex scalar multiplication and involution; neither preservation of a unit nor faithfulness is built in.

Main citations

Lean source signature (exact)

abbrev NonUnitalCStarRepresentation (A : Type u)
    [NonUnitalCStarAlgebra A] (H : Type v)
    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

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