Physicslib4.AQFT.HaagKastler.Net

Haag-Kastler nets

This file bundles the data of Axiom 1 (def:local-algebras) together with the propositional content of Axioms 2, 3 and 5 into a single structure HaagKastlerNet, formalising the blueprint declaration def:haag-kastler-net (section 10.6 of the AQFT-in-Lean blueprint).

Main definitions

• Physicslib4.AQFT.HaagKastler.HaagKastlerNet: a structure consisting of a LocalNet (the Axiom 1 data) plus proofs of Isotony, LocalCommutativity and LorentzCovariance.

Supporting lemmas

• HaagKastlerNet.commute_ι_of_spacelike_symm: the symmetric restatement of commute_ι_of_spacelike.
• HaagKastlerNet.isQuasilocalObservable_of_isSelfAdjoint, HaagKastlerNet.isQuasilocalObservable_add, HaagKastlerNet.isQuasilocalObservable_smul, HaagKastlerNet.isQuasilocalObservable_smul_add_smul: membership and closure API for the net's quasilocal observables, under self-adjointness, addition, scaling, and real-linear combinations.

Notes

• The structure does not bundle Axiom 4. The existence of a quasilocal algebra is a theorem, exists_quasilocalAlgebra (thrm:quasilocal-algebra-exists), which builds the algebra from the net alone; HaagKastlerNet.quasilocal is defined from it. Axiom 4 proper (def:quasilocal-completeness) is a bridge principle relating physical observables to the formalism, with no mathematical consumers, and is encoded separately in Physicslib4/AQFT/HaagKastler/ObservableBridge.lean.

• The structure does not bundle Axiom 6 (Primitivity), which the sharpened axioms do not adopt.

structure Physicslib4.AQFT.HaagKastler.HaagKastlerNet : Type (u + 1)

A Haag–Kastler net on Minkowski spacetime: a net of local algebras satisfying Axioms 1, 2, 3 and 5.

The structure bundles the local algebras B ↦ 𝔘(B) of Axiom 1, the isotony family of Axiom 2, and proofs of local commutativity (Axiom 3) and Lorentz covariance (Axiom 5). Theorems about a theory take a HaagKastlerNet as hypothesis and use each axiom as a field.

Two things are not fields. The quasilocal algebra is constructed from the net, as HaagKastlerNet.quasilocal. Axiom 4, that every physical observable is a quasilocal observable, relates the formalism to the world rather than constraining the net; it is the separate structure ObservableCorrespondence. Primitivity, the sixth axiom of 1964, is not adopted. nonempty_haagKastlerNet shows that the axioms are consistent.

Blueprint: def:haag-kastler-net

• U : LocalNet

  The local algebras B ↦ 𝔘(B) (Axiom 1).

  Implementation note: the universe is named, as LocalNet.{u}, so that HaagKastlerNet takes it as a parameter and nets with algebras in any universe are allowed.

• isotony : Isotony self.U

  The isotony embeddings i(B₁, B₂) : 𝔘(B₁) → 𝔘(B₂) (Axiom 2).

• localCommutativity : LocalCommutativity self.U self.isotony

  Local commutativity (Axiom 3): for completely spacelike diamonds B₁, B₂ and every diamond B ⊇ B₁ ∪ B₂, the images of 𝔘(B₁) and 𝔘(B₂) in 𝔘(B) commute.

• lorentzCovariance : LorentzCovariance self.U self.isotony

  Lorentz covariance (Axiom 5): the identity component of the Poincaré group acts on the net, compatibly with isotony.

@[reducible, inline]

abbrev Physicslib4.AQFT.HaagKastler.HaagKastlerNet.algebra (N : HaagKastlerNet) (B : Set StandardMinkowskiSpacetime.Carrier) : Type u_1

The local algebra 𝔘(B) assigned by the net to a region B (the Axiom 1 data, via the underlying LocalNet).

Equations

• N.algebra B = N.U.algebra B

noncomputable def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.emptyEquivComplex (N : HaagKastlerNet) : N.algebra ∅ ≃⋆ₐ[ℂ] ℂ

