Local von Neumann algebras and spacelike commutation

In a representation π of the quasilocal algebra, the local von Neumann algebra of a region B is the bicommutant R(B) = π(𝔘(B))'' of the local observable operators. Mathlib models the commutant by Set.centralizer, so R(B) is the double centralizer.

The headline result is microcausality at the von Neumann level: for completely spacelike-separated regions B₁, B₂, the local algebras commute, R(B₁) ⊆ R(B₂)'. It is the von Neumann form of Einstein causality (einstein_causality): elementwise commutation of the local operators, pushed through the centralizer.

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localOperators (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : Set (H →L[ℂ] H)

The local observable operators of a region B in a representation π: the image π(𝔘(B)) of the local algebra.

Equations

• N.localOperators π B = Set.range fun (a : N.U.algebra B) => π ((N.commAlgebra.ι B) a)

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : Set (H →L[ℂ] H)

The local von Neumann algebra R(B) = π(𝔘(B))'', the bicommutant of the local observable operators (the commutant being Set.centralizer).

Equations

• N.localVonNeumann π B = (N.localOperators π B).centralizer.centralizer

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_subset_centralizer (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) : N.localVonNeumann π B₁ ⊆ (N.localVonNeumann π B₂).centralizer

Microcausality at the von Neumann level. For completely spacelike-separated basis regions B₁, B₂, the local von Neumann algebras commute: R(B₁) ⊆ R(B₂)'. This is the von Neumann form of Einstein causality.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_mono (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) : N.localVonNeumann π B₁ ⊆ N.localVonNeumann π B₂

Isotony of the net of von Neumann algebras. For basis regions B₁ ⊆ B₂, the local von Neumann algebras are nested: R(B₁) ⊆ R(B₂). The local observables of B₁ embed into those of B₂ via the quasilocal isotony coherence (ι_inclusion), and the double commutant is monotone.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.eq_zero_of_commute_of_cyclic {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] {S : Set (H →L[ℂ] H)} {Ω : H} (hcyc : Dense ((fun (T : H →L[ℂ] H) => T Ω) '' S)) {R : H →L[ℂ] H} (hcomm : ∀ T ∈ S, R * T = T * R) (hRΩ : R Ω = 0) : R = 0

Statistical independence (abstract form). If Ω is cyclic for a set S of operators (the vectors T Ω, T ∈ S, are dense), then any operator R commuting with every element of S and annihilating Ω is zero.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_separating (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) {Ω : H} (hcyc : Dense ((fun (T : H →L[ℂ] H) => T Ω) '' N.localOperators π B₁)) {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumann π B₂) (hRΩ : R Ω = 0) : R = 0

Statistical independence (Schlieder property), Minkowski spacetime. If Ω is cyclic for the local observables of B₁ - in Minkowski spacetime this cyclicity is supplied by the Reeh-Schlieder theorem - then a nonzero element of the spacelike-separated local von Neumann algebra R(B₂) cannot annihilate Ω: R Ω = 0 ⟹ R = 0. So Ω is separating for R(B₂). The cyclicity hypothesis is the Reeh-Schlieder input (which rests on the spectrum condition); the implication itself is elementary.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localOperators_selfAdjoint (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) (x : H →L[ℂ] H) : x ∈ N.localOperators π B → star x ∈ N.localOperators π B

The local observable operators π(𝔘(B)) form a self-adjoint set: π and the quasilocal embedding ι are *-homomorphisms, so star (π (ι B a)) = π (ι B (star a)).

noncomputable def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : VonNeumannAlgebra H

The local von Neumann algebra R(B) as a genuine VonNeumannAlgebra: the bicommutant of the self-adjoint set of local observable operators. Its underlying set is localVonNeumann π B.

Equations

• N.localVonNeumannAlgebra π B = Physicslib4.GNS.vonNeumannOfSelfAdjoint (N.localOperators π B) ⋯

@[simp]

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.coe_localVonNeumannAlgebra (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (B : Set StandardMinkowskiSpacetime.Carrier) : ↑(N.localVonNeumannAlgebra π B) = N.localVonNeumann π B

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) : N.localVonNeumannAlgebra π B₁ ≤ (N.localVonNeumannAlgebra π B₂).commutant

Microcausality, bundled (Minkowski). For completely spacelike-separated regions, R(B₁) ≤ R(B₂)' as von Neumann algebras (VonNeumannAlgebra.commutant).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B B' : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) (hB' : IsAlexandrovBasisSet B') (hsub : B' ⊆ StandardMinkowskiSpacetime.spacelikeComplement standardMinkowskiTimeOrientation B) : N.localVonNeumannAlgebra π B' ≤ (N.localVonNeumannAlgebra π B).commutant

Additive-free locality (Minkowski). A bounded region lying in the spacelike complement of B has its local algebra inside the commutant of R(B): for basis sets B' ⊆ B^⊥, R(B') ≤ R(B)'. This repackages microcausality through the spacelike complement, keeping strictly to bounded (diamond) regions — no algebra is attached to the unbounded complement.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_mono (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) : N.localVonNeumannAlgebra π B₁ ≤ N.localVonNeumannAlgebra π B₂

Isotony, bundled (Minkowski). B₁ ⊆ B₂ ⟹ R(B₁) ≤ R(B₂) as von Neumann algebras.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_separating (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) {Ω : H} (hcyc : Dense ((fun (T : H →L[ℂ] H) => T Ω) '' N.localOperators π B₁)) {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumannAlgebra π B₂) (hRΩ : R Ω = 0) : R = 0

Statistical independence, bundled (Minkowski). If Ω is cyclic for the local observables of B₁ (the Reeh-Schlieder input), then Ω is separating for the bundled local von Neumann algebra R(B₂) of a spacelike-separated region: any R ∈ R(B₂) with R Ω = 0 is zero.

noncomputable def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.vonNeumannNet (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.commAlgebra.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : { B : Set StandardMinkowskiSpacetime.Carrier // IsAlexandrovBasisSet B } →o VonNeumannAlgebra H

The net of von Neumann algebras as an order-preserving map. Packaging isotony, the assignment B ↦ R(B) is a monotone map from the poset of basis regions (ordered by inclusion) to the von Neumann algebras of B(H). This is the statement that the local net is a functor on the inclusion poset: containment of regions is sent to containment of algebras.

Equations

• One or more equations did not get rendered due to their size.