diff --git a/Physicslib4.lean b/Physicslib4.lean index fefab54..aa17a99 100644 --- a/Physicslib4.lean +++ b/Physicslib4.lean @@ -6,6 +6,7 @@ import Physicslib4.AQFT.HaagKastler.LocalCommutativity import Physicslib4.AQFT.HaagKastler.LocalVonNeumann import Physicslib4.AQFT.HaagKastler.LorentzCovariance import Physicslib4.AQFT.HaagKastler.Net +import Physicslib4.AQFT.HaagKastler.Purity import Physicslib4.AQFT.HaagKastler.QuasilocalAction import Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra import Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness @@ -21,6 +22,7 @@ import Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebras import Physicslib4.AQFT.HaagKastlerCurved.LocalCommutativity import Physicslib4.AQFT.HaagKastlerCurved.LocalVonNeumann import Physicslib4.AQFT.HaagKastlerCurved.Net +import Physicslib4.AQFT.HaagKastlerCurved.Purity import Physicslib4.AQFT.HaagKastlerCurved.Spacetime import Physicslib4.AQFT.HaagKastlerCurved.StabilizerAction import Physicslib4.AQFT.HaagKastlerCurved.StabilizerKMS @@ -33,6 +35,7 @@ import Physicslib4.Basic import Physicslib4.GNS.Basic import Physicslib4.GNS.CauchySchwarz import Physicslib4.GNS.Construction +import Physicslib4.GNS.ExtremeState import Physicslib4.GNS.Irreducibility import Physicslib4.GNS.NullSpace import Physicslib4.GNS.RadonNikodym diff --git a/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean b/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean index 5803459..612645f 100644 --- a/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean +++ b/Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Lean Community -/ import Physicslib4.AQFT.HaagKastler.EinsteinCausality +import Physicslib4.GNS.Irreducibility /-! # Local von Neumann algebras and spacelike commutation @@ -116,6 +117,50 @@ theorem localVonNeumann_separating N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs (Set.subset_centralizer_centralizer hA) exact (Set.mem_centralizer_iff.mp hA') R hR +/-- The local observable operators `π(𝔘(B))` form a self-adjoint set: `π` and the +quasilocal embedding `ι` are `*`-homomorphisms, so `star (π (ι B a)) = π (ι B (star a))`. -/ +theorem localOperators_selfAdjoint (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) + (B : Set StandardMinkowskiSpacetime.Carrier) : + ∀ x ∈ N.localOperators π B, star x ∈ N.localOperators π B := by + rintro x ⟨a, rfl⟩ + exact ⟨star a, by simp only [map_star]⟩ + +/-- 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`. -/ +noncomputable def localVonNeumannAlgebra (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) + (B : Set StandardMinkowskiSpacetime.Carrier) : VonNeumannAlgebra H := + vonNeumannOfSelfAdjoint (N.localOperators π B) (N.localOperators_selfAdjoint π B) + +@[simp] theorem coe_localVonNeumannAlgebra (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) + (B : Set StandardMinkowskiSpacetime.Carrier) : + (N.localVonNeumannAlgebra π B : Set (H →L[ℂ] H)) = N.localVonNeumann π B := + coe_vonNeumannOfSelfAdjoint _ _ + +/-- **Microcausality, bundled (Minkowski).** For completely spacelike-separated +regions, `R(B₁) ≤ R(B₂)'` as von Neumann algebras (`VonNeumannAlgebra.commutant`). -/ +theorem localVonNeumannAlgebra_le_commutant + (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ + (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) + (hs : Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime + standardMinkowskiTimeOrientation B₁ B₂) : + N.localVonNeumannAlgebra π B₁ ≤ (N.localVonNeumannAlgebra π B₂).commutant := by + rw [← SetLike.coe_subset_coe] + simp only [coe_localVonNeumannAlgebra, VonNeumannAlgebra.coe_commutant] + exact N.localVonNeumann_subset_centralizer π hB₁ hB₂ hs + +/-- **Isotony, bundled (Minkowski).** `B₁ ⊆ B₂ ⟹ R(B₁) ≤ R(B₂)` as von Neumann +algebras. -/ +theorem localVonNeumannAlgebra_mono + (π : 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₂ := by + rw [← SetLike.coe_subset_coe] + simp only [coe_localVonNeumannAlgebra] + exact N.localVonNeumann_mono π hB₁ hB₂ h + end HaagKastlerNet end HaagKastler end AQFT diff --git a/Physicslib4/AQFT/HaagKastler/Purity.lean b/Physicslib4/AQFT/HaagKastler/Purity.lean new file mode 100644 index 0000000..b9ed7cb --- /dev/null +++ b/Physicslib4/AQFT/HaagKastler/Purity.lean @@ -0,0 +1,66 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.AQFT.HaagKastler.Net +import Physicslib4.GNS.RadonNikodym +import Physicslib4.GNS.ExtremeState + +/-! +# Purity of states on the quasilocal algebra + +The canonical quasilocal algebra `𝔘` of a Minkowski Haag-Kastler net is a unital +C*-algebra, so the abstract characterizations of purity apply to it. This file +registers them for `𝔘`: + +* a state on `𝔘` is pure iff it is an extreme point of the state space; +* a state on `𝔘` is pure iff its GNS representation is irreducible. + +Unlike the curved setting, Minkowski spacetime has a single global quasilocal +algebra `𝔘`, so these are statements about its global state space - the natural +home for the vacuum and other distinguished states. + +## Main results + +* `Physicslib4.AQFT.HaagKastler.HaagKastlerNet.pure_iff_extreme` +* `Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_pure_iff_irreducible` +-/ + +namespace Physicslib4 +namespace AQFT +namespace HaagKastler +namespace HaagKastlerNet + +open Physicslib4.GNS +open scoped InnerProductSpace + +variable (N : HaagKastlerNet) + +/-- **Pure ⟺ extreme point for the quasilocal algebra.** A state `ω` on the +canonical quasilocal algebra `𝔘` of a Minkowski Haag-Kastler net is pure if and +only if it is an extreme point of the state space of `𝔘`. This is the abstract +equivalence `isPure_iff_isExtremePoint` applied to the C*-algebra `𝔘`. -/ +theorem pure_iff_extreme (ω : State N.quasilocal.carrier) : + IsPure ω ↔ ω.IsExtremePoint := + isPure_iff_isExtremePoint ω + +/-- **Pure ⟺ irreducible GNS representation for the quasilocal algebra.** For a +state `ω` on the quasilocal algebra `𝔘`, there is a GNS triple `(H, π, Ω)` +reproducing `ω` in which `ω` is pure if and only if the representation `π` is +irreducible (its commutant is trivial). This combines the GNS construction with +the abstract `isPure_iff_isIrreducible`. -/ +theorem exists_gns_pure_iff_irreducible (ω : State N.quasilocal.carrier) : + ∃ (H : Type) + (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H) + (π : N.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H), + IsCyclicVector π Ω ∧ + (∀ a : N.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (IsPure ω ↔ IsIrreducible π) := by + obtain ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, _⟩ := gns_construction ω + exact ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, isPure_iff_isIrreducible hcyc hrep⟩ + +end HaagKastlerNet +end HaagKastler +end AQFT +end Physicslib4 diff --git a/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean b/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean index 54954d8..484841b 100644 --- a/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean +++ b/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean @@ -9,6 +9,8 @@ import Physicslib4.Spacetime.MinkowskiDirected import Physicslib4.Spacetime.LorentzCausality import Physicslib4.Analysis.CStarDenseExtend import Physicslib4.GNS.UnitaryRepresentation +import Physicslib4.GNS.RadonNikodym +import Physicslib4.GNS.ExtremeState /-! # Towards the intertwiner on the generated subalgebra @@ -543,7 +545,8 @@ theorem IsInvariantState.exists_gns_unitary (C : CovariantQuasilocalAlgebra) (∀ L L' : InhomogeneousLorentzGroup, U (L' * L) = (U L).trans (U L')) ∧ U 1 = LinearIsometryEquiv.refl ℂ H ∧ (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H), - U L (π a ((U L).symm x)) = π (C.action L a) x) := + U L (π a ((U L).symm x)) = π (C.action L a) x) ∧ + Physicslib4.GNS.IsCyclicVector π Ω := -- This is the specialization of the algebra-agnostic -- `GNS.exists_gns_unitary_of_invariant` to the quasilocal algebra `𝔘` with the -- covariance action `β = C.action`: invariance is `hω`, multiplicativity is @@ -584,6 +587,49 @@ theorem IsInvariantState.exists_gns_unitary_strongContinuous Physicslib4.GNS.exists_gns_unitary_of_invariant_strongContinuous C.action ω hω C.action_mul_apply C.action_one_apply hwc +open scoped InnerProductSpace in +/-- **Irreducible covariant representation of a pure invariant state (Minkowski).** +A state `ω` on the quasilocal algebra that is both invariant under the covariance +action and pure yields a GNS representation that is simultaneously *covariant* - +implemented by a unitary representation `U` of the inhomogeneous Lorentz group +fixing the cyclic vector `Ω`, with the operator covariance +`U(L) π(a) U(L)⁻¹ = π(β_L a)` - and *irreducible*. It combines +`IsInvariantState.exists_gns_unitary` (a covariant GNS triple with invariant cyclic +`Ω`) with purity ⟹ irreducibility (`isPure_iff_isIrreducible`). + +This is a necessary precursor to, but not yet, a *vacuum* representation: a genuine +vacuum would additionally require the spectrum condition (positivity of the energy- +momentum spectrum), which is not available here. -/ +theorem IsInvariantState.exists_gns_irreducible_covariant (C : CovariantQuasilocalAlgebra) + {ω : Physicslib4.GNS.State C.quasilocal.carrier} (hω : C.IsInvariantState ω) + (hpure : Physicslib4.GNS.IsPure ω) : + ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : InhomogeneousLorentzGroup → (H ≃ₗᵢ[ℂ] H)), + Physicslib4.GNS.IsCyclicVector π Ω ∧ + (∀ a : C.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier), + U L (π a Ω) = π (C.action L a) Ω) ∧ + (∀ L : InhomogeneousLorentzGroup, U L Ω = Ω) ∧ + (∀ L L' : InhomogeneousLorentzGroup, U (L' * L) = (U L).trans (U L')) ∧ + U 1 = LinearIsometryEquiv.refl ℂ H ∧ + (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H), + U L (π a ((U L).symm x)) = π (C.action L a) x) ∧ + Physicslib4.GNS.IsIrreducible π := by + obtain ⟨H, i1, i2, i3, π, Ω, U, hrepro, himpl, hUΩ, hmul, hUone, hopcov, hcyc⟩ := + IsInvariantState.exists_gns_unitary C hω + exact ⟨H, i1, i2, i3, π, Ω, U, hcyc, hrepro, himpl, hUΩ, hmul, hUone, hopcov, + (Physicslib4.GNS.isPure_iff_isIrreducible hcyc hrepro).mp hpure⟩ + +/-- **Purity is covariance-invariant (Minkowski).** A state `ω` on the quasilocal +algebra is pure if and only if its pullback `ω ∘ β_L` along the covariance +automorphism is pure: purity is preserved by the `*`-automorphism `β_L = C.action L`. +Specialization of `isPure_precomp_iff`. -/ +theorem isPure_precomp_action_iff (C : CovariantQuasilocalAlgebra) + (ω : Physicslib4.GNS.State C.quasilocal.carrier) (L : InhomogeneousLorentzGroup) : + Physicslib4.GNS.IsPure (ω.precomp (C.action L)) ↔ Physicslib4.GNS.IsPure ω := + Physicslib4.GNS.isPure_precomp_iff ω (C.action L) + end CovariantQuasilocalAlgebra /-- The trivial net with its trivial quasilocal algebra is a covariant quasilocal diff --git a/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean b/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean index bc94b48..262df56 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Lean Community -/ import Physicslib4.AQFT.HaagKastlerCurved.EinsteinCausality +import Physicslib4.GNS.Irreducibility /-! # Local von Neumann algebras and spacelike commutation (curved spacetime) @@ -132,6 +133,60 @@ theorem localVonNeumann_separating (Set.subset_centralizer_centralizer hA) exact (Set.mem_centralizer_iff.mp hA') R hR +/-- The local observable operators `π(𝔘(B'))` form a self-adjoint set: `π` and the +isotony embedding `commIsotony` are `*`-homomorphisms. -/ +theorem localOperators_selfAdjoint {B : Set M.Carrier} + (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B' : Set M.Carrier⦄ (hB' : M.IsBasisSet B') (hB : M.IsBasisSet B) (h : B' ⊆ B) : + ∀ x ∈ N.localOperators π hB' hB h, star x ∈ N.localOperators π hB' hB h := by + rintro x ⟨a, rfl⟩ + exact ⟨star a, by simp only [map_star]⟩ + +/-- The **local von Neumann algebra** `R(B')` as a genuine `VonNeumannAlgebra`: the +bicommutant of the self-adjoint set of local observable operators inside `B(H)`. +Its underlying set is `localVonNeumann π hB' hB h`. -/ +noncomputable def localVonNeumannAlgebra {B : Set M.Carrier} + (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B' : Set M.Carrier⦄ (hB' : M.IsBasisSet B') (hB : M.IsBasisSet B) (h : B' ⊆ B) : + VonNeumannAlgebra H := + vonNeumannOfSelfAdjoint (N.localOperators π hB' hB h) + (N.localOperators_selfAdjoint π hB' hB h) + +@[simp] theorem coe_localVonNeumannAlgebra {B : Set M.Carrier} + (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B' : Set M.Carrier⦄ (hB' : M.IsBasisSet B') (hB : M.IsBasisSet B) (h : B' ⊆ B) : + (N.localVonNeumannAlgebra π hB' hB h : Set (H →L[ℂ] H)) + = N.localVonNeumann π hB' hB h := + coe_vonNeumannOfSelfAdjoint _ _ + +/-- **Microcausality, bundled (curved spacetime).** For completely spacelike-separated +subregions `B₁, B₂ ⊆ B`, the bundled local von Neumann algebras commute, +`R(B₁) ≤ R(B₂)'`. -/ +theorem localVonNeumannAlgebra_le_commutant {B : Set M.Carrier} + (hB : M.IsBasisSet B) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B₁ B₂ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) + (hs : M.IsCompletelySpacelike B₁ B₂) (h₁ : B₁ ⊆ B) (h₂ : B₂ ⊆ B) : + N.localVonNeumannAlgebra π hB₁ hB h₁ + ≤ (N.localVonNeumannAlgebra π hB₂ hB h₂).commutant := by + rw [← SetLike.coe_subset_coe] + simp only [coe_localVonNeumannAlgebra, VonNeumannAlgebra.coe_commutant] + exact N.localVonNeumann_subset_centralizer hB π hB₁ hB₂ hs h₁ h₂ + +/-- **Isotony, bundled (curved spacetime).** `B₁ ⊆ B₂ ⊆ B` (with the isotony +coherence) gives `R(B₁) ≤ R(B₂)`. -/ +theorem localVonNeumannAlgebra_mono {B : Set M.Carrier} + (hB : M.IsBasisSet B) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) + ⦃B₁ B₂ : Set M.Carrier⦄ (hB₁ : M.IsBasisSet B₁) (hB₂ : M.IsBasisSet B₂) + (h₁₂ : B₁ ⊆ B₂) (h₂ : B₂ ⊆ B) + (hcoh : ∀ a : N.algebra B₁, + N.commIsotony hB₁ hB (h₁₂.trans h₂) a + = N.commIsotony hB₂ hB h₂ (N.commIsotony hB₁ hB₂ h₁₂ a)) : + N.localVonNeumannAlgebra π hB₁ hB (h₁₂.trans h₂) + ≤ N.localVonNeumannAlgebra π hB₂ hB h₂ := by + rw [← SetLike.coe_subset_coe] + simp only [coe_localVonNeumannAlgebra] + exact N.localVonNeumann_mono hB π hB₁ hB₂ h₁₂ h₂ hcoh + end HaagKastlerNet end HaagKastlerCurved end AQFT diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean b/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean new file mode 100644 index 0000000..3c00d5b --- /dev/null +++ b/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean @@ -0,0 +1,67 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.AQFT.HaagKastlerCurved.Net +import Physicslib4.GNS.RadonNikodym +import Physicslib4.GNS.ExtremeState + +/-! +# Purity of states on curved local algebras + +The local algebra `𝔘(B)` of a Haag-Kastler net in curved spacetime is a unital +C*-algebra, so the abstract characterizations of purity of a state apply to it +verbatim. This file registers them for `𝔘(B)`: + +* a state on `𝔘(B)` is pure iff it is an extreme point of the state space; +* a state on `𝔘(B)` is pure iff its GNS representation is irreducible. + +There is no quasilocal algebra in curved spacetime, so these statements are +phrased per region, on each local algebra `𝔘(B)` separately - which is exactly +the right generality, since each `𝔘(B)` is itself a C*-algebra with its own state +space and GNS representations. + +## Main results + +* `Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.pure_iff_extreme` +* `Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_pure_iff_irreducible` +-/ + +namespace Physicslib4 +namespace AQFT +namespace HaagKastlerCurved +namespace HaagKastlerNet + +open Physicslib4.GNS +open scoped InnerProductSpace + +variable {M : LorentzianSpacetime} (N : HaagKastlerNet M) + +/-- **Pure ⟺ extreme point for a curved local algebra.** A state `ω` on the local +algebra `𝔘(B)` of a curved Haag-Kastler net is pure if and only if it is an +extreme point of the state space of `𝔘(B)`. This is the abstract equivalence +`isPure_iff_isExtremePoint` applied to the C*-algebra `𝔘(B)`. -/ +theorem pure_iff_extreme {B : Set M.Carrier} (ω : State (N.algebra B)) : + IsPure ω ↔ ω.IsExtremePoint := + isPure_iff_isExtremePoint ω + +/-- **Pure ⟺ irreducible GNS representation for a curved local algebra.** For a +state `ω` on the local algebra `𝔘(B)`, there is a GNS triple `(H, π, Ω)` +reproducing `ω` in which `ω` is pure if and only if the representation `π` is +irreducible (its commutant is trivial). This combines the GNS construction with +the abstract `isPure_iff_isIrreducible`. -/ +theorem exists_gns_pure_iff_irreducible {B : Set M.Carrier} (ω : State (N.algebra B)) : + ∃ (H : Type) + (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H) + (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H), + IsCyclicVector π Ω ∧ + (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (IsPure ω ↔ IsIrreducible π) := by + obtain ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, _⟩ := gns_construction ω + exact ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, isPure_iff_isIrreducible hcyc hrep⟩ + +end HaagKastlerNet +end HaagKastlerCurved +end AQFT +end Physicslib4 diff --git a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean index 116ff19..3d0f311 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean @@ -5,6 +5,8 @@ Authors: Lean Community -/ import Physicslib4.AQFT.HaagKastlerCurved.Net import Physicslib4.GNS.UnitaryRepresentation +import Physicslib4.GNS.RadonNikodym +import Physicslib4.GNS.ExtremeState /-! # Stabilizer action on a curved local algebra and its GNS unitary @@ -139,7 +141,8 @@ theorem exists_gns_unitary_stabilizer (B : Set M.Carrier) U (g' * g) = (U g).trans (U g')) ∧ U 1 = LinearIsometryEquiv.refl ℂ H ∧ (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B) (x : H), - U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) := + U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) ∧ + IsCyclicVector π Ω := Physicslib4.GNS.exists_gns_unitary_of_invariant (N.stabAutHom B) ω hinv (fun g g' a => N.stabAutHom_mul B g g' a) (fun a => N.stabAutHom_one B a) @@ -180,6 +183,51 @@ theorem exists_gns_unitary_stabilizer_strongContinuous [TopologicalSpace M.Isom] ω hinv (fun g g' a => N.stabAutHom_mul B g g' a) (fun a => N.stabAutHom_one B a) hwc +/-- **Irreducible covariant representation of a pure invariant state (curved +spacetime).** A state `ω` on a local algebra `𝔘(B)` that is invariant under the +stabilizer action and pure yields a GNS representation that is simultaneously +*covariant* - implemented by a unitary representation `U` of the stabilizer +`Stab(B)` fixing the cyclic vector `Ω`, with the operator covariance +`U(g) π(a) U(g)⁻¹ = π(g · a)` - and *irreducible*. It is the curved, per-region +analogue (there is no quasilocal algebra), combining `exists_gns_unitary_stabilizer` +with purity ⟹ irreducibility (`isPure_iff_isIrreducible`). + +As in the Minkowski case this is a precursor to, not, a *vacuum*: curved spacetime +has no global vacuum, and the analogue of the spectrum condition (the Hadamard / +microlocal spectrum condition) is a separate requirement not imposed here. -/ +theorem exists_gns_irreducible_covariant_stabilizer (B : Set M.Carrier) + (ω : State (N.algebra B)) + (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B), + ω (N.stabAutHom B g a) = ω a) + (hpure : IsPure ω) : + ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : ↥(MulAction.stabilizer M.Isom B) → (H ≃ₗᵢ[ℂ] H)), + IsCyclicVector π Ω ∧ + (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B), + U g (π a Ω) = π (N.stabAutHom B g a) Ω) ∧ + (∀ g : ↥(MulAction.stabilizer M.Isom B), U g Ω = Ω) ∧ + (∀ g g' : ↥(MulAction.stabilizer M.Isom B), + U (g' * g) = (U g).trans (U g')) ∧ + U 1 = LinearIsometryEquiv.refl ℂ H ∧ + (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B) (x : H), + U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) ∧ + IsIrreducible π := by + obtain ⟨H, i1, i2, i3, π, Ω, U, hrepro, himpl, hUΩ, hmul, hUone, hopcov, hcyc⟩ := + N.exists_gns_unitary_stabilizer B ω hinv + exact ⟨H, i1, i2, i3, π, Ω, U, hcyc, hrepro, himpl, hUΩ, hmul, hUone, hopcov, + (isPure_iff_isIrreducible hcyc hrepro).mp hpure⟩ + +/-- **Purity is invariant under the stabilizer action (curved spacetime).** A state +`ω` on a local algebra `𝔘(B)` is pure if and only if its pullback `ω ∘ \hatα_g` +along the stabilizer automorphism is pure, for any `g ∈ Stab(B)`. Specialization of +`isPure_precomp_iff`. -/ +theorem isPure_precomp_stabAut_iff (B : Set M.Carrier) + (ω : State (N.algebra B)) (g : ↥(MulAction.stabilizer M.Isom B)) : + IsPure (ω.precomp (N.stabAutHom B g)) ↔ IsPure ω := + isPure_precomp_iff ω (N.stabAutHom B g) + end HaagKastlerNet end HaagKastlerCurved diff --git a/Physicslib4/GNS/ExtremeState.lean b/Physicslib4/GNS/ExtremeState.lean new file mode 100644 index 0000000..09d6937 --- /dev/null +++ b/Physicslib4/GNS/ExtremeState.lean @@ -0,0 +1,380 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.GNS.Irreducibility +import Physicslib4.GNS.CauchySchwarz +import Mathlib.Analysis.CStarAlgebra.Basic +import Mathlib.Analysis.CStarAlgebra.Spectrum + +/-! +# Pure states and extreme points of the state space + +A state `ω` on a unital C*-algebra `A` is **pure** (`Physicslib4.GNS.IsPure`) when +every positive functional `ψ` dominated by `ω` is a scalar multiple of `ω`. The +convex-geometric counterpart is that `ω` is an **extreme point** of the (convex) +state space: it is not a nontrivial convex combination of two distinct states. + +This file proves the equivalence + +`IsPure ω ↔ ω.IsExtremePoint`, + +a classical characterization of purity. The analytic crux is the identity + +`‖φ‖ = (φ 1).re` + +for a positive linear functional `φ` on a unital C*-algebra +(`norm_eq_re_apply_one_of_positive`), obtained from the Cauchy-Schwarz inequality +for positive functionals together with the C*-norm identity `‖star b * b‖ = ‖b‖²`. +It is the bridge that lets us normalize positive functionals into states and back. + +* `‖ψ‖ = (ψ 1).re` recovers the normalization `ω 1 = 1` for states + (`State.apply_one`), pins the convex coefficients in the forward direction, and + rescales the two pieces `ψ` and `ω - ψ` into states in the backward direction. +-/ + +namespace Physicslib4 +namespace GNS + +open scoped ComplexOrder + +variable {A : Type*} [CStarAlgebra A] + +private lemma complex_ofReal_nonneg {r : ℝ} (hr : 0 ≤ r) : (0 : ℂ) ≤ (r : ℂ) := + Complex.nonneg_iff.mpr ⟨by simpa using hr, by simp⟩ + +private lemma complex_inv_ofReal_nonneg {r : ℝ} (hr : 0 ≤ r) : (0 : ℂ) ≤ ((r : ℂ))⁻¹ := by + rw [← Complex.ofReal_inv]; exact complex_ofReal_nonneg (inv_nonneg.mpr hr) + +private lemma norm_inv_ofReal_pos {r : ℝ} (hr : 0 < r) : ‖((r : ℂ))⁻¹‖ = r⁻¹ := by + rw [norm_inv, Complex.norm_real, Real.norm_of_nonneg hr.le] + +/-- A C*-algebra carrying a state is nontrivial (a state has operator norm `1`, +so the algebra cannot be the zero ring). -/ +private lemma nontrivial_of_state (ω : State A) : Nontrivial A := by + rcases subsingleton_or_nontrivial A with hs | hn + · exfalso + have h0 : ω.toContinuousLinearMap = 0 := by + ext a + rw [Subsingleton.elim a 0, map_zero, ContinuousLinearMap.zero_apply] + have hnorm := ω.isNormalized + rw [h0, norm_zero] at hnorm + exact one_ne_zero hnorm.symm + · exact hn + +/-- **Norm of a positive functional.** For a positive linear functional `φ` on a +unital C*-algebra, `‖φ‖ = (φ 1).re`. The reverse bound `(φ 1).re ≤ ‖φ‖` is +immediate from `‖1‖ = 1`; the forward bound uses Cauchy-Schwarz with the first +slot equal to `1`, namely `‖φ b‖² ≤ (φ 1).re · (φ (b* b)).re ≤ (φ 1).re · ‖φ‖ · ‖b‖²`, +which gives `‖φ‖² ≤ (φ 1).re · ‖φ‖`. -/ +theorem norm_eq_re_apply_one_of_positive [Nontrivial A] {φ : A →L[ℂ] ℂ} + (hpos : ∀ a : A, 0 ≤ φ (star a * a)) : ‖φ‖ = (φ 1).re := by + have hNnn : (0 : ℝ) ≤ ‖φ‖ := norm_nonneg _ + have hφ1 : (0 : ℂ) ≤ φ 1 := by have := hpos 1; rwa [star_one, one_mul] at this + have hμnn : 0 ≤ (φ 1).re := (Complex.nonneg_iff.mp hφ1).1 + -- reverse bound: `(φ 1).re ≤ ‖φ‖` + have hrev : (φ 1).re ≤ ‖φ‖ := by + have h1 : (φ 1).re ≤ ‖φ 1‖ := (le_abs_self _).trans (Complex.abs_re_le_norm _) + have h2 : ‖φ 1‖ ≤ ‖φ‖ * ‖(1 : A)‖ := φ.le_opNorm 1 + rw [CStarRing.norm_one, mul_one] at h2 + exact h1.trans h2 + -- key bound from Cauchy-Schwarz + have hbound : ∀ b : A, ‖φ b‖ ^ 2 ≤ (φ 1).re * ‖φ‖ * ‖b‖ ^ 2 := by + intro b + have hcs := cauchy_schwarz_inequality (φ : A →ₗ[ℂ] ℂ) + (by intro c; simpa using hpos c) 1 b + simp only [ContinuousLinearMap.coe_coe, star_one, one_mul] at hcs + rw [Complex.normSq_eq_norm_sq] at hcs + have hb1 : (φ (star b * b)).re ≤ ‖φ (star b * b)‖ := + (le_abs_self _).trans (Complex.abs_re_le_norm _) + have hb2 : ‖φ (star b * b)‖ ≤ ‖φ‖ * ‖star b * b‖ := φ.le_opNorm _ + rw [CStarRing.norm_star_mul_self] at hb2 + have hbb : (φ (star b * b)).re ≤ ‖φ‖ * (‖b‖ * ‖b‖) := hb1.trans hb2 + calc ‖φ b‖ ^ 2 ≤ (φ 1).re * (φ (star b * b)).re := hcs + _ ≤ (φ 1).re * (‖φ‖ * (‖b‖ * ‖b‖)) := mul_le_mul_of_nonneg_left hbb hμnn + _ = (φ 1).re * ‖φ‖ * ‖b‖ ^ 2 := by ring + -- forward bound: `‖φ‖ ≤ (φ 1).re` + have hfwd : ‖φ‖ ≤ (φ 1).re := by + by_cases hN0 : ‖φ‖ = 0 + · rw [hN0]; exact hμnn + · have hNpos : 0 < ‖φ‖ := lt_of_le_of_ne hNnn (Ne.symm hN0) + have hμN : 0 ≤ (φ 1).re * ‖φ‖ := mul_nonneg hμnn hNnn + set C : ℝ := Real.sqrt ((φ 1).re * ‖φ‖) with hC_def + have hCnn : 0 ≤ C := Real.sqrt_nonneg _ + have hCsq : C ^ 2 = (φ 1).re * ‖φ‖ := Real.sq_sqrt hμN + have hble : ∀ b : A, ‖φ b‖ ≤ C * ‖b‖ := by + intro b + have hsq : ‖φ b‖ ^ 2 ≤ (C * ‖b‖) ^ 2 := by rw [mul_pow, hCsq]; exact hbound b + have h0 : 0 ≤ C * ‖b‖ := mul_nonneg hCnn (norm_nonneg _) + have hle := Real.sqrt_le_sqrt hsq + rwa [Real.sqrt_sq (norm_nonneg _), Real.sqrt_sq h0] at hle + have hNC : ‖φ‖ ≤ C := φ.opNorm_le_bound hCnn hble + have hN2 : ‖φ‖ ^ 2 ≤ (φ 1).re * ‖φ‖ := by + nlinarith [mul_nonneg (sub_nonneg.mpr hNC) (add_nonneg hCnn hNnn), hCsq] + nlinarith [hN2, hNpos] + exact le_antisymm hfwd hrev + +/-- A state evaluates to `1` on the unit: `ω 1 = 1`. The real part is `‖ω‖ = 1` +(via `norm_eq_re_apply_one_of_positive` and normalization), and the imaginary part +vanishes by positivity at `1`. -/ +theorem State.apply_one (ω : State A) : (ω 1 : ℂ) = 1 := by + haveI := nontrivial_of_state ω + have hpos : ∀ a, 0 ≤ ω.toContinuousLinearMap (star a * a) := ω.isPositive + have hn := norm_eq_re_apply_one_of_positive hpos + rw [ω.isNormalized] at hn + have him : (ω.toContinuousLinearMap 1).im = 0 := by + have h0 : (0 : ℂ) ≤ ω.toContinuousLinearMap 1 := by + have := ω.isPositive 1; rwa [star_one, one_mul] at this + exact (Complex.nonneg_iff.mp h0).2.symm + apply Complex.ext + · change (ω.toContinuousLinearMap 1).re = (1 : ℂ).re + rw [Complex.one_re]; exact hn.symm + · change (ω.toContinuousLinearMap 1).im = (1 : ℂ).im + rw [Complex.one_im]; exact him + +/-- A state `ω` is an **extreme point** of the state space if it is not a +nontrivial convex combination of two distinct states: whenever +`ω = t·ω₁ + (1-t)·ω₂` with `0 < t < 1` and `ω₁, ω₂` states, then `ω₁ = ω₂` +(and hence both equal `ω`). -/ +def State.IsExtremePoint (ω : State A) : Prop := + ∀ (ω₁ ω₂ : State A) (t : ℝ), 0 < t → t < 1 → + (∀ a, (ω a : ℂ) = (t : ℂ) * ω₁ a + (1 - t : ℂ) * ω₂ a) → ω₁ = ω₂ + +/-- **Pure ⟹ extreme point.** If `ω` is pure and decomposes as a convex +combination `ω = t·ω₁ + (1-t)·ω₂` of states with `0 < t < 1`, then `t·ω₁` is a +positive functional dominated by `ω`, hence (by purity) a scalar multiple of `ω`; +evaluating at `1` (where all states give `1`) pins the scalar to `t`, forcing +`ω₁ = ω`, and symmetrically `ω₂ = ω`. -/ +theorem isExtremePoint_of_isPure (ω : State A) (hpure : IsPure ω) : + ω.IsExtremePoint := by + haveI := nontrivial_of_state ω + intro ω₁ ω₂ t ht0 ht1 hcomb + set ψ : A →L[ℂ] ℂ := (t : ℂ) • ω₁.toContinuousLinearMap with hψ_def + have hψapp : ∀ a, ψ a = (t : ℂ) * ω₁ a := by + intro a; rw [hψ_def] + show ((t : ℂ) • ω₁.toContinuousLinearMap) a = (t : ℂ) * ω₁ a + rw [ContinuousLinearMap.smul_apply]; rfl + have htne : (t : ℂ) ≠ 0 := by rw [Ne, Complex.ofReal_eq_zero]; exact ht0.ne' + have h1tne : (1 - (t : ℂ)) ≠ 0 := by + have he : (1 - (t : ℂ)) = ((1 - t : ℝ) : ℂ) := by push_cast; ring + rw [he, Ne, Complex.ofReal_eq_zero]; exact (by linarith : (0 : ℝ) < 1 - t).ne' + -- `ψ` is positive and dominated by `ω` + have hψpos : ∀ a, 0 ≤ ψ (star a * a) := by + intro a; rw [hψapp] + exact mul_nonneg (complex_ofReal_nonneg ht0.le) (ω₁.isPositive a) + have hψdom : ∀ a, ψ (star a * a) ≤ ω (star a * a) := by + intro a + have hc := hcomb (star a * a) + have hnn : (0 : ℂ) ≤ (1 - (t : ℂ)) * ω₂ (star a * a) := by + refine mul_nonneg ?_ (ω₂.isPositive a) + have he : (1 - (t : ℂ)) = ((1 - t : ℝ) : ℂ) := by push_cast; ring + rw [he]; exact complex_ofReal_nonneg (by linarith) + rw [hψapp] + have hsub : ω (star a * a) - (t : ℂ) * ω₁ (star a * a) + = (1 - (t : ℂ)) * ω₂ (star a * a) := by rw [hc]; ring + exact sub_nonneg.mp (hsub ▸ hnn) + -- purity gives the scalar + obtain ⟨s, hs⟩ := hpure ψ hψpos hψdom + have e1 := hs 1 + rw [hψapp, ω₁.apply_one, ω.apply_one, mul_one, mul_one] at e1 + -- `e1 : (t : ℂ) = s` + have hst : s = (t : ℂ) := e1.symm + have hω1eq : ∀ a, ω₁ a = ω a := by + intro a + have ea := hs a + rw [hψapp, hst] at ea + exact mul_left_cancel₀ htne ea + have hω1 : ω₁ = ω := DFunLike.ext _ _ hω1eq + have hω2eq : ∀ a, ω₂ a = ω a := by + intro a + have hc := hcomb a + rw [hω1eq a] at hc + have hh : (1 - (t : ℂ)) * ω₂ a = (1 - (t : ℂ)) * ω a := by linear_combination -hc + exact mul_left_cancel₀ h1tne hh + have hω2 : ω₂ = ω := DFunLike.ext _ _ hω2eq + exact hω1.trans hω2.symm + +/-- **Extreme point ⟹ pure.** If `ω` is an extreme point and `ψ` is a positive +functional dominated by `ω`, set `λ = (ψ 1).re ∈ [0,1]`. For `λ ∈ (0,1)` the +rescaled functionals `λ⁻¹·ψ` and `(1-λ)⁻¹·(ω-ψ)` are states (normalized via +`norm_eq_re_apply_one_of_positive`) with `ω = λ·(λ⁻¹ψ) + (1-λ)·((1-λ)⁻¹(ω-ψ))`, so +extremality identifies them and forces `ψ = λ·ω`. The boundary cases `λ = 0` +(`ψ = 0`) and `λ = 1` (`ψ = ω`) are handled separately. -/ +theorem isPure_of_isExtremePoint (ω : State A) (hext : ω.IsExtremePoint) : + IsPure ω := by + haveI := nontrivial_of_state ω + intro ψ hψpos hψdom + have hω1 : (ω 1 : ℂ) = 1 := ω.apply_one + have hψ1 : (0 : ℂ) ≤ ψ 1 := by have := hψpos 1; rwa [star_one, one_mul] at this + set lam : ℝ := (ψ 1).re with hlam_def + have hlam_nn : 0 ≤ lam := (Complex.nonneg_iff.mp hψ1).1 + have hψnorm : ‖ψ‖ = lam := norm_eq_re_apply_one_of_positive hψpos + -- `λ ≤ 1` + have hlam_le1 : lam ≤ 1 := by + have hd := hψdom 1 + rw [star_one, one_mul] at hd + have hre := (Complex.le_def.mp hd).1 + rw [hlam_def] + calc (ψ 1).re ≤ (ω 1).re := hre + _ = 1 := by rw [hω1, Complex.one_re] + rcases eq_or_lt_of_le hlam_nn with hlam0 | hlampos + · -- `λ = 0` : `ψ = 0` + refine ⟨0, fun a => ?_⟩ + have hψ0 : ψ = 0 := by + rw [← norm_eq_zero]; rw [hψnorm, ← hlam0] + rw [hψ0]; simp + · rcases eq_or_lt_of_le hlam_le1 with hlam1 | hlamlt1 + · -- `λ = 1` : `ψ = ω` + refine ⟨1, fun a => ?_⟩ + have hpossub : ∀ c, 0 ≤ (ω.toContinuousLinearMap - ψ) (star c * c) := by + intro c; rw [ContinuousLinearMap.sub_apply]; exact sub_nonneg.mpr (hψdom c) + have hval : ((ω.toContinuousLinearMap - ψ) 1).re = 0 := by + rw [ContinuousLinearMap.sub_apply, Complex.sub_re] + change (ω 1).re - (ψ 1).re = 0 + rw [hω1, Complex.one_re, ← hlam_def, hlam1]; ring + have hnormsub := norm_eq_re_apply_one_of_positive hpossub + rw [hval] at hnormsub + have hzero : ω.toContinuousLinearMap - ψ = 0 := norm_eq_zero.mp hnormsub + have heq : ω.toContinuousLinearMap = ψ := sub_eq_zero.mp hzero + rw [one_mul] + change ψ a = ω.toContinuousLinearMap a + rw [heq] + · -- `0 < λ < 1` : genuine convex decomposition + have hlamne : (lam : ℂ) ≠ 0 := by + rw [Ne, Complex.ofReal_eq_zero]; exact hlampos.ne' + have h1lampos : 0 < 1 - lam := by linarith + have h1lam_ofReal_ne : (((1 - lam : ℝ) : ℂ)) ≠ 0 := by + rw [Ne, Complex.ofReal_eq_zero]; exact h1lampos.ne' + -- the two rescaled states + have hpos1 : ∀ a, 0 ≤ (((lam : ℂ))⁻¹ • ψ) (star a * a) := by + intro a; rw [ContinuousLinearMap.smul_apply] + exact mul_nonneg (complex_inv_ofReal_nonneg hlampos.le) (hψpos a) + have hnorm1 : ‖((lam : ℂ))⁻¹ • ψ‖ = 1 := by + rw [norm_smul, norm_inv_ofReal_pos hlampos, hψnorm, inv_mul_cancel₀ hlampos.ne'] + have hpossub : ∀ c, 0 ≤ (ω.toContinuousLinearMap - ψ) (star c * c) := by + intro c; rw [ContinuousLinearMap.sub_apply]; exact sub_nonneg.mpr (hψdom c) + have hnormsub : ‖ω.toContinuousLinearMap - ψ‖ = 1 - lam := by + rw [norm_eq_re_apply_one_of_positive hpossub, ContinuousLinearMap.sub_apply, + Complex.sub_re] + change (ω 1).re - (ψ 1).re = 1 - lam + rw [hω1, Complex.one_re, ← hlam_def] + have hpos2 : ∀ a, 0 ≤ ((((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ)) + (star a * a) := by + intro a; rw [ContinuousLinearMap.smul_apply] + exact mul_nonneg (complex_inv_ofReal_nonneg h1lampos.le) (hpossub a) + have hnorm2 : ‖(((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ)‖ = 1 := by + rw [norm_smul, norm_inv_ofReal_pos h1lampos, hnormsub, inv_mul_cancel₀ h1lampos.ne'] + -- bundle as states + set s1 : State A := ⟨((lam : ℂ))⁻¹ • ψ, hpos1, hnorm1⟩ with hs1 + set s2 : State A := + ⟨(((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ), hpos2, hnorm2⟩ with hs2 + have hs1a : ∀ a, s1 a = ((lam : ℂ))⁻¹ * ψ a := by + intro a; rw [hs1] + change (((lam : ℂ))⁻¹ • ψ) a = ((lam : ℂ))⁻¹ * ψ a + rw [ContinuousLinearMap.smul_apply]; rfl + have hs2a : ∀ a, s2 a = (((1 - lam : ℝ) : ℂ))⁻¹ * (ω a - ψ a) := by + intro a; rw [hs2] + change ((((1 - lam : ℝ) : ℂ))⁻¹ • (ω.toContinuousLinearMap - ψ)) a + = (((1 - lam : ℝ) : ℂ))⁻¹ * (ω a - ψ a) + rw [ContinuousLinearMap.smul_apply, ContinuousLinearMap.sub_apply]; rfl + have hcancel : (lam : ℂ) * ((lam : ℂ))⁻¹ = 1 := mul_inv_cancel₀ hlamne + have hcancel2 : (1 - (lam : ℂ)) * (((1 - lam : ℝ) : ℂ))⁻¹ = 1 := by + rw [show (1 - (lam : ℂ)) = (((1 - lam : ℝ) : ℂ)) from by push_cast; ring] + exact mul_inv_cancel₀ h1lam_ofReal_ne + have hdecomp : ∀ a, ω a = (lam : ℂ) * s1 a + (1 - lam : ℂ) * s2 a := by + intro a + rw [hs1a, hs2a, ← mul_assoc, ← mul_assoc, hcancel, hcancel2, one_mul, one_mul] + ring + have key : s1 = s2 := hext s1 s2 lam hlampos hlamlt1 hdecomp + refine ⟨(lam : ℂ), fun a => ?_⟩ + have h := hdecomp a + rw [key] at h + have he : (lam : ℂ) * s2 a + (1 - lam : ℂ) * s2 a = s2 a := by ring + rw [he] at h + rw [← key, hs1a a] at h + -- `h : ω a = (lam⁻¹ : ℂ) * ψ a` + rw [h, ← mul_assoc, hcancel, one_mul] + +/-- **Purity ⟺ extreme point of the state space.** -/ +theorem isPure_iff_isExtremePoint (ω : State A) : IsPure ω ↔ ω.IsExtremePoint := + ⟨isExtremePoint_of_isPure ω, isPure_of_isExtremePoint ω⟩ + +/-- A `*`-automorphism of a C*-algebra as a continuous `ℂ`-linear map; it is +isometric (`StarAlgEquiv.isometry`), hence bounded with norm `≤ 1`. -/ +noncomputable def starAlgEquivCLM (Φ : A ≃⋆ₐ[ℂ] A) : A →L[ℂ] A := + Φ.toAlgEquiv.toLinearMap.mkContinuous 1 fun a => by + rw [one_mul] + have hni : ‖Φ a‖ = ‖a‖ := by + have h := (StarAlgEquiv.isometry Φ).dist_eq a 0 + simpa [dist_eq_norm, map_zero] using h + exact le_of_eq hni + +@[simp] theorem starAlgEquivCLM_apply (Φ : A ≃⋆ₐ[ℂ] A) (a : A) : + starAlgEquivCLM Φ a = Φ a := rfl + +/-- The **pullback of a state along a `*`-automorphism** `Φ`: `a ↦ ω (Φ a)`. It is +again a state - positivity is the `Φ`-equivariance of `star a * a`, and the +normalization `‖ω ∘ Φ‖ = 1` follows since `Φ` is unital (`(ω∘Φ)(1) = ω(1) = 1`) +and positive functionals have norm equal to their value at `1`. -/ +noncomputable def State.precomp (ω : State A) (Φ : A ≃⋆ₐ[ℂ] A) : State A where + toContinuousLinearMap := ω.toContinuousLinearMap.comp (starAlgEquivCLM Φ) + isPositive := fun a => by + rw [ContinuousLinearMap.comp_apply, starAlgEquivCLM_apply, map_mul, map_star] + exact ω.isPositive (Φ a) + isNormalized := by + haveI := nontrivial_of_state ω + have hpos : ∀ a, 0 ≤ (ω.toContinuousLinearMap.comp (starAlgEquivCLM Φ)) (star a * a) := by + intro a + rw [ContinuousLinearMap.comp_apply, starAlgEquivCLM_apply, map_mul, map_star] + exact ω.isPositive (Φ a) + rw [norm_eq_re_apply_one_of_positive hpos, ContinuousLinearMap.comp_apply, + starAlgEquivCLM_apply, map_one] + rw [show ω.toContinuousLinearMap 1 = ω 1 from rfl, ω.apply_one, Complex.one_re] + +@[simp] theorem State.precomp_apply (ω : State A) (Φ : A ≃⋆ₐ[ℂ] A) (a : A) : + (ω.precomp Φ) a = ω (Φ a) := rfl + +/-- Pulling back by `Φ` and then `Φ⁻¹` recovers the original state. -/ +theorem State.precomp_precomp_symm (ω : State A) (Φ : A ≃⋆ₐ[ℂ] A) : + (ω.precomp Φ).precomp Φ.symm = ω := by + apply DFunLike.ext + intro a + simp only [State.precomp_apply, StarAlgEquiv.apply_symm_apply] + +/-- **Purity is preserved by pullback along a `*`-automorphism** (one direction). +If `ω` is pure, so is `ω ∘ Φ`. A dominated positive functional `ψ ≤ ω ∘ Φ` becomes +`ψ ∘ Φ⁻¹ ≤ ω` after transport, which purity sends to a scalar multiple of `ω`; +transporting back gives `ψ` proportional to `ω ∘ Φ`. -/ +theorem isPure_precomp_of_isPure {ω : State A} (Φ : A ≃⋆ₐ[ℂ] A) (hpure : IsPure ω) : + IsPure (ω.precomp Φ) := by + intro ψ hψpos hψdom + set ψ' : A →L[ℂ] ℂ := ψ.comp (starAlgEquivCLM Φ.symm) with hψ'_def + have hψ'app : ∀ a, ψ' a = ψ (Φ.symm a) := fun a => by + rw [hψ'_def, ContinuousLinearMap.comp_apply, starAlgEquivCLM_apply] + have hψ'pos : ∀ a, 0 ≤ ψ' (star a * a) := by + intro a; rw [hψ'app, map_mul, map_star]; exact hψpos (Φ.symm a) + have hψ'dom : ∀ a, ψ' (star a * a) ≤ ω (star a * a) := by + intro a + rw [hψ'app, map_mul, map_star] + have hrhs : (ω.precomp Φ) (star (Φ.symm a) * Φ.symm a) = ω (star a * a) := by + rw [State.precomp_apply, map_mul, map_star, StarAlgEquiv.apply_symm_apply] + exact (hψdom (Φ.symm a)).trans (le_of_eq hrhs) + obtain ⟨t, ht⟩ := hpure ψ' hψ'pos hψ'dom + refine ⟨t, fun b => ?_⟩ + have hb := ht (Φ b) + rw [hψ'app, StarAlgEquiv.symm_apply_apply] at hb + rw [State.precomp_apply] + exact hb + +/-- **Purity is invariant under a `*`-automorphism**: `ω ∘ Φ` is pure iff `ω` is. +On a Haag-Kastler net with `Φ = β_L` the covariance automorphism, this says purity +of a state is a covariance-invariant property. -/ +theorem isPure_precomp_iff (ω : State A) (Φ : A ≃⋆ₐ[ℂ] A) : + IsPure (ω.precomp Φ) ↔ IsPure ω := by + refine ⟨fun h => ?_, isPure_precomp_of_isPure Φ⟩ + have h2 := isPure_precomp_of_isPure Φ.symm h + rwa [State.precomp_precomp_symm] at h2 + +end GNS +end Physicslib4 diff --git a/Physicslib4/GNS/Irreducibility.lean b/Physicslib4/GNS/Irreducibility.lean index d85b03b..a48721c 100644 --- a/Physicslib4/GNS/Irreducibility.lean +++ b/Physicslib4/GNS/Irreducibility.lean @@ -7,6 +7,7 @@ import Physicslib4.GNS.Construction import Mathlib.Analysis.InnerProductSpace.Adjoint import Mathlib.Analysis.InnerProductSpace.Positive import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap +import Mathlib.Analysis.VonNeumannAlgebra.Basic /-! # Irreducibility of representations and Schur's lemma @@ -349,5 +350,95 @@ theorem isIrreducible_of_isPure _ = (2⁻¹ : ℂ) • ((p + Complex.I * q) • (1 : H →L[ℂ] H)) := by rw [hval] _ = (2⁻¹ * (p + Complex.I * q)) • 1 := by rw [smul_smul] +/-- The **von Neumann algebra generated by a representation** `π`: the bicommutant +(double `Set.centralizer`) of the image `π(A)`, i.e. `π(A)''`. -/ +def gnsVonNeumann (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) : Set (H →L[ℂ] H) := + Set.centralizer (Set.centralizer (Set.range π)) + +omit [CStarAlgebra A] in +/-- The commutant (`Set.centralizer`) of a self-adjoint set of operators is +itself self-adjoint. -/ +theorem star_mem_setCentralizer {S : Set (H →L[ℂ] H)} (hS : ∀ x ∈ S, star x ∈ S) + {a : H →L[ℂ] H} (ha : a ∈ Set.centralizer S) : star a ∈ Set.centralizer S := by + simp only [Set.mem_centralizer_iff] at ha ⊢ + intro m hm + have h2 := congrArg star (ha (star m) (hS m hm)) + simp only [star_mul, star_star] at h2 + exact h2.symm + +omit [CStarAlgebra A] in +/-- The commutant of a self-adjoint set of operators is `*`-closed (subalgebra +form, used to build the `StarSubalgebra`). -/ +theorem star_mem_subalgebraCentralizer {T : Set (H →L[ℂ] H)} + (hT : ∀ x ∈ T, star x ∈ T) {a : H →L[ℂ] H} + (ha : a ∈ Subalgebra.centralizer ℂ T) : + star a ∈ Subalgebra.centralizer ℂ T := by + simp only [Subalgebra.mem_centralizer_iff] at ha ⊢ + intro m hm + have h2 := congrArg star (ha (star m) (hT m hm)) + simp only [star_mul, star_star] at h2 + exact h2.symm + +/-- The commutant of a self-adjoint set of operators, packaged as a +`StarSubalgebra` (it is a subalgebra, and `*`-closed by the previous lemma). -/ +noncomputable def starSubalgebraCentralizer (T : Set (H →L[ℂ] H)) + (hT : ∀ x ∈ T, star x ∈ T) : StarSubalgebra ℂ (H →L[ℂ] H) where + toSubalgebra := Subalgebra.centralizer ℂ T + star_mem' ha := star_mem_subalgebraCentralizer hT ha + +omit [CStarAlgebra A] in +@[simp] theorem coe_starSubalgebraCentralizer (T : Set (H →L[ℂ] H)) + (hT : ∀ x ∈ T, star x ∈ T) : + (starSubalgebraCentralizer T hT : Set (H →L[ℂ] H)) = Set.centralizer T := + Subalgebra.coe_centralizer ℂ T + +omit [CStarAlgebra A] in +theorem carrier_starSubalgebraCentralizer (T : Set (H →L[ℂ] H)) + (hT : ∀ x ∈ T, star x ∈ T) : + (starSubalgebraCentralizer T hT).carrier = Set.centralizer T := + Subalgebra.coe_centralizer ℂ T + +/-- **The bicommutant of a self-adjoint set is a von Neumann algebra.** For a +self-adjoint set `S` of bounded operators, the double commutant `S''` is a von +Neumann algebra (it equals its own bicommutant, since `S'''' = S''`). -/ +noncomputable def vonNeumannOfSelfAdjoint (S : Set (H →L[ℂ] H)) + (hS : ∀ x ∈ S, star x ∈ S) : VonNeumannAlgebra H where + toStarSubalgebra := + starSubalgebraCentralizer (Set.centralizer S) (fun _ hx => star_mem_setCentralizer hS hx) + centralizer_centralizer' := by + rw [carrier_starSubalgebraCentralizer, Set.centralizer_centralizer_centralizer] + +omit [CStarAlgebra A] in +@[simp] theorem coe_vonNeumannOfSelfAdjoint (S : Set (H →L[ℂ] H)) + (hS : ∀ x ∈ S, star x ∈ S) : + (vonNeumannOfSelfAdjoint S hS : Set (H →L[ℂ] H)) + = Set.centralizer (Set.centralizer S) := + Subalgebra.coe_centralizer ℂ (Set.centralizer S) + +omit [CompleteSpace H] in +private theorem smul_one_mem_centralizer (c : ℂ) (S : Set (H →L[ℂ] H)) : + (c • 1 : H →L[ℂ] H) ∈ Set.centralizer S := + Set.mem_centralizer_iff.mpr fun M _ => by + rw [mul_smul_comm, smul_mul_assoc, mul_one, one_mul] + +/-- **An irreducible representation generates a factor.** The von Neumann algebra +`π(A)''` of an irreducible representation has *trivial center*: an operator lies in +the center `π(A)'' ∩ (π(A)'')'` if and only if it is a scalar multiple of the +identity. The center is contained in `(π(A)'')' = π(A)'` (the triple commutant +collapses to the single one), which irreducibility makes the scalars; conversely +scalars are central. -/ +theorem center_gnsVonNeumann_eq_of_isIrreducible {π : A →⋆ₐ[ℂ] (H →L[ℂ] H)} + (hirr : IsIrreducible π) : + gnsVonNeumann π ∩ Set.centralizer (gnsVonNeumann π) + = {T : H →L[ℂ] H | ∃ c : ℂ, T = c • 1} := by + ext T + simp only [Set.mem_inter_iff, Set.mem_setOf_eq] + constructor + · rintro ⟨_, hT'⟩ + rw [gnsVonNeumann, Set.centralizer_centralizer_centralizer] at hT' + exact hirr T fun a => Set.mem_centralizer_iff.mp hT' (π a) ⟨a, rfl⟩ + · rintro ⟨c, rfl⟩ + exact ⟨smul_one_mem_centralizer c _, smul_one_mem_centralizer c _⟩ + end GNS end Physicslib4 diff --git a/Physicslib4/GNS/RadonNikodym.lean b/Physicslib4/GNS/RadonNikodym.lean index 118666e..79ba1d2 100644 --- a/Physicslib4/GNS/RadonNikodym.lean +++ b/Physicslib4/GNS/RadonNikodym.lean @@ -283,5 +283,23 @@ theorem isPure_iff_isIrreducible {ω : State A} {π : A →⋆ₐ[ℂ] (H →L[ ⟨fun hpure => isIrreducible_of_isPure hcyc hrep hpure, fun hirr => isPure_of_isIrreducible hcyc hrep hirr⟩ +/-- **The GNS representation of a pure state is a factor.** For a pure state `ω` +there is a cyclic GNS triple `(H, π, Ω)` reproducing `ω` whose generated von +Neumann algebra `π(A)''` has *trivial center*: the center +`π(A)'' ∩ (π(A)'')'` equals the scalar operators. This combines the GNS +construction, purity ⟹ irreducibility (`isPure_iff_isIrreducible`), and +`center_gnsVonNeumann_eq_of_isIrreducible`. -/ +theorem exists_gns_factor_of_isPure.{u} {A : Type u} [CStarAlgebra A] + {ω : State A} (hpure : IsPure ω) : + ∃ (H : Type u) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : A →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H), + IsCyclicVector π Ω ∧ + (∀ a : A, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + gnsVonNeumann π ∩ Set.centralizer (gnsVonNeumann π) + = {T : H →L[ℂ] H | ∃ c : ℂ, T = c • 1} := by + obtain ⟨H, i1, i2, i3, π, Ω, hcyc, hrepro, _⟩ := gns_construction ω + exact ⟨H, i1, i2, i3, π, Ω, hcyc, hrepro, + center_gnsVonNeumann_eq_of_isIrreducible ((isPure_iff_isIrreducible hcyc hrepro).mp hpure)⟩ + end GNS end Physicslib4 diff --git a/Physicslib4/GNS/UnitaryRepresentation.lean b/Physicslib4/GNS/UnitaryRepresentation.lean index ed2739a..ad0fb53 100644 --- a/Physicslib4/GNS/UnitaryRepresentation.lean +++ b/Physicslib4/GNS/UnitaryRepresentation.lean @@ -93,7 +93,8 @@ theorem exists_gns_unitary_of_invariant.{u} {A : Type u} [CStarAlgebra A] (∀ g : G, U g Ω = Ω) ∧ (∀ g g' : G, U (g' * g) = (U g).trans (U g')) ∧ U 1 = LinearIsometryEquiv.refl ℂ H ∧ - (∀ (g : G) (a : A) (x : H), U g (π a ((U g).symm x)) = π (γ g a) x) := by + (∀ (g : G) (a : A) (x : H), U g (π a ((U g).symm x)) = π (γ g a) x) ∧ + IsCyclicVector π Ω := by obtain ⟨H, _, _, _, π, Ω, hcyc, hrepro, _⟩ := gns_construction ω let cyc : A →ₗ[ℂ] H := { toFun := fun a => π a Ω @@ -123,7 +124,7 @@ theorem exists_gns_unitary_of_invariant.{u} {A : Type u} [CStarAlgebra A] (γ g).toAlgEquiv.toLinearEquiv.extendOfIsometry cyc cyc hcycdense hcycdense (hnorm g) have hUcyc : ∀ (g : G) (a : A), U g (cyc a) = cyc (γ g a) := fun g a => (γ g).toAlgEquiv.toLinearEquiv.extendOfIsometry_eq cyc cyc hcycdense hcycdense (hnorm g) a - refine ⟨H, inferInstance, inferInstance, inferInstance, π, Ω, U, hrepro, ?_, ?_, ?_, ?_, ?_⟩ + refine ⟨H, inferInstance, inferInstance, inferInstance, π, Ω, U, hrepro, ?_, ?_, ?_, ?_, ?_, hcyc⟩ · intro g a exact (γ g).toAlgEquiv.toLinearEquiv.extendOfIsometry_eq cyc cyc hcycdense hcycdense (hnorm g) a diff --git a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex index 033e439..a7da4d2 100644 --- a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex +++ b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex @@ -153,6 +153,15 @@ \subsection{Local von Neumann Algebras} Let $\pi$ be a $*$-representation of the quasilocal algebra on $H$. The \emph{local observable operators} of a region $\mathbf{B}$ are the image $\pi(\mathfrak{U}(\mathbf{B})) = \{\pi(\iota_{\mathbf{B}} a) : a \in \mathfrak{U}(\mathbf{B})\}$. The \emph{local von Neumann algebra} $R(\mathbf{B})$ is the bicommutant $\pi(\mathfrak{U}(\mathbf{B}))''$. \end{definition} +\begin{definition}[$R(\mathbf{B})$ as a von Neumann Algebra] + \label{def:local-von-neumann-algebra} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra, Physicslib4.GNS.vonNeumannOfSelfAdjoint} + \leanfile{Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean} + \leanok + \uses{def:local-von-neumann} + The local algebra $R(\mathbf{B})$ is registered as a genuine \texttt{VonNeumannAlgebra} (Mathlib's bundled structure), not merely a set of operators. The general fact is that the bicommutant $S''$ of any self-adjoint set $S$ of bounded operators is a von Neumann algebra: $S'$ is a $*$-subalgebra (the centralizer of a self-adjoint set is $*$-closed), and $S'' = S''''$ since the triple commutant collapses. The local observable operators $\pi(\mathfrak{U}(\mathbf{B}))$ are self-adjoint ($\pi$ and $\iota$ are $*$-homomorphisms), so $R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$ is a von Neumann algebra whose underlying set is the bicommutant of \ref{def:local-von-neumann}. +\end{definition} + \begin{theorem}[Microcausality at the von Neumann Level] \label{thrm:von-neumann-microcausality} \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_subset_centralizer} @@ -171,6 +180,15 @@ \subsection{Local von Neumann Algebras} For basis regions $\mathbf{B}_1 \subseteq \mathbf{B}_2$, the local von Neumann algebras are nested: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)$. The local observables of $\mathbf{B}_1$ embed into those of $\mathbf{B}_2$ via the quasilocal isotony coherence, and the double commutant is monotone. \end{theorem} +\begin{theorem}[Bundled von Neumann Microcausality and Isotony] + \label{thrm:von-neumann-bundled-order} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant, Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_mono} + \leanfile{Physicslib4/AQFT/HaagKastler/LocalVonNeumann.lean} + \leanok + \uses{def:local-von-neumann-algebra, thrm:von-neumann-microcausality, thrm:von-neumann-isotony} + Phrased on the bundled \texttt{VonNeumannAlgebra} $R(\mathbf{B})$ with its order $\le$ and Mathlib's commutant: for completely spacelike-separated regions $R(\mathbf{B}_1) \le R(\mathbf{B}_2)'$, and for $\mathbf{B}_1 \subseteq \mathbf{B}_2$, $R(\mathbf{B}_1) \le R(\mathbf{B}_2)$. Both reduce to the set-level statements through the coercion $\uparrow R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$. +\end{theorem} + \begin{theorem}[Statistical Independence (Schlieder Property)] \label{thrm:statistical-independence} \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_separating, Physicslib4.AQFT.HaagKastler.HaagKastlerNet.eq_zero_of_commute_of_cyclic} @@ -259,6 +277,75 @@ \subsection{Irreducibility and Schur's Lemma} A state $\omega$ is pure if and only if its cyclic GNS representation is irreducible. For the converse direction, given a dominated $\psi$, its Radon-Nikodym operator $T$ commutes with $\pi$, so by irreducibility $T = c \cdot 1$; the reproducing identity then gives $\psi(a) = c\,\omega(a)$, so $\psi$ is a scalar multiple of $\omega$ and $\omega$ is pure. \end{theorem} +Irreducibility has a von Neumann algebraic reading: the representation generates a \emph{factor}. + +\begin{theorem}[An Irreducible Representation Generates a Factor] + \label{thrm:irreducible-factor} + \lean{Physicslib4.GNS.center_gnsVonNeumann_eq_of_isIrreducible} + \leanfile{Physicslib4/GNS/Irreducibility.lean} + \leanok + \uses{def:irreducible-representation, def:local-von-neumann} + The von Neumann algebra $\pi(A)''$ generated by an irreducible representation has \emph{trivial center}: an operator lies in the center $\pi(A)'' \cap (\pi(A)'')'$ if and only if it is a scalar multiple of the identity. Indeed the center is contained in $(\pi(A)'')' = \pi(A)'$ (the triple commutant collapses to the single one), which irreducibility makes the scalars; conversely scalars are central. +\end{theorem} + +\begin{theorem}[The GNS Representation of a Pure State is a Factor] + \label{thrm:pure-factor} + \lean{Physicslib4.GNS.exists_gns_factor_of_isPure} + \leanfile{Physicslib4/GNS/RadonNikodym.lean} + \leanok + \uses{def:pure-state, thrm:pure-iff-irreducible, thrm:irreducible-factor, thrm:gns-construction-theorem} + For a pure state $\omega$ there is a cyclic GNS triple $(H, \pi, \Omega)$ reproducing $\omega$ whose generated von Neumann algebra $\pi(A)''$ has trivial center, i.e. is a factor. This combines the GNS construction, purity $\Rightarrow$ irreducibility (\ref{thrm:pure-iff-irreducible}), and \ref{thrm:irreducible-factor}. It applies verbatim to the quasilocal algebra $\mathfrak{U}$ and to each local algebra $\mathfrak{U}(\mathbf{B})$, since both are C*-algebras. +\end{theorem} + +The order-theoretic definition of purity (\ref{def:pure-state}) coincides with the convex-geometric one: $\omega$ is an extreme point of the state space. The analytic key is the normalization identity for positive functionals. + +\begin{theorem}[Norm of a Positive Functional] + \label{thrm:norm-positive-functional} + \lean{Physicslib4.GNS.norm_eq_re_apply_one_of_positive} + \leanfile{Physicslib4/GNS/ExtremeState.lean} + \leanok + \uses{lmm:cauchy-schwarz-inequality} + For a positive linear functional $\varphi$ on a unital C*-algebra, $\Vert\varphi\Vert = \mathrm{Re}\,\varphi(1)$. The bound $\mathrm{Re}\,\varphi(1) \le \Vert\varphi\Vert$ is immediate from $\Vert 1\Vert = 1$; conversely Cauchy-Schwarz with the first slot equal to $1$ gives $\Vert\varphi(b)\Vert^2 \le \mathrm{Re}\,\varphi(1)\cdot\mathrm{Re}\,\varphi(b^* b) \le \mathrm{Re}\,\varphi(1)\cdot\Vert\varphi\Vert\,\Vert b\Vert^2$, whence $\Vert\varphi\Vert^2 \le \mathrm{Re}\,\varphi(1)\cdot\Vert\varphi\Vert$. In particular every state satisfies $\omega(1) = 1$. +\end{theorem} + +\begin{definition}[Extreme Point of the State Space] + \label{def:extreme-state} + \lean{Physicslib4.GNS.State.IsExtremePoint} + \leanfile{Physicslib4/GNS/ExtremeState.lean} + \leanok + \uses{def:state} + A state $\omega$ is an \emph{extreme point} of the (convex) state space if it is not a nontrivial convex combination of two distinct states: whenever $\omega = t\,\omega_1 + (1-t)\,\omega_2$ with $0 < t < 1$ and $\omega_1, \omega_2$ states, then $\omega_1 = \omega_2$. +\end{definition} + +\begin{theorem}[Pure $\iff$ Extreme Point] + \label{thrm:pure-iff-extreme} + \lean{Physicslib4.GNS.isPure_iff_isExtremePoint} + \leanfile{Physicslib4/GNS/ExtremeState.lean} + \leanok + \uses{def:pure-state, def:extreme-state, thrm:norm-positive-functional} + A state $\omega$ is pure if and only if it is an extreme point of the state space. If $\omega$ is pure and $\omega = t\,\omega_1 + (1-t)\,\omega_2$, then $t\,\omega_1$ is a positive functional dominated by $\omega$, hence (by purity) a scalar multiple of $\omega$; evaluating at $1$, where every state gives $1$, pins the scalar to $t$ and forces $\omega_1 = \omega = \omega_2$. Conversely, if $\omega$ is extreme and $\psi \le \omega$ is dominated, set $\lambda = \mathrm{Re}\,\psi(1) \in [0,1]$; for $\lambda \in (0,1)$ the rescaled functionals $\lambda^{-1}\psi$ and $(1-\lambda)^{-1}(\omega - \psi)$ are states (normalized via \ref{thrm:norm-positive-functional}) whose convex combination is $\omega$, so extremality identifies them and forces $\psi = \lambda\,\omega$; the boundary cases $\lambda = 0$ and $\lambda = 1$ give $\psi = 0$ and $\psi = \omega$ respectively. +\end{theorem} + +These equivalences specialize to the quasilocal algebra $\mathfrak{U}$ of a Minkowski net, where they characterize purity of a global state - the natural setting for the vacuum and other distinguished states. + +\begin{theorem}[Pure $\iff$ Extreme Point on the Quasilocal Algebra] + \label{thrm:pure-iff-extreme-quasilocal} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.pure_iff_extreme} + \leanfile{Physicslib4/AQFT/HaagKastler/Purity.lean} + \leanok + \uses{def:pure-state, def:extreme-state, thrm:pure-iff-extreme, def:quasilocal-completeness} + A state $\omega$ on the canonical quasilocal algebra $\mathfrak{U}$ of a Haag-Kastler net is pure if and only if it is an extreme point of the state space of $\mathfrak{U}$. This is the abstract equivalence \ref{thrm:pure-iff-extreme} applied to the C*-algebra $\mathfrak{U}$. +\end{theorem} + +\begin{theorem}[Pure $\iff$ Irreducible GNS on the Quasilocal Algebra] + \label{thrm:pure-iff-irreducible-quasilocal} + \lean{Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_pure_iff_irreducible} + \leanfile{Physicslib4/AQFT/HaagKastler/Purity.lean} + \leanok + \uses{def:pure-state, def:irreducible-representation, thrm:pure-iff-irreducible, thrm:gns-construction-theorem, def:quasilocal-completeness} + For a state $\omega$ on the quasilocal algebra $\mathfrak{U}$ there is a GNS triple $(H, \pi, \Omega)$ reproducing $\omega$ in which $\omega$ is pure if and only if the representation $\pi$ is irreducible. This combines the GNS construction with the abstract \ref{thrm:pure-iff-irreducible}. +\end{theorem} + \subsection{Covariant States and the Covariance Action} The Lorentz covariance of a Haag-Kastler net (\ref{def:lorentz-covariance}) acts on the net fiberwise, through the $*$-isomorphisms $\alpha_L : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(L\cdot\mathbf{B})$. We record two consequences: the notion of a Lorentz-covariant family of local states, and the lift of the fiberwise action to a single dynamical $*$-automorphism of the quasilocal algebra. @@ -353,6 +440,26 @@ \subsection{Covariant States and the Covariance Action} For an invariant state $\omega$, the covariance action is implemented on the GNS Hilbert space by a family of unitaries $U(L)$ satisfying $U(L)\,\pi(a)\Omega = \pi(\beta_L a)\,\Omega$ and $U(L)\Omega = \Omega$. The unitaries are obtained by extending the densely-defined isometry $\pi(a)\Omega \mapsto \pi(\beta_L a)\Omega$ - isometric because $\omega$ preserves the GNS inner product $\langle \pi(a)\Omega, \pi(b)\Omega\rangle = \omega(a^* b)$ - to the whole GNS space. \end{theorem} +Combining invariance with purity makes the GNS representation both covariant and irreducible. We emphasise that this is a \emph{precursor} to a vacuum representation, not a vacuum itself: a genuine vacuum additionally requires the spectrum condition (positivity of the energy-momentum spectrum), which is not imposed - and indeed not expressible - here. + +\begin{theorem}[Irreducible Covariant Representation of a Pure Invariant State] + \label{thrm:irreducible-covariant-representation} + \lean{Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.IsInvariantState.exists_gns_irreducible_covariant} + \leanfile{Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean} + \leanok + \uses{thrm:invariant-state-gns-unitary, def:pure-state, def:irreducible-representation, thrm:pure-iff-irreducible} + A state $\omega$ on the quasilocal algebra that is both invariant under the covariance action and pure yields a GNS representation that is simultaneously \emph{covariant} - implemented by a unitary representation $U(L)$ of the inhomogeneous Lorentz group fixing the cyclic vector $\Omega$, with operator covariance $U(L)\,\pi(a)\,U(L)^{-1} = \pi(\beta_L a)$ - and \emph{irreducible}. This combines the covariant GNS triple of \ref{thrm:invariant-state-gns-unitary} with purity $\Rightarrow$ irreducibility (\ref{thrm:pure-iff-irreducible}). It is a necessary precursor to a vacuum representation; the spectrum condition would be the remaining ingredient. +\end{theorem} + +\begin{theorem}[Purity is Covariance-Invariant] + \label{thrm:purity-covariance-invariant} + \lean{Physicslib4.GNS.isPure_precomp_iff, Physicslib4.AQFT.HaagKastler.CovariantQuasilocalAlgebra.isPure_precomp_action_iff} + \leanfile{Physicslib4/GNS/ExtremeState.lean} + \leanok + \uses{def:pure-state, lmm:quasilocal-action-coherence} + Purity is preserved by any $*$-automorphism: for $\Phi : \mathfrak{U} \xrightarrow{\sim} \mathfrak{U}$, the pullback state $\omega \circ \Phi$ is pure if and only if $\omega$ is. A dominated positive functional $\psi \le \omega \circ \Phi$ transports to $\psi \circ \Phi^{-1} \le \omega$, which purity sends to a scalar multiple of $\omega$; transporting back gives $\psi$ proportional to $\omega \circ \Phi$. Applied to the covariance automorphism $\Phi = \beta_L$, this says purity of a state is a Lorentz-covariance-invariant property. +\end{theorem} + \subsection{The Separating Vector of a Faithful State} A faithful state has a sharper consequence at the level of the GNS construction than the faithfulness of its representation: its cyclic vector is also \emph{separating}. This is the basic datum of the modular (Tomita-Takesaki) theory of the associated von Neumann algebra. diff --git a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex index 35d8500..6346e37 100644 --- a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex +++ b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex @@ -152,6 +152,15 @@ \subsection{Local von Neumann Algebras in Curved Spacetime} Let $\pi$ be a $*$-representation of a containing basis algebra $\mathfrak{U}(\mathbf{B})$ on $H$. For a subregion $\mathbf{B}' \subseteq \mathbf{B}$, the \emph{local observable operators} are the image $\pi(\mathfrak{U}(\mathbf{B}'))$ under the isotony embedding, and the \emph{local von Neumann algebra} $R(\mathbf{B}')$ is the bicommutant $\pi(\mathfrak{U}(\mathbf{B}'))''$. \end{definition} +\begin{definition}[$R(\mathbf{B}')$ as a von Neumann Algebra (Curved Spacetime)] + \label{def:local-von-neumann-algebra-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean} + \leanok + \uses{def:local-von-neumann-in-curved-spacetime, def:local-von-neumann-algebra} + As in the Minkowski case, $R(\mathbf{B}')$ is registered as a genuine \texttt{VonNeumannAlgebra}: the local observable operators $\pi(\mathfrak{U}(\mathbf{B}'))$ are self-adjoint (the isotony embedding and $\pi$ are $*$-homomorphisms), so their bicommutant is a von Neumann algebra whose underlying set is the bicommutant of \ref{def:local-von-neumann-in-curved-spacetime}. The construction is the same general bicommutant-of-a-self-adjoint-set lemma. +\end{definition} + \begin{theorem}[Microcausality at the von Neumann Level (Curved Spacetime)] \label{thrm:von-neumann-microcausality-in-curved-spacetime} \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_subset_centralizer} @@ -170,6 +179,15 @@ \subsection{Local von Neumann Algebras in Curved Spacetime} For nested basis subregions $\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathbf{B}$, the local von Neumann algebras are nested: $R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)$. Unlike Minkowski, the curved Axiom 3 isotony embeddings are chosen witnesses with no built-in composition law, so the coherence of the embeddings (that the $\mathbf{B}_1 \hookrightarrow \mathbf{B}$ embedding factors through $\mathbf{B}_2$) is taken as an explicit hypothesis; it holds automatically whenever the Axiom 3 witnesses form a genuine inclusion family. Given it, the local observables of $\mathbf{B}_1$ embed into those of $\mathbf{B}_2$ and the double commutant is monotone. \end{theorem} +\begin{theorem}[Bundled von Neumann Microcausality and Isotony (Curved Spacetime)] + \label{thrm:von-neumann-bundled-order-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_le_commutant, Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_mono} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/LocalVonNeumann.lean} + \leanok + \uses{def:local-von-neumann-algebra-in-curved-spacetime, thrm:von-neumann-microcausality-in-curved-spacetime, thrm:von-neumann-isotony-in-curved-spacetime} + Phrased on the bundled \texttt{VonNeumannAlgebra} $R(\mathbf{B}')$ with its order $\le$ and Mathlib's commutant: for completely spacelike-separated subregions $R(\mathbf{B}_1) \le R(\mathbf{B}_2)'$, and for $\mathbf{B}_1 \subseteq \mathbf{B}_2$ (with the isotony coherence) $R(\mathbf{B}_1) \le R(\mathbf{B}_2)$. Both reduce to the set-level statements through the coercion $\uparrow R(\mathbf{B}') = \pi(\mathfrak{U}(\mathbf{B}'))''$. +\end{theorem} + \begin{theorem}[Statistical Independence (Schlieder Property)] \label{thrm:statistical-independence-in-curved-spacetime} \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_separating, Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.eq_zero_of_commute_of_cyclic} @@ -179,6 +197,28 @@ \subsection{Local von Neumann Algebras in Curved Spacetime} The abstract mechanism is: if $\Omega$ is cyclic for a set $S$ of operators, then any $R$ commuting with all of $S$ with $R\Omega = 0$ is zero (it vanishes on the dense set $S\Omega$). Applied to the net: if $\Omega$ is cyclic for the local observables of $\mathbf{B}_1$ - the role supplied in Minkowski spacetime by Reeh-Schlieder - then for a spacelike-separated subregion $\mathbf{B}_2$, every $R \in R(\mathbf{B}_2)$ with $R\Omega = 0$ is zero, since $R(\mathbf{B}_2)$ commutes with the observables of $\mathbf{B}_1$ by curved microcausality (\ref{thrm:von-neumann-microcausality-in-curved-spacetime}). Thus $\Omega$ is separating for $R(\mathbf{B}_2)$: a nonzero observable of one region cannot be annihilated by the cyclic vector of a spacelike-separated region, the operator-algebraic form of statistical independence. \end{theorem} +\subsection{Purity of States on Local Algebras in Curved Spacetime} + +Each local algebra $\mathfrak{U}(\mathbf{B})$ of a Haag-Kastler net in curved spacetime is itself a unital C*-algebra with its own state space and GNS representations. The abstract characterizations of purity therefore apply per region, registered here for $\mathfrak{U}(\mathbf{B})$. There is no quasilocal algebra in curved spacetime, so - unlike the Minkowski covariant-vacuum picture - these are genuinely local statements, one for each region. + +\begin{theorem}[Pure $\iff$ Extreme Point on a Local Algebra] + \label{thrm:pure-iff-extreme-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.pure_iff_extreme} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/Purity.lean} + \leanok + \uses{def:pure-state, def:extreme-state, thrm:pure-iff-extreme} + A state $\omega$ on the local algebra $\mathfrak{U}(\mathbf{B})$ is pure if and only if it is an extreme point of the state space of $\mathfrak{U}(\mathbf{B})$. This is the abstract equivalence \ref{thrm:pure-iff-extreme} applied to the C*-algebra $\mathfrak{U}(\mathbf{B})$. +\end{theorem} + +\begin{theorem}[Pure $\iff$ Irreducible GNS on a Local Algebra] + \label{thrm:pure-iff-irreducible-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_pure_iff_irreducible} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/Purity.lean} + \leanok + \uses{def:pure-state, def:irreducible-representation, thrm:pure-iff-irreducible, thrm:gns-construction-theorem} + For a state $\omega$ on the local algebra $\mathfrak{U}(\mathbf{B})$ there is a GNS triple $(H, \pi, \Omega)$ reproducing $\omega$ in which $\omega$ is pure if and only if the representation $\pi$ is irreducible (its commutant is trivial). This combines the GNS construction with the abstract \ref{thrm:pure-iff-irreducible}. +\end{theorem} + \subsection{Covariant States in Curved Spacetime} As in the Minkowski case, the isometric covariance (\ref{def:isometric-covariance-in-curved-spacetime}) acts fiberwise through the $*$-isomorphisms $\alpha_\varphi : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(\varphi(\mathbf{B}))$. Since there is no quasilocal algebra, only the local notion of a covariant family of states is available. @@ -243,6 +283,24 @@ \subsection{The Stabilizer GNS Unitary in Curved Spacetime} If moreover the isometry group carries a topology (the abstract interface supplies none, so it is an added hypothesis) and the matrix coefficients $\varphi \mapsto \omega\big(a^*\,\hat\alpha_\varphi b\big)$ are continuous on $\mathrm{Stab}(\mathbf{B})$, then the representation $U$ is strongly continuous: $\varphi \mapsto U(\varphi)\psi$ is continuous for every GNS vector $\psi$. The stabilizer subgroup inherits its topology as a subspace of the isometry group. \end{theorem} +\begin{theorem}[Irreducible Covariant Representation of a Pure Invariant State (Curved Spacetime)] + \label{thrm:irreducible-covariant-representation-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_irreducible_covariant_stabilizer} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean} + \leanok + \uses{thrm:gns-unitary-stabilizer-in-curved-spacetime, def:pure-state, def:irreducible-representation, thrm:pure-iff-irreducible-in-curved-spacetime} + A state $\omega$ on a local algebra $\mathfrak{U}(\mathbf{B})$ that is invariant under the stabilizer action and pure yields a GNS representation that is simultaneously \emph{covariant} - implemented by a unitary representation $U$ of $\mathrm{Stab}(\mathbf{B})$ fixing the cyclic vector $\Omega$, with operator covariance $U(\varphi)\,\pi(a)\,U(\varphi)^{-1} = \pi(\hat\alpha_\varphi a)$ - and \emph{irreducible}. This is the curved, per-region analogue of \ref{thrm:irreducible-covariant-representation} (there is no quasilocal algebra), combining \ref{thrm:gns-unitary-stabilizer-in-curved-spacetime} with purity $\Rightarrow$ irreducibility. It is not a vacuum: curved spacetime admits no global vacuum, and the analogue of the spectrum condition (the Hadamard / microlocal spectrum condition) is a separate requirement not imposed here. +\end{theorem} + +\begin{theorem}[Purity is Invariant under the Stabilizer Action] + \label{thrm:purity-covariance-invariant-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isPure_precomp_stabAut_iff} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean} + \leanok + \uses{def:pure-state, def:stabilizer-action-in-curved-spacetime, thrm:purity-covariance-invariant} + A state $\omega$ on a local algebra $\mathfrak{U}(\mathbf{B})$ is pure if and only if its pullback $\omega \circ \hat\alpha_\varphi$ along the stabilizer automorphism is pure, for every $\varphi \in \mathrm{Stab}(\mathbf{B})$. This is the curved specialization of \ref{thrm:purity-covariance-invariant}: purity is invariant under the isometric symmetry that fixes the region. +\end{theorem} + \subsection{KMS States for a Killing Flow} The stabilizer subgroup of a region is, in the genuinely curved examples, a one-parameter Killing flow rather than the full isometry group. Such a flow makes the local algebra $\mathfrak{U}(\mathbf{B})$ into a dynamical system, and the natural equilibrium states are the KMS states (\ref{def:kms-state}) for that flow. This is the precise sense in which the curved-spacetime thermal states are thermal: the Hartle-Hawking state on a Schwarzschild exterior is KMS for the stationary Killing flow at the Hawking temperature, and the Bunch-Davies state restricted to a de Sitter static patch is KMS for the boost Killing flow at the Gibbons-Hawking temperature. diff --git a/home_page/index.md b/home_page/index.md index 99691c1..06c3837 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -55,9 +55,9 @@ Chapter 10 assembles the formalisation-ready content, organised into six main bl - **Spacetime and causal structure.** Gives precise definitions of spacetime, Minkowski spacetime, and Lorentzian spacetime, together with the full apparatus of causal structure: timelike, spacelike, and null vectors; time orientation; future- and past-pointing vectors; paths, curves, and trips; causal trips; chronological and causal futures and pasts; spacelike separation; and the Alexandrov topology. Supporting lemmas establish the basic geometry (the causal classification trichotomy, the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors, convexity of the future and past cones, monotonicity of futures and pasts, symmetry of spacelike separation, and the fact that isometries preserve causal classification, chronology, and Alexandrov-basis sets). -- **Sharpened Haag–Kastler Axioms in Minkowski and curved spacetime.** States the sharpened axioms—Local Algebras, Isotony, Local Commutativity, Quasilocal Algebra, and Lorentz Covariance—bundled into a single `HaagKastlerNet` structure, together with their curved-spacetime generalisation (`HaagKastlerNet` in curved spacetime). Derives the operator form of Einstein Causality in both settings. Develops covariant families of local states, the lift of the fiberwise covariance action to a \*-automorphism of the quasilocal algebra, group-action coherence of the covariance automorphism, and GNS-unitary implementation of a Poincaré-invariant (vacuum) state. In the curved-spacetime setting, where no quasilocal algebra exists, the covariance action restricts to the stabiliser subgroup of a region, and the GNS unitary represents that stabiliser action. +- **Sharpened Haag–Kastler Axioms in Minkowski and curved spacetime.** States the sharpened axioms—Local Algebras, Isotony, Local Commutativity, Quasilocal Algebra, and Lorentz Covariance—bundled into a single `HaagKastlerNet` structure, together with their curved-spacetime generalisation (`HaagKastlerNet` in curved spacetime). Derives the operator form of Einstein Causality in both settings. Develops covariant families of local states, the lift of the fiberwise covariance action to a \*-automorphism of the quasilocal algebra, group-action coherence of the covariance automorphism, and GNS-unitary implementation of a Poincaré-invariant (vacuum) state. Proves that purity of a state is preserved by any \*-automorphism and is therefore a Lorentz-covariance-invariant property, and that a state that is both invariant and pure yields a GNS representation that is simultaneously covariant and irreducible—a necessary precursor to a vacuum representation. In the curved-spacetime setting, where no quasilocal algebra exists, the covariance action restricts to the stabiliser subgroup of a region, and the GNS unitary represents that stabiliser action; the same combination of invariance and purity yields an irreducible covariant GNS representation of the stabiliser subgroup. -- **Local von Neumann algebras and irreducibility.** Develops the von Neumann algebra layer of the theory: defines the local von Neumann algebra $$R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$$ of a region $$\mathbf{B}$$ in a representation $$\pi$$, and proves Microcausality (spacelike-separated local von Neumann algebras commute) and isotony of the von Neumann net. Introduces the notion of an irreducible representation via its commutant, and establishes the Topological Schur Lemma for cyclic representations. Proves the equivalence of purity of a state and irreducibility of its GNS representation (Pure $$\iff$$ Irreducible), including the GNS Radon–Nikodym theorem that realises every dominated positive functional as an operator in the commutant. All of these results are carried over to the curved-spacetime setting, where microcausality and isotony are expressed relative to a common containing local algebra rather than the (non-existent) quasilocal algebra. +- **Local von Neumann algebras and irreducibility.** Develops the von Neumann algebra layer of the theory: defines the local von Neumann algebra $$R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$$ of a region $$\mathbf{B}$$ in a representation $$\pi$$, and proves Microcausality (spacelike-separated local von Neumann algebras commute) and isotony of the von Neumann net. Introduces the notion of an irreducible representation via its commutant, and establishes the Topological Schur Lemma for cyclic representations. Proves the equivalence of purity of a state and irreducibility of its GNS representation (Pure $$\iff$$ Irreducible), including the GNS Radon–Nikodym theorem that realises every dominated positive functional as an operator in the commutant. Proves that the norm of any positive linear functional on a unital C\*-algebra equals its value on the unit, and uses this to establish that purity and being an extreme point of the state space are equivalent characterisations of the same condition (Pure $$\iff$$ Extreme Point). Proves that an irreducible representation generates a von Neumann algebra with trivial centre—a factor—and consequently that the GNS representation of a pure state is a factor. All of these results are carried over to the curved-spacetime setting, where microcausality and isotony are expressed relative to a common containing local algebra rather than the (non-existent) quasilocal algebra, and where purity of a state on a local algebra is equivalently characterised by extreme-point status and by irreducibility of the local GNS representation. - **Separating vectors and faithful states.** Proves that the cyclic vector of a faithful state is also separating for the image of the GNS representation—the basic datum of Tomita–Takesaki modular theory. This result holds in any representation reproducing a faithful state, not only the canonical GNS one. @@ -97,6 +97,7 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: - Local von Neumann Algebra (Minkowski and curved spacetime) - Irreducible Representation - Pure State +- Extreme Point of the State Space **KMS condition** - One-Parameter Automorphism Group, KMS State @@ -128,40 +129,52 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: - Uniqueness and existence of the quasilocal covariance lift - Group-action coherence of the covariance automorphism - Existence for the trivial net -- GNS-unitary implementation of an invariant state (Theorem 86) +- GNS-unitary implementation of an invariant state (Theorem 96) +- Irreducible covariant GNS representation of a pure invariant state (Theorem 97) +- Purity is covariance-invariant: purity of a state is preserved under pullback by any \*-automorphism, and in particular under the covariance automorphism $$\beta_L$$ (Theorem 98) - Einstein Causality in a representation (Theorem 65) **Covariance – curved spacetime** - Composition of covariance in curved spacetime - The stabiliser action is a group action -- GNS unitary representation of the stabiliser (Theorem 112); strongly continuous stabiliser GNS unitary -- Einstein Causality in a representation, curved spacetime (Theorem 104) +- GNS unitary representation of the stabiliser (Theorem 129); strongly continuous stabiliser GNS unitary (Theorem 130) +- Irreducible covariant GNS representation of a pure invariant state on a local algebra (Theorem 131) +- Purity is invariant under the stabiliser action (Theorem 132) +- Einstein Causality in a representation, curved spacetime (Theorem 116) **Local von Neumann algebras – Minkowski spacetime** -- Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 67) -- Isotony of the von Neumann net (Theorem 68) -- Statistical Independence (Schlieder Property): if the cyclic vector of one region is cyclic for its local observables, it is separating for the local von Neumann algebra of any spacelike-separated region (Theorem 69) -- Topological Schur Lemma for cyclic representations (Theorem 70) -- Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 71) -- Pure state implies irreducible GNS representation (Theorem 73) -- GNS Radon–Nikodym form is bounded (Theorem 74) -- GNS Radon–Nikodym operator exists and commutes with the representation (Theorem 75) -- Pure state $$\iff$$ irreducible GNS representation (Theorem 76) +- Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 68) +- Isotony of the von Neumann net (Theorem 69) +- Statistical Independence (Schlieder Property): if the cyclic vector of one region is cyclic for its local observables, it is separating for the local von Neumann algebra of any spacelike-separated region (Theorem 71) +- Topological Schur Lemma for cyclic representations (Theorem 73) +- Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 74) +- Pure state implies irreducible GNS representation (Theorem 76) +- GNS Radon–Nikodym form is bounded (Theorem 77) +- GNS Radon–Nikodym operator exists and commutes with the representation (Theorem 78) +- Pure state $$\iff$$ irreducible GNS representation (Theorem 79) +- An irreducible representation generates a von Neumann algebra with trivial centre, i.e. a factor (Theorem 80) +- The GNS representation of a pure state generates a factor (Theorem 81) +- Norm of a positive linear functional equals its value on the unit (Theorem 82) +- Pure state $$\iff$$ extreme point of the state space (Theorem 84) +- Pure state $$\iff$$ extreme point of the state space of the quasilocal algebra (Theorem 85) +- Pure state $$\iff$$ irreducible GNS representation on the quasilocal algebra (Theorem 86) **Local von Neumann algebras – curved spacetime** -- Microcausality relative to a containing local algebra (Theorem 106) -- Isotony of the curved von Neumann net (Theorem 107) -- Statistical Independence (Schlieder Property) in curved spacetime: if the cyclic vector of one subregion is cyclic for its local observables, it is separating for the local von Neumann algebra of any completely spacelike-separated subregion (Theorem 109) +- Microcausality relative to a containing local algebra (Theorem 119) +- Isotony of the curved von Neumann net (Theorem 120) +- Statistical Independence (Schlieder Property) in curved spacetime: if the cyclic vector of one subregion is cyclic for its local observables, it is separating for the local von Neumann algebra of any completely spacelike-separated subregion (Theorem 122) +- Pure state $$\iff$$ extreme point of the state space of a local algebra (Theorem 123) +- Pure state $$\iff$$ irreducible GNS representation on a local algebra (Theorem 124) **KMS condition** - Boundary coincidence for $$a = 1$$ -- $$i\beta$$-periodic entire extension (strip Schwarz reflection) -- Strip-Liouville holds for $$\beta > 0$$ -- KMS states are invariant (Theorem 94) -- Uniqueness on the strip from boundary values: two strip-functions sharing both boundary lines agree everywhere on the strip (Theorem 96) -- Uniqueness of the KMS correlation function: the analytic completion of a KMS correlation function for any pair $$(a, b)$$ is unique (Theorem 97) -- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 117) -- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 119) +- $$i\beta$$-periodic entire extension (strip Schwarz reflection) (Theorem 104) +- Strip-Liouville holds for $$\beta > 0$$ (Theorem 105) +- KMS states are invariant (Theorem 106) +- Uniqueness on the strip from boundary values: two strip-functions sharing both boundary lines agree everywhere on the strip (Theorem 107) +- Uniqueness of the KMS correlation function: the analytic completion of a KMS correlation function for any pair $$(a, b)$$ is unique (Theorem 108) +- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 134) +- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 136) ### Axioms