Physicslib4.GNS.Covariance

GNS covariance under a *-isomorphism

The GNS data transports covariantly along an isomorphism of the algebras. Let Φ : A ≃⋆ₐ[ℂ] B be a *-isomorphism of unital C*-algebras and ω a state on B. Then the GNS representation of the pullback state ω ∘ Φ (State.comp) is unitarily equivalent to π_ω ∘ Φ.

The mechanism is GNS uniqueness. Because Φ is surjective, the pulled-back representation π_ω ∘ Φ of A on the same Hilbert space H_ω has the same cyclic vector Ω_ω (the two orbits coincide as sets), and it reproduces ω ∘ Φ by the defining equation of the pullback state. So (H_ω, π_ω ∘ Φ, Ω_ω) and any GNS triple of ω ∘ Φ are two cyclic representations of A attached to the one state ω ∘ Φ, and gns_unique supplies the intertwining unitary.

Combined with the invariance of irreducibility and factoriality under unitary equivalence, this is the mechanism by which superselection sectors transport along an isomorphism of the observable algebra.

theorem Physicslib4.GNS.isCyclicVector_comp_of_surjective {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : B →⋆ₐ[ℂ] H →L[ℂ] H} {Ω : H} (hcyc : IsCyclicVector π Ω) {Φ : A →⋆ₐ[ℂ] B} (hsurj : Function.Surjective ⇑Φ) : IsCyclicVector (π.comp Φ) Ω

Cyclicity pulls back along a surjective *-homomorphism. If Ω is cyclic for π : B →⋆ₐ[ℂ] (H →L[ℂ] H) and Φ : A →⋆ₐ[ℂ] B is surjective, then Ω is cyclic for the composite representation π ∘ Φ of A: surjectivity makes the two orbits {π (Φ a) Ω} and {π b Ω} coincide as sets, so density transfers.

theorem Physicslib4.GNS.exists_unitary_of_gns_comp {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] (Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) {H₁ : Type u_4} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), (ω.comp Φ.toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_5} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : B), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : ∃ (U : H₁ ≃ₗᵢ[ℂ] H₂), U Ω₁ = Ω₂ ∧ ∀ (a : A) (x : H₁), U ((π₁ a) x) = (π₂ (Φ a)) (U x)

GNS covariance: along a *-isomorphism Φ : A → B, the GNS data of ω ∘ Φ and of ω correspond.

Let ω be a state on B, (H₁, π₁, Ω₁) a cyclic representation of A reproducing the pullback ω ∘ Φ (State.comp), and (H₂, π₂, Ω₂) a cyclic representation of B reproducing ω. Then there is a unitary U : H₁ → H₂ with UΩ₁ = Ω₂ and

U π₁(a) = π₂(Φ(a)) U for all a ∈ A.

So relabelling the observables by an isomorphism changes the GNS representation only by a unitary. The proof applies GNS uniqueness (gns_unique) to π₁ and to π₂ ∘ Φ, which has the same cyclic vector Ω₂ because Φ is surjective (isCyclicVector_comp_of_surjective). For a Haag–Kastler net, Φ can be the covariance isomorphism α_L of Axiom 5 between local algebras.

Implementation note: U is a linear isometric equivalence H₁ ≃ₗᵢ[ℂ] H₂, and the intertwining is stated pointwise, U(π₁(a)x) = π₂(Φ(a))(Ux).

Blueprint: thrm:gns-covariance

theorem Physicslib4.GNS.unitaryEquiv_comp_of_gns {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] (Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) {H₁ : Type u_4} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), (ω.comp Φ.toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_5} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : B), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : UnitaryEquiv π₁ (π₂.comp Φ.toStarAlgHom)

The GNS representation of a pullback state ω ∘ Φ is unitarily equivalent to π ∘ Φ.

With the hypotheses of exists_unitary_of_gns_comp, π₁ and the composite π₂ ∘ Φ are unitarily equivalent representations of A (UnitaryEquiv). Since unitary equivalence preserves irreducibility and the factor property, the sector type is transported along Φ (isIrreducible_iff_of_gns_comp, isFactor_iff_of_gns_comp).

Blueprint: thrm:gns-covariance-unitary-equiv

Transport of the representation type along a surjection

theorem Physicslib4.GNS.range_comp_of_surjective {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : B →⋆ₐ[ℂ] H →L[ℂ] H) {Φ : A →⋆ₐ[ℂ] B} (hsurj : Function.Surjective ⇑Φ) : Set.range ⇑(π.comp Φ) = Set.range ⇑π

Pullback along a surjection preserves the image. For surjective Φ : A →⋆ₐ[ℂ] B, the composite π ∘ Φ has the same image as π.

theorem Physicslib4.GNS.isIrreducible_comp_iff {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : B →⋆ₐ[ℂ] H →L[ℂ] H} {Φ : A →⋆ₐ[ℂ] B} (hsurj : Function.Surjective ⇑Φ) : IsIrreducible (π.comp Φ) ↔ IsIrreducible π

Irreducibility is unchanged by pullback along a surjection. Irreducibility is triviality of the commutant of the image, and the image is unchanged, so π ∘ Φ is irreducible exactly when π is.

theorem Physicslib4.GNS.gnsVonNeumann_comp_of_surjective {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] {H : Type u_3} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : B →⋆ₐ[ℂ] H →L[ℂ] H) {Φ : A →⋆ₐ[ℂ] B} (hsurj : Function.Surjective ⇑Φ) : gnsVonNeumann (π.comp Φ) = gnsVonNeumann π

The generated von Neumann algebra is unchanged by pullback along a surjection. Both are the double commutant of the same image: (π ∘ Φ)(A)'' = π(B)''.

theorem Physicslib4.GNS.isIrreducible_iff_of_gns_comp {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] (Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) {H₁ : Type u_4} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), (ω.comp Φ.toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_5} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : B), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : IsIrreducible π₁ ↔ IsIrreducible π₂

Irreducibility transports along a *-isomorphism. With the GNS hypotheses of exists_unitary_of_gns_comp, the GNS representation of the pullback state ω ∘ Φ is irreducible exactly when the GNS representation of ω is.

theorem Physicslib4.GNS.isFactor_iff_of_gns_comp {A : Type u_1} [CStarAlgebra A] {B : Type u_2} [CStarAlgebra B] (Φ : A ≃⋆ₐ[ℂ] B) (ω : State B) {H₁ : Type u_4} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] (π₁ : A →⋆ₐ[ℂ] H₁ →L[ℂ] H₁) (Ω₁ : H₁) (hcyc₁ : IsCyclicVector π₁ Ω₁) (hrep₁ : ∀ (a : A), (ω.comp Φ.toStarAlgHom) a = inner ℂ Ω₁ ((π₁ a) Ω₁)) {H₂ : Type u_5} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] (π₂ : B →⋆ₐ[ℂ] H₂ →L[ℂ] H₂) (Ω₂ : H₂) (hcyc₂ : IsCyclicVector π₂ Ω₂) (hrep₂ : ∀ (b : B), ω b = inner ℂ Ω₂ ((π₂ b) Ω₂)) : IsFactor (gnsVonNeumann π₁) ↔ IsFactor (gnsVonNeumann π₂)

Factoriality transports along a *-isomorphism. With the GNS hypotheses of exists_unitary_of_gns_comp, π₁(A)'' is a factor exactly when π₂(B)'' is. So an isomorphism of the observable algebra preserves the type of the superselection sector.