Unitary equivalence of nonunital representations

MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent

def

Defines unitary equivalence by an onto complex-linear isometry intertwining the two representations.

Statement

Let A be a complex C*-algebra, not assumed unital; let π and ρ be representations of A on complex Hilbert spaces H and K, respectively. They are unitarily equivalent when an onto complex-linear isometry U from H to K intertwines every represented operator at every vector.

Definition

UnitaryEquivalent π ρ ↔ ∃ U : H ≃ₗᵢ[ℂ] K, ∀ a x, U (π a x) = ρ a (U x).

Assumptions

Let A be a complex C*-algebra, not assumed unital; let π and ρ be representations of A on complex Hilbert spaces H and K, respectively.

Conclusion

They are unitarily equivalent when an onto complex-linear isometry U from H to K intertwines every represented operator at every vector.

Main citations

• MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation

  Exact formal dependency; inspect the linked Card and exact source.

Lean source signature (exact)

def UnitaryEquivalent (pi : NonUnitalCStarRepresentation A H)
    (rho : NonUnitalCStarRepresentation A K) : Prop

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