Polish

Physicslib4/AQFT/HaagKastler/LorentzCovariance.lean

@@ -39,6 +39,13 @@ axioms, section 10.6 of the AQFT-in-Lean blueprint):
   `Physicslib4/Spacetime/LorentzCausality.lean`, which proves that the action preserves
   Alexandrov basis sets (`isAlexandrovBasisSet_smul`).
 
+## Supporting lemmas
+
+* `InhomogeneousLorentzGroup.timelike_separated_smul_iff`,
+  `InhomogeneousLorentzGroup.spacelike_separated_smul_iff`,
+  `InhomogeneousLorentzGroup.null_separated_smul_iff`: Lorentz invariance of the sign of the
+  Minkowski interval, one lemma per causal class.
+
 ## Modelling notes
 
 * The Lorentz-action data is given as: a group `InhomogeneousLorentzGroup`,

Physicslib4/AQFT/HaagKastler/Net.lean

@@ -25,6 +25,17 @@ blueprint).
   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

Physicslib4/AQFT/HaagKastler/QuasilocalObservable.lean

@@ -25,6 +25,14 @@ quasilocal observables of a representation.
   those operators, shown to be exactly the self-adjoint elements in
   the range of `π`.
 
+## Supporting lemmas
+
+* `quasilocalObservables_eq`: set-builder characterisation of `quasilocalObservables`,
+  mirroring `isQuasilocalObservable_iff`.
+* `one_mem_quasilocalObservables`, `add_mem_quasilocalObservables`,
+  `smul_mem_quasilocalObservables`: membership API showing `quasilocalObservables` contains
+  the identity and is closed under addition and (self-adjoint) scaling.
+
 ## Note on the file name, and on Axiom 4
 
 Despite its name, this file does not formalise Axiom 4. The existence of a

Physicslib4/AQFT/HaagKastlerCurved/EinsteinCausality.lean

@@ -34,7 +34,9 @@ namespace HaagKastlerNet
 open Physicslib4.GNS
 open scoped InnerProductSpace
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+universe u v
+
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- **Einstein causality in a representation (curved spacetime).** For any
 `*`-representation `π` of a containing basis algebra `𝔘(B)`, the images of the
@@ -57,7 +59,7 @@ reproducing `ω` in which the local observables of completely spacelike-separate
 subregions commute as operators on `H`. -/
 theorem exists_gns_einstein_causality {B : Set M.Carrier} (hB : M.IsBasisSet B)
     (ω : State (N.algebra B)) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧

Physicslib4/AQFT/HaagKastlerCurved/GeneralCovariance.lean

@@ -158,6 +158,9 @@ Quantifying over *all* Lorentzian spacetimes, rather than over the metrics on
 one fixed carrier, is what makes general covariance a statement about the
 theory: the pullback of any `L` is again an object of the same family, so both
 sides of the equivalence are always in scope.
+
+The nets of a net theory share one universe for their local algebras, the
+universe parameter of `NetTheory`.
 -/
 abbrev NetTheory :=
   ∀ L : Spacetime.LorentzianSpacetime, HaagKastlerNet L.toAbstractIdentityComponent

Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean

@@ -48,9 +48,13 @@ theorem isometricCovariance_trivial_identityComponent (L : LorentzianSpacetime)
   Physicslib4.AQFT.HaagKastlerCurved.trivialLocalNet_isometricCovariance _
 
 /-- Over the concrete spacetime (with the identity-component isometry group),
-the full set of curved-spacetime Haag-Kastler axioms is jointly satisfiable. -/
+the full set of curved-spacetime Haag-Kastler axioms is jointly satisfiable.
+
+The witness is the trivial net, whose algebras are `ℂ`, so the net is stated
+with its algebras in universe `0` (as in
+`Physicslib4.AQFT.HaagKastlerCurved.nonempty_haagKastlerNet`). -/
 theorem nonempty_haagKastlerNet_identityComponent (L : LorentzianSpacetime) :
-    Nonempty (Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet
+    Nonempty (Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.{_, 0}
       L.toAbstractIdentityComponent) :=
   Physicslib4.AQFT.HaagKastlerCurved.nonempty_haagKastlerNet _
 

Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebra.lean

@@ -31,6 +31,14 @@ AQFT-in-Lean blueprint):
 * `Physicslib4.AQFT.HaagKastlerCurved.LocalAlgebra` (Axiom 4,
   `def:local-completeness-in-curved-spacetime`).
 
