MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation
abbrev
Names -representations of a complex -algebra on a Hilbert space when no unit equation is required.
Statement
Let
be a complex
-algebra
considered without assuming a unit, and let
be a complex Hilbert space.
NonUnitalCStarRepresentation A H is the type of
-representations
for which no equation involving a unit is required.
Definition
For and , such a map satisfies Each is a bounded complex-linear operator. Nonzero action, irreducibility, injectivity and unit preservation are separate conditions in later declarations.
Assumptions
The Hilbert space is complete. Neither nor is required to be separable or nonzero. A unital algebra is allowed; the abbreviation merely does not require the representation to preserve its unit.
Conclusion
The result is a type of -representations, not a theorem asserting that a chosen representation is nonzero, irreducible or faithful.
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 representation of a possibly genuinely nonunital complex C-star
algebra. -/
abbrev NonUnitalCStarRepresentation (A : Type u)
[NonUnitalCStarAlgebra A] (H : Type v)
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] :=
A →⋆ₙₐ[ℂ] (H →L[ℂ] H)| In the source | Mathematical meaning |
|---|---|
(A : Type u) [NonUnitalCStarAlgebra A] |
The complex -algebra , with no assumption requiring or forbidding a unit. |
(H : Type v) |
The space on which algebra elements will act. |
[NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] |
The complete complex Hilbert-space structure on . |
H →L[ℂ] H |
The space of bounded complex-linear maps from to itself, with composition as multiplication and adjoint as star. |
A →⋆ₙₐ[ℂ] (H →L[ℂ] H) |
The entire right-hand side: the type of -representations , with no unit-preservation field. |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation
Accepted content SHA-256: d540acbe030253d81f4fb82cc96f4c7815a17c9b722d5ebe4363a1407930e3e0
Accepted source guide SHA-256: 08c4aa46c05d4d43d72447d03b53f3e9dfc8f244ee40997d20a9c032f9cb24fc
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73