Unitary equivalence of representations

Two *-representations π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁) and π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂) are unitarily equivalent when there is a Hilbert-space isometric isomorphism U : H₁ ≃ₗᵢ[ℂ] H₂ intertwining them: U (π₁ a x) = π₂ a (U x). This is the basic equivalence of the representation theory underlying superselection sectors.

This file defines UnitaryEquiv, proves it is an equivalence relation (reflexive, symmetric, transitive), and shows that the two central representation-theoretic properties — irreducibility and factoriality (trivial center of the generated von Neumann algebra) — are invariants of unitary equivalence. The transport is packaged through the cross-space conjugation conjMulEquiv U : (H₁ →L[ℂ] H₁) ≃* (H₂ →L[ℂ] H₂), T ↦ U T U⁻¹, which carries π₁(A) onto π₂(A), centralizers onto centralizers, and scalars onto scalars.

def Physicslib4.GNS.UnitaryEquiv {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) : Prop

Two *-representations of A are unitarily equivalent when an isometric isomorphism of the underlying Hilbert spaces intertwines them.

Equations

• Physicslib4.GNS.UnitaryEquiv π₁ π₂ = ∃ (U : H₁ ≃ₗᵢ[ℂ] H₂), ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)

Equivalence relation

theorem Physicslib4.GNS.UnitaryEquiv.refl {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) : UnitaryEquiv π π

Unitary equivalence is reflexive.

theorem Physicslib4.GNS.UnitaryEquiv.symm {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h : UnitaryEquiv π₁ π₂) : UnitaryEquiv π₂ π₁

Unitary equivalence is symmetric.

theorem Physicslib4.GNS.UnitaryEquiv.trans {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {H₃ : Type u_4} [NormedAddCommGroup H₃] [InnerProductSpace ℂ H₃] [CompleteSpace H₃] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} {π₃ : A →⋆ₐ[ℂ] H₃ →L[ℂ] H₃} (h₁₂ : UnitaryEquiv π₁ π₂) (h₂₃ : UnitaryEquiv π₂ π₃) : UnitaryEquiv π₁ π₃

Unitary equivalence is transitive.

Cross-space conjugation of operators

noncomputable def Physicslib4.GNS.conjCLM {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : H₂ →L[ℂ] H₂

Conjugation of an operator T : H₁ →L H₁ by a unitary U : H₁ ≃ₗᵢ H₂, producing U T U⁻¹ : H₂ →L H₂.

Equations

• Physicslib4.GNS.conjCLM U T = ↑↑U ∘SL T ∘SL ↑↑U.symm

@[simp]

theorem Physicslib4.GNS.conjCLM_apply {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) (x : H₂) : (conjCLM U T) x = U (T (U.symm x))

noncomputable def Physicslib4.GNS.conjMulEquiv {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] (U : H₁ ≃ₗᵢ[ℂ] H₂) : (H₁ →L[ℂ] H₁) ≃* (H₂ →L[ℂ] H₂)

Conjugation by U as a multiplicative isomorphism of operator algebras (H₁ →L H₁) ≃* (H₂ →L H₂).

Equations

• Physicslib4.GNS.conjMulEquiv U = { toFun := Physicslib4.GNS.conjCLM U, invFun := Physicslib4.GNS.conjCLM U.symm, left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }

@[simp]

theorem Physicslib4.GNS.conjMulEquiv_apply {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : (conjMulEquiv U) T = conjCLM U T

theorem Physicslib4.GNS.mulEquiv_image_centralizer {M : Type u_5} {N : Type u_6} [Monoid M] [Monoid N] (e : M ≃* N) (s : Set M) : ⇑e '' s.centralizer = (⇑e '' s).centralizer

The general fact that a multiplicative isomorphism carries centralizers to centralizers.

theorem Physicslib4.GNS.conjMulEquiv_pi {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} {U : H₁ ≃ₗᵢ[ℂ] H₂} (hU : ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)) (a : A) : (conjMulEquiv U) (π₁ a) = π₂ a

Conjugation carries π₁(a) to π₂(a) when U intertwines the two representations.

theorem Physicslib4.GNS.conjMulEquiv_image_range {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} {U : H₁ ≃ₗᵢ[ℂ] H₂} (hU : ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)) : ⇑(conjMulEquiv U) '' Set.range ⇑π₁ = Set.range ⇑π₂

Conjugation carries the image of π₁ onto the image of π₂.

theorem Physicslib4.GNS.conjMulEquiv_image_scalar {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] (U : H₁ ≃ₗᵢ[ℂ] H₂) : ⇑(conjMulEquiv U) '' scalarOperators H₁ = scalarOperators H₂

Conjugation fixes the scalar operators setwise.

Invariance of irreducibility and factoriality

theorem Physicslib4.GNS.isIrreducible_iff_centralizer {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {π : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} : IsIrreducible π ↔ (Set.range ⇑π).centralizer = scalarOperators H₁

Irreducibility is exactly triviality of the commutant: the commutant of the image π(A) is the scalar operators.

theorem Physicslib4.GNS.UnitaryEquiv.isIrreducible {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h : UnitaryEquiv π₁ π₂) (hirr : IsIrreducible π₁) : IsIrreducible π₂

Irreducibility is a unitary invariant. If π₁ is unitarily equivalent to π₂ and π₁ is irreducible, then so is π₂.

theorem Physicslib4.GNS.UnitaryEquiv.isIrreducible_iff {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h : UnitaryEquiv π₁ π₂) : IsIrreducible π₁ ↔ IsIrreducible π₂

Irreducibility is invariant under unitary equivalence (iff form).

theorem Physicslib4.GNS.conjMulEquiv_image_gnsVonNeumann {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} {U : H₁ ≃ₗᵢ[ℂ] H₂} (hU : ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ a) (U x)) : gnsVonNeumann π₂ = ⇑(conjMulEquiv U) '' gnsVonNeumann π₁

Conjugation carries the generated von Neumann algebra of π₁ onto that of π₂.

theorem Physicslib4.GNS.UnitaryEquiv.isFactor {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h : UnitaryEquiv π₁ π₂) (hf : IsFactor (gnsVonNeumann π₁)) : IsFactor (gnsVonNeumann π₂)

Factoriality is a unitary invariant. If π₁ is unitarily equivalent to π₂ and the von Neumann algebra π₁(A)'' is a factor, then so is π₂(A)''.

theorem Physicslib4.GNS.UnitaryEquiv.isFactor_iff {A : Type u_1} [CStarAlgebra A] {H₁ : Type u_2} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] {H₂ : Type u_3} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] {π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁} {π₂ : A →⋆ₐ[ℂ] H₂ →L[ℂ] H₂} (h : UnitaryEquiv π₁ π₂) : IsFactor (gnsVonNeumann π₁) ↔ IsFactor (gnsVonNeumann π₂)

Factoriality is invariant under unitary equivalence (iff form).