+## Supporting lemmas
+
+* `localObservables_eq`: set-builder characterisation of `localObservables`, the
+  curved mirror of `quasilocalObservables_eq`.
+* `one_mem_localObservables`, `add_mem_localObservables`, `smul_mem_localObservables`:
+  membership API showing `localObservables` contains the identity and is closed
+  under addition and scaling.
+
 ## Modelling notes
 
 * On a generic Lorentzian spacetime there is **no** quasilocal
@@ -55,7 +63,9 @@ namespace HaagKastlerCurved
 
 open Physicslib4 Physicslib4.GNS
 
-variable {M : LorentzianSpacetime}
+universe u v
+
+variable {M : LorentzianSpacetime.{u}}
 
 /--
 **Local Observable** (blueprint `def:local-observable`).
@@ -71,15 +81,15 @@ local algebra.
 Blueprint reference: `def:local-observable`.
 -/
 def IsLocalObservable {U : LocalNet M} {B : Set M.Carrier}
-    {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H) : Prop :=
   ∃ a : U.algebra B, IsSelfAdjoint a ∧ T = π a
 
 /-- Every local observable is self-adjoint: it is the image of a
 self-adjoint element of the local algebra under a `*`-homomorphism.
 This is the self-adjointness clause of `def:local-observable`. -/
 theorem IsLocalObservable.isSelfAdjoint {U : LocalNet M} {B : Set M.Carrier}
-    {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     {π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)} {T : H →L[ℂ] H}
     (hT : IsLocalObservable π T) : IsSelfAdjoint T := by
   obtain ⟨a, ha, rfl⟩ := hT
@@ -91,9 +101,9 @@ element `a` of it, the GNS construction provides a `*`-representation
 in which `π a` is a local observable. This is the existence content of
 `def:local-observable`, tying together `thrm:gns-construction-theorem`
 and `def:state`. -/
-theorem exists_isLocalObservable {U : LocalNet M} {B : Set M.Carrier}
+theorem exists_isLocalObservable {U : LocalNet.{u, v} M} {B : Set M.Carrier}
     (ω : State (U.algebra B)) {a : U.algebra B} (ha : IsSelfAdjoint a) :
-    ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
+    ∃ (H : Type v) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H)
       (_ : CompleteSpace H) (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)),
         IsLocalObservable π (π a) ∧ IsSelfAdjoint (π a) := by
   obtain ⟨H, hng, hip, hcs, π, _, _, _, _⟩ := gns_construction ω
@@ -110,11 +120,15 @@ This is the curved reading of "all observables are local
 observables": the observables of the theory are exactly the images
 of self-adjoint local elements.
 
+The Hilbert spaces `H` range over the universe `v` of the local
+algebras, which is the universe of the GNS spaces that
+`gns_construction` produces for them (as in the Minkowski net).
+
 Blueprint reference: `def:local-completeness-in-curved-spacetime`.
 -/
-def LocalAlgebra (U : LocalNet M) : Prop :=
+def LocalAlgebra (U : LocalNet.{u, v} M) : Prop :=
   ∀ ⦃B : Set M.Carrier⦄, M.IsBasisSet B →
