Geometric covariance of the local von Neumann net

In the covariant representation of a Haag-Kastler net, the implementing unitaries U(L) carry the local von Neumann algebra of a region B onto that of the Lorentz-transformed region L · B: U(L) · R(B) · U(L)⁻¹ = R(L · B).

This is the statement that the symmetry group acts geometrically on the net of von Neumann algebras. It rests on three ingredients, all already available:

• Operator covariance U(L) π(a) U(L)⁻¹ = π(β_L a) (from the GNS unitary construction, IsInvariantState.exists_gns_unitary);
• the fact that the covariance automorphism β_L = C.action L maps the local image ι_B(𝔘(B)) onto ι_{L·B}(𝔘(L·B)) (from action_ι and surjectivity of the covariance equivalence covEquiv);
• the algebraic fact that conjugation by a unit is a multiplicative automorphism, which therefore commutes with the bicommutant.

The reusable algebraic core is MulEquiv.image_centralizer: a multiplicative automorphism maps the centralizer of a set onto the centralizer of its image, hence maps bicommutants to bicommutants.

theorem Physicslib4.GNS.isFactor_gnsVonNeumann_of_isIrreducible {A : Type u_1} [CStarAlgebra A] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {π : A →⋆ₐ[ℂ] H →L[ℂ] H} (hirr : IsIrreducible π) : IsFactor (gnsVonNeumann π)

The von Neumann algebra of an irreducible representation is a factor. This restates center_gnsVonNeumann_eq_of_isIrreducible in the factor vocabulary (Physicslib4.IsFactor, the predicate used for orbit-invariance): the center π(A)'' ∩ (π(A)'')' is exactly the scalars.

def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.covLocalOperators {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : Set (H →L[ℂ] H)

The local observable operators of a region B in a representation π of the quasilocal algebra of a covariant net: the image π(ι_B(𝔘(B))).

Equations

• C.covLocalOperators π B = Set.range fun (a : C.net.U.algebra B) => π ((C.quasilocal.ι B) a)

def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.covLocalVonNeumann {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : Set (H →L[ℂ] H)

The local von Neumann algebra R(B) = π(ι_B(𝔘(B)))'' in a representation π of the covariant net's quasilocal algebra.

Equations

• C.covLocalVonNeumann π B = (C.covLocalOperators π B).centralizer.centralizer

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.lieConj_image_covLocalOperators {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Uop : H ≃ₗᵢ[ℂ] H) (L : InhomogeneousLorentzGroup) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (hcov : ∀ (a : C.quasilocal.carrier) (x : H), Uop ((π a) (Uop.symm x)) = (π ((C.action L) a)) x) : ⇑(lieConj Uop) '' C.covLocalOperators π B = C.covLocalOperators π (L • B)

Conjugation carries the local operators of B onto those of L · B. Given operator covariance U π(a) U⁻¹ = π(β_L a), the conjugation lieConj U maps the local observable operators of B onto those of L · B.

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.lieConj_image_covLocalVonNeumann {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Uop : H ≃ₗᵢ[ℂ] H) (L : InhomogeneousLorentzGroup) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (hcov : ∀ (a : C.quasilocal.carrier) (x : H), Uop ((π a) (Uop.symm x)) = (π ((C.action L) a)) x) : ⇑(lieConj Uop) '' C.covLocalVonNeumann π B = C.covLocalVonNeumann π (L • B)

Geometric covariance of the local von Neumann net (Minkowski). In a covariant representation π of the quasilocal algebra with operator covariance U(L) π(a) U(L)⁻¹ = π(β_L a), conjugation by the implementing unitary U(L) carries the local von Neumann algebra of a region B onto that of the Lorentz-transformed region L · B: U(L) · R(B) · U(L)⁻¹ = R(L · B).

The operator covariance hypothesis is exactly the last clause provided by IsInvariantState.exists_gns_unitary, so this holds in the covariant GNS representation of any invariant state.

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.covLocalOperators_selfAdjoint {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) (x : H →L[ℂ] H) : x ∈ C.covLocalOperators π B → star x ∈ C.covLocalOperators π B

The local observable operators of a region form a self-adjoint set.

noncomputable def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.covLocalVonNeumannAlgebra {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : VonNeumannAlgebra H

The local von Neumann algebra R(B) as a bundled VonNeumannAlgebra.

Equations

• C.covLocalVonNeumannAlgebra π B = Physicslib4.GNS.vonNeumannOfSelfAdjoint (C.covLocalOperators π B) ⋯

@[simp]

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.coe_covLocalVonNeumannAlgebra {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : ↑(C.covLocalVonNeumannAlgebra π B) = C.covLocalVonNeumann π B

noncomputable def Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.covLocalVonNeumannEquiv {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Uop : H ≃ₗᵢ[ℂ] H) (L : InhomogeneousLorentzGroup) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (hcov : ∀ (a : C.quasilocal.carrier) (x : H), Uop ((π a) (Uop.symm x)) = (π ((C.action L) a)) x) : ↥(C.covLocalVonNeumannAlgebra π B).toStarSubalgebra ≃⋆ₐ[ℂ] ↥(C.covLocalVonNeumannAlgebra π (L • B)).toStarSubalgebra

Geometric covariance as a von Neumann algebra isomorphism (Minkowski). Conjugation by the implementing unitary U(L) is the *-isomorphism R(B) ≃ R(L · B) of local von Neumann algebras: it restricts the conjugation *-automorphism T ↦ U(L) T U(L)⁻¹ of B(H) (Mathlib's LinearIsometryEquiv.conjStarAlgEquiv), whose image of R(B) is exactly R(L · B) by geometric covariance.

Equations

• C.covLocalVonNeumannEquiv π Uop L hB hcov = Physicslib4.restrictStarAlgEquiv Uop.conjStarAlgEquiv ⋯ ⋯

theorem Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.covLocalVonNeumann_isFactor_smul {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (C : CovariantQuasilocalAlgebra) (π : C.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (Uop : H ≃ₗᵢ[ℂ] H) (L : InhomogeneousLorentzGroup) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (hcov : ∀ (a : C.quasilocal.carrier) (x : H), Uop ((π a) (Uop.symm x)) = (π ((C.action L) a)) x) (h : IsFactor (C.covLocalVonNeumann π B)) : IsFactor (C.covLocalVonNeumann π (L • B))

Orbit-invariance of factoriality (Minkowski). If the local von Neumann algebra R(B) of a region is a factor (trivial center), then so is R(L · B) for every Lorentz transformation L. Geometric covariance exhibits R(L · B) as the unitary conjugate U(L) R(B) U(L)⁻¹, and conjugation preserves the factor property. So being a factor is constant along the Lorentz orbit of a region.