Numina/aqft in lean

.github/workflows/lean_action_ci.yml

@@ -24,3 +24,15 @@ jobs:
           build: true
           lint: true
           mk_all-check: true
+
+      - name: Check declarations named in the blueprint exist
+        run: |
+          set -euo pipefail
+          grep -rho '\\lean{[^}]*}' blueprint/src --include='*.tex' \
+            | sed -e 's/^\\lean{//' -e 's/}$//' \
+            | tr ',' '\n' \
+            | sed -e 's/^[[:space:]]*//' -e 's/[[:space:]]*$//' \
+            | grep -v '^$' \
+            | sort -u > lean_decls.txt
+          echo "Checking $(wc -l < lean_decls.txt) declarations named in the blueprint."
+          ~/.elan/bin/lake exe checkdecls lean_decls.txt

.gitignore

@@ -1 +1,5 @@
 /.lake
+
+# Prover scratch copies: private per-declaration working files written by the
+# prover tooling. They duplicate real declarations in the same namespace.
+scratch_*

Physicslib4.lean

@@ -7,16 +7,20 @@ import Physicslib4.AQFT.HaagKastler.LocalCommutativity
 import Physicslib4.AQFT.HaagKastler.LocalVonNeumann
 import Physicslib4.AQFT.HaagKastler.LorentzCovariance
 import Physicslib4.AQFT.HaagKastler.Net
+import Physicslib4.AQFT.HaagKastler.ObservableBridge
 import Physicslib4.AQFT.HaagKastler.Purity
 import Physicslib4.AQFT.HaagKastler.QuasilocalAction
 import Physicslib4.AQFT.HaagKastler.QuasilocalAlgebra
-import Physicslib4.AQFT.HaagKastler.QuasilocalCompleteness
+import Physicslib4.AQFT.HaagKastler.QuasilocalColimit
+import Physicslib4.AQFT.HaagKastler.QuasilocalExistence
 import Physicslib4.AQFT.HaagKastler.QuasilocalIntertwiner
 import Physicslib4.AQFT.HaagKastler.QuasilocalKMS
+import Physicslib4.AQFT.HaagKastler.QuasilocalObservable
 import Physicslib4.AQFT.HaagKastler.VacuumState
 import Physicslib4.AQFT.HaagKastlerCurved.Concrete
 import Physicslib4.AQFT.HaagKastlerCurved.CovariantState
 import Physicslib4.AQFT.HaagKastlerCurved.EinsteinCausality
+import Physicslib4.AQFT.HaagKastlerCurved.GeneralCovariance
 import Physicslib4.AQFT.HaagKastlerCurved.GeometricCovariance
 import Physicslib4.AQFT.HaagKastlerCurved.IdentityComponent
 import Physicslib4.AQFT.HaagKastlerCurved.IsometricCovariance
@@ -32,6 +36,7 @@ import Physicslib4.AQFT.HaagKastlerCurved.StabilizerAction
 import Physicslib4.AQFT.HaagKastlerCurved.StabilizerKMS
 import Physicslib4.AQFT.KMS
 import Physicslib4.AQFT.PositiveEnergy
+import Physicslib4.Analysis.CStarCompletion
 import Physicslib4.Analysis.CStarDenseExtend
 import Physicslib4.Analysis.HorizontalLineRemovable
 import Physicslib4.Analysis.StripPeriodicExtension
@@ -41,6 +46,7 @@ import Physicslib4.GNS.Amplification
 import Physicslib4.GNS.Basic
 import Physicslib4.GNS.CauchySchwarz
 import Physicslib4.GNS.Construction
+import Physicslib4.GNS.Covariance
 import Physicslib4.GNS.DirectSum
 import Physicslib4.GNS.ExtremeState
 import Physicslib4.GNS.Irreducibility
@@ -57,7 +63,10 @@ import Physicslib4.Spacetime.Basic
 import Physicslib4.Spacetime.CausalComplement
 import Physicslib4.Spacetime.CausalStructure
 import Physicslib4.Spacetime.Causality
+import Physicslib4.Spacetime.CrossMetricIsometry
 import Physicslib4.Spacetime.Curves
+import Physicslib4.Spacetime.Diffeo
+import Physicslib4.Spacetime.DiffeoPath
 import Physicslib4.Spacetime.Isometry
 import Physicslib4.Spacetime.IsometryCausality
 import Physicslib4.Spacetime.IsometryTopology