-    ∀ {H : Type} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
+    ∀ {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
       (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (T : H →L[ℂ] H),
         IsSelfAdjoint T → T ∈ Set.range π → IsLocalObservable π T
 
@@ -136,7 +150,7 @@ theorem localAlgebra_of (U : LocalNet M) : LocalAlgebra U := by
 
 section Observables
 
-variable {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+variable {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
   [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   {π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)}
 
@@ -197,14 +211,14 @@ end Observables
 /-- The set of *local observables* on the GNS Hilbert space `H` for the
 representation `π`: all bounded operators of the form `π a` with `a` a
 self-adjoint element of the local algebra. -/
-def localObservables {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+def localObservables {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
     [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) : Set (H →L[ℂ] H) :=
   {T | IsLocalObservable π T}
 
 /-- The local observables are exactly the self-adjoint elements lying in the
 range of the representation `π`. -/
-theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
     [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
     (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) :
     localObservables π
@@ -215,7 +229,7 @@ theorem localObservables_eq {U : LocalNet M} {B : Set M.Carrier} {H : Type}
 
 section ObservablesSet
 
-variable {U : LocalNet M} {B : Set M.Carrier} {H : Type}
+variable {U : LocalNet M} {B : Set M.Carrier} {H : Type*}
   [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   (π : U.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
 

Physicslib4/AQFT/HaagKastlerCurved/LocalAlgebras.lean

@@ -35,13 +35,20 @@ Alexandrov-basis predicate replaced by the abstract interface
 `M : LorentzianSpacetime`. The empty-region normalisation
 `𝔘(∅) = ℂ · 1` is encoded by a `StarAlgEquiv` between the fiber over
 `∅` and `ℂ`.
+
+As in the Minkowski `LocalNet`, the local algebras are universe
+polymorphic: `LocalNet.{u, v} M` assigns algebras in `Type v` over a
+spacetime `M : LorentzianSpacetime.{u}`, with `v` independent of the
+carrier's universe `u`.
 -/
 
 namespace Physicslib4
 namespace AQFT
 namespace HaagKastlerCurved
 
-variable (M : LorentzianSpacetime)
+universe u v
+
+variable (M : LorentzianSpacetime.{u})
 
 /--
 **Axiom 1 (Local Algebras), curved spacetime.** The *data* of a
@@ -58,8 +65,9 @@ Blueprint reference: `def:local-algebras-in-curved-spacetime`.
 -/
 structure LocalNet where
   /-- The C*-algebra `𝔘(B)` assigned to a (would-be Alexandrov-basis)
-  region `B`. -/
-  algebra : Set M.Carrier → Type
+  region `B`. It lives in the universe `v`, independent of the
+  universe of `M.Carrier`. -/
+  algebra : Set M.Carrier → Type v
   /-- The `CStarAlgebra` instance on each fiber `𝔘(B)`. -/
   instCStarAlgebra : ∀ B, CStarAlgebra (algebra B)
   /-- Normalisation: `𝔘(∅) = ℂ · 1`, encoded as a `*`-algebra

Physicslib4/AQFT/HaagKastlerCurved/Net.lean

@@ -27,6 +27,19 @@ AQFT-in-Lean blueprint).
   `Isotony`, `LocalCommutativity`, `LocalAlgebra`, and
   `IsometricCovariance`.
 
+## Supporting lemmas
+
+* `commIsotony_injective`: restates `Isotony.injective` through the net's chosen
+  `commIsotony`.
+* `commute_of_spacelike_symm`: the symmetric restatement of `commute_of_spacelike`,
+  the curved mirror of `commute_ι_of_spacelike_symm`.
+* `isLocalObservable_of_isSelfAdjoint`, `isLocalObservable_add`,
+  `isLocalObservable_smul`, `isLocalObservable_smul_add_smul`: membership and
+  closure API for the net's local observables, the curved mirrors of the
+  quasilocal-observable API in `Physicslib4.AQFT.HaagKastler.Net`.
+* `trivialSpacetime`: the trivial Lorentzian spacetime underlying the joint
+  satisfiability witness mentioned above.
+
 ## Notes
 
 * As in the Minkowski case, joint satisfiability of the axioms is
@@ -40,17 +53,26 @@ namespace HaagKastlerCurved
 
 open scoped Pointwise
 
+universe u v
+
 /--
 A *Haag-Kastler net* on (the Alexandrov-basis sets of) a Lorentzian
 spacetime `M`: the data of Axiom 1
 (`def:local-algebras-in-curved-spacetime`) together with proofs of
 Axioms 2-5.
 
+`HaagKastlerNet.{u, v} M` has its spacetime `M` in universe `u` and its
+local algebras in universe `v`, independent of `u`.
+
 Blueprint reference: `def:haag-kastler-net-in-curved-spacetime`.
 -/
-structure HaagKastlerNet (M : LorentzianSpacetime) where
-  /-- The underlying assignment `B ↦ 𝔘(B)` (Axiom 1). -/
-  U : LocalNet M
+structure HaagKastlerNet (M : LorentzianSpacetime.{u}) where
+  /-- The underlying assignment `B ↦ 𝔘(B)` (Axiom 1).
+
+  Written `LocalNet.{u, v}` rather than `LocalNet` so that the universe `v`
+  of the local algebras is a parameter of this structure, as in the
+  Minkowski `HaagKastlerNet`. -/
+  U : LocalNet.{u, v} M
   /-- *Isotony*: the chosen functorial family of unital `*`-monomorphisms
   implementing inclusions of basis sets (Axiom 2). This is data, carrying the
   identity and composition laws. -/
@@ -69,7 +91,7 @@ structure HaagKastlerNet (M : LorentzianSpacetime) where
 
 namespace HaagKastlerNet
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} M)
 
 /-- The local algebra `𝔘(B)` assigned by the net to a region `B`
 (the Axiom 1 data, via the underlying `LocalNet M`). -/
@@ -248,7 +270,7 @@ theorem commute_of_spacelike_mono
 
 section Observables
 
-variable {B : Set M.Carrier} {H : Type}
+variable {B : Set M.Carrier} {H : Type v}
   [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
   (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H))
 
@@ -315,8 +337,10 @@ def trivialSpacetime : LorentzianSpacetime where
 
 /-- The *trivial local net* over **any** abstract Lorentzian spacetime: every
 region is assigned the C*-algebra `ℂ`, with the empty-region normalisation the
-identity isomorphism. -/
-noncomputable def trivialLocalNet (M : LorentzianSpacetime) : LocalNet M where
+identity isomorphism.
+
+Its algebras live in universe `0`, because `ℂ : Type`. -/
+noncomputable def trivialLocalNet (M : LorentzianSpacetime.{u}) : LocalNet.{u, 0} M where
   algebra := fun _ => ℂ
   instCStarAlgebra := fun _ => inferInstance
   emptyEquivComplex := StarAlgEquiv.refl ℂ ℂ
@@ -356,9 +380,9 @@ theorem trivialLocalNet_isometricCovariance (M : LorentzianSpacetime) :
   · intro _ _ _ _ _ _ _; rfl
 
 /-- The trivial net over any abstract Lorentzian spacetime, bundled as a
-Haag-Kastler net. -/
-noncomputable def trivialHaagKastlerNet (M : LorentzianSpacetime) :
-    HaagKastlerNet M where
+Haag-Kastler net, with its algebras in universe `0`. -/
+noncomputable def trivialHaagKastlerNet (M : LorentzianSpacetime.{u}) :
+    HaagKastlerNet.{u, 0} M where
   U := trivialLocalNet M
   isotony := trivialLocalNetIsotony M
   localCommutativity := trivialLocalNet_localCommutativity M
@@ -367,9 +391,15 @@ noncomputable def trivialHaagKastlerNet (M : LorentzianSpacetime) :
 
 /-- **The curved-spacetime Haag-Kastler axioms are jointly satisfiable over
 every Lorentzian spacetime.** The trivial net (every region ↦ `ℂ`) is a
-Haag-Kastler net. -/
-theorem nonempty_haagKastlerNet (M : LorentzianSpacetime) :
-    Nonempty (HaagKastlerNet M) :=
+Haag-Kastler net.
+
+Stated with the algebras in universe `0` because the witness is built from `ℂ`,
+which lives in `Type`. Consistency of the axioms needs only one model, so
+nothing is lost; a witness in an arbitrary universe would come from a `ULift`
+of this one. The same choice is made for the Minkowski
+`HaagKastler.nonempty_haagKastlerNet`. -/
+theorem nonempty_haagKastlerNet (M : LorentzianSpacetime.{u}) :
+    Nonempty (HaagKastlerNet.{u, 0} M) :=
   ⟨trivialHaagKastlerNet M⟩
 
 end HaagKastlerCurved

Physicslib4/AQFT/HaagKastlerCurved/Purity.lean

@@ -38,7 +38,9 @@ namespace HaagKastlerNet
 open Physicslib4.GNS
 open scoped InnerProductSpace Pointwise
 
-variable {M : LorentzianSpacetime} (N : HaagKastlerNet M)
+universe u v
+
+variable {M : LorentzianSpacetime.{u}} (N : HaagKastlerNet.{u, v} 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
@@ -54,7 +56,7 @@ 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)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
@@ -69,7 +71,7 @@ generated von Neumann algebra `π(𝔘(B))''` has trivial center (its center equ
 scalars). The abstract `GNS.exists_gns_factor_of_isPure` at the C*-algebra `𝔘(B)`. -/
 theorem exists_gns_factor_of_isPure {B : Set M.Carrier} {ω : State (N.algebra B)}
     (hpure : IsPure ω) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
@@ -84,7 +86,7 @@ von Neumann algebra is all of `𝓑(H)`: `π(𝔘(B))'' = 𝓑(H)`. The abstract
 `GNS.exists_gns_generates_all_of_isPure` at the C*-algebra `𝔘(B)`. -/
 theorem exists_gns_generates_all_of_isPure {B : Set M.Carrier} {ω : State (N.algebra B)}
     (hpure : IsPure ω) :
-    ∃ (H : Type)
+    ∃ (H : Type v)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