Physicslib4.AQFT.HaagKastler.LocalVonNeumann

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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) : Set (H →L[ℂ] H)

The local operators of a diamond B in a representation π: the image π(ι_B(𝔘(B))).

Here π is a *-representation of the quasilocal algebra 𝔘 on a Hilbert space H, and ι_B embeds the local algebra 𝔘(B) in 𝔘. The result is a set of bounded operators on H, written π(𝔘(B)) for short.

Blueprint: def:local-von-neumann

Equations

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

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

The local von Neumann algebra R(B) = π(𝔘(B))'' of a diamond B, as a set of operators.

As you will recall, the commutant S' of a set S of bounded operators is the set of bounded operators commuting with every element of S, and the bicommutant S'' is the commutant of S'. By von Neumann's bicommutant theorem, π(𝔘(B))'' is the weak operator closure of the unital *-algebra π(𝔘(B)), and it is in general larger. localVonNeumannAlgebra is the same set as a bundled von Neumann algebra.

Implementation note: the commutant is Mathlib's Set.centralizer in the bounded operators on H.

Blueprint: def:local-von-neumann

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_subset_centralizer (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) : N.localVonNeumann π hB₁ ⊆ (N.localVonNeumann π hB₂).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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) : N.localVonNeumann π hB₁ ⊆ N.localVonNeumann π hB₂

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.quasilocal.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 π hB₁)) {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumann π hB₂) (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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) (x : H →L[ℂ] H) : x ∈ N.localOperators π hB → star x ∈ N.localOperators π hB

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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) : VonNeumannAlgebra H

The local von Neumann algebra R(B) = π(𝔘(B))'' of a diamond B, as a von Neumann algebra.

The local operators π(𝔘(B)) form a self-adjoint set, and the bicommutant of a self-adjoint set is a von Neumann algebra (Physicslib4.GNS.vonNeumannOfSelfAdjoint). This is that algebra, an element of Mathlib's VonNeumannAlgebra; its underlying set is localVonNeumann (coe_localVonNeumannAlgebra). Inclusions and commutants of local algebras are stated for it with ≤ and VonNeumannAlgebra.commutant.

Blueprint: def:local-von-neumann-algebra

Equations

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

@[simp]

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) : N.localVonNeumannAlgebra π hB₁ ≤ (N.localVonNeumannAlgebra π hB₂).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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B B' : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) (hB' : IsAlexandrovBasisSet B') (hsub : B' ⊆ StandardMinkowskiSpacetime.spacelikeComplement standardMinkowskiTimeOrientation B) : N.localVonNeumannAlgebra π hB' ≤ (N.localVonNeumannAlgebra π hB).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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) : N.localVonNeumannAlgebra π hB₁ ≤ N.localVonNeumannAlgebra π hB₂

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.quasilocal.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 π hB₁)) {R : H →L[ℂ] H} (hR : R ∈ N.localVonNeumannAlgebra π hB₂) (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.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : { B : Set StandardMinkowskiSpacetime.Carrier // IsAlexandrovBasisSet B } →o VonNeumannAlgebra H

The net of local von Neumann algebras B ↦ R(B) in a representation π, as a monotone map.

The map sends each diamond B to R(B) = π(𝔘(B))'' and is monotone, B₁ ⊆ B₂ implying R(B₁) ≤ R(B₂) (localVonNeumannAlgebra_mono): this is isotony for the von Neumann algebras.

Blueprint: def:von-neumann-net

Equations

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

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.commutant_le_commutant_of_le {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] {M₁ M₂ : VonNeumannAlgebra H} (h : M₁ ≤ M₂) : M₂.commutant ≤ M₁.commutant

Antitonicity of the commutant. For bundled von Neumann algebras M₁ ≤ M₂ on H, the commutants reverse the inclusion: M₂' ≤ M₁'.

noncomputable def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.relativeCommutant (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) : VonNeumannAlgebra H

The relative commutant of a nested pair R(B₁) ⊆ R(B₂): the von Neumann algebra R(B₁)' ∩ R(B₂), built as the meet of the star-subalgebras of the commutant of R(B₁) and of R(B₂). Its underlying set is R(B₁)' ∩ R(B₂). This is the basic object of the theory of local-algebra inclusions.

Equations

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

@[simp]

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.coe_relativeCommutant (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) : ↑(N.relativeCommutant π hB₁ hB₂) = (N.localVonNeumann π hB₁).centralizer ∩ N.localVonNeumann π hB₂

The underlying set of the relative commutant is R(B₁)' ∩ R(B₂).

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

The relative commutant lies in the larger algebra: R(B₁)' ∩ R(B₂) ≤ R(B₂).

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

The relative commutant commutes with the smaller algebra: its underlying set is contained in R(B₁)'.

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

The relative commutant contains the center of the ambient algebra. For B₁ ⊆ B₂, the center R(B₂) ∩ R(B₂)' is contained in R(B₁)' ∩ R(B₂). Via isotony R(B₁) ≤ R(B₂) and antitonicity of the commutant.

def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsIrreducibleInclusion (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) : Prop

The inclusion R(B₁) ⊆ R(B₂) is irreducible when its relative commutant is trivial: R(B₁)' ∩ R(B₂) = ℂ·1. This is the subfactor-theoretic notion of an irreducible inclusion.

Equations

• N.IsIrreducibleInclusion π hB₁ hB₂ = (↑(N.relativeCommutant π hB₁ hB₂) = Physicslib4.scalarOperators H)

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

An irreducible inclusion forces the ambient algebra to be a factor. If B₁ ⊆ B₂ and the inclusion R(B₁) ⊆ R(B₂) is irreducible, then R(B₂) is a factor (trivial center). The center R(B₂) ∩ R(B₂)' lies inside the relative commutant (center_le_relativeCommutant), which is the scalars by hypothesis; and the scalars are always central, giving equality.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isIrreducibleInclusion_self_iff_isFactor (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) : N.IsIrreducibleInclusion π hB hB ↔ IsFactor (N.localVonNeumann π hB)

Self-inclusion is irreducible iff the algebra is a factor. The trivial inclusion R(B) ⊆ R(B) is irreducible exactly when R(B) is a factor: the relative commutant of the self-inclusion is R(B)' ∩ R(B), i.e. the center of R(B) (up to the order of intersection), which equals the scalars iff R(B) has trivial center. This is the converse-completing companion to isFactor_of_isIrreducibleInclusion.