§10.7 Haag–Kastler Axioms in curved spacetime (pp. 330–340)

51 items, Definitions 638–688. The axioms are restated for a Lorentzian spacetime: Local Algebras (Definition 638), Isotony (Definition 639, again supplying the family as chosen data with identity and composition laws), Local Commutativity (Definition 640, which uses the Axiom 2 family rather than choosing its own witnesses), local observables (Definition 641), Local Completeness (Definition 642), and Isometric Covariance (Definition 643, whose coherence condition, as in Minkowski, is stated for the Axiom 2 isotony family), bundled into a HaagKastlerNet in curved spacetime (Definition 644), and the axioms are jointly satisfiable (Theorem 645). This form of Axioms 2 and 3 has a visible consequence downstream: statements about nested regions have to factor a three-fold inclusion \(\mathbf{B}_1 \subseteq \mathbf{B}_2 \subseteq \mathbf{B}\) inside a common containing algebra, and that factorisation is the composition law of Axiom 2, so no coherence hypothesis is needed at any such site—curved isotony (Theorem 651) and the curved von Neumann net (Definition 653) are unconditional. An explicit hypothesis remains only where the abstract interface genuinely cannot supply it, namely basis-set preservation in Geometric Covariance (Theorem 657), discharged for nets arising from a concrete geometric spacetime; the coherence of the stabiliser action with the isotony embeddings is condition (3) of Axiom 5 transported along \(g \cdot \mathbf{B} = \mathbf{B}\).

§10.7.1 Einstein Causality in Curved Spacetime (p. 333, items 646–647). The operator form of local commutativity, expressed in a representation of a common containing local algebra rather than of a global quasilocal algebra (Theorem 646), and its restriction to subregions of completely spacelike-separated regions on a concrete spacetime (Lemma 647).
§10.7.2 Local von Neumann Algebras in Curved Spacetime (p. 333, items 648–659). The Minkowski development of §10.6.5 mirrored relative to a containing region: the local von Neumann algebra of a subregion and its bundled registration (Definitions 648–649), Microcausality (Theorem 650), unconditional Isotony (Theorem 651), the bundled form (Theorem 652), the net as an order-preserving map on the poset of subregions (Definition 653), Statistical Independence in set-level and bundled forms (Theorems 654–655), additive-free locality (Theorem 656), and Geometric Covariance via the stabiliser GNS representation (Theorem 657) with orbit-invariance of factoriality (Theorem 658) and the upgrade to a *-algebra isomorphism (Theorem 659).
§10.7.3 Relative Commutants of Nested Local Algebras in Curved Spacetime (p. 335, items 660–668). The curved counterpart of §10.6.6: the relative commutant of a nested pair inside a containing region (Definition 660), its containment in the larger algebra, commutation with the smaller, and containment of the centre (Theorems 661–663), irreducible inclusions (Definition 664) and their consequences (Theorems 665–666), plus the abelian/centre facts specialised to curved local algebras (Theorems 667–668).
§10.7.4 Purity of States on Local Algebras in Curved Spacetime (p. 337, items 669–673). Each local algebra is a unital C*-algebra with its own state space, so the abstract purity characterisations are registered per region: Pure \(\iff\) Extreme Point (Theorem 669), Pure \(\iff\) Irreducible GNS (Theorem 670), the GNS representation of a pure state generates a factor and indeed all of \(\mathcal{B}(H)\) (Theorem 671), the Irreducible Dichotomy for a curved local algebra (Theorem 672), and GNS covariance for curved local algebras (Theorem 673).
§10.7.5 Covariant States in Curved Spacetime (p. 337, items 674–675). Covariant families of local states in curved spacetime (Definition 674) and their composition law (Lemma 675).
§10.7.6 The Stabilizer GNS Unitary in Curved Spacetime (p. 338, items 676–682). Since no quasilocal algebra exists on a generic Lorentzian spacetime, the covariance action restricts to the stabiliser subgroup \(\mathrm{Stab}(\mathbf{B})\) of a region, giving automorphisms of the single local algebra \(\mathfrak{U}(\mathbf{B})\) (Definition 676) that form a genuine group action (Lemma 677). A stabiliser-invariant state carries a unitary GNS representation of \(\mathrm{Stab}(\mathbf{B})\) (Theorem 678), strongly continuous when the matrix coefficients are continuous (Theorem 679); a state both stabiliser-invariant and pure yields an irreducible covariant representation (Theorem 680); purity is invariant under the stabiliser action (Theorem 681), and GNS data transports along it (Theorem 682).
§10.7.7 KMS States for a Killing Flow (p. 339, items 683–688). Killing flows are identified as one-parameter subgroups of the stabiliser of a region, inducing a one-parameter automorphism group on \(\mathfrak{U}(\mathbf{B})\) (Definition 683, Lemma 684). KMS states for a Killing flow (Definition 685) are the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal. Such a state at positive inverse temperature automatically carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow, yielding the curved-spacetime thermal representation—the analogue of the Minkowski vacuum representation (Theorem 686); these states form a convex set (Theorem 687), and the corresponding ground state is recorded alongside them (Definition 688).

