§10.6 Haag–Kastler Axioms in Minkowski spacetime (pp. 289–330)

The largest section by definition and theorem count (162 items, Definitions 476–637). Each axiom is stated as a definition so that it appears as a node in the declaration graph.

The axioms and the quasilocal colimit (§10.6 and §10.6.1, pp. 289–305, items 476–504). Axiom 1 (Local Algebras, Definition 476) assigns an abstract C*-algebra to every Alexandrov-basis set, with \(\emptyset \mapsto \mathbb{C}1\). Axiom 2 (Isotony, Definition 477) supplies the family of unital *-monomorphisms \(i_{\mathbf{B}_1 \mathbf{B}_2}\) as chosen data, subject to injectivity, an identity law, and a composition law—so that \(\mathbf{B} \mapsto \mathfrak{U}(\mathbf{B})\) is a functor on the inclusion order of basis sets. The blueprint is explicit that the family cannot be an existence statement (the identity and composition conditions are equations between the maps themselves) and that the inclusion hypothesis is non-strict, matching the Lean. §10.6.1 then cashes this in: the diamonds are directed under inclusion (Lemma 478), the isotony family is a directed system in Mathlib’s sense (Lemma 479), and the direct limit carries a well-defined norm (Lemmas 480–482) making it a normed *-algebra (Lemma 483) satisfying the C*-inequality (Lemma 484) but not, in general, complete. A block of results stated for an arbitrary normed *-algebra under standing hypotheses (Definition 485) then carries the structure through completion—the involution and its extension (Definition 486, Lemma 487), the completion coercion as a bundled *-algebra homomorphism (Lemma 488), and the passage of the C*-inequality, the normed \(\mathbb{C}\)-algebra structure, and finally the C*-algebra property to the completion (Lemmas 489–491)—yielding that the completion of the quasilocal colimit is a C*-algebra (Lemma 492). The quasilocal algebra \(\mathfrak{U}\) is defined as that colimit-then-completion (Definition 493); the blueprint records why the shortcut of realising \(\mathfrak{U}\) as a closed *-subalgebra of an ambient C*-algebra is rejected—it would assume an ambient algebra containing copies of every \(\mathfrak{U}(\mathbf{B})\), for which the physics supplies no justification. Axiom 3 (Local Commutativity, Definition 494) follows. It is stated, exactly as in curved spacetime, through the isotony maps: completely spacelike local algebras commute in every local algebra \(\mathfrak{U}(\mathbf{B})\) containing both, and such a \(\mathbf{B}\) always exists because the diamonds are directed. It then holds in every quasilocal algebra (Lemma 495), and it is equivalent to commutation in some quasilocal algebra (Lemma 496). The quasilocal observable (Definition 497) follows. Axiom 4 (Quasilocal Completeness, Definition 498) is presented as a bridge principle—the one axiom joining physical reality to the formalism, asserting the one-way inclusion that every physical observable corresponds to a quasilocal observable, and therefore having no mathematical consumers. The mathematical content is a separate theorem: every local net satisfying Axiom 2 admits a quasilocal algebra, with an injective cocone of canonical embeddings whose images are dense (Theorem 499, with the supporting Lemmas 500–504). The indexing over Alexandrov-basis sets only is essential and not stylistic, since the algebras attached to non-basis subsets are junk fibres about which the axioms say nothing.
§10.6.2 The von Neumann Density Theorem (pp. 306–307, items 505–515). A subsection of general operator theory for a unital *-homomorphism \(\pi : \mathfrak{A} \to \mathcal{B}(H)\), whose only consumer is Theorem 515, the density result that keeps the bridge principle tenable in the presence of larger bicommutants: \(\pi_\omega(\mathfrak{U})\) is strongly dense in \(\pi_\omega(\mathfrak{U})''\). The density theorem is proved here following Murphy, Lemma 4.1.4. A closed subspace invariant under an operator and its adjoint has a commuting orthogonal projection (Lemma 505), so the closed cyclic subspace \(\overline{\pi(\mathfrak{A})\xi}\) reduces the representation (Lemma 506) and every \(T \in \pi(\mathfrak{A})\) maps \(\xi\) into it (Lemma 507). The finite amplification \(\pi^\iota\) on \(\ell^2(\iota; H)\) (Definition 508) is a unital *-homomorphism (Lemma 509); the block entries of an operator in its commutant lie in \(\pi(\mathfrak{A})'\) (Lemma 510), an operator on \(\ell^2(\iota; H)\) is recovered from its block entries (Lemma 511), and so \(\mathrm{diag}(T)\) lies in the amplified bicommutant (Lemma 512). Applying the one-vector case to the amplification approximates \(T\) on any finite set of vectors (Lemma 513), and a neighbourhood basis for the strong operator topology (Lemma 514) turns this into the density theorem (Theorem 515). The Kaplansky density theorem, which would also keep approximants self-adjoint, remains out of scope; nothing needs it.
§10.6.3 Lorentz Covariance and the Haag–Kastler Net (p. 308, items 516–517). Axiom 5 (Lorentz Covariance, Definition 516), whose coherence condition is stated for the Axiom 2 isotony family itself, and the bundled HaagKastlerNet (Definition 517) close the axiomatic block.
§10.6.4 Einstein Causality (p. 309, item 518). Derives the operator form of local commutativity in any *-representation of the quasilocal algebra (Theorem 518).
§10.6.5 Local von Neumann Algebras (p. 310, items 519–531). Defines the local von Neumann algebra \(R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''\) of a region in a representation (Definition 519), registers it as a first-class VonNeumannAlgebra via the bicommutant-of-a-self-adjoint-set lemma (Lemma 520, Definition 521), and proves Microcausality (Theorem 522) and Isotony of the von Neumann net (Theorem 523), together with their bundled forms (Theorem 524) and the region-indexed assignment \(\mathbf{B} \mapsto R(\mathbf{B})\) as an order-preserving map—the net of von Neumann algebras itself (Definition 525). It then proves the Statistical Independence (Schlieder) property in set-level and bundled forms (Theorems 526–527): 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. Additive-free locality (Theorem 528) expresses locality through the spacelike complement without attaching an algebra to the unbounded complement itself. Geometric Covariance (Theorem 529) shows conjugation by the implementing unitary carries \(R(\mathbf{B})\) onto \(R(L \cdot \mathbf{B})\); being a factor is therefore constant along the Lorentz orbit of a region (Theorem 530), and the set equality upgrades to a first-class *-algebra isomorphism of the bundled algebras (Theorem 531).
§10.6.6 Relative Commutants of Nested Local Algebras (p. 312, items 532–539). Organises the theory of inclusions \(R(\mathbf{B}_1) \subseteq R(\mathbf{B}_2)\) around the relative commutant \(R(\mathbf{B}_1)' \cap R(\mathbf{B}_2)\) (Definition 532). It proves antitonicity of the commutant (Theorem 533), that the relative commutant lies in the larger algebra and commutes with the smaller (Theorems 534–535), and that it always contains the centre of the ambient algebra (Theorem 536). An inclusion is irreducible when its relative commutant is trivial (Definition 537); an irreducible inclusion forces the ambient algebra to be a factor (Theorem 538), and the trivial self-inclusion is irreducible exactly when the algebra is a factor (Theorem 539).
§10.6.7 Irreducibility and Schur’s Lemma (p. 313, items 540–562). Introduces irreducible representations via their commutant (Definition 540) and establishes the Topological Schur Lemma for cyclic representations (Theorem 541) together with the operator-theoretic bridge identifying commutant scalars with coefficients proportional to the state (Theorem 542). Defines pure states (Definition 543) and proves “pure implies irreducible” directly (Theorem 544), then the full equivalence Pure \(\iff\) Irreducible (Theorem 547) via a GNS Radon–Nikodym theorem realising every dominated positive functional as an operator in the commutant (Theorems 545–546). An irreducible representation generates a factor (Theorem 548) and, more sharply, all of \(\mathcal{B}(H)\) (Theorem 549), with a bundled density form (Theorem 550); consequently the GNS representation of a pure state generates a factor (Theorem 551) and all of \(\mathcal{B}(H)\) (Theorem 552). The norm of a positive linear functional on a unital C*-algebra equals its value on the unit (Theorem 553), which supports Pure \(\iff\) Extreme Point of the state space (Definition 554, Theorem 555), the underlying convexity and the bridge to Mathlib’s extreme-points API (Theorem 556), and weak-* compactness of the state space (Theorem 560), which supplies the existence of pure states via Krein–Milman. The pullback of a state along a unital *-homomorphism is introduced as its own object (Definition 557) with functoriality (Theorem 558) and the invariance of purity under a *-isomorphism (Theorem 559). The section closes by specialising to the quasilocal algebra (Theorems 561–562).
§10.6.8 Unitary Equivalence and Superselection (p. 317, items 563–564). Defines unitary equivalence of representations (Definition 563) and shows irreducibility and factoriality are unitary invariants, transported by the cross-space conjugation induced by the implementing unitary (Theorem 564).
§10.6.9 GNS Covariance (p. 317, items 565–570). Cyclicity pulls back along a surjective *-homomorphism (Lemma 565), so GNS data transports covariantly along a *-isomorphism of the algebras (Theorem 566), restated as a unitary equivalence (Theorem 567). Pullback along a surjection preserves the image algebra (Lemma 568), whence superselection type transports along a *-isomorphism (Theorem 569): the whole sector structure is an invariant of the algebra, not of its presentation. Applied to the covariance equivalence \(\alpha_L : \mathfrak{U}(\mathbf{B}) \simeq \mathfrak{U}(L \cdot \mathbf{B})\) supplied by Axiom 5, this says the superselection type of a local state is constant along the Lorentz orbit of its region (Theorem 570).
§10.6.10 Disjointness and Quasi-Equivalence (p. 319, items 571–588). Defines disjointness via the vanishing of all intertwiners (Definition 571) and the coarser quasi-equivalence via a *-isomorphism of generated von Neumann algebras (Definition 572). Proves Schur’s Lemma in the form of the Irreducible Dichotomy—two irreducible representations are either disjoint or unitarily equivalent (Theorem 573)—together with Schur multiplicity (Lemma 574) and the triviality of the endomorphism algebra of an irreducible representation (Lemma 575). The commutant is packaged as the self-intertwiner (gauge) von Neumann algebra, trivial exactly when the representation is irreducible (Theorem 576), with double-commutant duality (Theorem 577) and the factor/triviality duality between an algebra and its commutant (Theorem 578). A supporting run develops the centre from scratch: abelian \(\iff\) self-commuting (Lemma 579), the centre \(Z(R) = R \cap R'\) (Definition 580) and its being a von Neumann algebra (Lemma 581), the general two-algebra intersection lemma that the relative commutants of §10.6.6 need (Lemma 582), the centre is abelian (Theorem 583), \(R\) is abelian iff it equals its centre (Lemma 584), a factor is abelian iff it is the scalars (Theorem 585), an algebra and its commutant share a centre (Theorem 586), and factoriality is triviality of the centre (Theorem 587). The Pure-State Dichotomy underlying superselection sectors (Theorem 588) closes the block.
§10.6.11 Direct Sums, Amplification, and Reducibility (p. 322, items 589–592). Defines the direct-sum representation on the \(\ell^2\)-direct sum (Definition 589), shows each summand embeds as a subrepresentation whose projection lies in the commutant of the sum (Theorem 590), defines the \(\iota\)-fold amplification (Definition 591), and proves a direct sum with at least two nonzero summands is reducible, so a multiply-amplified representation is never irreducible (Theorem 592).
§10.6.12 Covariant States and the Covariance Action (p. 322, items 593–621). Defines covariant families of local states (Definition 593) with their composition law (Lemma 594), and the lift of the fibrewise covariance action to a *-automorphism of the quasilocal algebra (Definition 595), with uniqueness (Lemma 596) and existence for every quasilocal algebra (Theorem 598), no covariance-compatibility hypothesis being needed because every quasilocal algebra is automatically covariance-compatible (Lemma 597), and the trivial net as a special case (Theorem 599). The covariant quasilocal algebra of a net is then simply its canonical quasilocal algebra together with the covariance action (Definition 600, realised in Lean as HaagKastlerNet.action, so the covariance dynamics are stated directly for the net), which is a genuine group action (Lemma 601). Invariant states are defined (Definition 602) and shown to be implemented by GNS unitaries (Theorem 603); since weak continuity of a unitary representation implies strong continuity (Lemma 604), the GNS unitary representation is strongly continuous whenever its matrix coefficients are continuous (Theorem 605); a state that is both invariant and pure yields a GNS representation that is simultaneously covariant and irreducible (Theorem 606). The spectrum condition follows. Positive energy (Definition 607) asks that a one-parameter unitary group be strongly continuous with positive generator; the trivial group has positive energy (Lemma 608), the generator is unique (Lemma 609), positivity and positive energy are unitarily invariant (Lemmas 610–611), a positive-energy group is strongly continuous (Lemma 612), the bounded case \(\exp(itP)\) is included (Lemma 613), and, by Stone’s Theorem, positive energy says exactly that \(V(t) = e^{itA}\) with \(A\) positive and self-adjoint (Theorem 614), all collected in Theorem 615. A vacuum state (Definition 616) is an invariant state whose translation groups have positive energy, with the consequences of invariance alone (Theorem 617), the future-timelike translation subgroup (Definition 618), and the vacuum state with that concrete predicate substituted in, leaving no free parameter (Definition 619). Purity is preserved by any *-automorphism and is therefore covariance-invariant (Theorem 620), and GNS data transports along the quasilocal covariance action (Theorem 621).
§10.6.13 The Separating Vector of a Faithful State (p. 328, item 622). The cyclic vector of a faithful state is also separating for the image of the representation (Theorem 622)—the basic datum of Tomita–Takesaki modular theory. This holds in any representation reproducing a faithful state, not only the canonical GNS one.
§10.6.14 The KMS Condition and Thermal Equilibrium (p. 328, items 623–632). Introduces one-parameter automorphism groups (Definition 623) and KMS states (Definition 624) as the algebraic characterisation of thermal equilibrium. The condition is phrased purely as an analyticity statement about correlation functions, so—unlike the spectrum condition—it needs no unbounded-operator theory. The KMS state set is convex (Theorem 625); a boundary-coincidence argument at \(a = 1\) (Lemma 626) together with the Strip-Liouville Principle (Definition 627), proved at positive inverse temperature via an \(i\beta\)-periodic entire extension (Theorem 628) and Liouville’s theorem (Theorem 629), yields that KMS states are automatically invariant under the time evolution (Theorem 630); uniqueness on the strip from boundary values (Theorem 631) gives uniqueness of the analytic completion of a KMS correlation function (Theorem 632).
§10.6.15 KMS States for the Covariance Flow (p. 329, items 633–637). A one-parameter subgroup of the inhomogeneous Lorentz group induces a one-parameter automorphism group on the quasilocal algebra via the covariance lift (Definition 633, Lemma 634); KMS states for that flow are defined accordingly (Definition 635) and shown convex (Theorem 636). The zero-temperature (\(\beta \to \infty\)) counterpart—a ground state for a covariance flow, whose GNS-implementing unitary group has positive energy—is recorded alongside it (Definition 637).

Where the Lean lives: Physicslib4/AQFT/HaagKastler/, Physicslib4/GNS/ (Irreducibility, Superselection, RadonNikodym, ExtremeState, …), Physicslib4/Operators/ (ReducingSubspace, DensityTheorem), Physicslib4/AQFT/KMS.lean, Physicslib4/Analysis/StripPeriodicExtension.lean

Items

Each blueprint subsection below is collapsed; click a heading to see its items. Every entry links to its node in the web blueprint and names the principal Lean declaration.

§10.6 The axioms (p. 289) — 2 items

Definition 476 — Axiom 1: Local Algebras · Physicslib4.AQFT.HaagKastler.LocalNet
Definition 477 — Axiom 2: Isotony · Physicslib4.AQFT.HaagKastler.Isotony

§10.6.1 The Quasilocal Colimit (p. 291) — 27 items

Lemma 478 — Alexandrov Diamonds are Directed under Inclusion · Physicslib4.AQFT.HaagKastler.Diamond (+2 more)
Lemma 479 — The Isotony Family is a Directed System · Physicslib4.AQFT.HaagKastler.transitionHom (+1 more)
Lemma 480 — The Colimit Norm is Well Defined · Physicslib4.AQFT.HaagKastler.QuasilocalColimit (+3 more)
Lemma 481 — Common Representatives for Two Colimit Elements · Physicslib4.AQFT.HaagKastler.exists_common_representatives
Lemma 482 — The Colimit Norm is a Ring Norm and a Normed-Space Norm · Physicslib4.AQFT.HaagKastler.instNonemptyDiamond (+3 more)
Lemma 483 — The Quasilocal Union is a Normed *-Algebra · Physicslib4.AQFT.HaagKastler.norm_eq_colimitNorm (+1 more)
Lemma 484 — The Colimit Satisfies the C*-Inequality · Physicslib4.AQFT.HaagKastler.colimitCStarRing
Definition 485 — Standing Hypotheses for the Completion Results · Physicslib4.CStarCompletion
Definition 486 — The Involution on a Completion · Physicslib4.instStarCompletion (+1 more)
Lemma 487 — The Involution Extends to the Completion · Physicslib4.instStarRingCompletion (+1 more)
Lemma 488 — The Completion Coercion as a Bundled *-Algebra Homomorphism · Physicslib4.coeStarAlgHom
Lemma 489 — The C*-Inequality Passes to the Completion · Physicslib4.instCStarRingCompletion
Lemma 490 — The Completion is a Normed \(\mathbb{C}\)-Algebra · Physicslib4.instNormedAlgebraCompletion
Lemma 491 — The Completion of a C*-Normed *-Algebra is a C*-Algebra · Physicslib4.instCStarAlgebraCompletion
Lemma 492 — The Completion of the Quasilocal Colimit is a C*-Algebra · Physicslib4.AQFT.HaagKastler.QuasilocalCompletion (+1 more)
Definition 493 — Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra
Definition 494 — Axiom 3: Local Commutativity · Physicslib4.AQFT.HaagKastler.LocalCommutativity
Lemma 495 — Local Commutativity Holds in Every Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.LocalCommutativity.commute_ι (+1 more)
Lemma 496 — Local Commutativity in the Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.localCommutativity_iff_exists_commute_ι
Definition 497 — Quasilocal Observable · Physicslib4.AQFT.HaagKastler.IsQuasilocalObservable (+1 more)
Definition 498 — Axiom 4: Quasilocal Completeness · Physicslib4.AQFT.HaagKastler.ObservableCorrespondence
Theorem 499 — Existence of a Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.exists_quasilocalAlgebra
Lemma 500 — The Canonical Embeddings into the Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.colimitStarOf (+1 more)
Lemma 501 — The Canonical Embeddings are Injective · Physicslib4.AQFT.HaagKastler.quasilocalEmbedding_injective
Lemma 502 — The Canonical Embeddings Form a Cocone · Physicslib4.AQFT.HaagKastler.quasilocalEmbedding_transitionHom
Lemma 503 — The Colimit is the Union of the Images of its Insertions · Physicslib4.AQFT.HaagKastler.exists_eq_colimitStarOf
Lemma 504 — The Images of the Canonical Embeddings are Dense · Physicslib4.AQFT.HaagKastler.dense_iUnion_range_quasilocalEmbedding

§10.6.2 The von Neumann Density Theorem (p. 306) — 11 items

Lemma 505 — Reducing Subspaces Give Commuting Projections · Physicslib4.commute_starProjection_of_invariant
Lemma 506 — Cyclic Subspaces Reduce the Representation · Physicslib4.starProjection_cyclic_mem_centralizer
Lemma 507 — The Bicommutant on a Single Vector · Physicslib4.apply_mem_closure_of_mem_bicommutant
Definition 508 — Finite Amplification · Physicslib4.diagAmplification (+2 more)
Lemma 509 — The Finite Amplification is a Unital *-Homomorphism · Physicslib4.diagAmplification
Lemma 510 — Block Entries of the Amplified Commutant · Physicslib4.blockEntry_mem_centralizer
Lemma 511 — Block Expansion on the Amplified Space · Physicslib4.apply_eq_sum_blockEntry
Lemma 512 — Diagonal Operators in the Amplified Bicommutant · Physicslib4.ampDiag_mem_bicommutant
Lemma 513 — The Bicommutant on Finitely Many Vectors · Physicslib4.exists_forall_norm_sub_lt_of_mem_bicommutant
Lemma 514 — A Neighbourhood Basis for the Strong Operator Topology · Physicslib4.AQFT.HaagKastler.hasBasis_nhds_ofFun
Theorem 515 — Quasilocal Observables are Strongly Dense in the Bicommutant · Physicslib4.AQFT.HaagKastler.dense_range_in_bicommutant — the von Neumann density theorem, proved locally from the lemmas above (see Formalisation status)

§10.6.3 Lorentz Covariance and the Haag–Kastler Net (p. 308) — 2 items

Definition 516 — Axiom 5: Lorentz Covariance · Physicslib4.AQFT.HaagKastler.LorentzCovariance
Definition 517 — Haag–Kastler Net · Physicslib4.AQFT.HaagKastler.HaagKastlerNet

§10.6.4 Einstein Causality (p. 309) — 1 item

Theorem 518 — Einstein Causality in a Representation · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.einstein_causality (+1 more)

§10.6.5 Local von Neumann Algebras (p. 310) — 13 items

Definition 519 — Local von Neumann Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localOperators (+1 more)
Lemma 520 — The Bicommutant of a Self-Adjoint Set is a von Neumann Algebra · Physicslib4.GNS.vonNeumannOfSelfAdjoint
Definition 521 — \(R(\mathbf{B})\) as a von Neumann Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra
Theorem 522 — Microcausality at the von Neumann Level · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_subset_centralizer
Theorem 523 — Isotony of the von Neumann Net · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_mono
Theorem 524 — Bundled von Neumann Microcausality and Isotony · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant (+1 more)
Definition 525 — The Net of von Neumann Algebras · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.vonNeumannNet
Theorem 526 — Statistical Independence (Schlieder Property) · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_separating (+1 more)
Theorem 527 — Statistical Independence, bundled · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_separating
Theorem 528 — Additive-Free Locality via the Spacelike Complement · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannAlgebra_le_commutant_of_subset_spacelikeComplement
Theorem 529 — Geometric Covariance of the von Neumann Net · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.lieConj_image_localVonNeumann (+1 more)
Theorem 530 — Orbit-Invariance of Factoriality · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumann_isFactor_smul
Theorem 531 — Geometric Covariance as a von Neumann Algebra Isomorphism · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.localVonNeumannEquiv

§10.6.6 Relative Commutants of Nested Local Algebras (p. 312) — 8 items

Definition 532 — Relative Commutant of a Nested Pair · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.relativeCommutant
Theorem 533 — Antitonicity of the Commutant · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.commutant_le_commutant_of_le
Theorem 534 — Relative Commutant Lies in the Larger Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.relativeCommutant_le_right
Theorem 535 — Relative Commutant Commutes with the Smaller Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.relativeCommutant_coe_subset_commutant
Theorem 536 — Relative Commutant Contains the Centre · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.center_le_relativeCommutant
Definition 537 — Irreducible Inclusion · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsIrreducibleInclusion
Theorem 538 — An Irreducible Inclusion has Factor Ambient · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isFactor_of_isIrreducibleInclusion
Theorem 539 — Self-Inclusion is Irreducible iff Factor · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isIrreducibleInclusion_self_iff_isFactor

§10.6.7 Irreducibility and Schur's Lemma (p. 313) — 23 items

Definition 540 — Irreducible Representation · Physicslib4.GNS.IsIrreducible
Theorem 541 — Topological Schur Lemma · Physicslib4.GNS.eq_smul_one_of_commute_of_cyclic
Theorem 542 — Commutant Scalar iff Proportional Coefficient · Physicslib4.GNS.isScalar_iff_coeff_proportional
Definition 543 — Pure State · Physicslib4.GNS.IsPure
Theorem 544 — Pure Implies Irreducible · Physicslib4.GNS.isIrreducible_of_isPure
Theorem 545 — The GNS Radon–Nikodym Form is Bounded · Physicslib4.GNS.gns_form_norm_le (+1 more)
Theorem 546 — The GNS Radon–Nikodym Operator · Physicslib4.GNS.rnOp (+3 more)
Theorem 547 — Pure \(\iff\) Irreducible · Physicslib4.GNS.isPure_iff_isIrreducible
Theorem 548 — An Irreducible Representation Generates a Factor · Physicslib4.GNS.center_gnsVonNeumann_eq_of_isIrreducible (+1 more)
Theorem 549 — Irreducibility \(\iff\) Generating \(\mathcal{B}(H)\) · Physicslib4.GNS.isIrreducible_iff_gnsVonNeumann_eq_univ (+1 more)
Theorem 550 — Bundled Density Form of Irreducibility · Physicslib4.GNS.coe_gnsVonNeumannAlgebra_eq_univ_of_isIrreducible (+1 more)
Theorem 551 — The GNS Representation of a Pure State is a Factor · Physicslib4.GNS.exists_gns_factor_of_isPure
Theorem 552 — The GNS Representation of a Pure State Generates \(\mathcal{B}(H)\) · Physicslib4.GNS.exists_gns_generates_all_of_isPure
Theorem 553 — Norm of a Positive Functional · Physicslib4.GNS.norm_eq_re_apply_one_of_positive
Definition 554 — Extreme Point of the State Space · Physicslib4.GNS.State.IsExtremePoint
Theorem 555 — Pure \(\iff\) Extreme Point · Physicslib4.GNS.isPure_iff_isExtremePoint
Theorem 556 — State-Space Convexity and the Extreme-Point Bridge · Physicslib4.GNS.convex_stateSpace (+1 more)
Definition 557 — Pullback of a State · Physicslib4.GNS.State.comp
Theorem 558 — Functoriality of the State Pullback · Physicslib4.GNS.State.comp_id (+1 more)
Theorem 559 — Purity is Invariant under a *-Isomorphism · Physicslib4.GNS.isPure_comp_iff
Theorem 560 — Weak-* Compactness of the State Space · Physicslib4.GNS.isCompact_weakStateSet
Theorem 561 — Pure \(\iff\) Extreme Point on the Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.pure_iff_extreme
Theorem 562 — Pure \(\iff\) Irreducible GNS on the Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.exists_gns_pure_iff_irreducible

§10.6.8 Unitary Equivalence and Superselection (p. 317) — 2 items

Definition 563 — Unitary Equivalence of Representations · Physicslib4.GNS.UnitaryEquiv
Theorem 564 — Irreducibility and Factoriality are Unitary Invariants · Physicslib4.GNS.UnitaryEquiv.isIrreducible_iff (+1 more)

§10.6.9 GNS Covariance (p. 317) — 6 items

Lemma 565 — Cyclicity pulls back along a surjective *-homomorphism · Physicslib4.GNS.isCyclicVector_comp_of_surjective
Theorem 566 — GNS covariance under a *-isomorphism · Physicslib4.GNS.exists_unitary_of_gns_comp
Theorem 567 — The GNS representation of a pullback state · Physicslib4.GNS.unitaryEquiv_comp_of_gns
Lemma 568 — Pullback along a surjection preserves the image algebra · Physicslib4.GNS.range_comp_of_surjective (+2 more)
Theorem 569 — Superselection type transports along a *-isomorphism · Physicslib4.GNS.isIrreducible_iff_of_gns_comp (+1 more)
Theorem 570 — GNS covariance for local algebras · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.unitaryEquiv_gns_covEquiv (+2 more)

§10.6.10 Disjointness and Quasi-Equivalence (p. 319) — 18 items

Definition 571 — Disjoint Representations · Physicslib4.GNS.AreDisjoint (+2 more)
Definition 572 — Quasi-Equivalence of Representations · Physicslib4.GNS.QuasiEquiv (+1 more)
Theorem 573 — Schur’s Lemma and the Irreducible Dichotomy · Physicslib4.GNS.UnitaryEquiv.of_intertwines_of_isIrreducible (+1 more)
Lemma 574 — Schur Multiplicity · Physicslib4.GNS.eq_smul_of_intertwines_of_isIrreducible
Lemma 575 — Endomorphism Algebra of an Irreducible Representation · Physicslib4.GNS.intertwines_self_iff_isScalar
Theorem 576 — The commutant (self-intertwiner) von Neumann algebra · Physicslib4.GNS.commutantVonNeumann (+2 more)
Theorem 577 — Double-Commutant Duality · Physicslib4.GNS.commutant_gnsVonNeumannAlgebra (+1 more)
Theorem 578 — A Factor and its Commutant; Triviality Duality · Physicslib4.GNS.isFactor_gnsVonNeumann_iff_isFactor_commutant (+1 more)
Lemma 579 — Abelian \(\iff\) Self-Commuting · Physicslib4.GNS.isAbelian_iff_le_commutant
Definition 580 — Centre of a von Neumann algebra · Physicslib4.GNS.vonNeumannCenter
Lemma 581 — The centre is a von Neumann algebra · Physicslib4.GNS.bicommutant_inter_commutant_eq
Lemma 582 — The intersection of two von Neumann algebras is a von Neumann algebra · Physicslib4.GNS.bicommutant_inter_eq
Theorem 583 — The centre of a von Neumann algebra is abelian · Physicslib4.GNS.vonNeumannCenter_isAbelian
Lemma 584 — \(R\) is abelian iff it equals its centre · Physicslib4.GNS.vonNeumannCenter_eq_self_iff_isAbelian
Theorem 585 — A factor is abelian iff it is the scalars · Physicslib4.GNS.isAbelian_iff_eq_scalars_of_isFactor
Theorem 586 — A von Neumann algebra and its commutant share a centre · Physicslib4.GNS.vonNeumannCenter_eq_commutant
Theorem 587 — A von Neumann algebra is a factor iff its centre is the scalars · Physicslib4.GNS.isFactor_iff_center_eq_scalars
Theorem 588 — The Pure-State Dichotomy · Physicslib4.GNS.exists_gns_areDisjoint_or_unitaryEquiv_of_isPure

§10.6.11 Direct Sums, Amplification, and Reducibility (p. 322) — 4 items

Definition 589 — Direct-Sum Representation · Physicslib4.GNS.directSum
Theorem 590 — Subrepresentations and Commutant of a Direct Sum · Physicslib4.GNS.intertwines_single (+1 more)
Definition 591 — Amplification · Physicslib4.GNS.amplification
Theorem 592 — Reducibility of a Direct Sum · Physicslib4.GNS.not_isIrreducible_directSum

§10.6.12 Covariant States and the Covariance Action (p. 322) — 29 items

Definition 593 — Covariant Family of Local States · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily
Lemma 594 — Composition of Covariance · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsCovariantFamily.comp
Definition 595 — Quasilocal Covariance Automorphism · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift
Lemma 596 — Uniqueness of the Quasilocal Lift · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.QuasilocalLift.unique
Lemma 597 — Every Quasilocal Algebra is Covariance-Compatible · Physicslib4.AQFT.HaagKastler.isCovariantQuasilocal
Theorem 598 — Existence of the Quasilocal Lift · Physicslib4.AQFT.HaagKastler.nonempty_quasilocalLift
Theorem 599 — Existence for the Trivial Net · Physicslib4.AQFT.HaagKastler.nonempty_trivialQuasilocalLift
Definition 600 — Covariant Quasilocal Algebra · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.action
Lemma 601 — Group-Action Coherence of the Covariance Automorphism · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.action_one (+1 more)
Definition 602 — Invariant State · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsInvariantState
Theorem 603 — GNS Unitary Implementation of an Invariant State · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsInvariantState.exists_gns_unitary (+1 more)
Lemma 604 — Weak Continuity Implies Strong Continuity · Physicslib4.strongContinuous_of_weak
Theorem 605 — Strongly Continuous GNS Unitary of an Invariant State · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsInvariantState.exists_gns_unitary_strongContinuous (+1 more)
Theorem 606 — Irreducible Covariant Representation of a Pure Invariant State · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsInvariantState.exists_gns_irreducible_covariant
Definition 607 — Positive Energy · Physicslib4.AQFT.IsPositiveEnergy
Lemma 608 — The Trivial Group has Positive Energy · Physicslib4.AQFT.isPositiveEnergy_const_refl
Lemma 609 — Uniqueness of the Generator · Physicslib4.AQFT.generator_eq_of_eq_expUnitary
Lemma 610 — Unitary Conjugation Preserves Positivity · Physicslib4.Spectral.Unbounded.IsPositive.of_conj
Lemma 611 — Positive Energy is Unitarily Invariant · Physicslib4.AQFT.IsPositiveEnergy.conj
Lemma 612 — A Positive-Energy Group is Strongly Continuous · Physicslib4.AQFT.IsPositiveEnergy.strongContinuous
Lemma 613 — The Bounded Case · Physicslib4.AQFT.isPositiveEnergy_exp
Theorem 614 — Positive Energy in Exponential Form · Physicslib4.AQFT.isPositiveEnergy_iff_exists_exp
Theorem 615 — Properties of Positive Energy · Physicslib4.AQFT.isPositiveEnergy_const_refl (+5 more)
Definition 616 — Vacuum State · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumState
Theorem 617 — Consequences of Invariance for a Vacuum State · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumState.invariant (+1 more)
Definition 618 — Future-Timelike Translation Subgroup · Physicslib4.AQFT.HaagKastler.translationSub (+3 more)
Definition 619 — Vacuum State with the Concrete Spectrum Condition · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsVacuumStateConcrete
Theorem 620 — Purity is Covariance-Invariant · Physicslib4.GNS.isPure_precomp_iff (+1 more)
Theorem 621 — GNS covariance along the quasilocal action · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.unitaryEquiv_gns_action (+2 more)

§10.6.13 The Separating Vector of a Faithful State (p. 328) — 1 item

Theorem 622 — Separating Vector of a Faithful State · Physicslib4.GNS.separating_of_faithful (+1 more)

§10.6.14 The KMS Condition and Thermal Equilibrium (p. 328) — 10 items

Definition 623 — One-Parameter Automorphism Group · Physicslib4.AQFT.IsOneParameterAut
Definition 624 — KMS State · Physicslib4.AQFT.IsKMSState
Theorem 625 — The KMS State Set is Convex · Physicslib4.AQFT.IsKMSState.convexCombo
Lemma 626 — Boundary Coincidence for \(a = 1\) · Physicslib4.AQFT.IsKMSState.correlationOne
Definition 627 — Strip-Liouville Principle · Physicslib4.AQFT.StripLiouville
Theorem 628 — \(i\beta\)-Periodic Entire Extension (Strip Schwarz Reflection) · Physicslib4.exists_bounded_entire_extension_of_strip_periodic
Theorem 629 — Strip-Liouville Holds for \(\beta > 0\) · Physicslib4.AQFT.stripLiouville_of_pos
Theorem 630 — KMS States are Invariant · Physicslib4.AQFT.IsKMSState.invariant_of_pos
Theorem 631 — Uniqueness on the Strip from Boundary Values · Physicslib4.eqOn_strip_of_eq_boundary
Theorem 632 — Uniqueness of the KMS Correlation Function · Physicslib4.AQFT.IsKMSState.correlation_eqOn

§10.6.15 KMS States for the Covariance Flow (p. 329) — 5 items

Definition 633 — Covariance-Flow Automorphism Family · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.flowAut
Lemma 634 — A Lorentz One-Parameter Subgroup Induces a One-Parameter Group · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isOneParameterAut_flowAut
Definition 635 — KMS State for the Covariance Flow · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsKMSStateForFlow
Theorem 636 — Convexity of the Covariance-Flow KMS States · Physicslib4.AQFT.HaagKastler.HaagKastlerNet.IsKMSStateForFlow.convexCombo
Definition 637 — Ground State for a Covariance Flow · Physicslib4.AQFT.HaagKastler.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.5 Spacetime · §10.7 Curved →