@@ -67,4 +76,6 @@ import Physicslib4.Spacetime.LorentzCone
 import Physicslib4.Spacetime.LorentzOrthogonal
 import Physicslib4.Spacetime.LorentzianSpacetime
 import Physicslib4.Spacetime.Minkowski
+import Physicslib4.Spacetime.MinkowskiDilation
 import Physicslib4.Spacetime.MinkowskiDirected
+import Physicslib4.Spacetime.Pullback

Physicslib4/AQFT/HaagKastler/EinsteinCausality.lean

@@ -36,7 +36,9 @@ namespace HaagKastlerNet
 open Physicslib4.GNS
 open scoped InnerProductSpace
 
-variable (N : HaagKastlerNet)
+universe u
+
+variable (N : HaagKastlerNet.{u})
 
 /-- **Einstein causality in a representation.** For any `*`-representation `π` of
 the quasilocal algebra witnessing local commutativity, the images of the local
@@ -51,25 +53,25 @@ theorem einstein_causality
     (hs : Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime
       standardMinkowskiTimeOrientation B₁ B₂)
     (a : N.U.algebra B₁) (b : N.U.algebra B₂) :
-    Commute (π (N.commAlgebra.ι B₁ a)) (π (N.commAlgebra.ι B₂ b)) :=
+    Commute (π (N.commAlgebra.ι hB₁ a)) (π (N.commAlgebra.ι hB₂ b)) :=
   (N.commute_ι_of_spacelike hB₁ hB₂ hs a b).map π
 
 /-- **Einstein causality on a GNS Hilbert space.** For any state `ω` on the
 quasilocal algebra there is a GNS triple `(H, π, Ω)` reproducing `ω` in which the
 local observables of completely spacelike-separated regions commute as operators
 on `H`. -/
 theorem exists_gns_einstein_causality (ω : State N.commAlgebra.carrier) :