Where the Lean lives: Physicslib4/AQFT/HaagKastlerCurved/ (LocalVonNeumann, StabilizerAction, StabilizerKMS, Purity, GeometricCovariance, …)

Items

Every entry links to its node in the web blueprint and names the principal Lean declaration.

§10.7 The axioms (p. 330)

Definition 638 — Axiom 1: Local Algebras · Physicslib4.AQFT.HaagKastlerCurved.LocalNet
Definition 639 — Axiom 2: Isotony · Physicslib4.AQFT.HaagKastlerCurved.Isotony
Definition 640 — Axiom 3: Local Commutativity · Physicslib4.AQFT.HaagKastlerCurved.LocalCommutativity
Definition 641 — Local Observable · Physicslib4.AQFT.HaagKastlerCurved.IsLocalObservable (+1 more)
Definition 642 — Axiom 4: Local Completeness · Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebra
Definition 643 — Axiom 5: Isometric Covariance · Physicslib4.AQFT.HaagKastlerCurved.IsometricCovariance (implemented via the explicitly orientation-preserving subgroup — see Formalisation status)
Definition 644 — Haag–Kastler Net in Curved Spacetime · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet
Theorem 645 — The Curved Haag–Kastler Axioms are Jointly Satisfiable · Physicslib4.Spacetime.LorentzianSpacetime.nonempty_haagKastlerNet_identityComponent (+2 more)

§10.7.1 Einstein Causality in Curved Spacetime (p. 333)

