MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent
def
Defines equivalence by one surjective isometry intertwining all algebra actions.
Statement
Let be a complex -algebra, with no unit assumed, and let and be -representations on complex Hilbert spaces. They are unitarily equivalent precisely when the following condition holds.
Definition
There exists a surjective complex-linear isometry such that Equivalently, for all , or . The inverse exists because is onto as well as isometric. An abstract isomorphism of and without these intertwining equations is not the defined condition.
Assumptions
Both representations have the same source algebra. Neither irreducibility, nonzero action, separability, nor finite dimension is required.
Conclusion
One unitary from onto intertwines the two actions of every algebra element.
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.
def UnitaryEquivalent (pi : NonUnitalCStarRepresentation A H)
(rho : NonUnitalCStarRepresentation A K) : Prop :=
∃ U : H ≃ₗᵢ[ℂ] K, ∀ (a : A) (x : H), U (pi a x) = rho a (U x)| In the source | Mathematical meaning |
|---|---|
(pi : NonUnitalCStarRepresentation A H) |
The representation on the complete complex Hilbert space . |
(rho : NonUnitalCStarRepresentation A K) |
The representation of the same on the complete complex Hilbert space . |
∃ U : H ≃ₗᵢ[ℂ] K |
Choose one complex-linear isometric equivalence , including surjectivity and an inverse. |
∀ (a : A) (x : H) |
That same must work for every algebra element and every vector in its domain. |
U (pi a x) = rho a (U x) |
Act by in and then apply , or first apply and then act by in ; the two resulting vectors are equal. |
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF · Back to Project
Exact content identity
Declaration: MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent
Accepted content SHA-256: 098cb190191b380a9c3446b3de808b5737235cbd46c11ee75113ccf4ca622ea0
Accepted source guide SHA-256: 6a635660384b2f89fd8a4b3786b7fcf4bc221d50a0b2942732d496444b8c3e7f
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73