-    ∃ (H : Type)
+    ∃ (H : Type u)
       (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) (_ : CompleteSpace H)
       (π : N.commAlgebra.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H),
         IsCyclicVector π Ω ∧
         (∀ a : N.commAlgebra.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧
-        ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄,
-          IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ →
+        ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
+          (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂),
           Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime
             standardMinkowskiTimeOrientation B₁ B₂ →
           ∀ (a : N.U.algebra B₁) (b : N.U.algebra B₂),
-            Commute (π (N.commAlgebra.ι B₁ a)) (π (N.commAlgebra.ι B₂ b)) := by
+            Commute (π (N.commAlgebra.ι hB₁ a)) (π (N.commAlgebra.ι hB₂ b)) := by
   obtain ⟨H, i1, i2, i3, π, Ω, hcyc, hrep, _⟩ := gns_construction ω
   exact ⟨H, i1, i2, i3, π, Ω, hcyc, hrep,
     fun B₁ B₂ hB₁ hB₂ hs a b => N.einstein_causality π hB₁ hB₂ hs a b⟩

Physicslib4/AQFT/HaagKastler/GeometricCovariance.lean

@@ -61,15 +61,15 @@ variable {H : Type*} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteS
 quasilocal algebra of a covariant net: the image `π(ι_B(𝔘(B)))`. -/
 def covLocalOperators (C : CovariantQuasilocalAlgebra)
     (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
-    (B : Set StandardMinkowskiSpacetime.Carrier) : Set (H →L[ℂ] H) :=
-  Set.range fun a : C.net.U.algebra B => π (C.quasilocal.ι B a)
+    ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) : Set (H →L[ℂ] H) :=
+  Set.range fun a : C.net.U.algebra B => π (C.quasilocal.ι hB a)
 
 /-- The local von Neumann algebra `R(B) = π(ι_B(𝔘(B)))''` in a representation `π`
 of the covariant net's quasilocal algebra. -/
 def covLocalVonNeumann (C : CovariantQuasilocalAlgebra)
     (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
-    (B : Set StandardMinkowskiSpacetime.Carrier) : Set (H →L[ℂ] H) :=
-  Set.centralizer (Set.centralizer (C.covLocalOperators π B))
+    ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) : Set (H →L[ℂ] H) :=
+  Set.centralizer (Set.centralizer (C.covLocalOperators π hB))
 
 /-- **Conjugation carries the local operators of `B` onto those of `L · B`.**
 Given operator covariance `U π(a) U⁻¹ = π(β_L a)`, the conjugation `lieConj U`
@@ -80,7 +80,8 @@ theorem lieConj_image_covLocalOperators (C : CovariantQuasilocalAlgebra)
     (hB : IsAlexandrovBasisSet B)
     (hcov : ∀ (a : C.quasilocal.carrier) (x : H),
       Uop (π a (Uop.symm x)) = π (C.action L a) x) :
-    Physicslib4.lieConj Uop '' C.covLocalOperators π B = C.covLocalOperators π (L • B) := by
+    Physicslib4.lieConj Uop '' C.covLocalOperators π hB
+      = C.covLocalOperators π (isAlexandrovBasisSet_smul L hB) := by
   have hconj : ∀ a : C.quasilocal.carrier,
       Physicslib4.lieConj Uop (π a) = π (C.action L a) := by
     intro a
@@ -91,11 +92,11 @@ theorem lieConj_image_covLocalOperators (C : CovariantQuasilocalAlgebra)
   simp only [covLocalOperators, Set.mem_image, Set.mem_range]
   constructor
   · rintro ⟨_, ⟨a, rfl⟩, rfl⟩
-    exact ⟨C.net.covEquiv L B a, by rw [hconj (C.quasilocal.ι B a), action_ι C L hB a]⟩
+    exact ⟨C.net.covEquiv L B a, by rw [hconj (C.quasilocal.ι hB a), action_ι C L hB a]⟩
   · rintro ⟨a', rfl⟩
-    refine ⟨π (C.quasilocal.ι B ((C.net.covEquiv L B).symm a')),
+    refine ⟨π (C.quasilocal.ι hB ((C.net.covEquiv L B).symm a')),
       ⟨(C.net.covEquiv L B).symm a', rfl⟩, ?_⟩
-    rw [hconj (C.quasilocal.ι B ((C.net.covEquiv L B).symm a')),
+    rw [hconj (C.quasilocal.ι hB ((C.net.covEquiv L B).symm a')),
       action_ι C L hB ((C.net.covEquiv L B).symm a'), StarAlgEquiv.apply_symm_apply]
 
 /-- **Geometric covariance of the local von Neumann net (Minkowski).** In a
@@ -114,30 +115,31 @@ theorem lieConj_image_covLocalVonNeumann (C : CovariantQuasilocalAlgebra)
     (hB : IsAlexandrovBasisSet B)
     (hcov : ∀ (a : C.quasilocal.carrier) (x : H),
       Uop (π a (Uop.symm x)) = π (C.action L a) x) :
-    Physicslib4.lieConj Uop '' C.covLocalVonNeumann π B
-      = C.covLocalVonNeumann π (L • B) := by
+    Physicslib4.lieConj Uop '' C.covLocalVonNeumann π hB
+      = C.covLocalVonNeumann π (isAlexandrovBasisSet_smul L hB) := by
   unfold covLocalVonNeumann
-  rw [(Physicslib4.lieConj Uop).image_centralizer_centralizer (C.covLocalOperators π B),
+  rw [(Physicslib4.lieConj Uop).image_centralizer_centralizer (C.covLocalOperators π hB),
     C.lieConj_image_covLocalOperators π Uop L hB hcov]
 
 /-- The local observable operators of a region form a self-adjoint set. -/
 theorem covLocalOperators_selfAdjoint (C : CovariantQuasilocalAlgebra)
     (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
-    (B : Set StandardMinkowskiSpacetime.Carrier) :
-    ∀ x ∈ C.covLocalOperators π B, star x ∈ C.covLocalOperators π B := by
+    ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) :
+    ∀ x ∈ C.covLocalOperators π hB, star x ∈ C.covLocalOperators π hB := by
   rintro x ⟨a, rfl⟩
   exact ⟨star a, by simp only [map_star]⟩
 
 /-- The local von Neumann algebra `R(B)` as a bundled `VonNeumannAlgebra`. -/
 noncomputable def covLocalVonNeumannAlgebra (C : CovariantQuasilocalAlgebra)
     (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
-    (B : Set StandardMinkowskiSpacetime.Carrier) : VonNeumannAlgebra H :=
-  vonNeumannOfSelfAdjoint (C.covLocalOperators π B) (C.covLocalOperators_selfAdjoint π B)
+    ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) :
+    VonNeumannAlgebra H :=
+  vonNeumannOfSelfAdjoint (C.covLocalOperators π hB) (C.covLocalOperators_selfAdjoint π hB)
 
 @[simp] theorem coe_covLocalVonNeumannAlgebra (C : CovariantQuasilocalAlgebra)
     (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H))
-    (B : Set StandardMinkowskiSpacetime.Carrier) :
-    (C.covLocalVonNeumannAlgebra π B : Set (H →L[ℂ] H)) = C.covLocalVonNeumann π B :=
+    ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄ (hB : IsAlexandrovBasisSet B) :
+    (C.covLocalVonNeumannAlgebra π hB : Set (H →L[ℂ] H)) = C.covLocalVonNeumann π hB :=
   coe_vonNeumannOfSelfAdjoint _ _
 
 /-- **Geometric covariance as a von Neumann algebra isomorphism (Minkowski).**
@@ -152,39 +154,40 @@ noncomputable def covLocalVonNeumannEquiv (C : CovariantQuasilocalAlgebra)
     (hB : IsAlexandrovBasisSet B)
     (hcov : ∀ (a : C.quasilocal.carrier) (x : H),
       Uop (π a (Uop.symm x)) = π (C.action L a) x) :
-    (C.covLocalVonNeumannAlgebra π B).toStarSubalgebra ≃⋆ₐ[ℂ]
-      (C.covLocalVonNeumannAlgebra π (L • B)).toStarSubalgebra := by
+    (C.covLocalVonNeumannAlgebra π hB).toStarSubalgebra ≃⋆ₐ[ℂ]
+      (C.covLocalVonNeumannAlgebra π (isAlexandrovBasisSet_smul L hB)).toStarSubalgebra := by
+  let hL : IsAlexandrovBasisSet (L • B) := isAlexandrovBasisSet_smul L hB
   have hfun : (⇑(LinearIsometryEquiv.conjStarAlgEquiv Uop) : (H →L[ℂ] H) → (H →L[ℂ] H))
       = ⇑(Physicslib4.lieConj Uop) := by
     funext T; exact (Physicslib4.lieConj_apply_eq_conjStarAlgEquiv Uop T).symm
-  have himg : ⇑(LinearIsometryEquiv.conjStarAlgEquiv Uop) '' C.covLocalVonNeumann π B
-      = C.covLocalVonNeumann π (L • B) := by
+  have himg : ⇑(LinearIsometryEquiv.conjStarAlgEquiv Uop) '' C.covLocalVonNeumann π hB
+      = C.covLocalVonNeumann π hL := by
     rw [hfun]; exact C.lieConj_image_covLocalVonNeumann π Uop L hB hcov
   have himg' : ⇑(LinearIsometryEquiv.conjStarAlgEquiv Uop).symm ''
-      C.covLocalVonNeumann π (L • B) = C.covLocalVonNeumann π B := by
+      C.covLocalVonNeumann π hL = C.covLocalVonNeumann π hB := by
     rw [← himg, Set.image_image]
     simp only [StarAlgEquiv.symm_apply_apply, Set.image_id']
   refine Physicslib4.restrictStarAlgEquiv (LinearIsometryEquiv.conjStarAlgEquiv Uop)
     (fun x hx => ?_) (fun y hy => ?_)
-  · have hx' : x ∈ C.covLocalVonNeumann π B := by
-      have h1 : x ∈ ((C.covLocalVonNeumannAlgebra π B).toStarSubalgebra : Set (H →L[ℂ] H)) := hx
+  · have hx' : x ∈ C.covLocalVonNeumann π hB := by
+      have h1 : x ∈ ((C.covLocalVonNeumannAlgebra π hB).toStarSubalgebra : Set (H →L[ℂ] H)) := hx
       rwa [VonNeumannAlgebra.coe_toStarSubalgebra, coe_covLocalVonNeumannAlgebra] at h1
     have hmem : LinearIsometryEquiv.conjStarAlgEquiv Uop x
-        ∈ C.covLocalVonNeumann π (L • B) := by
+        ∈ C.covLocalVonNeumann π hL := by
       rw [← himg]; exact Set.mem_image_of_mem _ hx'
     change LinearIsometryEquiv.conjStarAlgEquiv Uop x
-      ∈ (C.covLocalVonNeumannAlgebra π (L • B)).toStarSubalgebra
+      ∈ (C.covLocalVonNeumannAlgebra π hL).toStarSubalgebra
     rw [← SetLike.mem_coe, VonNeumannAlgebra.coe_toStarSubalgebra, coe_covLocalVonNeumannAlgebra]
     exact hmem
-  · have hy' : y ∈ C.covLocalVonNeumann π (L • B) := by
-      have h1 : y ∈ ((C.covLocalVonNeumannAlgebra π (L • B)).toStarSubalgebra : Set (H →L[ℂ] H)) :=
+  · have hy' : y ∈ C.covLocalVonNeumann π hL := by
+      have h1 : y ∈ ((C.covLocalVonNeumannAlgebra π hL).toStarSubalgebra : Set (H →L[ℂ] H)) :=
         hy
       rwa [VonNeumannAlgebra.coe_toStarSubalgebra, coe_covLocalVonNeumannAlgebra] at h1
     have hmem : (LinearIsometryEquiv.conjStarAlgEquiv Uop).symm y
-        ∈ C.covLocalVonNeumann π B := by
+        ∈ C.covLocalVonNeumann π hB := by
       rw [← himg']; exact Set.mem_image_of_mem _ hy'
     change (LinearIsometryEquiv.conjStarAlgEquiv Uop).symm y
-      ∈ (C.covLocalVonNeumannAlgebra π B).toStarSubalgebra
+      ∈ (C.covLocalVonNeumannAlgebra π hB).toStarSubalgebra
     rw [← SetLike.mem_coe, VonNeumannAlgebra.coe_toStarSubalgebra, coe_covLocalVonNeumannAlgebra]
     exact hmem
 
@@ -199,8 +202,8 @@ theorem covLocalVonNeumann_isFactor_smul (C : CovariantQuasilocalAlgebra)
     (hB : IsAlexandrovBasisSet B)
     (hcov : ∀ (a : C.quasilocal.carrier) (x : H),
       Uop (π a (Uop.symm x)) = π (C.action L a) x)
-    (h : Physicslib4.IsFactor (C.covLocalVonNeumann π B)) :
-    Physicslib4.IsFactor (C.covLocalVonNeumann π (L • B)) := by
+    (h : Physicslib4.IsFactor (C.covLocalVonNeumann π hB)) :
+    Physicslib4.IsFactor (C.covLocalVonNeumann π (isAlexandrovBasisSet_smul L hB)) := by
   rw [← C.lieConj_image_covLocalVonNeumann π Uop L hB hcov]
   exact h.conj Uop
 

Physicslib4/AQFT/HaagKastler/Isotony.lean

@@ -46,12 +46,38 @@ spacetime is implemented by a *unital `*`-monomorphism*
 `𝔘(B₁) ↪ 𝔘(B₂)`.
 
 Blueprint reference: `def:isotony`.
+
+The family is *chosen data*, not an existence statement: the identity and
+composition laws below are equations between the maps themselves, so there is
+nothing to state unless the maps are fixed. An axiom of the form "for each
+inclusion there exists some monomorphism" cannot express functoriality at all.
+
+`map_self` and `map_comp` say exactly that `B ↦ 𝔘(B)` is a functor on the
+inclusion order of basis sets. They are *required* rather than derived because
+they constrain the net's chosen embeddings, not the spacetime. Their payoff is
+that the local algebras form a genuine directed system, which is what gives the
+quasilocal algebra (`def:quasilocal-algebra`) its algebra structure.
 -/
-def Isotony (U : LocalNet) : Prop :=
-  ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄,
+structure Isotony (U : LocalNet) where
+  /-- The chosen unital `*`-monomorphism implementing each inclusion of basis
+  sets. This is data, which is what makes the two laws below statable. -/
+  map : ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄,
     IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ → B₁ ⊆ B₂ →
-      ∃ φ : StarAlgHom ℂ (U.algebra B₁) (U.algebra B₂),
-        Function.Injective φ
+      StarAlgHom ℂ (U.algebra B₁) (U.algebra B₂)
+  /-- Each chosen embedding is injective, i.e. a monomorphism. -/
+  injective : ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
+    (h₁ : IsAlexandrovBasisSet B₁) (h₂ : IsAlexandrovBasisSet B₂) (h : B₁ ⊆ B₂),
+    Function.Injective (map h₁ h₂ h)
+  /-- **Identity law.** The embedding along `B ⊆ B` is the identity. -/
+  map_self : ∀ ⦃B : Set StandardMinkowskiSpacetime.Carrier⦄
+    (h : IsAlexandrovBasisSet B),
+    map h h (subset_refl B) = StarAlgHom.id ℂ (U.algebra B)
+  /-- **Composition law.** The embedding along `B₁ ⊆ B₃` factors through any
+  intermediate `B₂`. -/
+  map_comp : ∀ ⦃B₁ B₂ B₃ : Set StandardMinkowskiSpacetime.Carrier⦄
+    (h₁ : IsAlexandrovBasisSet B₁) (h₂ : IsAlexandrovBasisSet B₂)
+    (h₃ : IsAlexandrovBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃),
+    (map h₂ h₃ h₂₃).comp (map h₁ h₂ h₁₂) = map h₁ h₃ (h₁₂.trans h₂₃)
 
 /-- **Isotony is reflexive.** Every Alexandrov-basis set embeds into
 itself via the identity unital `*`-monomorphism, independently of any
@@ -69,9 +95,8 @@ theorem Isotony.trans {U : LocalNet} (h : Isotony U)
     (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂)
     (hB₃ : IsAlexandrovBasisSet B₃) (h₁₂ : B₁ ⊆ B₂) (h₂₃ : B₂ ⊆ B₃) :
     ∃ φ : StarAlgHom ℂ (U.algebra B₁) (U.algebra B₃), Function.Injective φ := by
-  obtain ⟨φ, hφ⟩ := h hB₁ hB₂ h₁₂
-  obtain ⟨ψ, hψ⟩ := h hB₂ hB₃ h₂₃
-  exact ⟨ψ.comp φ, fun a b hab => hφ (hψ (by simpa using hab))⟩
+  refine ⟨(h.map hB₂ hB₃ h₂₃).comp (h.map hB₁ hB₂ h₁₂), ?_⟩
+  simpa using (h.injective hB₂ hB₃ h₂₃).comp (h.injective hB₁ hB₂ h₁₂)
 
 end HaagKastler
 end AQFT

Physicslib4/AQFT/HaagKastler/LocalCommutativity.lean

@@ -35,9 +35,10 @@ axioms, section 10.3 of the AQFT-in-Lean blueprint):
   completely-spacelike local algebras commute pointwise.
 
 * The quasilocal algebra itself — including its density / completion
-  property — is the subject of Axiom 4 (`QuasilocalCompleteness`);
-  here we only *use* the structure to phrase commutativity. The two
-  axioms can in principle share the same witness.
+  property — is *constructed* from the net by
+  `exists_quasilocalAlgebra` (`thrm:quasilocal-algebra-exists`); here
+  we only *use* the structure to phrase commutativity, and the
+  existential above may be witnessed by that canonical algebra.
 -/
 
 namespace Physicslib4
@@ -58,14 +59,14 @@ commute pointwise inside `Q.carrier`.
 
 Blueprint reference: `def:local-commutativity`.
 -/
-def LocalCommutativity (U : LocalNet) : Prop :=
-  ∃ Q : QuasilocalAlgebra U,
-    ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄,
-      IsAlexandrovBasisSet B₁ → IsAlexandrovBasisSet B₂ →
+def LocalCommutativity (U : LocalNet) (i : Isotony U) : Prop :=
+  ∃ Q : QuasilocalAlgebra U i,
+    ∀ ⦃B₁ B₂ : Set StandardMinkowskiSpacetime.Carrier⦄
+      (hB₁ : IsAlexandrovBasisSet B₁) (hB₂ : IsAlexandrovBasisSet B₂),
       Spacetime.IsCompletelySpacelike StandardMinkowskiSpacetime
         standardMinkowskiTimeOrientation B₁ B₂ →
       ∀ (a : U.algebra B₁) (b : U.algebra B₂),
-        Commute (Q.ι B₁ a) (Q.ι B₂ b)
+        Commute (Q.ι hB₁ a) (Q.ι hB₂ b)
 
 end HaagKastler
 end AQFT