Net-level normalisation 𝔘(∅) ≃⋆ₐ[ℂ] ℂ.

Equations

• N.emptyEquivComplex = N.U.emptyEquivComplex

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.mul_comm_algebra_empty (N : HaagKastlerNet) (a b : N.algebra ∅) : a * b = b * a

The empty-region algebra 𝔘(∅) is commutative.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.finrank_algebra_empty (N : HaagKastlerNet) : Module.finrank ℂ (N.algebra ∅) = 1

The empty-region algebra 𝔘(∅) is one-dimensional over ℂ.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isotony_refl (N : HaagKastlerNet) {B : Set StandardMinkowskiSpacetime.Carrier} : ∃ (φ : N.algebra B →⋆ₐ[ℂ] N.algebra B), Function.Injective ⇑φ

Isotony, reflexivity. Every Alexandrov-basis set embeds into itself via the identity unital *-monomorphism.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isotony_trans (N : HaagKastlerNet) ⦃B₁ B₂ B₃ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hB₃ : IsAlexandrovBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃) : ∃ (φ : N.algebra B₁ →⋆ₐ[ℂ] N.algebra B₃), Function.Injective ⇑φ

Isotony, transitivity. For inclusions B₁ ⊆ B₂ ⊆ B₃ of Alexandrov-basis sets, the net's isotony embeddings compose to a unital *-monomorphism 𝔘(B₁) ↪ 𝔘(B₃).

noncomputable def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.quasilocal (N : HaagKastlerNet) : QuasilocalAlgebra N.U N.isotony

The quasilocal algebra 𝔘 of the net, with its embeddings ι_B : 𝔘(B) → 𝔘.

The algebra is constructed, not assumed: exists_quasilocalAlgebra builds one from the local algebras and isotony alone, as the completion of their directed colimit, and this definition chooses it. Results about the net's quasilocal observables, representations and states are stated for this algebra.

Blueprint: thrm:quasilocal-algebra-exists

Equations

• N.quasilocal = Classical.choice ⋯

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.norm_ι (N : HaagKastlerNet) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) (a : N.algebra B) : ‖(N.quasilocal.ι hB) a‖ = ‖a‖

Each local algebra 𝔘(B) of an Alexandrov-basis set embeds norm-preservingly into the canonical quasilocal algebra 𝔘.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isometry_ι (N : HaagKastlerNet) {B : Set StandardMinkowskiSpacetime.Carrier} (hB : IsAlexandrovBasisSet B) : Isometry ⇑(N.quasilocal.ι hB)

Each local embedding 𝔘(B) ↪ 𝔘 into the canonical quasilocal algebra is an isometry (the metric form of norm_ι).

noncomputable def Physicslib4.AQFT.HaagKastler.HaagKastlerNet.covEquiv (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) : N.algebra B ≃⋆ₐ[ℂ] N.algebra (L • B)

The *-isomorphism α_L : 𝔘(B) → 𝔘(LB) by which a Poincaré transformation L acts on the net.

Axiom 5 (lorentzCovariance) asserts that such a family exists; this definition chooses one. covEquiv_one, covEquiv_mul and covEquiv_isotony restate the three conditions of the axiom for it.

Equations

• N.covEquiv L B = Exists.choose ⋯ L B

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.finrank_algebra_smul (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) : Module.finrank ℂ (N.algebra B) = Module.finrank ℂ (N.algebra (L • B))

Lorentz invariance of the local dimension. The local algebras of a region B and of its Lorentz translate L·B have the same ℂ-dimension: the covariance equivalence is in particular a ℂ-linear isomorphism 𝔘(B) ≃ₗ[ℂ] 𝔘(L·B).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.norm_covEquiv (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) {B : Set StandardMinkowskiSpacetime.Carrier} (a : N.algebra B) : ‖(N.covEquiv L B) a‖ = ‖a‖