Theorem 646 — Einstein Causality in a Representation (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.einstein_causality (+1 more)
Lemma 647 — Local Commutativity for Subregions (Concrete Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.commute_of_spacelike_mono_geometric

§10.7.2 Local von Neumann Algebras in Curved Spacetime (p. 333)

Definition 648 — Local von Neumann Algebra in Curved Spacetime · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localOperators (+1 more)
Definition 649 — \(R(\mathbf{B}')\) as a von Neumann Algebra (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra
Theorem 650 — Microcausality at the von Neumann Level (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_subset_centralizer
Theorem 651 — Isotony of the von Neumann Net (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_mono
Theorem 652 — Bundled von Neumann Microcausality and Isotony (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_le_commutant (+1 more)
Definition 653 — The Net of von Neumann Algebras in Curved Spacetime · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.vonNeumannNet
Theorem 654 — Statistical Independence (Schlieder Property) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_separating (+1 more)
Theorem 655 — Statistical Independence, bundled (curved spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_separating
Theorem 656 — Additive-Free Locality via the Spacelike Complement (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement_geometric
Theorem 657 — Geometric Covariance of the von Neumann Net (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.lieConj_image_localVonNeumann (+3 more)
Theorem 658 — Orbit-Invariance of Factoriality (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumann_isFactor_smul
Theorem 659 — Geometric Covariance as a von Neumann Algebra Isomorphism (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannEquiv

§10.7.3 Relative Commutants of Nested Local Algebras in Curved Spacetime (p. 335)

Definition 660 — Relative Commutant of a Nested Pair (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.relativeCommutant
Theorem 661 — Relative Commutant Lies in the Larger Algebra (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.relativeCommutant_le_right
Theorem 662 — Relative Commutant Commutes with the Smaller Algebra (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.relativeCommutant_coe_subset_commutant
Theorem 663 — Relative Commutant Contains the Centre (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.center_le_relativeCommutant
Definition 664 — Irreducible Inclusion (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsIrreducibleInclusion
Theorem 665 — An Irreducible Inclusion has Factor Ambient (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isFactor_of_isIrreducibleInclusion
Theorem 666 — Self-Inclusion is Irreducible iff Factor (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isIrreducibleInclusion_self_iff_isFactor
Theorem 667 — Abelian Local von Neumann Algebras (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_center_isAbelian (+1 more)
Theorem 668 — Centre Duality for Local von Neumann Algebras (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.localVonNeumannAlgebra_center_eq_commutant (+1 more)

§10.7.4 Purity of States on Local Algebras in Curved Spacetime (p. 337)

Theorem 669 — Pure \(\iff\) Extreme Point on a Local Algebra · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.pure_iff_extreme
Theorem 670 — Pure \(\iff\) Irreducible GNS on a Local Algebra · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_pure_iff_irreducible
Theorem 671 — Pure GNS on a Local Algebra is a Factor Generating \(\mathcal{B}(H)\) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_factor_of_isPure (+1 more)
Theorem 672 — The Irreducible Dichotomy for a Curved Local Algebra · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.areDisjoint_or_unitaryEquiv_of_isIrreducible
Theorem 673 — GNS covariance for curved local algebras · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.unitaryEquiv_gns_covEquiv (+2 more)

§10.7.5 Covariant States in Curved Spacetime (p. 337)

Definition 674 — Covariant Family of Local States in Curved Spacetime · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsCovariantFamily
Lemma 675 — Composition of Covariance in Curved Spacetime · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsCovariantFamily.comp

§10.7.6 The Stabiliser GNS Unitary in Curved Spacetime (p. 338)

Definition 676 — Stabiliser Action on a Local Algebra · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.stabAut
Lemma 677 — The Stabiliser Action is a Group Action · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.stabAut_one (+1 more)
Theorem 678 — GNS Unitary Representation of the Stabiliser · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_unitary_stabilizer (+1 more)
Theorem 679 — Strongly Continuous Stabiliser GNS Unitary · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_unitary_stabilizer_strongContinuous (+1 more)
Theorem 680 — Irreducible Covariant Representation of a Pure Invariant State (Curved Spacetime) · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.exists_gns_irreducible_covariant_stabilizer
Theorem 681 — Purity is Invariant under the Stabiliser Action · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isPure_precomp_stabAut_iff
Theorem 682 — GNS covariance along the stabiliser action · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.unitaryEquiv_gns_stabAut (+2 more)

§10.7.7 KMS States for a Killing Flow (p. 339)

Definition 683 — Killing-Flow Automorphism Family · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.flowAut
Lemma 684 — A Killing Flow Induces a One-Parameter Group · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.isOneParameterAut_flowAut
Definition 685 — KMS State for a Killing Flow · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow
Theorem 686 — The Killing-Flow KMS Thermal Representation · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow.exists_gns_unitary_strongContinuous
Theorem 687 — Convexity of the Killing-Flow KMS States · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsKMSStateForFlow.convexCombo
Definition 688 — Ground State for a Killing Flow · Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.IsGroundStateForFlow (+2 more)

Home · §10.1 GNS · §10.2 Spectral · §10.3 Unbounded · §10.4 Stone · §10.5 Spacetime · §10.6 Minkowski · §10.7 Curved · §10.8 Covariance · Axioms · Guide

← §10.6 Minkowski · §10.8 Covariance →