Lorentz invariance of the local norm. The covariance equivalence is a *-isomorphism of C*-algebras, hence isometric: ‖α a‖ = ‖a‖.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.commute_covEquiv_iff (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) {B : Set StandardMinkowskiSpacetime.Carrier} (a b : N.algebra B) : Commute ((N.covEquiv L B) a) ((N.covEquiv L B) b) ↔ Commute a b

Lorentz transport of commutativity. Two local elements commute iff their images under the covariance equivalence commute.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.covEquiv_one (N : HaagKastlerNet) (B : Set StandardMinkowskiSpacetime.Carrier) (a : N.algebra B) : (N.covEquiv 1 B) a = ⋯.mp a

Covariance, identity. The action of the identity Lorentz transformation is the identity automorphism (modulo the canonical identification 𝔘(B) = 𝔘(1·B) from one_smul).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.covEquiv_mul (N : HaagKastlerNet) (L L' : InhomogeneousLorentzGroup) (B : Set StandardMinkowskiSpacetime.Carrier) (a : N.algebra B) : (N.covEquiv (L' * L) B) a = ⋯.mp ((N.covEquiv L' (L • B)) ((N.covEquiv L B) a))

Covariance, composition. The action is multiplicative in the group element: α (L'·L) = α L' ∘ α L (modulo the canonical identification 𝔘((L'·L)·B) = 𝔘(L'·(L·B)) from mul_smul).

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.covEquiv_isotony (N : HaagKastlerNet) (L : InhomogeneousLorentzGroup) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂) (a : N.algebra B₁) : (N.covEquiv L B₂) ((N.isotony.map hB₁ hB₂ h) a) = (N.isotony.map ⋯ ⋯ ⋯) ((N.covEquiv L B₁) a)

Covariance commutes with isotony (Axiom 5 (3)): the covariance equivalences intertwine the Axiom 2 isotony embeddings, α_L ∘ i_{B₁B₂} = i_{L·B₁, L·B₂} ∘ α_L.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.commute_ι_of_spacelike (N : HaagKastlerNet) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : N.algebra B₁) (b : N.algebra B₂) : Commute ((N.quasilocal.ι hB₁) a) ((N.quasilocal.ι hB₂) b)

Local commutativity. The images in the canonical quasilocal algebra quasilocal of two completely-spacelike basis algebras commute. Axiom 3 asserts commutation in a common containing local algebra; LocalCommutativity.commute_ι transfers it to every quasilocal algebra.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.commute_ι_of_spacelike_symm (N : HaagKastlerNet) ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄ (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂) (hs : StandardMinkowskiSpacetime.IsCompletelySpacelike standardMinkowskiTimeOrientation B₁ B₂) (a : N.algebra B₁) (b : N.algebra B₂) : Commute ((N.quasilocal.ι hB₂) b) ((N.quasilocal.ι hB₁) a)

Local commutativity is symmetric. Commutation of completely-spacelike local algebras holds in either order.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isQuasilocalObservable_iff (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {T : H →L[ℂ] H} : IsQuasilocalObservable N.quasilocal π T ↔ IsSelfAdjoint T ∧ T ∈ Set.range ⇑π

Characterisation of the net's quasilocal observables. An operator on the GNS Hilbert space is a quasilocal observable iff it is self-adjoint and lies in the range of the representation π of the canonical quasilocal algebra.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isQuasilocalObservable_of_isSelfAdjoint (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) (T : H →L[ℂ] H) (hT : IsSelfAdjoint T) (hmem : T ∈ Set.range ⇑π) : IsQuasilocalObservable N.quasilocal π T

Every self-adjoint operator in the range of π is a quasilocal observable of the net.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isQuasilocalObservable_one (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) : IsQuasilocalObservable N.quasilocal π 1

The identity operator is a quasilocal observable of the net.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isQuasilocalObservable_add (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {S T : H →L[ℂ] H} (hS : IsQuasilocalObservable N.quasilocal π S) (hT : IsQuasilocalObservable N.quasilocal π T) : IsQuasilocalObservable N.quasilocal π (S + T)

The net's quasilocal observables are closed under addition.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isQuasilocalObservable_smul (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {c : ℂ} {T : H →L[ℂ] H} (hT : IsQuasilocalObservable N.quasilocal π T) (hc : IsSelfAdjoint c) : IsQuasilocalObservable N.quasilocal π (c • T)

The net's quasilocal observables are closed under scaling by a self-adjoint (i.e. real) complex scalar.

theorem Physicslib4.AQFT.HaagKastler.HaagKastlerNet.isQuasilocalObservable_smul_add_smul (N : HaagKastlerNet) {H : Type u_1} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] (π : N.quasilocal.carrier →⋆ₐ[ℂ] H →L[ℂ] H) {c d : ℂ} {S T : H →L[ℂ] H} (hc : IsSelfAdjoint c) (hd : IsSelfAdjoint d) (hS : IsQuasilocalObservable N.quasilocal π S) (hT : IsQuasilocalObservable N.quasilocal π T) : IsQuasilocalObservable N.quasilocal π (c • S + d • T)

Real-linear combinations of the net's quasilocal observables are quasilocal observables.

The trivial net and joint satisfiability of the axioms

The Haag-Kastler axioms are not vacuous: the trivial net, assigning the one-dimensional C*-algebra ℂ to every region, satisfies all of Axioms 1-5. This witnesses Nonempty HaagKastlerNet, i.e. the five axioms are jointly consistent.

noncomputable def Physicslib4.AQFT.HaagKastler.trivialLocalNet : LocalNet

The trivial local net: every region is assigned the C*-algebra ℂ, with the empty-region normalisation being the identity isomorphism.

Equations

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

def Physicslib4.AQFT.HaagKastler.trivialBasisSet : Set StandardMinkowskiSpacetime.Carrier

A concrete Alexandrov-basis set of standard Minkowski spacetime (I⁺(0) ∩ I⁻(0)), used as a witness that basis sets exist.

Equations

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

theorem Physicslib4.AQFT.HaagKastler.isAlexandrovBasisSet_trivialBasisSet : IsAlexandrovBasisSet trivialBasisSet

def Physicslib4.AQFT.HaagKastler.trivialLocalNetIsotony : Isotony trivialLocalNet

The trivial net's Axiom 2 data: every local algebra is ℂ and every inclusion is implemented by the identity, which is trivially functorial.

This must precede trivialQuasilocalAlgebra, which is indexed by it.

Equations

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

noncomputable def Physicslib4.AQFT.HaagKastler.trivialQuasilocalAlgebra : QuasilocalAlgebra trivialLocalNet trivialLocalNetIsotony

The trivial quasilocal algebra for the trivial net: ambient C*-algebra ℂ, with every local embedding the identity ℂ →⋆ₐ[ℂ] ℂ. The cocone condition ι_inclusion is stated against the Axiom 2 family trivialLocalNetIsotony.

Equations

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

theorem Physicslib4.AQFT.HaagKastler.trivialLocalNet_localCommutativity : LocalCommutativity trivialLocalNet trivialLocalNetIsotony

The trivial local net satisfies Axiom 3 (local commutativity), since ℂ is commutative.

theorem Physicslib4.AQFT.HaagKastler.trivialLocalNet_lorentzCovariance : LorentzCovariance trivialLocalNet trivialLocalNetIsotony

The trivial local net satisfies Axiom 5 (Lorentz covariance), realized by the identity automorphism of ℂ at every basis set.

noncomputable def Physicslib4.AQFT.HaagKastler.trivialHaagKastlerNet : HaagKastlerNet

The trivial Haag-Kastler net: the trivial local net (every region ↦ ℂ) bundled with proofs of Axioms 2-5.

Equations

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

theorem Physicslib4.AQFT.HaagKastler.nonempty_haagKastlerNet : Nonempty HaagKastlerNet

The Haag-Kastler axioms are jointly satisfiable. The trivial net (every region ↦ ℂ) is a Haag-Kastler net, so HaagKastlerNet is nonempty.

Stated at universe 0 because the witness is built from ℂ, which lives in Type. Consistency of the axioms needs only one model, so nothing is lost; the library gives no witness in other universes.