diff --git a/Physicslib4.lean b/Physicslib4.lean index 2b23aea..879964b 100644 --- a/Physicslib4.lean +++ b/Physicslib4.lean @@ -37,17 +37,22 @@ import Physicslib4.Analysis.HorizontalLineRemovable import Physicslib4.Analysis.StripPeriodicExtension import Physicslib4.Analysis.StrongContinuity import Physicslib4.Basic +import Physicslib4.GNS.Amplification import Physicslib4.GNS.Basic import Physicslib4.GNS.CauchySchwarz import Physicslib4.GNS.Construction +import Physicslib4.GNS.DirectSum import Physicslib4.GNS.ExtremeState import Physicslib4.GNS.Irreducibility import Physicslib4.GNS.NullSpace import Physicslib4.GNS.PureStateExists import Physicslib4.GNS.RadonNikodym import Physicslib4.GNS.Separating +import Physicslib4.GNS.Superselection +import Physicslib4.GNS.UnitaryEquiv import Physicslib4.GNS.UnitaryRepresentation import Physicslib4.Operators.Conjugation +import Physicslib4.Operators.LpDiagonal import Physicslib4.Spacetime.Basic import Physicslib4.Spacetime.CausalStructure import Physicslib4.Spacetime.Causality diff --git a/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean b/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean index a79ea9a..fd04ee0 100644 --- a/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean +++ b/Physicslib4/AQFT/HaagKastler/QuasilocalIntertwiner.lean @@ -602,6 +602,49 @@ theorem IsInvariantState.exists_gns_unitary_strongContinuous Physicslib4.GNS.exists_gns_unitary_of_invariant_strongContinuous C.action ω hω C.action_mul_apply C.action_one_apply hwc +open scoped InnerProductSpace in +/-- **Bundled GNS unitary representation of an invariant state.** The bundled form +of `IsInvariantState.exists_gns_unitary`: the implementing unitaries are returned +as a genuine unitary representation `U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)` +(a bundled group homomorphism), rather than a bare family with separate group-law +clauses. It feeds the covariance group homomorphism `C.actionHom` into the bundled +analytic core `GNS.exists_gns_unitaryRep_of_invariant`. -/ +theorem IsInvariantState.exists_gns_unitaryRep (C : CovariantQuasilocalAlgebra) + {ω : Physicslib4.GNS.State C.quasilocal.carrier} (hω : C.IsInvariantState ω) : + ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)), + (∀ a : C.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier), + U L (π a Ω) = π (C.action L a) Ω) ∧ + (∀ L : InhomogeneousLorentzGroup, U L Ω = Ω) ∧ + (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H), + U L (π a ((U L).symm x)) = π (C.action L a) x) ∧ + Physicslib4.GNS.IsCyclicVector π Ω := + Physicslib4.GNS.exists_gns_unitaryRep_of_invariant C.actionHom ω hω + +open scoped InnerProductSpace in +/-- **Bundled strongly continuous GNS unitary representation of an invariant state.** +The bundled form of `IsInvariantState.exists_gns_unitary_strongContinuous`: the +strongly continuous implementing unitaries are returned as a bundled group +homomorphism `U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)`. -/ +theorem IsInvariantState.exists_gns_unitaryRep_strongContinuous + (C : CovariantQuasilocalAlgebra) + {ω : Physicslib4.GNS.State C.quasilocal.carrier} (hω : C.IsInvariantState ω) + (hwc : ∀ a b : C.quasilocal.carrier, + Continuous fun L : InhomogeneousLorentzGroup => (ω (star a * C.action L b) : ℂ)) : + ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : C.quasilocal.carrier →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : InhomogeneousLorentzGroup →* (H ≃ₗᵢ[ℂ] H)), + (∀ a : C.quasilocal.carrier, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier), + U L (π a Ω) = π (C.action L a) Ω) ∧ + (∀ L : InhomogeneousLorentzGroup, U L Ω = Ω) ∧ + (∀ ψ : H, Continuous fun L : InhomogeneousLorentzGroup => U L ψ) ∧ + (∀ (L : InhomogeneousLorentzGroup) (a : C.quasilocal.carrier) (x : H), + U L (π a ((U L).symm x)) = π (C.action L a) x) := + Physicslib4.GNS.exists_gns_unitaryRep_of_invariant_strongContinuous C.actionHom ω hω hwc + open scoped InnerProductSpace in /-- **Irreducible covariant representation of a pure invariant state (Minkowski).** A state `ω` on the quasilocal algebra that is both invariant under the covariance diff --git a/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean b/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean index 676fa27..040a4b0 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/IdentityComponent.lean @@ -69,6 +69,31 @@ can be rewritten to the concrete subgroup. -/ = ↥(Spacetime.Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation) := rfl +/-- The abstract isometry group of the `toAbstract` bridge inherits the +topological-group topology of the concrete isometry group. This discharges the +`[TopologicalSpace M.Isom]` hypothesis of the curved covariance/KMS results +(e.g. the strongly continuous stabilizer GNS unitary) automatically for a net +over a concrete Lorentzian spacetime — no explicit topology argument is needed. -/ +noncomputable instance instTopologicalSpaceToAbstractIsom (L : LorentzianSpacetime) : + TopologicalSpace (L.toAbstract).Isom := + inferInstanceAs (TopologicalSpace (Isometry L.toSpacetime)) + +/-- The abstract isometry group of the `toAbstractIdentityComponent` bridge +inherits the subspace topology of the oriented identity-component subgroup, +discharging `[TopologicalSpace M.Isom]` automatically over a concrete spacetime. -/ +noncomputable instance instTopologicalSpaceToAbstractIdentityComponentIsom + (L : LorentzianSpacetime) : + TopologicalSpace (L.toAbstractIdentityComponent).Isom := + inferInstanceAs (TopologicalSpace + ↥(Spacetime.Isometry.orientedIdentityComponent L.toSpacetime L.timeOrientation)) + +/-- Confirmation that the `[TopologicalSpace M.Isom]` requirement of the curved +results is met by both bridges over a concrete spacetime. -/ +example (L : LorentzianSpacetime) : True := by + have _ : TopologicalSpace (L.toAbstract).Isom := inferInstance + have _ : TopologicalSpace (L.toAbstractIdentityComponent).Isom := inferInstance + trivial + open scoped Pointwise in /-- **Axiom 5 basis-set preservation, stated over the abstract bridge.** Every isometry `φ` of the abstract spacetime carries Alexandrov-basis sets to basis diff --git a/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean b/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean index 81620f2..825e318 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/Purity.lean @@ -6,6 +6,7 @@ Authors: Lean Community import Physicslib4.AQFT.HaagKastlerCurved.Net import Physicslib4.GNS.RadonNikodym import Physicslib4.GNS.ExtremeState +import Physicslib4.GNS.Superselection /-! # Purity of states on curved local algebras @@ -90,6 +91,19 @@ theorem exists_gns_generates_all_of_isPure {B : Set M.Carrier} {ω : State (N.al gnsVonNeumann π = Set.univ := GNS.exists_gns_generates_all_of_isPure hpure +/-- **The irreducible dichotomy for curved local algebras.** Two irreducible +representations of a curved local algebra `𝔘(B)` are either disjoint or unitarily +equivalent. The abstract `GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible` at the +C*-algebra `𝔘(B)`. -/ +theorem areDisjoint_or_unitaryEquiv_of_isIrreducible {B : Set M.Carrier} + {H₁ H₂ : Type*} + [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] + [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] + {π₁ : N.algebra B →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} {π₂ : N.algebra B →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} + (h1 : GNS.IsIrreducible π₁) (h2 : GNS.IsIrreducible π₂) : + GNS.AreDisjoint π₁ π₂ ∨ GNS.UnitaryEquiv π₁ π₂ := + GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible h1 h2 + end HaagKastlerNet end HaagKastlerCurved end AQFT diff --git a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean index da87760..4cc9ea5 100644 --- a/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean +++ b/Physicslib4/AQFT/HaagKastlerCurved/StabilizerAction.lean @@ -199,6 +199,51 @@ theorem exists_gns_unitary_stabilizer_strongContinuous [TopologicalSpace M.Isom] ω hinv (fun g g' a => N.stabAutHom_mul B g g' a) (fun a => N.stabAutHom_one B a) hwc +/-- **Bundled GNS unitary representation of the stabilizer.** The bundled form of +`exists_gns_unitary_stabilizer`: the implementing unitaries are returned as a +genuine unitary representation `U : ↥Stab(B) →* (H ≃ₗᵢ[ℂ] H)`, feeding the +stabilizer group homomorphism `stabAutMonoidHom` into the bundled analytic core +`GNS.exists_gns_unitaryRep_of_invariant`. -/ +theorem exists_gns_unitaryRep_stabilizer (B : Set M.Carrier) + (ω : State (N.algebra B)) + (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B), + ω (N.stabAutHom B g a) = ω a) : + ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : ↥(MulAction.stabilizer M.Isom B) →* (H ≃ₗᵢ[ℂ] H)), + (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B), + U g (π a Ω) = π (N.stabAutHom B g a) Ω) ∧ + (∀ g : ↥(MulAction.stabilizer M.Isom B), U g Ω = Ω) ∧ + (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B) (x : H), + U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) ∧ + IsCyclicVector π Ω := + Physicslib4.GNS.exists_gns_unitaryRep_of_invariant (N.stabAutMonoidHom B) ω hinv + +/-- **Bundled strongly continuous GNS unitary representation of the stabilizer.** +The bundled form of `exists_gns_unitary_stabilizer_strongContinuous`: the strongly +continuous implementing unitaries are returned as a bundled group homomorphism +`U : ↥Stab(B) →* (H ≃ₗᵢ[ℂ] H)`. -/ +theorem exists_gns_unitaryRep_stabilizer_strongContinuous [TopologicalSpace M.Isom] + (B : Set M.Carrier) (ω : State (N.algebra B)) + (hinv : ∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B), + ω (N.stabAutHom B g a) = ω a) + (hwc : ∀ a b : N.algebra B, + Continuous fun g : ↥(MulAction.stabilizer M.Isom B) => + (ω (star a * N.stabAutHom B g b) : ℂ)) : + ∃ (H : Type) (_ : NormedAddCommGroup H) (_ : InnerProductSpace ℂ H) + (_ : CompleteSpace H) (π : N.algebra B →⋆ₐ[ℂ] (H →L[ℂ] H)) (Ω : H) + (U : ↥(MulAction.stabilizer M.Isom B) →* (H ≃ₗᵢ[ℂ] H)), + (∀ a : N.algebra B, (ω a : ℂ) = ⟪Ω, π a Ω⟫_ℂ) ∧ + (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B), + U g (π a Ω) = π (N.stabAutHom B g a) Ω) ∧ + (∀ g : ↥(MulAction.stabilizer M.Isom B), U g Ω = Ω) ∧ + (∀ ψ : H, Continuous fun g : ↥(MulAction.stabilizer M.Isom B) => U g ψ) ∧ + (∀ (g : ↥(MulAction.stabilizer M.Isom B)) (a : N.algebra B) (x : H), + U g (π a ((U g).symm x)) = π (N.stabAutHom B g a) x) := + Physicslib4.GNS.exists_gns_unitaryRep_of_invariant_strongContinuous + (N.stabAutMonoidHom B) ω hinv hwc + /-- **Irreducible covariant representation of a pure invariant state (curved spacetime).** A state `ω` on a local algebra `𝔘(B)` that is invariant under the stabilizer action and pure yields a GNS representation that is simultaneously diff --git a/Physicslib4/GNS/Amplification.lean b/Physicslib4/GNS/Amplification.lean new file mode 100644 index 0000000..40606b4 --- /dev/null +++ b/Physicslib4/GNS/Amplification.lean @@ -0,0 +1,104 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.GNS.DirectSum + +/-! +# Amplification and reducibility of direct sums + +Two consequences of the direct-sum construction (`Physicslib4.GNS.DirectSum`): + +* **Reducibility.** The summand projections lie in the commutant, so if the + direct-sum representation is irreducible they must be scalars + (`summandProj_isScalar_of_isIrreducible`); consequently a direct sum with two + summands carrying nonzero vectors is reducible (`not_isIrreducible_directSum`). +* **Amplification.** The `ι`-fold amplification `ι · π := ⊕_{ι} π` of a single + representation, in which `π` embeds as each summand (`amplification_intertwines_single`). + +## The quasi-equivalence `π ~ ι · π` + +The quasi-equivalence of a representation with its amplification (`QuasiEquiv π (ι · π)`) +is **not** proved here. It requires a `*`-isomorphism of the generated von Neumann +algebras `π(A)'' ≃⋆ₐ (ι·π)(A)''`. The natural map is `T ↦ lpDiag (fun _ ↦ T)` +(the diagonal), which is an injective `*`-homomorphism carrying `π a ↦ (ι·π) a`; +but *surjectivity* onto `(ι·π)(A)''` is exactly the amplification commutant theorem +`(π ⊗ 1)' = π' ⊗ B(K)` (equivalently `(π ⊗ 1)'' = π'' ⊗ ℂ1`), a genuine von Neumann +algebra result that Mathlib does not currently provide. It is recorded as deferred. +-/ + +namespace Physicslib4 +namespace GNS + +variable {A : Type*} [CStarAlgebra A] +variable {ι : Type*} [DecidableEq ι] {H : ι → Type*} + [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] [∀ i, CompleteSpace (H i)] +variable (π : ∀ i, A →⋆ₐ[ℂ] (H i →L[ℂ] H i)) + +/-! ### Reducibility -/ + +/-- If the direct-sum representation is irreducible, each summand projection is a +scalar operator (irreducibility means the commutant is trivial). -/ +theorem summandProj_isScalar_of_isIrreducible (hirr : IsIrreducible (directSum π)) (j : ι) : + summandProj (H := H) j ∈ scalarOperators (lp H 2) := + isIrreducible_iff_centralizer.mp hirr ▸ summandProj_mem_commutant π j + +set_option linter.unusedDecidableInType false in +/-- A direct sum with two summands carrying nonzero vectors is **reducible**: the +projection onto one summand is a non-scalar element of the commutant. -/ +theorem not_isIrreducible_directSum {j k : ι} (hjk : j ≠ k) + {v : H j} (hv : v ≠ 0) {w : H k} (hw : w ≠ 0) : + ¬ IsIrreducible (directSum π) := by + intro hirr + obtain ⟨c, hc⟩ := summandProj_isScalar_of_isIrreducible π hirr j + have hjv : lp.single 2 j v ≠ 0 := by + rw [← norm_ne_zero_iff, lp.norm_single (by norm_num)] + exact norm_ne_zero_iff.mpr hv + have hkw : lp.single 2 k w ≠ 0 := by + rw [← norm_ne_zero_iff, lp.norm_single (by norm_num)] + exact norm_ne_zero_iff.mpr hw + have e1 := DFunLike.congr_fun hc (lp.single 2 j v) + have e2 := DFunLike.congr_fun hc (lp.single 2 k w) + simp only [summandProj_apply, ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply, + lp.single_apply_self] at e1 + simp only [summandProj_apply, lp.single_apply_ne 2 k w hjk, lp.single_zero, + ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] at e2 + have hc1 : c = 1 := by + have h0 : (1 - c) • lp.single 2 j v = 0 := by rw [sub_smul, one_smul, ← e1, sub_self] + rcases smul_eq_zero.mp h0 with h | h + · exact (sub_eq_zero.mp h).symm + · exact absurd h hjv + have hc0 : c = 0 := by + rcases smul_eq_zero.mp e2.symm with h | h + · exact h + · exact absurd h hkw + rw [hc1] at hc0 + exact one_ne_zero hc0 + +end GNS + +/-! ### Amplification -/ + +namespace GNS + +variable {A : Type*} [CStarAlgebra A] +variable {H₀ : Type*} [NormedAddCommGroup H₀] [InnerProductSpace ℂ H₀] [CompleteSpace H₀] +variable {ι : Type*} [DecidableEq ι] +variable (π : A →⋆ₐ[ℂ] (H₀ →L[ℂ] H₀)) + +/-- The `ι`-fold **amplification** `ι · π := ⊕_{i : ι} π` of a representation, on the +ℓ²-direct sum of `ι` copies of `H₀`. -/ +noncomputable def amplification : + A →⋆ₐ[ℂ] (lp (fun _ : ι => H₀) 2 →L[ℂ] lp (fun _ : ι => H₀) 2) := + directSum (fun _ : ι => π) + +/-- In the amplification, `π` embeds as each summand: the isometric inclusion of the +`j`-th copy `H₀ ↪ ℓ²(ι, H₀)` intertwines `π` with `ι · π`. -/ +theorem amplification_intertwines_single (j : ι) : + Intertwines π (amplification (ι := ι) π) + (lp.singleContinuousLinearMap ℂ (fun _ : ι => H₀) 2 j) := + intertwines_single (fun _ : ι => π) j + +end GNS +end Physicslib4 diff --git a/Physicslib4/GNS/DirectSum.lean b/Physicslib4/GNS/DirectSum.lean new file mode 100644 index 0000000..259f4d8 --- /dev/null +++ b/Physicslib4/GNS/DirectSum.lean @@ -0,0 +1,128 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.Operators.LpDiagonal +import Physicslib4.GNS.Superselection + +/-! +# Direct sums of representations + +Given a family of `*`-representations `π i : A →⋆ₐ[ℂ] (H i →L[ℂ] H i)` of a +C*-algebra `A` on Hilbert spaces `H i`, the **direct-sum representation** +`⊕ᵢ πᵢ` acts on the ℓ²-direct sum `lp H 2` by the diagonal operator of +`fun i ↦ π i a` (uniformly bounded by `‖a‖`, since a `*`-homomorphism of +C*-algebras is contractive). + +This file builds `directSum π : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2)` and proves the two +basic structural facts: + +* `intertwines_single` — each summand embeds as a **subrepresentation**: the + isometric inclusion `H j ↪ lp H 2` intertwines `π j` with `directSum π`; +* `summandProj_mem_commutant` — the orthogonal **projection onto the `j`-th + summand lies in the commutant** of `directSum π`, so a direct sum of two or more + nonzero summands is reducible. +-/ + +namespace Physicslib4 +namespace GNS + +variable {A : Type*} [CStarAlgebra A] +variable {ι : Type*} [DecidableEq ι] {H : ι → Type*} + [∀ i, NormedAddCommGroup (H i)] [∀ i, InnerProductSpace ℂ (H i)] [∀ i, CompleteSpace (H i)] +variable (π : ∀ i, A →⋆ₐ[ℂ] (H i →L[ℂ] H i)) + +/-! ### Coordinate evaluation -/ + +/-- Coordinate evaluation `x ↦ x j` as a continuous linear map `lp H 2 →L H j` +(norm `≤ 1`). -/ +noncomputable def lpEvalCLM (j : ι) : lp H 2 →L[ℂ] H j := + LinearMap.mkContinuous + { toFun := fun x => x j + map_add' := fun _ _ => rfl + map_smul' := fun _ _ => rfl } + 1 + (fun x => by simpa using lp.norm_apply_le_norm (p := 2) (by norm_num) x j) + +omit [DecidableEq ι] [∀ (i : ι), CompleteSpace (H i)] in +@[simp] theorem lpEvalCLM_apply (j : ι) (x : lp H 2) : lpEvalCLM j x = x j := rfl + +/-! ### The direct-sum representation -/ + +/-- The value of the direct-sum representation on `a`: the diagonal operator of the +family `fun i ↦ π i a`, uniformly bounded by `‖a‖`. -/ +noncomputable def directSumFun (a : A) : lp H 2 →L[ℂ] lp H 2 := + lpDiag (fun i => π i a) (norm_nonneg a) (fun i => NonUnitalStarAlgHom.norm_apply_le (π i) a) + +omit [DecidableEq ι] in +@[simp] theorem directSumFun_apply_coe (a : A) (x : lp H 2) (i : ι) : + (directSumFun π a x) i = π i a (x i) := rfl + +/-- The **direct-sum representation** `⊕ᵢ πᵢ` on the ℓ²-direct sum `lp H 2`. -/ +noncomputable def directSum : A →⋆ₐ[ℂ] (lp H 2 →L[ℂ] lp H 2) where + toFun := directSumFun π + map_one' := by refine lpDiag_ext fun x i => ?_; simp [map_one] + map_mul' a b := by + refine lpDiag_ext fun x i => ?_; simp [map_mul, ContinuousLinearMap.mul_apply] + map_zero' := by + refine lpDiag_ext fun x i => ?_ + change π i 0 (x i) = (0 : lp H 2) i + rw [map_zero]; rfl + map_add' a b := by + refine lpDiag_ext fun x i => ?_ + change π i (a + b) (x i) = π i a (x i) + π i b (x i) + rw [map_add (π i) a b]; rfl + commutes' r := by + refine lpDiag_ext fun x i => ?_ + simp [Algebra.algebraMap_eq_smul_one, ContinuousLinearMap.smul_apply, + ContinuousLinearMap.one_apply, lp.coeFn_smul] + map_star' a := by + simp only [directSumFun] + rw [lpDiag_star] + refine lpDiag_ext fun x i => ?_ + change π i (star a) (x i) = star (π i a) (x i) + rw [map_star (π i) a] + +omit [DecidableEq ι] in +@[simp] theorem directSum_apply (a : A) : directSum π a = directSumFun π a := rfl + +/-! ### Subrepresentations and commutant projections -/ + +/-- Each summand is a **subrepresentation**: the isometric inclusion `H j ↪ lp H 2` +intertwines `π j` with the direct-sum representation. -/ +theorem intertwines_single (j : ι) : + Intertwines (π j) (directSum π) (lp.singleContinuousLinearMap ℂ H 2 j) := by + intro a v + apply lp.ext + funext i + simp only [lp.singleContinuousLinearMap_apply, directSum_apply, directSumFun_apply_coe, + lp.single_apply] + rcases eq_or_ne i j with h | h + · subst h; simp + · simp [Pi.single_eq_of_ne h] + +/-- The orthogonal projection onto the `j`-th summand, `x ↦ single j (x j)`. -/ +noncomputable def summandProj (j : ι) : lp H 2 →L[ℂ] lp H 2 := + (lp.singleContinuousLinearMap ℂ H 2 j).comp (lpEvalCLM j) + +omit [∀ (i : ι), CompleteSpace (H i)] in +@[simp] theorem summandProj_apply (j : ι) (x : lp H 2) : + summandProj j x = lp.single 2 j (x j) := by + simp [summandProj, lp.singleContinuousLinearMap_apply] + +/-- The **projection onto the `j`-th summand commutes with the whole +representation**, hence lies in the commutant of `directSum π`. -/ +theorem summandProj_mem_commutant (j : ι) : + summandProj (H := H) j ∈ Set.centralizer (Set.range (directSum π)) := by + rw [Set.mem_centralizer_iff] + rintro _ ⟨a, rfl⟩ + refine lpDiag_ext fun x i => ?_ + simp only [ContinuousLinearMap.mul_apply, directSum_apply, directSumFun_apply_coe, + summandProj_apply, lp.single_apply] + rcases eq_or_ne i j with h | h + · subst h; simp + · simp [Pi.single_eq_of_ne h] + +end GNS +end Physicslib4 diff --git a/Physicslib4/GNS/Superselection.lean b/Physicslib4/GNS/Superselection.lean new file mode 100644 index 0000000..22e3b63 --- /dev/null +++ b/Physicslib4/GNS/Superselection.lean @@ -0,0 +1,493 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.GNS.UnitaryEquiv +import Physicslib4.GNS.RadonNikodym + +/-! +# Disjointness and quasi-equivalence of representations + +Building on `UnitaryEquiv`, this file introduces the two coarser comparisons of +`*`-representations from superselection theory: + +* an **intertwiner** is a bounded operator `T : H₁ →L H₂` with `T π₁(a) = π₂(a) T`; +* two representations are **disjoint** (`AreDisjoint`) when the only intertwiner is + `0` — equivalently, they share no unitarily equivalent subrepresentation; +* two representations are **quasi-equivalent** (`QuasiEquiv`) when there is a + `*`-isomorphism of the generated von Neumann algebras `π₁(A)'' ≃⋆ₐ π₂(A)''` + carrying `π₁(a)` to `π₂(a)`. + +We prove the basic algebra of intertwiners, that disjointness is symmetric and +irreflexive (unitarily equivalent representations are never disjoint), that +quasi-equivalence is an equivalence relation, and that unitary equivalence implies +quasi-equivalence. +-/ + +namespace Physicslib4 +namespace GNS + +open scoped InnerProductSpace + +variable {A : Type*} [CStarAlgebra A] +variable {H₁ : Type*} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] +variable {H₂ : Type*} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] +variable {H₃ : Type*} [NormedAddCommGroup H₃] [InnerProductSpace ℂ H₃] [CompleteSpace H₃] + +/-! ### Intertwiners -/ + +/-- `T : H₁ →L H₂` **intertwines** `π₁` and `π₂` when `T π₁(a) = π₂(a) T`. -/ +def Intertwines (π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) (π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)) + (T : H₁ →L[ℂ] H₂) : Prop := + ∀ (a : A) (x : H₁), T (π₁ a x) = π₂ a (T x) + +variable {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} + {π₃ : A →⋆ₐ[ℂ] (H₃ →L[ℂ] H₃)} + +theorem intertwines_zero : Intertwines π₁ π₂ (0 : H₁ →L[ℂ] H₂) := fun a x => by simp + +theorem Intertwines.add {S T : H₁ →L[ℂ] H₂} (hS : Intertwines π₁ π₂ S) + (hT : Intertwines π₁ π₂ T) : Intertwines π₁ π₂ (S + T) := fun a x => by + simp only [ContinuousLinearMap.add_apply, hS a x, hT a x, map_add] + +theorem Intertwines.smul {T : H₁ →L[ℂ] H₂} (c : ℂ) (hT : Intertwines π₁ π₂ T) : + Intertwines π₁ π₂ (c • T) := fun a x => by + simp only [ContinuousLinearMap.smul_apply, hT a x, map_smul] + +/-- The composition of intertwiners is an intertwiner. -/ +theorem Intertwines.comp {S : H₂ →L[ℂ] H₃} {T : H₁ →L[ℂ] H₂} + (hS : Intertwines π₂ π₃ S) (hT : Intertwines π₁ π₂ T) : + Intertwines π₁ π₃ (S.comp T) := fun a x => by + simp only [ContinuousLinearMap.comp_apply] + rw [hT a x, hS a (T x)] + +/-- The adjoint of an intertwiner `π₁ → π₂` is an intertwiner `π₂ → π₁`. -/ +theorem Intertwines.adjoint {T : H₁ →L[ℂ] H₂} (hT : Intertwines π₁ π₂ T) : + Intertwines π₂ π₁ (ContinuousLinearMap.adjoint T) := by + have hcomp : ∀ a : A, (ContinuousLinearMap.adjoint T).comp (π₂ a) + = (π₁ a).comp (ContinuousLinearMap.adjoint T) := by + intro a + have h1 : T.comp (π₁ (star a)) = (π₂ (star a)).comp T := + ContinuousLinearMap.ext (fun x => hT (star a) x) + have h2 := congrArg ContinuousLinearMap.adjoint h1 + rw [ContinuousLinearMap.adjoint_comp, ContinuousLinearMap.adjoint_comp] at h2 + have hp1 : ContinuousLinearMap.adjoint (π₁ (star a)) = π₁ a := by + rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star, star_star] + have hp2 : ContinuousLinearMap.adjoint (π₂ (star a)) = π₂ a := by + rw [← ContinuousLinearMap.star_eq_adjoint, ← map_star, star_star] + rw [hp1, hp2] at h2 + exact h2.symm + intro a x + have hx := DFunLike.congr_fun (hcomp a) x + simpa only [ContinuousLinearMap.comp_apply] using hx + +/-! ### Disjointness -/ + +/-- Two representations are **disjoint** when the only operator intertwining them +is `0`. -/ +def AreDisjoint (π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) (π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)) : + Prop := + ∀ T : H₁ →L[ℂ] H₂, Intertwines π₁ π₂ T → T = 0 + +/-- Disjointness is symmetric (take adjoints of intertwiners). -/ +theorem AreDisjoint.symm (h : AreDisjoint π₁ π₂) : AreDisjoint π₂ π₁ := by + intro T hT + have h0 : ContinuousLinearMap.adjoint T = 0 := h _ hT.adjoint + rw [← ContinuousLinearMap.adjoint_adjoint T, h0, map_zero] + +/-- A representation on a nonzero Hilbert space is never disjoint from itself (the +identity is a nonzero intertwiner). -/ +theorem not_areDisjoint_self [Nontrivial H₁] (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + ¬ AreDisjoint π π := by + intro h + obtain ⟨v, hv⟩ := exists_ne (0 : H₁) + have h1 : (1 : H₁ →L[ℂ] H₁) = 0 := h 1 (fun a x => by simp) + exact hv (by simpa using ContinuousLinearMap.ext_iff.mp h1 v) + +/-- **Unitarily equivalent representations are not disjoint** (on nonzero spaces): +the implementing unitary is a nonzero intertwiner. -/ +theorem UnitaryEquiv.not_areDisjoint [Nontrivial H₁] (h : UnitaryEquiv π₁ π₂) : + ¬ AreDisjoint π₁ π₂ := by + obtain ⟨U, hU⟩ := h + intro hd + have hint : Intertwines π₁ π₂ (↑U.toContinuousLinearEquiv : H₁ →L[ℂ] H₂) := by + intro a x + simp only [ContinuousLinearEquiv.coe_coe, + LinearIsometryEquiv.coe_toContinuousLinearEquiv] + exact hU a x + have h0 : (↑U.toContinuousLinearEquiv : H₁ →L[ℂ] H₂) = 0 := hd _ hint + obtain ⟨v, hv⟩ := exists_ne (0 : H₁) + have hUv : U v = 0 := by + have := ContinuousLinearMap.ext_iff.mp h0 v + simpa only [ContinuousLinearEquiv.coe_coe, + LinearIsometryEquiv.coe_toContinuousLinearEquiv, + ContinuousLinearMap.zero_apply] using this + exact hv (U.injective (hUv.trans (map_zero U).symm)) + +/-! ### Schur's lemma and the irreducible dichotomy -/ + +/-- **Schur's lemma.** A nonzero intertwiner between two irreducible representations +rescales to a unitary: `π₁` and `π₂` are unitarily equivalent. The operator `T⋆T` +commutes with `π₁`, hence is a positive scalar `r · 1`; the normalisation +`(√r)⁻¹ · T` is then a linear isometry, and `T T⋆` being a nonzero scalar makes it +surjective, i.e. a unitary equivalence. -/ +theorem UnitaryEquiv.of_intertwines_of_isIrreducible + (h1 : IsIrreducible π₁) (h2 : IsIrreducible π₂) + {T : H₁ →L[ℂ] H₂} (hT : Intertwines π₁ π₂ T) (hT0 : T ≠ 0) : + UnitaryEquiv π₁ π₂ := by + obtain ⟨c, hc⟩ := h1 ((ContinuousLinearMap.adjoint T).comp T) + (fun a => ContinuousLinearMap.ext fun x => ((hT.adjoint.comp hT) a x).symm) + obtain ⟨d, hd⟩ := h2 (T.comp (ContinuousLinearMap.adjoint T)) + (fun a => ContinuousLinearMap.ext fun x => ((hT.comp hT.adjoint) a x).symm) + -- `⟪T x, T x⟫ = c ⟪x, x⟫`. + have hcT : ∀ x : H₁, inner ℂ (T x) (T x) = c * inner ℂ x x := by + intro x + rw [← ContinuousLinearMap.adjoint_inner_right T x (T x)] + change inner ℂ x (((ContinuousLinearMap.adjoint T).comp T) x) = c * inner ℂ x x + rw [hc] + simp [inner_smul_right] + -- a witness with `T x₀ ≠ 0`. + obtain ⟨x₀, hx₀⟩ : ∃ x, T x ≠ 0 := by + by_contra h; simp only [not_exists, not_not] at h + exact hT0 (ContinuousLinearMap.ext fun x => by simp [h x]) + -- `‖T x‖² = c.re ‖x‖²`, so `c.re =: r > 0`. + have hnorm2 : ∀ x : H₁, ‖T x‖ ^ 2 = RCLike.re c * ‖x‖ ^ 2 := by + intro x + have h0 := congrArg RCLike.re (hcT x) + rwa [RCLike.mul_re, inner_self_im, mul_zero, sub_zero, inner_self_eq_norm_sq, + inner_self_eq_norm_sq] at h0 + set r : ℝ := RCLike.re c with hr_def + have hr_pos : 0 < r := by + have := hnorm2 x₀ + have hx₀0 : x₀ ≠ 0 := fun h => hx₀ (by rw [h, map_zero]) + have hxpos : (0:ℝ) < ‖x₀‖ ^ 2 := pow_pos (norm_pos_iff.mpr hx₀0) 2 + have hTpos : (0:ℝ) < ‖T x₀‖ ^ 2 := pow_pos (norm_pos_iff.mpr hx₀) 2 + nlinarith [this, hxpos, hTpos] + have hsr : 0 < Real.sqrt r := Real.sqrt_pos.mpr hr_pos + have hnorm : ∀ x : H₁, ‖T x‖ = Real.sqrt r * ‖x‖ := by + intro x + rw [← Real.sqrt_sq (norm_nonneg (T x)), hnorm2 x, Real.sqrt_mul hr_pos.le, + Real.sqrt_sq (norm_nonneg x)] + -- the rescaled isometry. + have hfnorm : ∀ x : H₁, ‖((Real.sqrt r)⁻¹ : ℂ) • T x‖ = ‖x‖ := by + intro x + rw [norm_smul, norm_inv, Complex.norm_real, Real.norm_of_nonneg (Real.sqrt_nonneg r), + hnorm x, ← mul_assoc, inv_mul_cancel₀ (ne_of_gt hsr), one_mul] + -- `T` is surjective (from `T T⋆ = d • 1`, `d ≠ 0`). + have hdT : ∀ y : H₂, + inner ℂ ((ContinuousLinearMap.adjoint T) y) ((ContinuousLinearMap.adjoint T) y) + = d * inner ℂ y y := by + intro y + rw [← ContinuousLinearMap.adjoint_inner_right (ContinuousLinearMap.adjoint T) y + ((ContinuousLinearMap.adjoint T) y), ContinuousLinearMap.adjoint_adjoint] + change inner ℂ y ((T.comp (ContinuousLinearMap.adjoint T)) y) = d * inner ℂ y y + rw [hd] + simp [inner_smul_right] + have hd0 : d ≠ 0 := by + obtain ⟨y, hy⟩ : ∃ y, (ContinuousLinearMap.adjoint T) y ≠ 0 := by + by_contra h; simp only [not_exists, not_not] at h + have hadj : ContinuousLinearMap.adjoint T = 0 := + ContinuousLinearMap.ext fun x => by simp [h x] + exact hx₀ (by rw [← ContinuousLinearMap.adjoint_adjoint T, hadj]; simp) + intro hdz + have hz := hdT y + rw [hdz, zero_mul] at hz + exact hy (inner_self_eq_zero.mp hz) + have hTsurj : Function.Surjective T := by + intro y + refine ⟨d⁻¹ • (ContinuousLinearMap.adjoint T) y, ?_⟩ + rw [map_smul] + have : T ((ContinuousLinearMap.adjoint T) y) = d • y := by + have h' : T ((ContinuousLinearMap.adjoint T) y) + = (T.comp (ContinuousLinearMap.adjoint T)) y := rfl + rw [h', hd]; simp + rw [this, smul_smul, inv_mul_cancel₀ hd0, one_smul] + -- bundle the isometry and its surjectivity. + let fLI : H₁ →ₗᵢ[ℂ] H₂ := + { toLinearMap := ((Real.sqrt r)⁻¹ : ℂ) • (T : H₁ →ₗ[ℂ] H₂) + norm_map' := hfnorm } + have hfsurj : Function.Surjective fLI := by + intro y + obtain ⟨x, hx⟩ := hTsurj (((Real.sqrt r) : ℂ) • y) + refine ⟨x, ?_⟩ + change ((Real.sqrt r)⁻¹ : ℂ) • T x = y + rw [hx, smul_smul] + rw [← Complex.ofReal_inv, ← Complex.ofReal_mul, inv_mul_cancel₀ (ne_of_gt hsr), + Complex.ofReal_one, one_smul] + refine ⟨LinearIsometryEquiv.ofSurjective fLI hfsurj, fun a x => ?_⟩ + rw [LinearIsometryEquiv.coe_ofSurjective] + change ((Real.sqrt r)⁻¹ : ℂ) • T (π₁ a x) = π₂ a (((Real.sqrt r)⁻¹ : ℂ) • T x) + rw [hT a x, map_smul] + +/-- **The irreducible dichotomy.** Two irreducible representations are either disjoint +or unitarily equivalent. -/ +theorem areDisjoint_or_unitaryEquiv_of_isIrreducible + (h1 : IsIrreducible π₁) (h2 : IsIrreducible π₂) : + AreDisjoint π₁ π₂ ∨ UnitaryEquiv π₁ π₂ := by + by_cases hd : AreDisjoint π₁ π₂ + · exact Or.inl hd + · refine Or.inr ?_ + rw [AreDisjoint] at hd + obtain ⟨T, hT'⟩ := not_forall.mp hd + obtain ⟨hT, hT0⟩ := Classical.not_imp.mp hT' + exact UnitaryEquiv.of_intertwines_of_isIrreducible h1 h2 hT hT0 + +/-- **Schur multiplicity.** The space of intertwiners between two irreducible +representations is at most one-dimensional: any two intertwiners with `S ≠ 0` are +proportional, `T = λ • S`. -/ +theorem eq_smul_of_intertwines_of_isIrreducible + (h1 : IsIrreducible π₁) (h2 : IsIrreducible π₂) + {S T : H₁ →L[ℂ] H₂} (hS : Intertwines π₁ π₂ S) (hT : Intertwines π₁ π₂ T) + (hS0 : S ≠ 0) : ∃ lam : ℂ, T = lam • S := by + obtain ⟨a, ha⟩ := h1 ((ContinuousLinearMap.adjoint S).comp S) + (fun x => ContinuousLinearMap.ext fun y => ((hS.adjoint.comp hS) x y).symm) + obtain ⟨b, hb⟩ := h1 ((ContinuousLinearMap.adjoint S).comp T) + (fun x => ContinuousLinearMap.ext fun y => ((hS.adjoint.comp hT) x y).symm) + obtain ⟨c, hc⟩ := h2 (S.comp (ContinuousLinearMap.adjoint S)) + (fun x => ContinuousLinearMap.ext fun y => ((hS.comp hS.adjoint) x y).symm) + obtain ⟨x₀, hx₀⟩ : ∃ x, S x ≠ 0 := by + by_contra h; simp only [not_exists, not_not] at h + exact hS0 (ContinuousLinearMap.ext fun x => by simp [h x]) + have ha0 : a ≠ 0 := by + intro haz + apply hx₀ + refine (inner_self_eq_zero (𝕜 := ℂ)).mp ?_ + rw [← ContinuousLinearMap.adjoint_inner_right S x₀ (S x₀)] + change inner ℂ x₀ (((ContinuousLinearMap.adjoint S).comp S) x₀) = 0 + rw [ha, haz]; simp + have hc0 : c ≠ 0 := by + obtain ⟨y, hy⟩ : ∃ y, (ContinuousLinearMap.adjoint S) y ≠ 0 := by + by_contra h; simp only [not_exists, not_not] at h + have hadj : ContinuousLinearMap.adjoint S = 0 := + ContinuousLinearMap.ext fun x => by simp [h x] + exact hx₀ (by rw [← ContinuousLinearMap.adjoint_adjoint S, hadj]; simp) + intro hcz + apply hy + refine (inner_self_eq_zero (𝕜 := ℂ)).mp ?_ + rw [← ContinuousLinearMap.adjoint_inner_right (ContinuousLinearMap.adjoint S) y + ((ContinuousLinearMap.adjoint S) y), ContinuousLinearMap.adjoint_adjoint] + change inner ℂ y ((S.comp (ContinuousLinearMap.adjoint S)) y) = 0 + rw [hc, hcz]; simp + refine ⟨b / a, ?_⟩ + -- `S⋆` is injective (from `S S⋆ = c • 1`, `c ≠ 0`). + have hSadj_inj : Function.Injective (ContinuousLinearMap.adjoint S) := by + intro u v huv + have happ : (S.comp (ContinuousLinearMap.adjoint S)) u + = (S.comp (ContinuousLinearMap.adjoint S)) v := by + rw [ContinuousLinearMap.comp_apply, ContinuousLinearMap.comp_apply, huv] + rw [hc] at happ + simp only [ContinuousLinearMap.smul_apply, ContinuousLinearMap.one_apply] at happ + have hcuv : c • (u - v) = 0 := by rw [smul_sub, happ, sub_self] + rcases smul_eq_zero.mp hcuv with h | h + · exact absurd h hc0 + · exact sub_eq_zero.mp h + -- `S⋆ ((T − (b/a) • S) x) = 0`, so by injectivity `T = (b/a) • S`. + have hkey : ∀ x, (ContinuousLinearMap.adjoint S) ((T - (b / a) • S) x) = 0 := by + intro x + have hTx : (ContinuousLinearMap.adjoint S) (T x) = b • x := by + have := DFunLike.congr_fun hb x + simpa using this + have hSx : (ContinuousLinearMap.adjoint S) (S x) = a • x := by + have := DFunLike.congr_fun ha x + simpa using this + rw [ContinuousLinearMap.sub_apply, ContinuousLinearMap.smul_apply, map_sub, map_smul, + hTx, hSx, smul_smul, div_mul_cancel₀ b ha0, sub_self] + have hzero : T - (b / a) • S = 0 := by + ext x + have hx := hkey x + rw [← map_zero (ContinuousLinearMap.adjoint S)] at hx + simpa using hSadj_inj hx + exact sub_eq_zero.mp hzero + +/-! ### The endomorphism algebra of an irreducible representation -/ + +/-- A self-intertwiner is exactly an operator in the commutant of the representation. -/ +theorem intertwines_self_iff_mem_centralizer {π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {T : H₁ →L[ℂ] H₁} : Intertwines π π T ↔ T ∈ Set.centralizer (Set.range π) := by + rw [Set.mem_centralizer_iff] + constructor + · rintro h _ ⟨a, rfl⟩ + ext x + simpa only [ContinuousLinearMap.mul_apply] using (h a x).symm + · intro h a x + simpa only [ContinuousLinearMap.mul_apply] using + (DFunLike.congr_fun (h (π a) ⟨a, rfl⟩) x).symm + +/-- **The endomorphism algebra of an irreducible representation is `ℂ · 1`.** Every +self-intertwiner of an irreducible representation is a scalar multiple of the +identity. -/ +theorem intertwines_self_iff_isScalar {π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + (h : IsIrreducible π) {T : H₁ →L[ℂ] H₁} : + Intertwines π π T ↔ ∃ c : ℂ, T = c • 1 := by + rw [intertwines_self_iff_mem_centralizer, isIrreducible_iff_centralizer.mp h] + exact Iff.rfl + +/-! ### The pure-state dichotomy -/ + +/-- **The pure-state dichotomy.** The GNS representations of two pure states are +either disjoint or unitarily equivalent. Pure states thus fall into superselection +sectors: the sector of a pure state is the unitary-equivalence class of its +(irreducible) GNS representation. -/ +theorem exists_gns_areDisjoint_or_unitaryEquiv_of_isPure.{u} {A : Type u} [CStarAlgebra A] + {ω₁ ω₂ : State A} (h1 : IsPure ω₁) (h2 : IsPure ω₂) : + ∃ (K₁ : Type u) (_ : NormedAddCommGroup K₁) (_ : InnerProductSpace ℂ K₁) + (_ : CompleteSpace K₁) (π₁ : A →⋆ₐ[ℂ] (K₁ →L[ℂ] K₁)) (Ω₁ : K₁) + (K₂ : Type u) (_ : NormedAddCommGroup K₂) (_ : InnerProductSpace ℂ K₂) + (_ : CompleteSpace K₂) (π₂ : A →⋆ₐ[ℂ] (K₂ →L[ℂ] K₂)) (Ω₂ : K₂), + (∀ a : A, (ω₁ a : ℂ) = ⟪Ω₁, π₁ a Ω₁⟫_ℂ) ∧ + (∀ a : A, (ω₂ a : ℂ) = ⟪Ω₂, π₂ a Ω₂⟫_ℂ) ∧ + (AreDisjoint π₁ π₂ ∨ UnitaryEquiv π₁ π₂) := by + obtain ⟨K₁, i1, i2, i3, π₁, Ω₁, hcyc₁, hrep₁, _⟩ := gns_construction ω₁ + obtain ⟨K₂, j1, j2, j3, π₂, Ω₂, hcyc₂, hrep₂, _⟩ := gns_construction ω₂ + refine ⟨K₁, i1, i2, i3, π₁, Ω₁, K₂, j1, j2, j3, π₂, Ω₂, hrep₁, hrep₂, ?_⟩ + exact areDisjoint_or_unitaryEquiv_of_isIrreducible + ((isPure_iff_isIrreducible hcyc₁ hrep₁).mp h1) + ((isPure_iff_isIrreducible hcyc₂ hrep₂).mp h2) + +/-! ### Quasi-equivalence -/ + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +theorem conjCLM_add (U : H₁ ≃ₗᵢ[ℂ] H₂) (S T : H₁ →L[ℂ] H₁) : + conjCLM U (S + T) = conjCLM U S + conjCLM U T := by + ext x; simp [map_add] + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +theorem conjCLM_mul (U : H₁ ≃ₗᵢ[ℂ] H₂) (S T : H₁ →L[ℂ] H₁) : + conjCLM U (S * T) = conjCLM U S * conjCLM U T := by + ext x + simp only [conjCLM_apply, ContinuousLinearMap.mul_apply, + LinearIsometryEquiv.symm_apply_apply] + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +theorem conjCLM_smul (U : H₁ ≃ₗᵢ[ℂ] H₂) (c : ℂ) (T : H₁ →L[ℂ] H₁) : + conjCLM U (c • T) = c • conjCLM U T := by + ext x; simp [map_smul] + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +theorem conjCLM_leftInv (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : + conjCLM U.symm (conjCLM U T) = T := by + ext x; simp + +/-- Conjugation by a unitary preserves the adjoint (star). -/ +theorem conjCLM_star (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : + conjCLM U (star T) = star (conjCLM U T) := by + conv_rhs => rw [ContinuousLinearMap.star_eq_adjoint] + rw [ContinuousLinearMap.eq_adjoint_iff] + intro x y + rw [conjCLM_apply, conjCLM_apply, ContinuousLinearMap.star_eq_adjoint] + calc ⟪U (ContinuousLinearMap.adjoint T (U.symm x)), y⟫_ℂ + = ⟪U (ContinuousLinearMap.adjoint T (U.symm x)), U (U.symm y)⟫_ℂ := by + rw [LinearIsometryEquiv.apply_symm_apply] + _ = ⟪ContinuousLinearMap.adjoint T (U.symm x), U.symm y⟫_ℂ := + LinearIsometryEquiv.inner_map_map U _ _ + _ = ⟪U.symm x, T (U.symm y)⟫_ℂ := + ContinuousLinearMap.adjoint_inner_left T (U.symm y) (U.symm x) + _ = ⟪U (U.symm x), U (T (U.symm y))⟫_ℂ := + (LinearIsometryEquiv.inner_map_map U _ _).symm + _ = ⟪x, U (T (U.symm y))⟫_ℂ := by rw [LinearIsometryEquiv.apply_symm_apply] + +/-- Conjugation by a unitary as a `*`-algebra isomorphism of the operator +algebras. -/ +noncomputable def conjStarAlgEquiv (U : H₁ ≃ₗᵢ[ℂ] H₂) : + (H₁ →L[ℂ] H₁) ≃⋆ₐ[ℂ] (H₂ →L[ℂ] H₂) where + toFun := conjCLM U + invFun := conjCLM U.symm + left_inv T := by ext x; simp + right_inv S := by ext x; simp + map_mul' := conjCLM_mul U + map_add' := conjCLM_add U + map_smul' := conjCLM_smul U + map_star' := conjCLM_star U + +@[simp] theorem conjStarAlgEquiv_apply (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : + conjStarAlgEquiv U T = conjCLM U T := rfl + +@[simp] theorem conjStarAlgEquiv_symm_apply (U : H₁ ≃ₗᵢ[ℂ] H₂) (S : H₂ →L[ℂ] H₂) : + (conjStarAlgEquiv U).symm S = conjCLM U.symm S := rfl + +/-- A `*`-isomorphism carrying the underlying set of one star-subalgebra onto that +of another restricts to a `*`-isomorphism between them (cross-space form). -/ +def restrictStarAlgEquiv' {B C : Type*} + [Ring B] [StarRing B] [Algebra ℂ B] [StarModule ℂ B] + [Ring C] [StarRing C] [Algebra ℂ C] [StarModule ℂ C] + (e : B ≃⋆ₐ[ℂ] C) {S : StarSubalgebra ℂ B} {T : StarSubalgebra ℂ C} + (hfwd : ∀ x ∈ S, e x ∈ T) (hbwd : ∀ y ∈ T, e.symm y ∈ S) : S ≃⋆ₐ[ℂ] T where + toFun x := ⟨e x, hfwd x x.2⟩ + invFun y := ⟨e.symm y, hbwd y y.2⟩ + left_inv x := Subtype.ext (by simp) + right_inv y := Subtype.ext (by simp) + map_mul' x y := Subtype.ext (by simp) + map_add' x y := Subtype.ext (by simp) + map_smul' r x := Subtype.ext (by simp) + map_star' x := Subtype.ext (map_star e _) + +theorem coe_gnsVonNeumann_toStarSubalgebra (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : + ((gnsVonNeumannAlgebra π).toStarSubalgebra : Set (H₁ →L[ℂ] H₁)) = gnsVonNeumann π := + coe_gnsVonNeumannAlgebra π + +/-- The generators `π(a)` lie in the generated von Neumann algebra `π(A)''`. -/ +theorem pi_mem_gnsVonNeumann (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) (a : A) : + π a ∈ (gnsVonNeumannAlgebra π).toStarSubalgebra := by + rw [← SetLike.mem_coe, coe_gnsVonNeumann_toStarSubalgebra] + unfold gnsVonNeumann + exact Set.mem_centralizer_iff.mpr + (fun M hM => (Set.mem_centralizer_iff.mp hM (π a) ⟨a, rfl⟩).symm) + +/-- Two representations are **quasi-equivalent** when there is a `*`-isomorphism of +their generated von Neumann algebras carrying `π₁(a)` to `π₂(a)`. -/ +def QuasiEquiv (π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) (π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)) : + Prop := + ∃ Φ : (gnsVonNeumannAlgebra π₁).toStarSubalgebra + ≃⋆ₐ[ℂ] (gnsVonNeumannAlgebra π₂).toStarSubalgebra, + ∀ a : A, (Φ ⟨π₁ a, pi_mem_gnsVonNeumann π₁ a⟩ : H₂ →L[ℂ] H₂) = π₂ a + +/-- Quasi-equivalence is reflexive. -/ +theorem QuasiEquiv.refl (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : QuasiEquiv π π := + ⟨StarAlgEquiv.refl, fun _ => rfl⟩ + +/-- Quasi-equivalence is symmetric. -/ +theorem QuasiEquiv.symm (h : QuasiEquiv π₁ π₂) : QuasiEquiv π₂ π₁ := by + obtain ⟨Φ, hΦ⟩ := h + refine ⟨Φ.symm, fun a => ?_⟩ + have hstep : Φ ⟨π₁ a, pi_mem_gnsVonNeumann π₁ a⟩ + = ⟨π₂ a, pi_mem_gnsVonNeumann π₂ a⟩ := Subtype.ext (hΦ a) + rw [← hstep, StarAlgEquiv.symm_apply_apply] + +/-- Quasi-equivalence is transitive. -/ +theorem QuasiEquiv.trans (h₁₂ : QuasiEquiv π₁ π₂) (h₂₃ : QuasiEquiv π₂ π₃) : + QuasiEquiv π₁ π₃ := by + obtain ⟨Φ, hΦ⟩ := h₁₂ + obtain ⟨Ψ, hΨ⟩ := h₂₃ + refine ⟨Φ.trans Ψ, fun a => ?_⟩ + have hstep : Φ ⟨π₁ a, pi_mem_gnsVonNeumann π₁ a⟩ + = ⟨π₂ a, pi_mem_gnsVonNeumann π₂ a⟩ := Subtype.ext (hΦ a) + rw [StarAlgEquiv.trans_apply, hstep] + exact hΨ a + +/-- **Unitary equivalence implies quasi-equivalence.** The conjugation +`*`-isomorphism restricts to a `*`-isomorphism of the generated von Neumann +algebras carrying `π₁(a)` to `π₂(a)`. -/ +theorem UnitaryEquiv.quasiEquiv (h : UnitaryEquiv π₁ π₂) : QuasiEquiv π₁ π₂ := by + obtain ⟨U, hU⟩ := h + have hfwd : ∀ x ∈ (gnsVonNeumannAlgebra π₁).toStarSubalgebra, + conjStarAlgEquiv U x ∈ (gnsVonNeumannAlgebra π₂).toStarSubalgebra := by + intro T hT + rw [← SetLike.mem_coe, coe_gnsVonNeumann_toStarSubalgebra] at hT ⊢ + rw [conjStarAlgEquiv_apply, conjMulEquiv_image_gnsVonNeumann hU] + exact ⟨T, hT, (conjMulEquiv_apply U T)⟩ + have hbwd : ∀ y ∈ (gnsVonNeumannAlgebra π₂).toStarSubalgebra, + (conjStarAlgEquiv U).symm y ∈ (gnsVonNeumannAlgebra π₁).toStarSubalgebra := by + intro S hS + rw [← SetLike.mem_coe, coe_gnsVonNeumann_toStarSubalgebra] at hS ⊢ + rw [conjMulEquiv_image_gnsVonNeumann hU] at hS + obtain ⟨T, hT, rfl⟩ := hS + rw [conjStarAlgEquiv_symm_apply, conjMulEquiv_apply, conjCLM_leftInv] + exact hT + refine ⟨restrictStarAlgEquiv' (conjStarAlgEquiv U) hfwd hbwd, fun a => ?_⟩ + change conjStarAlgEquiv U (π₁ a) = π₂ a + rw [conjStarAlgEquiv_apply, ← conjMulEquiv_apply] + exact conjMulEquiv_pi hU a + +end GNS +end Physicslib4 diff --git a/Physicslib4/GNS/UnitaryEquiv.lean b/Physicslib4/GNS/UnitaryEquiv.lean new file mode 100644 index 0000000..6647b11 --- /dev/null +++ b/Physicslib4/GNS/UnitaryEquiv.lean @@ -0,0 +1,210 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Physicslib4.GNS.Irreducibility +import Physicslib4.Operators.Conjugation + +/-! +# Unitary equivalence of representations + +Two `*`-representations `π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)` and +`π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)` are **unitarily equivalent** when there is a +Hilbert-space isometric isomorphism `U : H₁ ≃ₗᵢ[ℂ] H₂` intertwining them: +`U (π₁ a x) = π₂ a (U x)`. This is the basic equivalence of the representation +theory underlying superselection sectors. + +This file defines `UnitaryEquiv`, proves it is an equivalence relation +(reflexive, symmetric, transitive), and shows that the two central +representation-theoretic properties — **irreducibility** and **factoriality** +(trivial center of the generated von Neumann algebra) — are invariants of unitary +equivalence. The transport is packaged through the cross-space conjugation +`conjMulEquiv U : (H₁ →L[ℂ] H₁) ≃* (H₂ →L[ℂ] H₂)`, `T ↦ U T U⁻¹`, which carries +`π₁(A)` onto `π₂(A)`, centralizers onto centralizers, and scalars onto scalars. +-/ + +namespace Physicslib4 +namespace GNS + +variable {A : Type*} [CStarAlgebra A] +variable {H₁ : Type*} [NormedAddCommGroup H₁] [InnerProductSpace ℂ H₁] [CompleteSpace H₁] +variable {H₂ : Type*} [NormedAddCommGroup H₂] [InnerProductSpace ℂ H₂] [CompleteSpace H₂] +variable {H₃ : Type*} [NormedAddCommGroup H₃] [InnerProductSpace ℂ H₃] [CompleteSpace H₃] + +/-- Two `*`-representations of `A` are **unitarily equivalent** when an isometric +isomorphism of the underlying Hilbert spaces intertwines them. -/ +def UnitaryEquiv (π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) (π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)) : + Prop := + ∃ U : H₁ ≃ₗᵢ[ℂ] H₂, ∀ (a : A) (x : H₁), U (π₁ a x) = π₂ a (U x) + +/-! ### Equivalence relation -/ + +/-- Unitary equivalence is reflexive. -/ +theorem UnitaryEquiv.refl (π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)) : UnitaryEquiv π π := + ⟨LinearIsometryEquiv.refl ℂ H₁, fun _ _ => rfl⟩ + +/-- Unitary equivalence is symmetric. -/ +theorem UnitaryEquiv.symm {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} (h : UnitaryEquiv π₁ π₂) : UnitaryEquiv π₂ π₁ := by + obtain ⟨U, hU⟩ := h + refine ⟨U.symm, fun a y => U.injective ?_⟩ + rw [LinearIsometryEquiv.apply_symm_apply, hU, LinearIsometryEquiv.apply_symm_apply] + +/-- Unitary equivalence is transitive. -/ +theorem UnitaryEquiv.trans {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} {π₃ : A →⋆ₐ[ℂ] (H₃ →L[ℂ] H₃)} + (h₁₂ : UnitaryEquiv π₁ π₂) (h₂₃ : UnitaryEquiv π₂ π₃) : UnitaryEquiv π₁ π₃ := by + obtain ⟨U, hU⟩ := h₁₂ + obtain ⟨V, hV⟩ := h₂₃ + refine ⟨U.trans V, fun a x => ?_⟩ + simp only [LinearIsometryEquiv.trans_apply] + rw [hU, hV] + +/-! ### Cross-space conjugation of operators -/ + +/-- Conjugation of an operator `T : H₁ →L H₁` by a unitary `U : H₁ ≃ₗᵢ H₂`, +producing `U T U⁻¹ : H₂ →L H₂`. -/ +noncomputable def conjCLM (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : H₂ →L[ℂ] H₂ := + (↑U.toContinuousLinearEquiv : H₁ →L[ℂ] H₂).comp + (T.comp (↑U.symm.toContinuousLinearEquiv : H₂ →L[ℂ] H₁)) + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +@[simp] theorem conjCLM_apply (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) (x : H₂) : + conjCLM U T x = U (T (U.symm x)) := by + simp [conjCLM, ContinuousLinearMap.comp_apply, ContinuousLinearEquiv.coe_coe, + LinearIsometryEquiv.coe_toContinuousLinearEquiv] + +/-- Conjugation by `U` as a multiplicative isomorphism of operator algebras +`(H₁ →L H₁) ≃* (H₂ →L H₂)`. -/ +noncomputable def conjMulEquiv (U : H₁ ≃ₗᵢ[ℂ] H₂) : + (H₁ →L[ℂ] H₁) ≃* (H₂ →L[ℂ] H₂) where + toFun := conjCLM U + invFun := conjCLM U.symm + left_inv T := by ext x; simp + right_inv S := by ext x; simp + map_mul' S T := by + ext x; simp [ContinuousLinearMap.mul_apply] + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +@[simp] theorem conjMulEquiv_apply (U : H₁ ≃ₗᵢ[ℂ] H₂) (T : H₁ →L[ℂ] H₁) : + conjMulEquiv U T = conjCLM U T := rfl + +/-- The general fact that a multiplicative isomorphism carries centralizers to +centralizers. -/ +theorem mulEquiv_image_centralizer {M N : Type*} [Monoid M] [Monoid N] (e : M ≃* N) + (s : Set M) : e '' Set.centralizer s = Set.centralizer (e '' s) := by + ext y + simp only [Set.mem_image, Set.mem_centralizer_iff] + constructor + · rintro ⟨x, hx, rfl⟩ _ ⟨m, hm, rfl⟩ + rw [← map_mul, ← map_mul, hx m hm] + · intro hy + refine ⟨e.symm y, fun m hm => ?_, e.apply_symm_apply y⟩ + apply e.injective + rw [map_mul, map_mul, e.apply_symm_apply] + exact hy (e m) ⟨m, hm, rfl⟩ + +/-- Conjugation carries `π₁(a)` to `π₂(a)` when `U` intertwines the two +representations. -/ +theorem conjMulEquiv_pi {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} {U : H₁ ≃ₗᵢ[ℂ] H₂} + (hU : ∀ (a : A) (x : H₁), U (π₁ a x) = π₂ a (U x)) (a : A) : + conjMulEquiv U (π₁ a) = π₂ a := by + ext x + rw [conjMulEquiv_apply, conjCLM_apply, hU, LinearIsometryEquiv.apply_symm_apply] + +/-- Conjugation carries the image of `π₁` onto the image of `π₂`. -/ +theorem conjMulEquiv_image_range {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} {U : H₁ ≃ₗᵢ[ℂ] H₂} + (hU : ∀ (a : A) (x : H₁), U (π₁ a x) = π₂ a (U x)) : + conjMulEquiv U '' Set.range π₁ = Set.range π₂ := by + ext S + simp only [Set.mem_image, Set.mem_range] + constructor + · rintro ⟨_, ⟨a, rfl⟩, rfl⟩ + exact ⟨a, (conjMulEquiv_pi hU a).symm⟩ + · rintro ⟨a, rfl⟩ + exact ⟨π₁ a, ⟨a, rfl⟩, conjMulEquiv_pi hU a⟩ + +omit [CompleteSpace H₁] [CompleteSpace H₂] in +/-- Conjugation fixes the scalar operators setwise. -/ +theorem conjMulEquiv_image_scalar (U : H₁ ≃ₗᵢ[ℂ] H₂) : + conjMulEquiv U '' scalarOperators H₁ = scalarOperators H₂ := by + have hfix : ∀ c : ℂ, conjMulEquiv U (c • 1) = c • 1 := by + intro c + ext x + rw [conjMulEquiv_apply, conjCLM_apply] + simp [map_smul] + ext S + simp only [scalarOperators, Set.mem_image, Set.mem_setOf_eq] + constructor + · rintro ⟨_, ⟨c, rfl⟩, rfl⟩ + exact ⟨c, hfix c⟩ + · rintro ⟨c, rfl⟩ + exact ⟨c • 1, ⟨c, rfl⟩, hfix c⟩ + +/-! ### Invariance of irreducibility and factoriality -/ + +/-- Irreducibility is exactly triviality of the commutant: the commutant of the +image `π(A)` is the scalar operators. -/ +theorem isIrreducible_iff_centralizer {π : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} : + IsIrreducible π ↔ Set.centralizer (Set.range π) = scalarOperators H₁ := by + constructor + · intro hirr + refine Set.Subset.antisymm (fun T hT => hirr T ?_) ?_ + · exact fun a => Set.mem_centralizer_iff.mp hT (π a) ⟨a, rfl⟩ + · rintro _ ⟨c, rfl⟩ + exact Set.mem_centralizer_iff.mpr fun M _ => by + rw [mul_smul_comm, smul_mul_assoc, mul_one, one_mul] + · intro hcent T hT + have hmem : T ∈ Set.centralizer (Set.range π) := + Set.mem_centralizer_iff.mpr (by rintro _ ⟨a, rfl⟩; exact hT a) + rw [hcent] at hmem + exact hmem + +/-- **Irreducibility is a unitary invariant.** If `π₁` is unitarily equivalent to +`π₂` and `π₁` is irreducible, then so is `π₂`. -/ +theorem UnitaryEquiv.isIrreducible {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} (h : UnitaryEquiv π₁ π₂) + (hirr : IsIrreducible π₁) : IsIrreducible π₂ := by + obtain ⟨U, hU⟩ := h + rw [isIrreducible_iff_centralizer] at hirr ⊢ + rw [← conjMulEquiv_image_range hU, ← mulEquiv_image_centralizer, hirr, + conjMulEquiv_image_scalar] + +/-- **Irreducibility is invariant under unitary equivalence** (iff form). -/ +theorem UnitaryEquiv.isIrreducible_iff {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} (h : UnitaryEquiv π₁ π₂) : + IsIrreducible π₁ ↔ IsIrreducible π₂ := + ⟨h.isIrreducible, h.symm.isIrreducible⟩ + +/-- Conjugation carries the generated von Neumann algebra of `π₁` onto that of +`π₂`. -/ +theorem conjMulEquiv_image_gnsVonNeumann {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} {U : H₁ ≃ₗᵢ[ℂ] H₂} + (hU : ∀ (a : A) (x : H₁), U (π₁ a x) = π₂ a (U x)) : + gnsVonNeumann π₂ = conjMulEquiv U '' gnsVonNeumann π₁ := by + unfold gnsVonNeumann + rw [← conjMulEquiv_image_range hU, ← mulEquiv_image_centralizer, + ← mulEquiv_image_centralizer] + +/-- **Factoriality is a unitary invariant.** If `π₁` is unitarily equivalent to +`π₂` and the von Neumann algebra `π₁(A)''` is a factor, then so is `π₂(A)''`. -/ +theorem UnitaryEquiv.isFactor {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} (h : UnitaryEquiv π₁ π₂) + (hf : IsFactor (gnsVonNeumann π₁)) : IsFactor (gnsVonNeumann π₂) := by + obtain ⟨U, hU⟩ := h + rw [conjMulEquiv_image_gnsVonNeumann hU] + unfold IsFactor at hf ⊢ + rw [← mulEquiv_image_centralizer, ← Set.image_inter (conjMulEquiv U).injective, hf, + conjMulEquiv_image_scalar] + +/-- **Factoriality is invariant under unitary equivalence** (iff form). -/ +theorem UnitaryEquiv.isFactor_iff {π₁ : A →⋆ₐ[ℂ] (H₁ →L[ℂ] H₁)} + {π₂ : A →⋆ₐ[ℂ] (H₂ →L[ℂ] H₂)} (h : UnitaryEquiv π₁ π₂) : + IsFactor (gnsVonNeumann π₁) ↔ IsFactor (gnsVonNeumann π₂) := + ⟨h.isFactor, h.symm.isFactor⟩ + +end GNS +end Physicslib4 diff --git a/Physicslib4/Operators/LpDiagonal.lean b/Physicslib4/Operators/LpDiagonal.lean new file mode 100644 index 0000000..af2420d --- /dev/null +++ b/Physicslib4/Operators/LpDiagonal.lean @@ -0,0 +1,136 @@ +/- +Copyright (c) 2026 Lean Community. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Lean Community +-/ +import Mathlib.Analysis.InnerProductSpace.l2Space +import Mathlib.Analysis.InnerProductSpace.Adjoint + +/-! +# The diagonal operator on an ℓ² direct sum + +Given a family of Hilbert spaces `E i` and a uniformly bounded family of operators +`T i : E i →L[𝕜] E i`, the **diagonal operator** `lpDiag T` acts on the ℓ²-direct +sum `lp E 2` coordinatewise: `(lpDiag T x) i = T i (x i)`. It is built from +`Memℓp.mono'` (well-definedness) and `LinearMap.mkContinuous` (the operator-norm +bound `‖lpDiag T‖ ≤ K`). + +This file records the `*`-algebra-hom laws of the diagonal operator, as a function +of the family: + +* `lpDiag_apply_coe` — the coordinate action; +* `lpDiag_congr` — the operator is independent of the chosen bound; +* `lpDiag_one`, `lpDiag_mul`, `lpDiag_add`, `lpDiag_smul` — the unital, multiplicative, + additive, and `𝕜`-linear laws; +* `lpDiag_star` — the adjoint of a diagonal is the diagonal of adjoints. + +These are the pieces from which a direct-sum `*`-representation `⊕ᵢ πᵢ` is assembled +(the diagonal operator of `fun i ↦ πᵢ a`, uniformly bounded by `‖a‖`). The file is +spacetime/AQFT-agnostic. +-/ + +open scoped InnerProductSpace ENNReal + +namespace Physicslib4 + +variable {𝕜 : Type*} [RCLike 𝕜] +variable {ι : Type*} {E : ι → Type*} + [∀ i, NormedAddCommGroup (E i)] [∀ i, InnerProductSpace 𝕜 (E i)] + +/-- Coordinatewise bound: `‖T i (x i)‖ ≤ ‖((K : 𝕜) • x) i‖` for a uniformly bounded +family. -/ +private theorem lpDiag_coord_bound (T : ∀ i, E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) + (hTK : ∀ i, ‖T i‖ ≤ K) (x : lp E 2) (i : ι) : + ‖T i (x i)‖ ≤ ‖((K : 𝕜) • x) i‖ := by + rw [lp.coeFn_smul, Pi.smul_apply, norm_smul, RCLike.norm_ofReal, abs_of_nonneg hK] + exact (T i).le_of_opNorm_le (hTK i) _ + +/-- The **diagonal operator** on the ℓ²-direct sum `lp E 2` induced by a uniformly +bounded family `T i : E i →L[𝕜] E i`, acting coordinatewise. -/ +noncomputable def lpDiag (T : ∀ i, E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) + (hTK : ∀ i, ‖T i‖ ≤ K) : lp E 2 →L[𝕜] lp E 2 := + LinearMap.mkContinuous + { toFun := fun x => + ⟨fun i => T i (x i), + (lp.memℓp ((K : 𝕜) • x)).mono' (lpDiag_coord_bound T hK hTK x)⟩ + map_add' := fun x y => by + ext i + change T i (x i + y i) = T i (x i) + T i (y i) + exact map_add (T i) (x i) (y i) + map_smul' := fun c x => by ext i; simp } + K + (fun x => by + have h : ‖(⟨fun i => T i (x i), + (lp.memℓp ((K : 𝕜) • x)).mono' (lpDiag_coord_bound T hK hTK x)⟩ : lp E 2)‖ + ≤ ‖(K : 𝕜) • x‖ := + lp.norm_mono (by norm_num) (lpDiag_coord_bound T hK hTK x) + rwa [norm_smul, RCLike.norm_ofReal, abs_of_nonneg hK] at h) + +@[simp] theorem lpDiag_apply_coe (T : ∀ i, E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) + (hTK : ∀ i, ‖T i‖ ≤ K) (x : lp E 2) (i : ι) : + (lpDiag T hK hTK x) i = T i (x i) := rfl + +/-- The diagonal operator depends only on the family, not on the chosen bound. -/ +theorem lpDiag_congr (T : ∀ i, E i →L[𝕜] E i) {K K' : ℝ} (hK : 0 ≤ K) (hK' : 0 ≤ K') + (hTK : ∀ i, ‖T i‖ ≤ K) (hTK' : ∀ i, ‖T i‖ ≤ K') : + lpDiag T hK hTK = lpDiag T hK' hTK' := + ContinuousLinearMap.ext fun _ => lp.ext (funext fun _ => rfl) + +/-- Coordinatewise extensionality for operators on `lp E 2`. -/ +theorem lpDiag_ext {F G : lp E 2 →L[𝕜] lp E 2} + (h : ∀ (x : lp E 2) (i : ι), (F x) i = (G x) i) : F = G := + ContinuousLinearMap.ext fun x => lp.ext (funext (h x)) + +/-- Diagonal of the identities is the identity. -/ +theorem lpDiag_one : + lpDiag (fun i => (1 : E i →L[𝕜] E i)) zero_le_one + (fun _ => by rw [ContinuousLinearMap.one_def]; exact ContinuousLinearMap.norm_id_le) + = (1 : lp E 2 →L[𝕜] lp E 2) := by + refine lpDiag_ext fun x i => ?_ + simp + +/-- The diagonal operator is multiplicative: the diagonal of the composites is the +composite of the diagonals. -/ +theorem lpDiag_mul (S T : ∀ i, E i →L[𝕜] E i) {KS KT KST : ℝ} + (hKS : 0 ≤ KS) (hKT : 0 ≤ KT) (hKST : 0 ≤ KST) + (hSK : ∀ i, ‖S i‖ ≤ KS) (hTK : ∀ i, ‖T i‖ ≤ KT) + (hSTK : ∀ i, ‖S i ∘L T i‖ ≤ KST) : + lpDiag (fun i => S i ∘L T i) hKST hSTK = lpDiag S hKS hSK ∘L lpDiag T hKT hTK := by + refine lpDiag_ext fun x i => ?_ + simp + +/-- The diagonal operator is additive. -/ +theorem lpDiag_add (S T : ∀ i, E i →L[𝕜] E i) {KS KT KST : ℝ} + (hKS : 0 ≤ KS) (hKT : 0 ≤ KT) (hKST : 0 ≤ KST) + (hSK : ∀ i, ‖S i‖ ≤ KS) (hTK : ∀ i, ‖T i‖ ≤ KT) + (hSTK : ∀ i, ‖S i + T i‖ ≤ KST) : + lpDiag (fun i => S i + T i) hKST hSTK = lpDiag S hKS hSK + lpDiag T hKT hTK := by + refine lpDiag_ext fun x i => ?_ + change (S i + T i) (x i) = S i (x i) + T i (x i) + exact ContinuousLinearMap.add_apply (S i) (T i) (x i) + +/-- The diagonal operator is `𝕜`-linear in the family. -/ +theorem lpDiag_smul (c : 𝕜) (T : ∀ i, E i →L[𝕜] E i) {K KcT : ℝ} + (hK : 0 ≤ K) (hKcT : 0 ≤ KcT) + (hTK : ∀ i, ‖T i‖ ≤ K) (hcTK : ∀ i, ‖c • T i‖ ≤ KcT) : + lpDiag (fun i => c • T i) hKcT hcTK = c • lpDiag T hK hTK := by + refine lpDiag_ext fun x i => ?_ + simp [lp.coeFn_smul] + +variable [∀ i, CompleteSpace (E i)] + +/-- The adjoint of a diagonal operator is the diagonal of the adjoints. -/ +theorem lpDiag_star (T : ∀ i, E i →L[𝕜] E i) {K : ℝ} (hK : 0 ≤ K) + (hTK : ∀ i, ‖T i‖ ≤ K) : + star (lpDiag T hK hTK) + = lpDiag (fun i => star (T i)) hK (fun i => by rw [norm_star]; exact hTK i) := by + rw [ContinuousLinearMap.star_eq_adjoint] + symm + rw [ContinuousLinearMap.eq_adjoint_iff] + intro x y + rw [lp.inner_eq_tsum, lp.inner_eq_tsum] + refine tsum_congr fun i => ?_ + rw [lpDiag_apply_coe, lpDiag_apply_coe, ContinuousLinearMap.star_eq_adjoint, + ContinuousLinearMap.adjoint_inner_left] + +end Physicslib4 diff --git a/Physicslib4/Spacetime/CausalStructure.lean b/Physicslib4/Spacetime/CausalStructure.lean index 8bd493f..bacce9c 100644 --- a/Physicslib4/Spacetime/CausalStructure.lean +++ b/Physicslib4/Spacetime/CausalStructure.lean @@ -100,6 +100,42 @@ theorem not_isNull_of_isSpacelike {x : M.Carrier} theorem isNull_zero {x : M.Carrier} : M.IsNull (0 : TangentSpace M.model x) := by simp [IsNull] +/-! ### Scaling invariance of the causal classification + +The causal type of a tangent vector depends only on the sign of `g(v,v)`, which +scales quadratically under `v ↦ c • v`. Hence for `c ≠ 0` the timelike / null / +spacelike classification is invariant under scaling — the algebraic fact behind +reparametrisation-invariance of the causal type of a curve. -/ + +/-- The metric square scales quadratically: `g(c•v, c•v) = c² · g(v,v)`. -/ +theorem val_smul_smul {x : M.Carrier} (c : ℝ) (v : TangentSpace M.model x) : + M.val x (c • v) (c • v) = c ^ 2 * M.val x v v := by + simp only [map_smul, ContinuousLinearMap.smul_apply, smul_eq_mul] + ring + +/-- **Scaling invariance of timelikeness.** For `c ≠ 0`, `c • v` is timelike iff +`v` is. -/ +theorem isTimelike_smul_iff {x : M.Carrier} {c : ℝ} (hc : c ≠ 0) + (v : TangentSpace M.model x) : M.IsTimelike (c • v) ↔ M.IsTimelike v := by + have hc2 : 0 < c ^ 2 := by positivity + simp only [IsTimelike, val_smul_smul] + constructor <;> intro h <;> nlinarith [hc2] + +/-- **Scaling invariance of nullness.** For `c ≠ 0`, `c • v` is null iff `v` is. -/ +theorem isNull_smul_iff {x : M.Carrier} {c : ℝ} (hc : c ≠ 0) + (v : TangentSpace M.model x) : M.IsNull (c • v) ↔ M.IsNull v := by + have hc2 : ¬ (c ^ 2 = 0) := pow_ne_zero 2 hc + simp only [IsNull, val_smul_smul, mul_eq_zero] + tauto + +/-- **Scaling invariance of spacelikeness.** For `c ≠ 0`, `c • v` is spacelike iff +`v` is. -/ +theorem isSpacelike_smul_iff {x : M.Carrier} {c : ℝ} (hc : c ≠ 0) + (v : TangentSpace M.model x) : M.IsSpacelike (c • v) ↔ M.IsSpacelike v := by + have hc2 : 0 < c ^ 2 := by positivity + simp only [IsSpacelike, val_smul_smul] + constructor <;> intro h <;> nlinarith [hc2] + /-! ### Time orientation -/ /-- @@ -191,6 +227,62 @@ theorem not_isFuturePointing_and_isPastPointing_of_isTimelike · exact absurd hn (M.not_isNull_of_isTimelike hv) exact lt_asymm hft hpt +/-! ### Positive-scaling invariance of orientation + +Unlike the causal *type* (invariant under any non-zero scaling), future/past- +pointing is preserved only under scaling by a **positive** scalar — scaling by a +negative one swaps the two. This is the algebraic fact behind the +reparametrisation-invariance of the *orientation* of a curve under +orientation-preserving reparametrisations. -/ + +/-- Linearity of the metric in the second argument: `g(t, c • v) = c · g(t, v)`. -/ +theorem val_field_smul (t : M.TimeOrientation) {x : M.Carrier} (c : ℝ) + (v : TangentSpace M.model x) : + M.val x (t.field x) (c • v) = c * M.val x (t.field x) v := by + simp only [map_smul, smul_eq_mul] + +/-- **Positive scaling preserves future-pointing** (forward direction). -/ +theorem isFuturePointing_smul_of (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} + (hc : 0 < c) {v : TangentSpace M.model x} (h : M.IsFuturePointing t v) : + M.IsFuturePointing t (c • v) := by + rcases h with ⟨htl, hlt⟩ | ⟨hnull, vs, hvs, htends⟩ + · exact Or.inl ⟨(M.isTimelike_smul_iff hc.ne' v).mpr htl, by + rw [val_field_smul]; exact mul_neg_of_pos_of_neg hc hlt⟩ + · refine Or.inr ⟨(M.isNull_smul_iff hc.ne' v).mpr hnull, + fun n => c • vs n, fun n => ⟨?_, ?_⟩, htends.const_smul c⟩ + · exact (M.isTimelike_smul_iff hc.ne' (vs n)).mpr (hvs n).1 + · rw [val_field_smul]; exact mul_neg_of_pos_of_neg hc (hvs n).2 + +/-- **Positive-scaling invariance of future-pointing.** For `c > 0`, `c • v` is +future-pointing iff `v` is. -/ +theorem isFuturePointing_smul_iff (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} + (hc : 0 < c) (v : TangentSpace M.model x) : + M.IsFuturePointing t (c • v) ↔ M.IsFuturePointing t v := by + refine ⟨fun h => ?_, M.isFuturePointing_smul_of t hc⟩ + have h' := M.isFuturePointing_smul_of t (inv_pos.mpr hc) h + rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul] at h' + +/-- **Positive scaling preserves past-pointing** (forward direction). -/ +theorem isPastPointing_smul_of (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} + (hc : 0 < c) {v : TangentSpace M.model x} (h : M.IsPastPointing t v) : + M.IsPastPointing t (c • v) := by + rcases h with ⟨htl, hgt⟩ | ⟨hnull, vs, hvs, htends⟩ + · exact Or.inl ⟨(M.isTimelike_smul_iff hc.ne' v).mpr htl, by + rw [val_field_smul]; exact mul_pos hc hgt⟩ + · refine Or.inr ⟨(M.isNull_smul_iff hc.ne' v).mpr hnull, + fun n => c • vs n, fun n => ⟨?_, ?_⟩, htends.const_smul c⟩ + · exact (M.isTimelike_smul_iff hc.ne' (vs n)).mpr (hvs n).1 + · rw [val_field_smul]; exact mul_pos hc (hvs n).2 + +/-- **Positive-scaling invariance of past-pointing.** For `c > 0`, `c • v` is +past-pointing iff `v` is. -/ +theorem isPastPointing_smul_iff (t : M.TimeOrientation) {x : M.Carrier} {c : ℝ} + (hc : 0 < c) (v : TangentSpace M.model x) : + M.IsPastPointing t (c • v) ↔ M.IsPastPointing t v := by + refine ⟨fun h => ?_, M.isPastPointing_smul_of t hc⟩ + have h' := M.isPastPointing_smul_of t (inv_pos.mpr hc) h + rwa [smul_smul, inv_mul_cancel₀ hc.ne', one_smul] at h' + end Spacetime end Physicslib4 diff --git a/Physicslib4/Spacetime/Curves.lean b/Physicslib4/Spacetime/Curves.lean index 4a9f8d5..19b1754 100644 --- a/Physicslib4/Spacetime/Curves.lean +++ b/Physicslib4/Spacetime/Curves.lean @@ -8,7 +8,11 @@ import Physicslib4.Spacetime.CausalStructure import Mathlib.Topology.ContinuousOn import Mathlib.Topology.Connected.Basic import Mathlib.Geometry.Manifold.ContMDiff.Basic +import Mathlib.Geometry.Manifold.ContMDiff.NormedSpace import Mathlib.Geometry.Manifold.MFDeriv.Basic +import Mathlib.Geometry.Manifold.MFDeriv.FDeriv +import Mathlib.Analysis.Calculus.Deriv.Comp +import Mathlib.Analysis.Calculus.Deriv.Basic import Mathlib.Analysis.Calculus.TangentCone.Real import Mathlib.Analysis.Convex.Topology @@ -129,6 +133,116 @@ theorem Path.uniqueDiffOn_parameterSpace (μ : M.Path) : (Set.Ioo_subset_Icc_self.trans (hoc.out hb ha)) exact ⟨(a + b) / 2, hIoo (Set.mem_Ioo.mpr ⟨by linarith, by linarith⟩)⟩ +/-! ### Tangent vector -/ + +/-- The **tangent vector** of a smooth path `μ` at parameter `s`: the manifold +derivative of `μ` along its parameter space, applied to the basis vector `1 : ℝ`. +This is the object all the causal predicates below are phrased in terms of. -/ +noncomputable def SmoothPath.tangent {M : Spacetime} (μ : M.SmoothPath) (s : ℝ) : + TangentSpace M.model (μ.toFun s) := + mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model μ.toFun μ.parameterSpace s (1 : ℝ) + +/-- Unfolding lemma for `SmoothPath.tangent` to the raw `mfderivWithin` form. -/ +theorem SmoothPath.tangent_def {M : Spacetime} (μ : M.SmoothPath) (s : ℝ) : + μ.tangent s + = mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model + μ.toFun μ.parameterSpace s (1 : ℝ) := rfl + +/-- The tangent vector of a smooth path is non-vanishing on the parameter +space (the `nonvanishing` field, restated via `tangent`). -/ +theorem SmoothPath.tangent_ne_zero {M : Spacetime} (μ : M.SmoothPath) {s : ℝ} + (hs : s ∈ μ.parameterSpace) : μ.tangent s ≠ 0 := + μ.nonvanishing s hs + +/-- **Reparametrisation chain rule for the tangent vector.** Composing a smooth +path `μ` with a (manifold-)differentiable reparametrisation `φ : ℝ → ℝ` that maps +`Σ'` into `μ`'s parameter space scales the tangent vector by the derivative of +`φ`: `tangent (μ ∘ φ) s = (φ'(s)) • tangent μ (φ s)`, where the scalar is the +one-dimensional manifold derivative of `φ`. This is the analytic heart of the +reparametrisation-invariance of the causal type of a curve. -/ +theorem SmoothPath.mfderivWithin_comp_reparam {M : Spacetime} (μ : M.SmoothPath) + {φ : ℝ → ℝ} {u : Set ℝ} {s : ℝ} + (hφ : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) + (modelWithCornersSelf ℝ ℝ) φ u s) + (hmaps : Set.MapsTo φ u μ.parameterSpace) + (huniq : UniqueMDiffWithinAt (modelWithCornersSelf ℝ ℝ) u s) + (hs : s ∈ u) : + mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model (μ.toFun ∘ φ) u s (1 : ℝ) + = (derivWithin φ u s) • μ.tangent (φ s) := by + have hg : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) M.model + μ.toFun μ.parameterSpace (φ s) := + (μ.smoothOn (φ s) (hmaps hs)).mdifferentiableWithinAt (by simp) + have hcomp := mfderivWithin_comp s hg hφ hmaps huniq + rw [hcomp] + change mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model μ.toFun μ.parameterSpace (φ s) + (mfderivWithin (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) φ u s (1 : ℝ)) + = derivWithin φ u s • μ.tangent (φ s) + rw [SmoothPath.tangent_def, ← ContinuousLinearMap.map_smul] + congr 1 + rw [mfderivWithin_eq_fderivWithin] + change (fderivWithin ℝ φ u s) 1 = (derivWithin φ u s : ℝ) • (1 : ℝ) + rw [smul_eq_mul, mul_one] + rfl + +/-- **Tangent vector under a reparametrisation.** If a reparametrisation +`φ : ℝ → ℝ` (differentiable, mapping `μ₁`'s parameter space into `μ₂`'s) identifies +the two paths pointwise (`μ₂ (φ s') = μ₁ s'` on `μ₁`'s parameter space), then the +tangent vectors are related by the derivative of `φ`: +`tangent μ₁ s = (φ'(s)) • tangent μ₂ (φ s)`. Combines the reparametrisation chain +rule with `mfderivWithin_congr` (the two paths agree on the parameter space, so +have equal within-derivatives). -/ +theorem SmoothPath.tangent_reparam_eq {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) + {φ : ℝ → ℝ} {s : ℝ} + (hφ : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) + (modelWithCornersSelf ℝ ℝ) φ μ₁.parameterSpace s) + (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) + (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') + (hs : s ∈ μ₁.parameterSpace) : + μ₁.tangent s = (derivWithin φ μ₁.parameterSpace s) • μ₂.tangent (φ s) := by + have huniq : UniqueMDiffWithinAt (modelWithCornersSelf ℝ ℝ) μ₁.parameterSpace s := + (Path.uniqueDiffOn_parameterSpace M μ₁.toPath s hs).uniqueMDiffWithinAt + have hcongr : mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model + μ₁.toFun μ₁.parameterSpace s + = mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model + (μ₂.toFun ∘ φ) μ₁.parameterSpace s := + mfderivWithin_congr (fun s' hs' => (heq s' hs').symm) (heq s hs).symm + rw [SmoothPath.tangent_def, hcongr] + exact μ₂.mfderivWithin_comp_reparam hφ hmaps huniq hs + +/-- **Non-vanishing of a reparametrisation derivative.** If `ψ ∘ φ = id` on a set +`u` (with `φ` mapping `u` into `v`, both maps differentiable within their sets, and +`u` having unique differentials at `x`), then the within-derivative of `φ` is +non-zero at `x`. This is the real-analytic fact behind the `derivWithin φ ≠ 0` +hypothesis of the pointwise reparametrisation lemmas, obtained by differentiating +the left-inverse identity via the chain rule. -/ +theorem derivWithin_ne_zero_of_leftInverse {φ ψ : ℝ → ℝ} {u v : Set ℝ} {x : ℝ} + (hφ : DifferentiableWithinAt ℝ φ u x) + (hψ : DifferentiableWithinAt ℝ ψ v (φ x)) + (hmaps : Set.MapsTo φ u v) + (huniq : UniqueDiffWithinAt ℝ u x) + (hx : x ∈ u) + (hinv : ∀ y ∈ u, ψ (φ y) = y) : + derivWithin φ u x ≠ 0 := by + intro hzero + have hcomp : derivWithin (ψ ∘ φ) u x + = derivWithin ψ v (φ x) * derivWithin φ u x := + derivWithin_comp x hψ hφ hmaps + have hid : derivWithin (ψ ∘ φ) u x = 1 := + (derivWithin_congr (fun y hy => hinv y hy) (hinv x hx)).trans + (derivWithin_id' x u huniq) + rw [hzero, mul_zero, hid] at hcomp + exact one_ne_zero hcomp + +/-- A `C^⊤` function `ℝ → ℝ` is manifold-differentiable within a set, for the +self models on `ℝ`. Bridges the `ContDiffOn` datum stored in `SmoothPathEquiv` to +the `MDifferentiableWithinAt` hypothesis required by the tangent reparametrisation +lemmas. -/ +theorem mdifferentiableWithinAt_of_contDiffOn {φ : ℝ → ℝ} {u : Set ℝ} + (h : ContDiffOn ℝ ⊤ φ u) {x : ℝ} (hx : x ∈ u) : + MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) + φ u x := + ((h.contDiffWithinAt hx).contMDiffWithinAt).mdifferentiableWithinAt (by simp) + /-! ### Reparametrisation equivalence -/ /-- @@ -163,6 +277,32 @@ def SmoothPathEquiv (μ₁ μ₂ : M.SmoothPath) : Prop := (∀ t ∈ μ₂.parameterSpace, φ (ψ t) = t) ∧ (∀ s ∈ μ₁.parameterSpace, μ₂.toFun (φ s) = μ₁.toFun s) +/-- +Two smooth paths are *orientation-preservingly* equivalent if they are related by +a smooth reparametrisation `φ` (as in `SmoothPathEquiv`) whose within-derivative is +everywhere positive on `μ₁`'s parameter space. Positivity of `φ'` is exactly what +distinguishes orientation-preserving from orientation-reversing reparametrisations, +and it is the extra datum needed to transport the *time orientation* of a curve +(future/past-pointing), not merely its causal type. +-/ +def OrientedSmoothPathEquiv (μ₁ μ₂ : M.SmoothPath) : Prop := + ∃ φ ψ : ℝ → ℝ, + ContDiffOn ℝ ⊤ φ μ₁.parameterSpace ∧ + ContDiffOn ℝ ⊤ ψ μ₂.parameterSpace ∧ + Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace ∧ + Set.MapsTo ψ μ₂.parameterSpace μ₁.parameterSpace ∧ + (∀ s ∈ μ₁.parameterSpace, ψ (φ s) = s) ∧ + (∀ t ∈ μ₂.parameterSpace, φ (ψ t) = t) ∧ + (∀ s ∈ μ₁.parameterSpace, μ₂.toFun (φ s) = μ₁.toFun s) ∧ + (∀ s ∈ μ₁.parameterSpace, 0 < derivWithin φ μ₁.parameterSpace s) + +/-- An orientation-preserving smooth reparametrisation is in particular a smooth +reparametrisation. -/ +theorem OrientedSmoothPathEquiv.toSmoothPathEquiv {μ₁ μ₂ : M.SmoothPath} + (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : M.SmoothPathEquiv μ₁ μ₂ := by + obtain ⟨φ, ψ, hφC, hψC, hφmaps, hψmaps, hψφ, hφψ, heq, _⟩ := h + exact ⟨φ, ψ, hφC, hψC, hφmaps, hψmaps, hψφ, hφψ, heq⟩ + /-! ### Curves -/ /-- A *curve* in a spacetime is an equivalence class of paths under @@ -191,26 +331,148 @@ vector at `s` (the image under `mfderivWithin` of `1 : ℝ`) is a timelike tangent vector at the spacetime point `μ s`. -/ def SmoothPath.IsTimelikeAt (μ : M.SmoothPath) (s : ℝ) : Prop := - M.IsTimelike - (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) + M.IsTimelike (μ.tangent s) + +/-- **Pointwise reparametrisation-invariance of timelikeness.** Under a +reparametrisation identifying `μ₁` with `μ₂` (as in `tangent_reparam_eq`) with +non-vanishing derivative `φ'(s) ≠ 0`, `μ₁` is timelike at `s` iff `μ₂` is timelike +at `φ s`. Combines the reparametrisation chain rule with the scaling invariance +`isTimelike_smul_iff`. -/ +theorem SmoothPath.isTimelikeAt_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) + {φ : ℝ → ℝ} {s : ℝ} + (hφ : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) + (modelWithCornersSelf ℝ ℝ) φ μ₁.parameterSpace s) + (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) + (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') + (hs : s ∈ μ₁.parameterSpace) + (hφ' : derivWithin φ μ₁.parameterSpace s ≠ 0) : + SmoothPath.IsTimelikeAt M μ₁ s ↔ SmoothPath.IsTimelikeAt M μ₂ (φ s) := by + simp only [SmoothPath.IsTimelikeAt] + rw [μ₁.tangent_reparam_eq μ₂ hφ hmaps heq hs, + show μ₁.toFun s = μ₂.toFun (φ s) from (heq s hs).symm] + exact M.isTimelike_smul_iff hφ' (μ₂.tangent (φ s)) + +/-- **Pointwise reparametrisation-invariance of the causal (timelike-or-null) +condition.** The direct analogue of `isTimelikeAt_reparam` for the disjunction +`timelike ∨ null`, via the reparametrisation chain rule together with the scaling +invariances `isTimelike_smul_iff` and `isNull_smul_iff`. -/ +theorem SmoothPath.causalAt_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) + {φ : ℝ → ℝ} {s : ℝ} + (hφ : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) + (modelWithCornersSelf ℝ ℝ) φ μ₁.parameterSpace s) + (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) + (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') + (hs : s ∈ μ₁.parameterSpace) + (hφ' : derivWithin φ μ₁.parameterSpace s ≠ 0) : + (M.IsTimelike (μ₁.tangent s) ∨ M.IsNull (μ₁.tangent s)) + ↔ (M.IsTimelike (μ₂.tangent (φ s)) ∨ M.IsNull (μ₂.tangent (φ s))) := by + rw [μ₁.tangent_reparam_eq μ₂ hφ hmaps heq hs, + show μ₁.toFun s = μ₂.toFun (φ s) from (heq s hs).symm] + exact or_congr (M.isTimelike_smul_iff hφ' (μ₂.tangent (φ s))) + (M.isNull_smul_iff hφ' (μ₂.tangent (φ s))) + +/-- **Pointwise reparametrisation-invariance of future-pointing.** Under an +orientation-preserving reparametrisation identifying `μ₁` with `μ₂` (positive +derivative `0 < φ'(s)`), `μ₁`'s tangent is future-pointing at `s` iff `μ₂`'s is at +`φ s`. Combines the reparametrisation chain rule with the positive-scaling +invariance `isFuturePointing_smul_iff`. -/ +theorem SmoothPath.isFuturePointing_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) + (t : M.TimeOrientation) {φ : ℝ → ℝ} {s : ℝ} + (hφ : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) + (modelWithCornersSelf ℝ ℝ) φ μ₁.parameterSpace s) + (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) + (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') + (hs : s ∈ μ₁.parameterSpace) + (hφ' : 0 < derivWithin φ μ₁.parameterSpace s) : + M.IsFuturePointing t (μ₁.tangent s) + ↔ M.IsFuturePointing t (μ₂.tangent (φ s)) := by + rw [μ₁.tangent_reparam_eq μ₂ hφ hmaps heq hs, + show μ₁.toFun s = μ₂.toFun (φ s) from (heq s hs).symm] + exact M.isFuturePointing_smul_iff t hφ' (μ₂.tangent (φ s)) + +/-- **Pointwise reparametrisation-invariance of past-pointing.** The dual of +`isFuturePointing_reparam`, via `isPastPointing_smul_iff`. -/ +theorem SmoothPath.isPastPointing_reparam {M : Spacetime} (μ₁ μ₂ : M.SmoothPath) + (t : M.TimeOrientation) {φ : ℝ → ℝ} {s : ℝ} + (hφ : MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) + (modelWithCornersSelf ℝ ℝ) φ μ₁.parameterSpace s) + (hmaps : Set.MapsTo φ μ₁.parameterSpace μ₂.parameterSpace) + (heq : ∀ s' ∈ μ₁.parameterSpace, μ₂.toFun (φ s') = μ₁.toFun s') + (hs : s ∈ μ₁.parameterSpace) + (hφ' : 0 < derivWithin φ μ₁.parameterSpace s) : + M.IsPastPointing t (μ₁.tangent s) + ↔ M.IsPastPointing t (μ₂.tangent (φ s)) := by + rw [μ₁.tangent_reparam_eq μ₂ hφ hmaps heq hs, + show μ₁.toFun s = μ₂.toFun (φ s) from (heq s hs).symm] + exact M.isPastPointing_smul_iff t hφ' (μ₂.tangent (φ s)) /-- A smooth path is timelike if its tangent vector is timelike at every point of the parameter space. -/ def SmoothPath.IsTimelike (μ : M.SmoothPath) : Prop := - ∀ s ∈ μ.parameterSpace, - M.IsTimelike - (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) + ∀ s ∈ μ.parameterSpace, M.IsTimelike (μ.tangent s) /-- A smooth path is *causal* if its tangent vector is either timelike or null at every point of the parameter space. -/ def SmoothPath.IsCausal (μ : M.SmoothPath) : Prop := ∀ s ∈ μ.parameterSpace, - M.IsTimelike (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) ∨ - M.IsNull (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) + M.IsTimelike (μ.tangent s) ∨ M.IsNull (μ.tangent s) + +/-- **Reparametrisation-invariance of timelikeness.** Two smooth paths related by +a smooth reparametrisation (`SmoothPathEquiv`) are timelike together: one is +timelike iff the other is. The forward direction uses the inverse diffeomorphism +`ψ` for surjectivity onto `μ₂`'s parameter space; both directions rest on the +pointwise `isTimelikeAt_reparam` (via the chain rule and scaling invariance), with +the reparametrisation derivative non-vanishing by +`derivWithin_ne_zero_of_leftInverse`. -/ +theorem SmoothPath.isTimelike_iff_of_smoothPathEquiv {M : Spacetime} + {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsTimelike M μ₁ ↔ SmoothPath.IsTimelike M μ₂ := by + obtain ⟨φ, ψ, hφC, hψC, hφmaps, hψmaps, hψφ, hφψ, heq⟩ := h + have hφmdiff : ∀ x ∈ μ₁.parameterSpace, + MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) + φ μ₁.parameterSpace x := + fun x hx => mdifferentiableWithinAt_of_contDiffOn hφC hx + have hφderiv : ∀ x ∈ μ₁.parameterSpace, derivWithin φ μ₁.parameterSpace x ≠ 0 := + fun x hx => derivWithin_ne_zero_of_leftInverse + ((hφC.differentiableOn (by simp)) x hx) + ((hψC.differentiableOn (by simp)) (φ x) (hφmaps hx)) + hφmaps (Path.uniqueDiffOn_parameterSpace M μ₁.toPath x hx) hx hψφ + constructor + · intro h₁ t ht + have hs : ψ t ∈ μ₁.parameterSpace := hψmaps ht + have hiff := μ₁.isTimelikeAt_reparam μ₂ (hφmdiff _ hs) hφmaps heq hs (hφderiv _ hs) + rw [hφψ t ht] at hiff + exact hiff.mp (h₁ _ hs) + · intro h₂ s hs + have hiff := μ₁.isTimelikeAt_reparam μ₂ (hφmdiff _ hs) hφmaps heq hs (hφderiv _ hs) + exact hiff.mpr (h₂ _ (hφmaps hs)) + +/-- **Reparametrisation-invariance of the causal condition.** Two smooth paths +related by a smooth reparametrisation (`SmoothPathEquiv`) are causal together. Same +structure as `isTimelike_iff_of_smoothPathEquiv`, using the pointwise +`causalAt_reparam`. -/ +theorem SmoothPath.isCausal_iff_of_smoothPathEquiv {M : Spacetime} + {μ₁ μ₂ : M.SmoothPath} (h : M.SmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsCausal M μ₁ ↔ SmoothPath.IsCausal M μ₂ := by + obtain ⟨φ, ψ, hφC, hψC, hφmaps, hψmaps, hψφ, hφψ, heq⟩ := h + have hφmdiff : ∀ x ∈ μ₁.parameterSpace, + MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) + φ μ₁.parameterSpace x := + fun x hx => mdifferentiableWithinAt_of_contDiffOn hφC hx + have hφderiv : ∀ x ∈ μ₁.parameterSpace, derivWithin φ μ₁.parameterSpace x ≠ 0 := + fun x hx => derivWithin_ne_zero_of_leftInverse + ((hφC.differentiableOn (by simp)) x hx) + ((hψC.differentiableOn (by simp)) (φ x) (hφmaps hx)) + hφmaps (Path.uniqueDiffOn_parameterSpace M μ₁.toPath x hx) hx hψφ + constructor + · intro h₁ t ht + have hs : ψ t ∈ μ₁.parameterSpace := hψmaps ht + have hiff := μ₁.causalAt_reparam μ₂ (hφmdiff _ hs) hφmaps heq hs (hφderiv _ hs) + rw [hφψ t ht] at hiff + exact hiff.mp (h₁ _ hs) + · intro h₂ s hs + have hiff := μ₁.causalAt_reparam μ₂ (hφmdiff _ hs) hφmaps heq hs (hφderiv _ hs) + exact hiff.mpr (h₂ _ (hφmaps hs)) /-- A *timelike smooth curve* is a smooth curve all of whose representative @@ -234,19 +496,13 @@ def IsCausalSmoothCurve (c : SmoothCurve M) : Prop := if its tangent vector is future-pointing at every parameter point. -/ def SmoothPath.IsFutureOriented (μ : M.SmoothPath) (t : M.TimeOrientation) : Prop := - ∀ s ∈ μ.parameterSpace, - M.IsFuturePointing t - (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) + ∀ s ∈ μ.parameterSpace, M.IsFuturePointing t (μ.tangent s) /-- A smooth path is *past-oriented* with respect to a time orientation `t` if its tangent vector is past-pointing at every parameter point. -/ def SmoothPath.IsPastOriented (μ : M.SmoothPath) (t : M.TimeOrientation) : Prop := - ∀ s ∈ μ.parameterSpace, - M.IsPastPointing t - (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) + ∀ s ∈ μ.parameterSpace, M.IsPastPointing t (μ.tangent s) /-- A *future-oriented smooth curve* is a smooth curve admitting a future-oriented representative smooth path (relative to a fixed time @@ -264,6 +520,240 @@ def IsPastOrientedSmoothCurve (t : M.TimeOrientation) (c : SmoothCurve M) : ∃ μ : M.SmoothPath, c = SmoothCurve.ofPath M μ ∧ SmoothPath.IsPastOriented M μ t +/-- **Reparametrisation-invariance of future-orientedness.** Two smooth paths +related by an orientation-preserving smooth reparametrisation +(`OrientedSmoothPathEquiv`) are future-oriented together: one is future-oriented +iff the other is. The forward direction uses the inverse diffeomorphism `ψ` for +surjectivity; both directions rest on the pointwise `isFuturePointing_reparam`, +with the reparametrisation derivative positive by hypothesis. -/ +theorem SmoothPath.isFutureOriented_iff_of_orientedSmoothPathEquiv {M : Spacetime} + {μ₁ μ₂ : M.SmoothPath} (t : M.TimeOrientation) + (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsFutureOriented M μ₁ t ↔ SmoothPath.IsFutureOriented M μ₂ t := by + obtain ⟨φ, ψ, hφC, hψC, hφmaps, hψmaps, hψφ, hφψ, heq, hpos⟩ := h + have hφmdiff : ∀ x ∈ μ₁.parameterSpace, + MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) + φ μ₁.parameterSpace x := + fun x hx => mdifferentiableWithinAt_of_contDiffOn hφC hx + constructor + · intro h₁ p hp + have hs : ψ p ∈ μ₁.parameterSpace := hψmaps hp + have hiff := + μ₁.isFuturePointing_reparam μ₂ t (hφmdiff _ hs) hφmaps heq hs (hpos _ hs) + rw [hφψ p hp] at hiff + exact hiff.mp (h₁ _ hs) + · intro h₂ s hs + have hiff := + μ₁.isFuturePointing_reparam μ₂ t (hφmdiff _ hs) hφmaps heq hs (hpos _ hs) + exact hiff.mpr (h₂ _ (hφmaps hs)) + +/-- **Reparametrisation-invariance of past-orientedness.** The dual of +`isFutureOriented_iff_of_orientedSmoothPathEquiv`, via `isPastPointing_reparam`. -/ +theorem SmoothPath.isPastOriented_iff_of_orientedSmoothPathEquiv {M : Spacetime} + {μ₁ μ₂ : M.SmoothPath} (t : M.TimeOrientation) + (h : M.OrientedSmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsPastOriented M μ₁ t ↔ SmoothPath.IsPastOriented M μ₂ t := by + obtain ⟨φ, ψ, hφC, hψC, hφmaps, hψmaps, hψφ, hφψ, heq, hpos⟩ := h + have hφmdiff : ∀ x ∈ μ₁.parameterSpace, + MDifferentiableWithinAt (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) + φ μ₁.parameterSpace x := + fun x hx => mdifferentiableWithinAt_of_contDiffOn hφC hx + constructor + · intro h₁ p hp + have hs : ψ p ∈ μ₁.parameterSpace := hψmaps hp + have hiff := + μ₁.isPastPointing_reparam μ₂ t (hφmdiff _ hs) hφmaps heq hs (hpos _ hs) + rw [hφψ p hp] at hiff + exact hiff.mp (h₁ _ hs) + · intro h₂ s hs + have hiff := + μ₁.isPastPointing_reparam μ₂ t (hφmdiff _ hs) hφmaps heq hs (hpos _ hs) + exact hiff.mpr (h₂ _ (hφmaps hs)) + +/-! ### Well-definedness of the causal type on smooth curves + +Timelikeness and causality are invariant under *any* smooth reparametrisation, so +they descend to genuine predicates on `SmoothCurve` (the quotient by +`SmoothPathEquiv`): a curve is timelike/causal iff any chosen representative is. +The transfer along the quotient uses the equivalence closure of `SmoothPathEquiv` +(via `Quot.eqvGen_exact`) together with the per-reparametrisation iffs. -/ + +/-- Timelikeness is invariant along the equivalence closure of `SmoothPathEquiv`. -/ +theorem SmoothPath.isTimelike_iff_of_eqvGen {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} + (h : Relation.EqvGen M.SmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsTimelike M μ₁ ↔ SmoothPath.IsTimelike M μ₂ := by + induction h with + | rel x y hxy => exact SmoothPath.isTimelike_iff_of_smoothPathEquiv hxy + | refl x => exact Iff.rfl + | symm x y _ ih => exact ih.symm + | trans x y z _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + +/-- **Well-definedness of timelikeness on smooth curves.** A smooth curve is +timelike (has a timelike representative) iff the chosen representative `μ` is +timelike; the value does not depend on the representative. -/ +theorem isTimelikeSmoothCurve_ofPath_iff {M : Spacetime} (μ : M.SmoothPath) : + IsTimelikeSmoothCurve M (SmoothCurve.ofPath M μ) ↔ SmoothPath.IsTimelike M μ := by + constructor + · rintro ⟨μ', heq, htl⟩ + exact (SmoothPath.isTimelike_iff_of_eqvGen (Quot.eqvGen_exact heq)).mpr htl + · intro htl + exact ⟨μ, rfl, htl⟩ + +/-- Causality is invariant along the equivalence closure of `SmoothPathEquiv`. -/ +theorem SmoothPath.isCausal_iff_of_eqvGen {M : Spacetime} {μ₁ μ₂ : M.SmoothPath} + (h : Relation.EqvGen M.SmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsCausal M μ₁ ↔ SmoothPath.IsCausal M μ₂ := by + induction h with + | rel x y hxy => exact SmoothPath.isCausal_iff_of_smoothPathEquiv hxy + | refl x => exact Iff.rfl + | symm x y _ ih => exact ih.symm + | trans x y z _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + +/-- **Well-definedness of causality on smooth curves.** -/ +theorem isCausalSmoothCurve_ofPath_iff {M : Spacetime} (μ : M.SmoothPath) : + IsCausalSmoothCurve M (SmoothCurve.ofPath M μ) ↔ SmoothPath.IsCausal M μ := by + constructor + · rintro ⟨μ', heq, hc⟩ + exact (SmoothPath.isCausal_iff_of_eqvGen (Quot.eqvGen_exact heq)).mpr hc + · intro hc + exact ⟨μ, rfl, hc⟩ + +/-! ### Oriented smooth curves and well-definedness of orientation + +The time orientation of a curve (future- vs past-pointing) is *not* invariant under +orientation-reversing reparametrisations, so it does not descend to `SmoothCurve`. +It does descend to the finer quotient by `OrientedSmoothPathEquiv`, which is the +correct home for future/past-oriented curves. -/ + +/-- An *oriented smooth curve*: an equivalence class of smooth paths under +orientation-preserving reparametrisation. Finer than `SmoothCurve` (which also +allows orientation-reversing reparametrisations), it is the natural domain on which +the time orientation of a curve is well-defined. -/ +def OrientedSmoothCurve : Type := Quot M.OrientedSmoothPathEquiv + +/-- Every smooth path determines an oriented smooth curve. -/ +def OrientedSmoothCurve.ofPath (μ : M.SmoothPath) : OrientedSmoothCurve M := + Quot.mk _ μ + +/-- An oriented smooth curve is *future-oriented* (relative to a time orientation +`t`) if it admits a future-oriented representative smooth path. -/ +def IsFutureOrientedCurve (t : M.TimeOrientation) (c : OrientedSmoothCurve M) : + Prop := + ∃ μ : M.SmoothPath, + c = OrientedSmoothCurve.ofPath M μ ∧ SmoothPath.IsFutureOriented M μ t + +/-- An oriented smooth curve is *past-oriented* (relative to a time orientation +`t`) if it admits a past-oriented representative smooth path. -/ +def IsPastOrientedCurve (t : M.TimeOrientation) (c : OrientedSmoothCurve M) : + Prop := + ∃ μ : M.SmoothPath, + c = OrientedSmoothCurve.ofPath M μ ∧ SmoothPath.IsPastOriented M μ t + +/-- Future-orientedness is invariant along the equivalence closure of +`OrientedSmoothPathEquiv`. -/ +theorem SmoothPath.isFutureOriented_iff_of_eqvGen {M : Spacetime} + (t : M.TimeOrientation) {μ₁ μ₂ : M.SmoothPath} + (h : Relation.EqvGen M.OrientedSmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsFutureOriented M μ₁ t ↔ SmoothPath.IsFutureOriented M μ₂ t := by + induction h with + | rel x y hxy => + exact SmoothPath.isFutureOriented_iff_of_orientedSmoothPathEquiv t hxy + | refl x => exact Iff.rfl + | symm x y _ ih => exact ih.symm + | trans x y z _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + +/-- **Well-definedness of future-orientedness on oriented smooth curves.** -/ +theorem isFutureOrientedCurve_ofPath_iff {M : Spacetime} (t : M.TimeOrientation) + (μ : M.SmoothPath) : + IsFutureOrientedCurve M t (OrientedSmoothCurve.ofPath M μ) + ↔ SmoothPath.IsFutureOriented M μ t := by + constructor + · rintro ⟨μ', heq, hfo⟩ + exact (SmoothPath.isFutureOriented_iff_of_eqvGen t (Quot.eqvGen_exact heq)).mpr hfo + · intro hfo + exact ⟨μ, rfl, hfo⟩ + +/-- Past-orientedness is invariant along the equivalence closure of +`OrientedSmoothPathEquiv`. -/ +theorem SmoothPath.isPastOriented_iff_of_eqvGen {M : Spacetime} + (t : M.TimeOrientation) {μ₁ μ₂ : M.SmoothPath} + (h : Relation.EqvGen M.OrientedSmoothPathEquiv μ₁ μ₂) : + SmoothPath.IsPastOriented M μ₁ t ↔ SmoothPath.IsPastOriented M μ₂ t := by + induction h with + | rel x y hxy => + exact SmoothPath.isPastOriented_iff_of_orientedSmoothPathEquiv t hxy + | refl x => exact Iff.rfl + | symm x y _ ih => exact ih.symm + | trans x y z _ _ ih₁ ih₂ => exact ih₁.trans ih₂ + +/-- **Well-definedness of past-orientedness on oriented smooth curves.** -/ +theorem isPastOrientedCurve_ofPath_iff {M : Spacetime} (t : M.TimeOrientation) + (μ : M.SmoothPath) : + IsPastOrientedCurve M t (OrientedSmoothCurve.ofPath M μ) + ↔ SmoothPath.IsPastOriented M μ t := by + constructor + · rintro ⟨μ', heq, hpo⟩ + exact (SmoothPath.isPastOriented_iff_of_eqvGen t (Quot.eqvGen_exact heq)).mpr hpo + · intro hpo + exact ⟨μ, rfl, hpo⟩ + +/-! ### Projection to the coarser quotient + +Every orientation-preserving reparametrisation is a smooth reparametrisation, so +there is a canonical projection `OrientedSmoothCurve → SmoothCurve` forgetting the +orientation. It sends `ofPath μ` to `ofPath μ`, hence is compatible with the +(orientation-independent) timelike and causal predicates. -/ + +/-- The canonical projection from oriented smooth curves to smooth curves, +forgetting the orientation. Well-defined because `OrientedSmoothPathEquiv` refines +`SmoothPathEquiv`. -/ +def OrientedSmoothCurve.toSmoothCurve (c : OrientedSmoothCurve M) : SmoothCurve M := + Quot.lift (fun μ => SmoothCurve.ofPath M μ) + (fun _ _ h => Quot.sound h.toSmoothPathEquiv) c + +@[simp] theorem OrientedSmoothCurve.toSmoothCurve_ofPath (μ : M.SmoothPath) : + (OrientedSmoothCurve.ofPath M μ).toSmoothCurve = SmoothCurve.ofPath M μ := rfl + +/-- The projection is surjective: every smooth curve underlies an oriented one. -/ +theorem OrientedSmoothCurve.toSmoothCurve_surjective : + Function.Surjective (OrientedSmoothCurve.toSmoothCurve M) := by + intro c + obtain ⟨μ, rfl⟩ := Quot.exists_rep c + exact ⟨OrientedSmoothCurve.ofPath M μ, rfl⟩ + +/-- **Compatibility with timelikeness.** The smooth curve underlying an oriented +smooth curve `ofPath μ` is timelike iff `μ` is — the timelike predicate factors +through the projection. -/ +theorem isTimelikeSmoothCurve_toSmoothCurve_ofPath (μ : M.SmoothPath) : + IsTimelikeSmoothCurve M (OrientedSmoothCurve.ofPath M μ).toSmoothCurve + ↔ SmoothPath.IsTimelike M μ := by + rw [OrientedSmoothCurve.toSmoothCurve_ofPath] + exact isTimelikeSmoothCurve_ofPath_iff μ + +/-- **Compatibility with causality.** -/ +theorem isCausalSmoothCurve_toSmoothCurve_ofPath (μ : M.SmoothPath) : + IsCausalSmoothCurve M (OrientedSmoothCurve.ofPath M μ).toSmoothCurve + ↔ SmoothPath.IsCausal M μ := by + rw [OrientedSmoothCurve.toSmoothCurve_ofPath] + exact isCausalSmoothCurve_ofPath_iff μ + +/-- A future-oriented oriented smooth curve projects to a causal smooth curve +(future-pointing tangents are timelike or null). -/ +theorem IsFutureOrientedCurve.isCausal_toSmoothCurve {t : M.TimeOrientation} + {c : OrientedSmoothCurve M} (h : IsFutureOrientedCurve M t c) : + IsCausalSmoothCurve M c.toSmoothCurve := by + obtain ⟨μ, rfl, hfo⟩ := h + exact (isCausalSmoothCurve_toSmoothCurve_ofPath M μ).mpr + (fun s hs => M.isTimelike_or_isNull_of_isFuturePointing t (hfo s hs)) + +/-- A past-oriented oriented smooth curve projects to a causal smooth curve. -/ +theorem IsPastOrientedCurve.isCausal_toSmoothCurve {t : M.TimeOrientation} + {c : OrientedSmoothCurve M} (h : IsPastOrientedCurve M t c) : + IsCausalSmoothCurve M c.toSmoothCurve := by + obtain ⟨μ, rfl, hpo⟩ := h + exact (isCausalSmoothCurve_toSmoothCurve_ofPath M μ).mpr + (fun s hs => M.isTimelike_or_isNull_of_isPastPointing t (hpo s hs)) + /-! ### Endpoints -/ /-- diff --git a/Physicslib4/Spacetime/IsometryCausality.lean b/Physicslib4/Spacetime/IsometryCausality.lean index 0bca820..b41b0c3 100644 --- a/Physicslib4/Spacetime/IsometryCausality.lean +++ b/Physicslib4/Spacetime/IsometryCausality.lean @@ -95,11 +95,8 @@ noncomputable def pushforwardPath (g : Isometry M) (μ : M.SmoothPath) : isometry applied to the tangent vector of `μ`. -/ theorem pushforwardPath_tangent (g : Isometry M) (μ : M.SmoothPath) {s : ℝ} (hs : s ∈ μ.parameterSpace) : - mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model (g.pushforwardPath μ).toFun - (g.pushforwardPath μ).parameterSpace s (1 : ℝ) - = mfderiv M.model M.model g.toDiffeo (μ.toFun s) - (mfderivWithin (modelWithCornersSelf ℝ ℝ) M.model - μ.toFun μ.parameterSpace s (1 : ℝ)) := + (g.pushforwardPath μ).tangent s + = mfderiv M.model M.model g.toDiffeo (μ.toFun s) (μ.tangent s) := mfderivWithin_comp_diffeo g μ hs /-- The pushforward of a timelike path is timelike: isometries preserve the @@ -219,6 +216,17 @@ noncomputable def orientedIdentityComponent (M : Spacetime) (t : M.TimeOrientati Subgroup (Isometry M) := Isometry.identityComponent M ⊓ futureOrientationPreserving M t +/-- The Axiom-5 isometry subgroups act **continuously** on spacetime points: both +the identity component and the oriented identity component inherit +`ContinuousSMul … M.Carrier` automatically from the full isometry group's +`ContinuousSMul` (`IsometryTopology`) via the subgroup action. Recorded here as a +confirmation, since these are the concrete `M.Isom` supplied to the curved +Haag-Kastler bridge. -/ +example (M : Spacetime) (t : M.TimeOrientation) : True := by + have _ : ContinuousSMul ↥(identityComponent M) M.Carrier := inferInstance + have _ : ContinuousSMul ↥(orientedIdentityComponent M t) M.Carrier := inferInstance + trivial + /-- Under future-orientation preservation, the pushforward of a future-oriented path is future-oriented. -/ theorem pushforwardPath_isFutureOriented (g : Isometry M) (μ : M.SmoothPath) diff --git a/blueprint/src/sections/sec10/10-2_spacetime.tex b/blueprint/src/sections/sec10/10-2_spacetime.tex index 3ccb40e..fae87aa 100644 --- a/blueprint/src/sections/sec10/10-2_spacetime.tex +++ b/blueprint/src/sections/sec10/10-2_spacetime.tex @@ -181,6 +181,42 @@ \section{Spacetime}\label{sctn:spacetime} A \textit{future-oriented smooth curve} is a smooth curve with a tangent vector that is future-pointing at every point. A \textit{past-oriented smooth curve} is a smooth curve with a tangent vector that is past-pointing at every point. \end{definition} +\begin{theorem}[Reparametrisation-Invariance of the Causal Type] + \label{thrm:smooth-curve-causal-well-defined} + \lean{Physicslib4.Spacetime.isTimelikeSmoothCurve_ofPath_iff, Physicslib4.Spacetime.isCausalSmoothCurve_ofPath_iff} + \leanfile{Physicslib4/Spacetime/Curves.lean} + \leanok + \uses{def:timelike-and-causal-smooth-curves} + The timelike and causal predicates are well-defined on smooth curves, independently of the chosen path representative: a smooth path is timelike (resp. causal) if and only if its associated smooth curve is. The invariance rests on the chain rule for the tangent under a smooth reparametrisation $\varphi$, namely $\mathrm{tangent}(\mu\circ\varphi)(s) = \varphi'(s)\cdot\mathrm{tangent}(\mu)(\varphi(s))$, together with the scale-invariance of the causal classification: since $g(c\,v, c\,v) = c^2\, g(v,v)$, the vector $c\,v$ is timelike/null exactly when $v$ is, for $c \neq 0$. +\end{theorem} + +\begin{definition}[Oriented Smooth Curve] + \label{def:oriented-smooth-curve} + \lean{Physicslib4.Spacetime.OrientedSmoothCurve} + \leanfile{Physicslib4/Spacetime/Curves.lean} + \leanok + \uses{def:curves} + An orientation-reversing reparametrisation flips the time-orientation of the tangent, so future/past orientation is well-defined only on the finer quotient by \emph{orientation-preserving} reparametrisations (those with positive within-derivative). An \emph{oriented smooth curve} is an equivalence class of smooth paths under this finer relation. +\end{definition} + +\begin{theorem}[Reparametrisation-Invariance of Orientation] + \label{thrm:oriented-curve-well-defined} + \lean{Physicslib4.Spacetime.isFutureOrientedCurve_ofPath_iff, Physicslib4.Spacetime.isPastOrientedCurve_ofPath_iff} + \leanfile{Physicslib4/Spacetime/Curves.lean} + \leanok + \uses{def:oriented-smooth-curve, def:future-and-past-oriented-smooth-curves} + Future- and past-orientation are well-defined on oriented smooth curves: a smooth path is future-oriented (resp. past-oriented) if and only if its oriented smooth curve is. The positive within-derivative of an orientation-preserving reparametrisation, together with the positive-scaling invariance of pointing vectors ($c\,v$ is future-pointing iff $v$ is, for $c > 0$), gives the invariance. +\end{theorem} + +\begin{theorem}[The Forgetful Projection of Oriented Curves] + \label{thrm:oriented-curve-projection} + \lean{Physicslib4.Spacetime.OrientedSmoothCurve.toSmoothCurve, Physicslib4.Spacetime.IsFutureOrientedCurve.isCausal_toSmoothCurve} + \leanfile{Physicslib4/Spacetime/Curves.lean} + \leanok + \uses{def:oriented-smooth-curve, def:curves, def:timelike-and-causal-smooth-curves} + Every oriented smooth curve has an underlying smooth curve, via a canonical surjection $\mathrm{OrientedSmoothCurve} \to \mathrm{SmoothCurve}$ that forgets the orientation data. The timelike and causal predicates factor through it, and a future- or past-oriented curve projects to a causal smooth curve. +\end{theorem} + \begin{definition}[Endpoints] \label{def:endpoints} \lean{Physicslib4.Spacetime.IsEndpoint, Physicslib4.Spacetime.IsPastEndpoint, Physicslib4.Spacetime.IsFutureEndpoint} diff --git a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex index 93da7b3..03ac155 100644 --- a/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex +++ b/blueprint/src/sections/sec10/10-3_haag-kastler-axioms.tex @@ -438,6 +438,122 @@ \subsection{Irreducibility and Schur's Lemma} For a state $\omega$ on the quasilocal algebra $\mathfrak{U}$ there is a GNS triple $(H, \pi, \Omega)$ reproducing $\omega$ in which $\omega$ is pure if and only if the representation $\pi$ is irreducible. This combines the GNS construction with the abstract \ref{thrm:pure-iff-irreducible}. \end{theorem} +\subsection{Unitary Equivalence and Superselection} + +The comparison of representations is the entry point to superselection theory. For $*$-representations $\pi : A \to \mathcal{B}(H)$ of a C*-algebra --- in particular of the quasilocal algebra $\mathfrak{U}$ or a local algebra $\mathfrak{U}(\mathbf{B})$ --- we record three successively coarser notions of sameness (unitary equivalence, quasi-equivalence, and the negation of the finest, disjointness) and the representation-theoretic invariants they preserve. + +\begin{definition}[Unitary Equivalence of Representations] + \label{def:unitary-equivalence} + \lean{Physicslib4.GNS.UnitaryEquiv} + \leanfile{Physicslib4/GNS/UnitaryEquiv.lean} + \leanok + \uses{thrm:gns-construction-theorem} + Two $*$-representations $\pi_1 : A \to \mathcal{B}(H_1)$ and $\pi_2 : A \to \mathcal{B}(H_2)$ are \emph{unitarily equivalent} when there is an isometric isomorphism $U : H_1 \simeq H_2$ of the underlying Hilbert spaces intertwining them: $U(\pi_1(a)\,x) = \pi_2(a)(U x)$. This is an equivalence relation --- reflexive, symmetric, and transitive. +\end{definition} + +\begin{theorem}[Irreducibility and Factoriality are Unitary Invariants] + \label{thrm:unitary-equiv-invariants} + \lean{Physicslib4.GNS.UnitaryEquiv.isIrreducible_iff, Physicslib4.GNS.UnitaryEquiv.isFactor_iff} + \leanfile{Physicslib4/GNS/UnitaryEquiv.lean} + \leanok + \uses{def:unitary-equivalence, def:irreducible-representation, thrm:irreducible-factor} + Unitarily equivalent representations share their representation-theoretic type: $\pi_1$ is irreducible if and only if $\pi_2$ is, and the generated von Neumann algebra $\pi_1(A)''$ is a factor if and only if $\pi_2(A)''$ is. The transport is packaged through the cross-space conjugation $T \mapsto U T U^{-1}$, a multiplicative isomorphism $\mathcal{B}(H_1) \simeq \mathcal{B}(H_2)$ that carries $\pi_1(A)$ onto $\pi_2(A)$, centralizers onto centralizers, and scalars onto scalars; irreducibility (commutant equal to the scalars) and factoriality (trivial center of $\pi(A)''$) are then preserved. +\end{theorem} + +\begin{definition}[Disjoint Representations] + \label{def:disjoint-representations} + \lean{Physicslib4.GNS.AreDisjoint} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{def:unitary-equivalence} + An \emph{intertwiner} $T : H_1 \to H_2$ between $\pi_1$ and $\pi_2$ satisfies $T(\pi_1(a)\,x) = \pi_2(a)(T x)$; intertwiners are closed under sums, scalars, composition, and the adjoint (the adjoint of a $\pi_1 \to \pi_2$ intertwiner is a $\pi_2 \to \pi_1$ intertwiner). Two representations are \emph{disjoint} when the only intertwiner between them is $0$. Disjointness is symmetric (take adjoints), and a representation on a nonzero Hilbert space is never disjoint from itself; more generally, unitarily equivalent representations on nonzero spaces are never disjoint, since the implementing unitary is a nonzero intertwiner. +\end{definition} + +\begin{definition}[Quasi-Equivalence of Representations] + \label{def:quasi-equivalence} + \lean{Physicslib4.GNS.QuasiEquiv} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{def:unitary-equivalence, thrm:irreducible-factor} + Two representations are \emph{quasi-equivalent} when there is a $*$-isomorphism of their generated von Neumann algebras $\pi_1(A)'' \simeq \pi_2(A)''$ carrying $\pi_1(a)$ to $\pi_2(a)$. This is an equivalence relation, and it is coarser than unitary equivalence: unitary equivalence implies quasi-equivalence, because the conjugation $*$-isomorphism $T \mapsto U T U^{-1}$ restricts to a $*$-isomorphism of the generated von Neumann algebras. +\end{definition} + +\begin{theorem}[Schur's Lemma and the Irreducible Dichotomy] + \label{thrm:irreducible-dichotomy} + \lean{Physicslib4.GNS.UnitaryEquiv.of_intertwines_of_isIrreducible, Physicslib4.GNS.areDisjoint_or_unitaryEquiv_of_isIrreducible} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{def:unitary-equivalence, def:disjoint-representations, def:irreducible-representation} + A nonzero intertwiner $T$ between two \emph{irreducible} representations rescales to a unitary equivalence: $T^\ast T$ commutes with $\pi_1$, hence is a positive scalar $r \cdot 1$ with $r > 0$, so $(\sqrt r)^{-1}\,T$ is a linear isometry; and $T T^\ast$ is a nonzero scalar (irreducibility of $\pi_2$), which makes $T$ surjective, so the isometry is a unitary. Consequently two irreducible representations are either \emph{disjoint} or \emph{unitarily equivalent} --- the foundational trichotomy of superselection theory, identifying sectors with unitary-equivalence classes of irreducible representations. +\end{theorem} + +\begin{lemma}[Schur Multiplicity] + \label{lmm:schur-multiplicity} + \lean{Physicslib4.GNS.eq_smul_of_intertwines_of_isIrreducible} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{thrm:irreducible-dichotomy, def:irreducible-representation} + The space of intertwiners between two irreducible representations is at most one-dimensional: any two intertwiners $S, T$ with $S \neq 0$ are proportional, $T = \lambda \cdot S$. Indeed $S^\ast S = a\cdot 1$ and $S^\ast T = b \cdot 1$ (commuting with $\pi_1$, hence scalar), and $S S^\ast = c \cdot 1$ with $c \neq 0$ (irreducibility of $\pi_2$) makes $S^\ast$ injective; since $S^\ast\big(T - (b/a)\,S\big) = 0$, injectivity gives $T = (b/a)\,S$. So irreducible representations intertwine multiplicity-free. +\end{lemma} + +\begin{lemma}[Endomorphism Algebra of an Irreducible Representation] + \label{lmm:endomorphism-scalar} + \lean{Physicslib4.GNS.intertwines_self_iff_isScalar} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{def:irreducible-representation, def:disjoint-representations} + The endomorphism algebra of an irreducible representation is $\mathbb{C}\cdot 1$: every self-intertwiner of an irreducible representation is a scalar multiple of the identity. This is the commutant form of irreducibility read through the intertwiner language, and it identifies each irreducible sector with a simple (one-dimensional-centred) object. +\end{lemma} + +\begin{theorem}[The Pure-State Dichotomy] + \label{thrm:pure-state-dichotomy} + \lean{Physicslib4.GNS.exists_gns_areDisjoint_or_unitaryEquiv_of_isPure} + \leanfile{Physicslib4/GNS/Superselection.lean} + \leanok + \uses{def:pure-state, thrm:irreducible-dichotomy, thrm:pure-iff-irreducible} + The GNS representations of two pure states are either disjoint or unitarily equivalent. Indeed the GNS representation of a pure state is irreducible (\ref{thrm:pure-iff-irreducible}), so the irreducible dichotomy (\ref{thrm:irreducible-dichotomy}) applies. Pure states thus fall into \emph{superselection sectors}: the sector of a pure state is the unitary-equivalence class of its irreducible GNS representation. +\end{theorem} + +\subsection{Direct Sums, Amplification, and Reducibility} + +Given a family of $*$-representations $\pi_i : A \to \mathcal{B}(H_i)$, their direct sum acts on the $\ell^2$-direct sum $\bigoplus_i H_i$. This is the construction underlying amplifications and the reducibility of non-primary representations. + +\begin{definition}[Direct-Sum Representation] + \label{def:direct-sum-representation} + \lean{Physicslib4.GNS.directSum} + \leanfile{Physicslib4/GNS/DirectSum.lean} + \leanok + \uses{thrm:gns-construction-theorem} + The \emph{direct sum} $\bigoplus_i \pi_i : A \to \mathcal{B}(\ell^2(\iota, H))$ of a family of $*$-representations acts coordinatewise: $(\bigoplus_i \pi_i)(a)$ is the diagonal operator $x \mapsto (\pi_i(a)\,x_i)_i$ on the $\ell^2$-direct sum. It is a $*$-representation, the diagonal being uniformly bounded by $\Vert a\Vert$ since each $\pi_i$ is contractive. +\end{definition} + +\begin{theorem}[Subrepresentations and Commutant of a Direct Sum] + \label{thrm:direct-sum-subrepresentation} + \lean{Physicslib4.GNS.intertwines_single, Physicslib4.GNS.summandProj_mem_commutant} + \leanfile{Physicslib4/GNS/DirectSum.lean} + \leanok + \uses{def:direct-sum-representation, def:disjoint-representations} + Each summand embeds as a subrepresentation: the isometric inclusion $H_j \hookrightarrow \ell^2(\iota, H)$ intertwines $\pi_j$ with $\bigoplus_i \pi_i$. Moreover the orthogonal projection onto the $j$-th summand lies in the commutant of the direct sum, so each summand is a reducing subspace. +\end{theorem} + +\begin{definition}[Amplification] + \label{def:amplification} + \lean{Physicslib4.GNS.amplification} + \leanfile{Physicslib4/GNS/Amplification.lean} + \leanok + \uses{def:direct-sum-representation} + The \emph{$\iota$-fold amplification} $\iota \cdot \pi := \bigoplus_{i : \iota} \pi$ of a single representation is the direct sum of $\iota$ copies of $\pi$; $\pi$ embeds as each summand. +\end{definition} + +\begin{theorem}[Reducibility of a Direct Sum] + \label{thrm:direct-sum-reducible} + \lean{Physicslib4.GNS.not_isIrreducible_directSum} + \leanfile{Physicslib4/GNS/Amplification.lean} + \leanok + \uses{def:direct-sum-representation, def:irreducible-representation, thrm:direct-sum-subrepresentation} + A direct sum with two summands carrying nonzero vectors is \emph{reducible}. Were $\bigoplus_i \pi_i$ irreducible, every summand projection would be a scalar (its commutant being trivial); but the projection onto one of two nonzero summands is a nontrivial projection, hence not scalar. In particular an amplification $\iota \cdot \pi$ with at least two copies (and $\pi$ acting on a nonzero space) is reducible --- the multiplicity is visible in the commutant. +\end{theorem} + \subsection{Covariant States and the Covariance Action} The Lorentz covariance of a Haag-Kastler net (\ref{def:lorentz-covariance}) acts on the net fiberwise, through the $*$-isomorphisms $\alpha_L : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(L\cdot\mathbf{B})$. We record two consequences: the notion of a Lorentz-covariant family of local states, and the lift of the fiberwise action to a single dynamical $*$-automorphism of the quasilocal algebra. diff --git a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex index cdc15a6..f33fec9 100644 --- a/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex +++ b/blueprint/src/sections/sec10/10-4_haag-kastler-axioms-in-curved-spacetime.tex @@ -277,6 +277,15 @@ \subsection{Purity of States on Local Algebras in Curved Spacetime} For a pure state $\omega$ on the local algebra $\mathfrak{U}(\mathbf{B})$ there is a cyclic GNS triple reproducing $\omega$ whose generated von Neumann algebra $\pi(\mathfrak{U}(\mathbf{B}))''$ has trivial center (it is a factor) and is in fact all of $\mathcal{B}(H)$. These are the abstract factor (\ref{thrm:pure-factor}) and density (\ref{thrm:pure-generates-all}) statements registered per region on the curved local algebra $\mathfrak{U}(\mathbf{B})$, the right generality in curved spacetime where there is no quasilocal algebra. \end{theorem} +\begin{theorem}[The Irreducible Dichotomy for a Curved Local Algebra] + \label{thrm:irreducible-dichotomy-in-curved-spacetime} + \lean{Physicslib4.AQFT.HaagKastlerCurved.HaagKastlerNet.areDisjoint_or_unitaryEquiv_of_isIrreducible} + \leanfile{Physicslib4/AQFT/HaagKastlerCurved/Purity.lean} + \leanok + \uses{thrm:irreducible-dichotomy, def:irreducible-representation} + Two irreducible representations of a curved local algebra $\mathfrak{U}(\mathbf{B})$ are either disjoint or unitarily equivalent. This is the abstract irreducible dichotomy (\ref{thrm:irreducible-dichotomy}) registered per region on the C*-algebra $\mathfrak{U}(\mathbf{B})$ --- the right generality in curved spacetime, where sectors are attached to the local algebras. +\end{theorem} + \subsection{Covariant States in Curved Spacetime} As in the Minkowski case, the isometric covariance (\ref{def:isometric-covariance-in-curved-spacetime}) acts fiberwise through the $*$-isomorphisms $\alpha_\varphi : \mathfrak{U}(\mathbf{B}) \to \mathfrak{U}(\varphi(\mathbf{B}))$. Since there is no quasilocal algebra, only the local notion of a covariant family of states is available. diff --git a/home_page/index.md b/home_page/index.md index 06cf5d1..152d833 100644 --- a/home_page/index.md +++ b/home_page/index.md @@ -40,60 +40,57 @@ If you'd like to contribute, you may find the following links useful: Chapters 1–9 of the blueprint unpack and analyse the original Haag–Kastler axioms one by one: - **Chapter 1** presents the original Haag–Kastler axioms as stated in the 1964 paper. -- **Chapter 2 (Axiom 0 – Minkowski Space)** examines the role of Minkowski spacetime and compares the standard, indiscrete, Euclidean, and Alexandrov topologies on it. -- **Chapter 3 (Axiom 1 – Local Algebras)** discusses the notion of regions of measurement and the assignment of a C\*-algebra to each such region. -- **Chapter 4 (Axiom 2 – Isotony)** introduces the GNS Construction in motivating context and studies the isotony condition—the requirement that inclusions of spacetime regions induce \*-monomorphisms of the corresponding algebras. -- **Chapter 5 (Axiom 3 – Local Commutativity)** introduces the notion of completely spacelike separated regions and the quasilocal algebra, and studies the requirement that observables localised in spacelike separated regions commute. -- **Chapter 6 (Axiom 4 – Quasilocal Algebra)** analyses the construction of the quasilocal algebra as the completion of the set-theoretic union of all local algebras, and the axiom that all observables are quasilocal. -- **Chapter 7 (Axiom 5 – Lorentz Covariance)** studies the action of the inhomogeneous Lorentz group (connected to the identity) on the net of local algebras and the covariance requirement. -- **Chapter 8 (Axiom 6 – Primitivity)** examines faithful and irreducible representations; this axiom is ultimately abandoned in the sharpened formulation. +- **Chapter 2 (Axiom 0 – Minkowski Space)** examines the role of Minkowski spacetime and compares the standard, indiscrete, Euclidean, and Alexandrov topologies on it, settling on the Alexandrov topology—generated by the "double cone" sets $$I^+(p) \cap I^-(q)$$—as the physically natural choice, which happens to coincide with the Euclidean topology on $$\mathbb{R}^4$$. +- **Chapter 3 (Axiom 1 – Local Algebras)** discusses the notion of regions of measurement and the assignment of a C\*-algebra to each such region, arguing that the "physically natural" regions are double cones $$I^+(p) \cap I^-(q)$$ rather than arbitrary open sets with compact closure, and rejecting the causal (light-cone) alternative $$J^+(p) \cap J^-(q)$$ because it would force single points to carry algebras, which conflicts with fields being operator-valued distributions. +- **Chapter 4 (Axiom 2 – Isotony)** introduces the GNS Construction in motivating context, studies the isotony condition—the requirement that inclusions of spacetime regions induce \*-monomorphisms of the corresponding algebras—and settles the "common unit" convention flagged in the original axiom by assigning the empty region the algebra $$\mathbb{C}1$$, so that every local algebra automatically contains a unit. +- **Chapter 5 (Axiom 3 – Local Commutativity)** introduces the notion of completely spacelike separated regions and the quasilocal algebra, and studies the requirement that observables localised in spacelike separated regions commute, clarifying that this commutation is to be understood inside the quasilocal algebra $$\mathfrak{U}$$, since isotony alone cannot place two spacelike-separated (and hence non-nested) regions in a common algebra. +- **Chapter 6 (Axiom 4 – Quasilocal Algebra)** analyses the construction of the quasilocal algebra as the completion of the set-theoretic union of all local algebras, and the axiom that $$\mathfrak{U}$$ contains all observables of interest—which is shown to mean that $$\pi_\omega(\mathfrak{U})$$ is strongly dense in the von Neumann algebra $$\pi_\omega(\mathfrak{U})''$$ it generates, so that any "missing" observable in $$\pi_\omega(\mathfrak{U})'' \setminus \pi_\omega(\mathfrak{U})$$ is experimentally indistinguishable from one in $$\mathfrak{U}$$. +- **Chapter 7 (Axiom 5 – Lorentz Covariance)** studies the action of the inhomogeneous Lorentz group (connected to the identity) on the net of local algebras and the covariance requirement, and shows, via the Bounded Linear Transformation Theorem, how this norm-one action extends uniquely from the dense union of local algebras to the whole quasilocal algebra. +- **Chapter 8 (Axiom 6 – Primitivity)** examines faithful and irreducible representations, noting that every unital C\*-algebra already has a faithful representation (Gelfand–Naimark) so primitivity is a genuinely extra condition; this axiom is ultimately abandoned in the sharpened formulation, following later presentations by Haag himself, on the grounds that its physical motivation is thin. - **Chapter 9 (Haag–Kastler Axioms in Curved Spacetime)** generalises the Haag–Kastler axioms from Minkowski spacetime to curved (Lorentzian) spacetime. It first pins down a precise definition of Lorentzian spacetime and its Alexandrov topology, then shows—via a Schwarzschild black-hole counterexample—that a quasilocal algebra need not exist on a generic Lorentzian spacetime, so Local Commutativity and the local-algebra axiom must be restated relative to a common containing region rather than a global algebra. The final section replaces Lorentz covariance with covariance under identity-component isometries; a formalisation remark notes that the Lean development works with the intersection of the identity component with the (explicitly orientation-preserving) isometry subgroup, since the inclusion of the identity component into the orientation-preserving isometries would otherwise rely on a Myers–Steenrod-type rigidity result not yet available in Mathlib—an implementation choice that does not alter the mathematical content of the axiom. -Chapter 10 assembles the formalisation-ready content, organised into seven main blocks: +Chapter 10 assembles the formalisation-ready content, organised into seven main blocks that follow the section structure of the chapter itself (§10.1–§10.4): -- **GNS Construction.** Carefully states and proves the GNS Construction Theorem in full detail—construction of the GNS Hilbert space, the \*-representation, the cyclic vector, faithfulness, and uniqueness up to unitary equivalence—since both the theorem and specific steps of its proof are used in the axioms that follow. +- **GNS Construction (§10.1).** Carefully states and proves the GNS Construction Theorem in full detail—construction of the GNS Hilbert space, the \*-representation, the cyclic vector, faithfulness, and uniqueness up to unitary equivalence—since both the theorem and specific steps of its proof are used in the axioms that follow. -- **Spacetime and causal structure.** Gives precise definitions of spacetime, Minkowski spacetime, and Lorentzian spacetime, together with the full apparatus of causal structure: timelike, spacelike, and null vectors; time orientation; future- and past-pointing vectors; paths, curves, and trips; causal trips; chronological and causal futures and pasts; spacelike separation; and the Alexandrov topology. Supporting lemmas establish the basic geometry (the causal classification trichotomy, the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors, convexity of the future and past cones, monotonicity of futures and pasts, symmetry of spacelike separation, and the fact that isometries preserve causal classification, chronology, and Alexandrov-basis sets). +- **Spacetime and causal structure (§10.2).** Gives precise definitions of spacetime, Minkowski spacetime, and Lorentzian spacetime, together with the full apparatus of causal structure: timelike, spacelike, and null vectors; time orientation; future- and past-pointing vectors; paths; curves and oriented curves, defined as equivalence classes of paths up to reparametrisation, with the causal type and the future/past orientation each shown to be well-defined on the quotient (Theorems 35 and 37) and a forgetful projection from oriented to unoriented curves (Theorem 38); trips and causal trips; chronological and causal futures and pasts; spacelike separation; and the Alexandrov topology. Supporting lemmas establish the basic geometry (the causal classification trichotomy, the reverse Cauchy–Schwarz and reverse triangle inequalities for timelike vectors, convexity of the future and past cones, monotonicity of futures and pasts, symmetry of spacelike separation, and, in §10.2.1, the fact that isometries preserve causal classification, chronology, and Alexandrov-basis sets). -- **Sharpened Haag–Kastler Axioms in Minkowski spacetime.** States the sharpened axioms—Local Algebras, Isotony, Local Commutativity, Quasilocal Completeness, and Lorentz Covariance—bundled into a single `HaagKastlerNet` structure (Definitions 57–64). Derives the operator form of Einstein Causality in a representation (Theorem 65). Then develops the covariance structure: - - Defines covariant families of local states (Definition 97) and the lift of the fiberwise covariance action to a \*-automorphism of the quasilocal algebra—the `QuasilocalCovarianceAutomorphism` (Definition 99)—and establishes its uniqueness (Lemma 100), existence (Theorem 101), and existence for the trivial net (Theorem 102). This data is bundled into a `CovariantQuasilocalAlgebra` structure (Definition 103), on which the covariance action is a genuine group action (Lemma 104). - - Defines invariant states (Definition 105) and proves GNS-unitary implementation of a Poincaré-invariant state (Theorem 106). - - Proves that a state that is both invariant and pure yields a GNS representation that is simultaneously covariant and irreducible—a necessary precursor to a vacuum representation (Theorem 107). - - Lays a "bounded-generator" scaffold toward the spectrum condition, deliberately sidestepping Stone's theorem and unbounded self-adjoint operators (not yet available for this purpose in Mathlib): positive energy for a bounded generator (Definition 108) together with its basic API—the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is automatically strongly continuous (Theorem 109); a generator-parameterised notion of vacuum state (Definition 110) and its Stone-free consequences, namely invariance and, for a pure state, irreducibility of the resulting covariant GNS representation (Theorem 111); the future-timelike translation subgroup of the inhomogeneous Lorentz group, which supplies the concrete family of one-parameter subgroups the spectrum condition is to be imposed on (Definition 112); and the vacuum-state definition with this concrete predicate substituted in, leaving no free parameter (Definition 113). - - Proves that purity of a state is preserved by any \*-automorphism and is therefore a Lorentz-covariance-invariant property (Theorem 114). +- **Sharpened Haag–Kastler Axioms in Minkowski spacetime (§10.3, §10.3.1, §10.3.6).** States the sharpened axioms—Local Algebras, Isotony, Local Commutativity, Quasilocal Completeness, and Lorentz Covariance—bundled into a single `HaagKastlerNet` structure (Definitions 61–68). Derives the operator form of Einstein Causality in a representation (Theorem 69). Then develops the covariance structure: + - Defines covariant families of local states (Definition 113) and the lift of the fiberwise covariance action to a \*-automorphism of the quasilocal algebra—the `QuasilocalCovarianceAutomorphism` (Definition 115)—and establishes its uniqueness (Lemma 116), existence (Theorem 117), and existence for the trivial net (Theorem 118). This data is bundled into a `CovariantQuasilocalAlgebra` structure (Definition 119), on which the covariance action is a genuine group action (Lemma 120). + - Defines invariant states (Definition 121) and proves GNS-unitary implementation of a Poincaré-invariant state (Theorem 122). + - Proves that a state that is both invariant and pure yields a GNS representation that is simultaneously covariant and irreducible—a necessary precursor to a vacuum representation (Theorem 123). + - Lays a "bounded-generator" scaffold toward the spectrum condition, deliberately sidestepping Stone's theorem and unbounded self-adjoint operators (not yet available for this purpose in Mathlib): positive energy for a bounded generator (Definition 124) together with its basic API—the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is automatically strongly continuous (Theorem 125); a generator-parameterised notion of vacuum state (Definition 126) and its Stone-free consequences, namely invariance and, for a pure state, irreducibility of the resulting covariant GNS representation (Theorem 127); the future-timelike translation subgroup of the inhomogeneous Lorentz group, which supplies the concrete family of one-parameter subgroups the spectrum condition is to be imposed on (Definition 128); and the vacuum-state definition with this concrete predicate substituted in, leaving no free parameter (Definition 129). + - Proves that purity of a state is preserved by any \*-automorphism and is therefore a Lorentz-covariance-invariant property (Theorem 130). -- **Sharpened Haag–Kastler Axioms in curved spacetime.** States the curved-spacetime axioms—Local Algebras, Isotony, Local Commutativity, Local Completeness, and Isometric Covariance—bundled into a `HaagKastlerNet` in curved spacetime (Definitions 131–137). Derives the operator form of Einstein Causality relative to a containing local algebra (Theorem 138). Then develops the curved-spacetime covariance structure: - - Defines covariant families of local states in curved spacetime (Definition 153) and proves their composition law (Lemma 154). - - Since no quasilocal algebra exists in a generic Lorentzian spacetime, the covariance action restricts to the stabiliser subgroup $$\mathrm{Stab}(\mathbf{B})$$ of a region—the isometries that fix $$\mathbf{B}$$—defining automorphisms of the single local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 155), and proves that this stabiliser action is a genuine group action (Lemma 156). - - Proves that a stabiliser-invariant state carries a unitary GNS representation of $$\mathrm{Stab}(\mathbf{B})$$ (Theorem 157), strongly continuous when the matrix coefficients are continuous (Theorem 158). - - Proves that a state that is both stabiliser-invariant and pure yields an irreducible covariant GNS representation of $$\mathrm{Stab}(\mathbf{B})$$—the curved-spacetime analogue of the precursor to a vacuum representation (Theorem 159). - - Proves that purity of a state on a local algebra is invariant under the stabiliser action (Theorem 160). +- **Sharpened Haag–Kastler Axioms in curved spacetime (§10.4, §10.4.1, §10.4.4, §10.4.5).** States the curved-spacetime axioms—Local Algebras, Isotony, Local Commutativity, Local Completeness, and Isometric Covariance—bundled into a `HaagKastlerNet` in curved spacetime (Definitions 147–153). Derives the operator form of Einstein Causality relative to a containing local algebra (Theorem 154). Then develops the curved-spacetime covariance structure: + - Defines covariant families of local states in curved spacetime (Definition 170) and proves their composition law (Lemma 171). + - Since no quasilocal algebra exists in a generic Lorentzian spacetime, the covariance action restricts to the stabiliser subgroup $$\mathrm{Stab}(\mathbf{B})$$ of a region—the isometries that fix $$\mathbf{B}$$—defining automorphisms of the single local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 172), and proves that this stabiliser action is a genuine group action (Lemma 173). + - Proves that a stabiliser-invariant state carries a unitary GNS representation of $$\mathrm{Stab}(\mathbf{B})$$ (Theorem 174), strongly continuous when the matrix coefficients are continuous (Theorem 175). + - Proves that a state that is both stabiliser-invariant and pure yields an irreducible covariant GNS representation of $$\mathrm{Stab}(\mathbf{B})$$—the curved-spacetime analogue of the precursor to a vacuum representation (Theorem 176). + - Proves that purity of a state on a local algebra is invariant under the stabiliser action (Theorem 177). -- **Local von Neumann algebras and irreducibility.** Develops the von Neumann algebra layer of the theory in both settings: - - Defines the local von Neumann algebra $$R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$$ of a region in a representation (Definitions 66–67, 139–140), and proves Microcausality (Theorems 68, 141) and Isotony of the von Neumann net (Theorems 69, 142), together with their bundled forms on Mathlib's `VonNeumannAlgebra` type (Theorems 70, 143), in both Minkowski and curved spacetime. Packages the region-indexed assignment $$\mathbf{B} \mapsto R(\mathbf{B})$$ as an order-preserving map on the poset of regions—the net of von Neumann algebras itself—both for the full quasilocal net in Minkowski spacetime (Definition 71) and, relative to a containing region, in curved spacetime (Definition 144). - - Proves the Statistical Independence (Schlieder) property: 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 (Theorems 72–73, 145–146). - - Proves Geometric Covariance of the von Neumann net: conjugation by the unitary implementing a symmetry carries the local von Neumann algebra of a region onto that of the transformed region, via the covariance representation in Minkowski spacetime (Theorem 74) and via the stabiliser GNS representation in curved spacetime (Theorem 147). As a consequence, being a factor is constant along the orbit of a region under the symmetry (Theorems 75, 148), and the underlying set-level equality upgrades to a first-class \*-algebra isomorphism of the bundled local von Neumann algebras (Theorems 76, 149). - - Introduces irreducible representations via their commutant (Definition 77) and establishes the Topological Schur Lemma for cyclic representations (Theorem 78), together with the operator-theoretic bridge identifying commutant scalars with coefficients proportional to the state (Theorem 79). - - Proves the equivalence Pure $$\iff$$ Irreducible (Theorem 84), including the GNS Radon–Nikodym theorem (Theorems 82–83) that realises every dominated positive functional as an operator in the commutant. - - Proves that the norm of any positive linear functional on a unital C\*-algebra equals its value on the unit (Theorem 90), and uses this to establish Pure $$\iff$$ Extreme Point of the state space (Theorem 92), the underlying convexity of the state space and its link to Mathlib's extreme-points API (Theorem 93), and the weak-\* compactness of the state space, which supplies the existence of pure states via Krein–Milman (Theorem 94). - - Proves that an irreducible representation generates a factor (Theorem 85) and, more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 86), with a bundled density form of this statement on Mathlib's `VonNeumannAlgebra` type (Theorem 87); consequently the GNS representation of a pure state generates a factor (Theorem 88) and, more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 89). - - Specialises all of the above to the quasilocal algebra $$\mathfrak{U}$$ (Theorems 95–96) and to each local algebra $$\mathfrak{U}(\mathbf{B})$$ in curved spacetime (Theorems 150–151), and shows in addition that the GNS representation of a pure state on a curved-spacetime local algebra generates a factor and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 152). +- **Local von Neumann algebras, irreducibility, and superselection theory (§10.3.2–§10.3.5, §10.4.2–§10.4.3).** This is the largest block, developing the von Neumann algebra layer of the theory in both settings, then the representation-theoretic machinery—irreducibility, purity, unitary equivalence, and direct sums—that sits on top of it: + - *Local algebras and the net.* Defines the local von Neumann algebra $$R(\mathbf{B}) = \pi(\mathfrak{U}(\mathbf{B}))''$$ of a region in a representation (Definitions 70–71 in Minkowski spacetime, Definitions 155–156 in curved spacetime), and proves Microcausality (Theorems 72, 157) and Isotony of the von Neumann net (Theorems 73, 158), together with their bundled forms on Mathlib's `VonNeumannAlgebra` type (Theorems 74, 159). Packages the region-indexed assignment $$\mathbf{B} \mapsto R(\mathbf{B})$$ as an order-preserving map on the poset of regions—the net of von Neumann algebras itself—both for the full quasilocal net in Minkowski spacetime (Definition 75) and, relative to a containing region, in curved spacetime (Definition 160). + - *Statistical independence and geometric covariance.* Proves the Statistical Independence (Schlieder) property: 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 (Theorems 76–77 in Minkowski spacetime, Theorems 161–162 in curved spacetime). Proves Geometric Covariance of the von Neumann net: conjugation by the unitary implementing a symmetry carries the local von Neumann algebra of a region onto that of the transformed region, via the covariance representation in Minkowski spacetime (Theorem 78) and via the stabiliser GNS representation in curved spacetime (Theorem 163). As a consequence, being a factor is constant along the orbit of a region under the symmetry (Theorems 79, 164), and the underlying set-level equality upgrades to a first-class \*-algebra isomorphism of the bundled local von Neumann algebras (Theorems 80, 165). + - *Irreducibility, purity, and Schur's Lemma.* Introduces irreducible representations via their commutant (Definition 81) and establishes the Topological Schur Lemma for cyclic representations (Theorem 82), together with the operator-theoretic bridge identifying commutant scalars with coefficients proportional to the state (Theorem 83). Defines pure states (Definition 84) and proves "pure implies irreducible" directly (Theorem 85), then the full equivalence Pure $$\iff$$ Irreducible (Theorem 88) via a GNS Radon–Nikodym theorem that realises every dominated positive functional as an operator in the commutant (Theorems 86–87). Proves that an irreducible representation generates a factor (Theorem 89) and, more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 90), with a bundled density form of this statement on Mathlib's `VonNeumannAlgebra` type (Theorem 91); consequently the GNS representation of a pure state generates a factor (Theorem 92) and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 93). Proves that the norm of any positive linear functional on a unital C\*-algebra equals its value on the unit (Theorem 94), and uses this to establish Pure $$\iff$$ Extreme Point of the state space (Definition 95, Theorem 96), the underlying convexity of the state space and its link to Mathlib's extreme-points API (Theorem 97), and the weak-\* compactness of the state space, which supplies the existence of pure states via Krein–Milman (Theorem 98). Specialises all of the above to the quasilocal algebra $$\mathfrak{U}$$ (Theorems 99–100) and to each local algebra $$\mathfrak{U}(\mathbf{B})$$ in curved spacetime (Theorems 166–168), and additionally registers, per region, the irreducible dichotomy discussed next (Theorem 169). + - *Unitary equivalence and superselection theory.* Defines unitary equivalence of representations as an equivalence relation (Definition 101), and shows irreducibility and factoriality are unitary invariants, transported by the cross-space conjugation induced by the implementing unitary (Theorem 102). Defines disjointness of representations via the vanishing of all intertwiners (Definition 103) and the coarser notion of quasi-equivalence via a \*-isomorphism of generated von Neumann algebras (Definition 104), with unitary equivalence shown to imply quasi-equivalence. Proves Schur's Lemma in the form of the Irreducible Dichotomy: a nonzero intertwiner between two irreducible representations rescales to a unitary equivalence, so two irreducible representations are always either disjoint or unitarily equivalent (Theorem 105)—the foundational trichotomy of superselection theory. Proves the space of intertwiners between two irreducible representations is at most one-dimensional (Lemma 106) and that the endomorphism algebra of an irreducible representation is exactly $$\mathbb{C} \cdot 1$$ (Lemma 107). Applies the dichotomy to GNS representations of pure states to obtain the Pure-State Dichotomy underlying superselection sectors (Theorem 108). + - *Direct sums, amplification, and reducibility.* Defines the direct-sum representation of a family of \*-representations on the $$\ell^2$$-direct sum of their Hilbert spaces (Definition 109), and shows each summand embeds as a subrepresentation whose projection lies in the commutant of the sum (Theorem 110). Defines the $$\iota$$-fold amplification of a single representation as the direct sum of $$\iota$$ copies of itself (Definition 111), and proves a direct sum with at least two nonzero summands is always reducible, so a multiply-amplified representation is never irreducible (Theorem 112). -- **Separating vectors and faithful states.** Proves that the cyclic vector of a faithful state is also separating for the image of the GNS representation (Theorem 115)—the basic datum of Tomita–Takesaki modular theory. This result holds in any representation reproducing a faithful state, not only the canonical GNS one. +- **Separating vectors and faithful states (§10.3.7).** Proves that the cyclic vector of a faithful state is also separating for the image of the GNS representation (Theorem 131)—the basic datum of Tomita–Takesaki modular theory. This result holds in any representation reproducing a faithful state, not only the canonical GNS one. -- **KMS condition and thermal equilibrium.** Introduces one-parameter automorphism groups and KMS states as the algebraic characterisation of thermal equilibrium. The main analytical ingredients are: - - The Strip-Liouville Principle (Definition 120): a function continuous and bounded on a closed strip, holomorphic on the open strip, and with equal boundary values on both edges must be constant along the real axis. - - This is proved at positive inverse temperature via a periodic entire extension—the strip Schwarz reflection (Theorem 121)—followed by Liouville's theorem (Theorem 122). +- **KMS condition and thermal equilibrium (§10.3.8, §10.3.9, §10.4.6).** Introduces one-parameter automorphism groups (Definition 132) and KMS states (Definition 133) as the algebraic characterisation of thermal equilibrium. The main analytical ingredients are: + - The Strip-Liouville Principle (Definition 136): a function continuous and bounded on a closed strip, holomorphic on the open strip, and with equal boundary values on both edges must be constant along the real axis. + - This is proved at positive inverse temperature via a periodic entire extension—the strip Schwarz reflection (Theorem 137)—followed by Liouville's theorem (Theorem 138). From these ingredients the following consequences are derived: - - Every KMS state at positive inverse temperature is automatically invariant under the time evolution (Theorem 123). - - The analytic completion of a KMS correlation function is unique: any two strip-functions sharing both boundary values agree everywhere on the strip (Theorems 124–125). - - The set of KMS states at fixed temperature and flow is convex (Theorem 118). + - Every KMS state at positive inverse temperature is automatically invariant under the time evolution, via a boundary-coincidence argument (Lemma 135, Theorem 139). + - The analytic completion of a KMS correlation function is unique: any two strip-functions sharing both boundary values agree everywhere on the strip (Theorems 140–141). + - The set of KMS states at fixed temperature and flow is convex (Theorem 134). - In the Minkowski setting, a one-parameter subgroup of the inhomogeneous Lorentz group induces a one-parameter automorphism group on the quasilocal algebra via the covariance lift (Lemma 127), and KMS states for that flow are defined accordingly (Definition 128; convexity Theorem 129). The corresponding zero-temperature ($$\beta \to \infty$$) notion—a ground state for a covariance flow, whose GNS-implementing unitary group has positive energy—is recorded alongside it (Definition 130). + In the Minkowski setting, a one-parameter subgroup of the inhomogeneous Lorentz group induces a one-parameter automorphism group on the quasilocal algebra via the covariance lift (Definition 142, Lemma 143), and KMS states for that flow are defined accordingly (Definition 144; convexity Theorem 145). The corresponding zero-temperature ($$\beta \to \infty$$) notion—a ground state for a covariance flow, whose GNS-implementing unitary group has positive energy—is recorded alongside it (Definition 146). - In the curved-spacetime setting, Killing flows are identified as one-parameter subgroups of the stabiliser of a region, inducing a one-parameter automorphism group on the local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 161, Lemma 162). KMS states for a Killing flow are the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal (Definition 163). A KMS state for a Killing flow 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 (equilibrium) representation (Theorem 164; convexity Theorem 165). The corresponding ground state for a Killing flow is recorded alongside it too (Definition 166). + In the curved-spacetime setting, Killing flows are identified as one-parameter subgroups of the stabiliser of a region, inducing a one-parameter automorphism group on the local algebra $$\mathfrak{U}(\mathbf{B})$$ (Definition 178, Lemma 179). KMS states for a Killing flow are the precise algebraic sense in which the Hartle–Hawking and Gibbons–Hawking states are thermal (Definition 180). A KMS state for a Killing flow 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 (equilibrium) representation (Theorem 181; convexity Theorem 182). The corresponding ground state for a Killing flow is recorded alongside it too (Definition 183). ## What is Being Formalised @@ -107,139 +104,161 @@ Only the content of Chapter 10 is formalised in Lean. This comprises: **Spacetime and causal structure** - Spacetime (Definition 19), Standard Minkowski Spacetime (Definition 20) - Timelike / Spacelike / Null Vectors (Definition 21), Time Orientation (Definition 25), Future- and Past-Pointing Vectors (Definition 26) -- Paths (Definition 31), Curves (Definition 32), Timelike and Causal Smooth Curves (Definition 33), Future- and Past-Oriented Smooth Curves (Definition 34), Endpoints (Definition 35) -- Trip (Definition 36), Causal Trip (Definition 37) -- Chronological Future and Past (Definition 38), Causal Future and Past (Definition 39) -- Spacelike Related (Definition 42), Completely Spacelike (Definition 43) -- Alexandrov Topology (Definition 46), Minkowski Spacetime (Definition 48), Lorentzian Spacetime (Definition 49) +- Paths (Definition 31), Curves (Definition 32), Timelike and Causal Smooth Curves (Definition 33), Future- and Past-Oriented Smooth Curves (Definition 34), Oriented Smooth Curve (Definition 36) +- Endpoints (Definition 39), Trip (Definition 40), Causal Trip (Definition 41) +- Chronological Future and Chronological Past (Definition 42), Causal Future and Causal Past (Definition 43) +- Spacelike Related (Definition 46), Completely Spacelike (Definition 47) +- Alexandrov Topology (Definition 50), Minkowski Spacetime (Definition 52), Lorentzian Spacetime (Definition 53) **Sharpened axioms – Minkowski spacetime** -- Axiom 1: Local Algebras (Definition 57), Axiom 2: Isotony (Definition 58) -- Quasilocal Algebra (Definition 59), Axiom 3: Local Commutativity (Definition 60) -- Quasilocal Observable (Definition 61), Axiom 4: Quasilocal Completeness (Definition 62) -- Axiom 5: Lorentz Covariance (Definition 63), Haag–Kastler Net (Definition 64) -- Covariant Family of Local States (Definition 97), Quasilocal Covariance Automorphism (Definition 99) -- Covariant Quasilocal Algebra (Definition 103), Invariant State (Definition 105) -- Positive Energy for a bounded generator (Definition 108), Vacuum State, generator-parameterised scaffold (Definition 110) -- Future-Timelike Translation Subgroup (Definition 112), Vacuum State with the Concrete Spectrum Condition (Definition 113) +- Axiom 1: Local Algebras (Definition 61), Axiom 2: Isotony (Definition 62) +- Quasilocal Algebra (Definition 63), Axiom 3: Local Commutativity (Definition 64) +- Quasilocal Observable (Definition 65), Axiom 4: Quasilocal Completeness (Definition 66) +- Axiom 5: Lorentz Covariance (Definition 67), Haag–Kastler Net (Definition 68) +- Covariant Family of Local States (Definition 113), Quasilocal Covariance Automorphism (Definition 115) +- Covariant Quasilocal Algebra (Definition 119), Invariant State (Definition 121) +- Positive Energy for a bounded generator (Definition 124), Vacuum State, generator-parameterised scaffold (Definition 126) +- Future-Timelike Translation Subgroup (Definition 128), Vacuum State with the Concrete Spectrum Condition (Definition 129) **Sharpened axioms – curved spacetime** -- Axiom 1: Local Algebras (Definition 131), Axiom 2: Isotony (Definition 132) -- Axiom 3: Local Commutativity (Definition 133), Local Observable (Definition 134) -- Axiom 4: Local Completeness (Definition 135), Axiom 5: Isometric Covariance (Definition 136) -- Haag–Kastler Net in Curved Spacetime (Definition 137) -- Covariant Family of Local States in Curved Spacetime (Definition 153) -- Stabiliser Action on a Local Algebra (Definition 155) -- Killing-Flow Automorphism Family (Definition 161), KMS State for a Killing Flow (Definition 163), Ground State for a Killing Flow (Definition 166) +- Axiom 1: Local Algebras (Definition 147), Axiom 2: Isotony (Definition 148) +- Axiom 3: Local Commutativity (Definition 149), Local Observable (Definition 150) +- Axiom 4: Local Completeness (Definition 151), Axiom 5: Isometric Covariance (Definition 152) +- Haag–Kastler Net in Curved Spacetime (Definition 153) +- Covariant Family of Local States in Curved Spacetime (Definition 170) +- Stabiliser Action on a Local Algebra (Definition 172) +- Killing-Flow Automorphism Family (Definition 178), KMS State for a Killing Flow (Definition 180), Ground State for a Killing Flow (Definition 183) **Local von Neumann algebras and irreducibility** -- Local von Neumann Algebra – Minkowski spacetime (Definition 66) -- The Net of von Neumann Algebras – Minkowski spacetime (Definition 71) -- Local von Neumann Algebra – curved spacetime (Definition 139) -- The Net of von Neumann Algebras – curved spacetime (Definition 144) -- Irreducible Representation (Definition 77) -- Pure State (Definition 80) -- Extreme Point of the State Space (Definition 91) +- Local von Neumann Algebra – Minkowski spacetime (Definition 70) +- $$R(\mathbf{B})$$ as a von Neumann Algebra – Minkowski spacetime (Definition 71) +- The Net of von Neumann Algebras – Minkowski spacetime (Definition 75) +- Local von Neumann Algebra – curved spacetime (Definition 155) +- $$R(\mathbf{B}')$$ as a von Neumann Algebra – curved spacetime (Definition 156) +- The Net of von Neumann Algebras – curved spacetime (Definition 160) +- Irreducible Representation (Definition 81) +- Pure State (Definition 84) +- Extreme Point of the State Space (Definition 95) + +**Unitary equivalence and superselection theory** +- Unitary Equivalence of Representations (Definition 101) +- Disjoint Representations (Definition 103) +- Quasi-Equivalence of Representations (Definition 104) + +**Direct sums, amplification, and reducibility** +- Direct-Sum Representation (Definition 109) +- Amplification (Definition 111) **KMS condition** -- One-Parameter Automorphism Group (Definition 116), KMS State (Definition 117) -- Covariance-Flow Automorphism Family (Definition 126), KMS State for the Covariance Flow (Definition 128), Ground State for a Covariance Flow (Definition 130) -- Strip-Liouville Principle (Definition 120) +- One-Parameter Automorphism Group (Definition 132), KMS State (Definition 133) +- Strip-Liouville Principle (Definition 136) +- Covariance-Flow Automorphism Family (Definition 142), KMS State for the Covariance Flow (Definition 144), Ground State for a Covariance Flow (Definition 146) ### Lemmas and Theorems **GNS Construction** - Cauchy–Schwarz inequality for states (Lemma 16) -- Equivalence of the two descriptions of the left-ideal $$\mathcal{N}$$ (Lemma 17); $$\mathcal{N}$$ is a closed linear subspace (Lemma 18) +- Equivalence of the two descriptions of the left ideal $$\mathcal{N}$$ (Lemma 17); $$\mathcal{N}$$ is a closed linear subspace (Lemma 18) - Full GNS Construction Theorem: Hilbert space, \*-representation, cyclic vector, faithfulness, uniqueness up to unitary equivalence (Theorem 15) **Causal structure** - Causal classification trichotomy (Lemma 22) - Reverse Cauchy–Schwarz inequality for timelike vectors (Lemma 23); reverse triangle inequality (Lemma 24) -- Sign lemma for the future cone (Lemma 28); definiteness of the spacelike complement (Lemma 29); convexity of the future and past cones (Lemma 30) -- Chronological precedence implies causal precedence (Lemma 40) -- Monotonicity of futures and pasts (Lemma 41); symmetry of spacelike separation (Lemma 44) -- Structural properties of complete spacelike separation (Lemma 45); basis sets are Alexandrov-open (Lemma 47); bundled spacelike separation and basis openness (Lemma 50) +- Orientation of pointing vectors is well-defined (Lemma 27); sign lemma for the future cone (Lemma 28); definiteness of the spacelike complement (Lemma 29); convexity of the future and past cones (Lemma 30) +- Reparametrisation-invariance of the causal type of a curve (Theorem 35); reparametrisation-invariance of future/past orientation (Theorem 37); the forgetful projection from oriented to unoriented curves (Theorem 38) +- Chronological precedence implies causal precedence (Lemma 44) +- Monotonicity of futures and pasts (Lemma 45); symmetry of spacelike separation (Lemma 48) +- Structural properties of complete spacelike separation (Lemma 49); basis sets are Alexandrov-open (Lemma 51); bundled spacelike separation and basis openness (Lemma 54) **Isometry preservation** -- Isometries preserve the causal classification (Lemma 51) -- Unique differentials along a path (Lemma 52); pushforward of a path under an isometry (Lemma 53) -- Isometries preserve chronology (Lemma 54); isometries preserve Alexandrov-basis sets, formalised for the oriented identity component of the isometry group (Lemma 55) -- Axiom 5 basis-set preservation (Lemma 56) +- Isometries preserve the causal classification (Lemma 55) +- Unique differentials along a path (Lemma 56); pushforward of a path under an isometry (Lemma 57) +- Isometries preserve chronology (Lemma 58); isometries preserve Alexandrov-basis sets, formalised for the oriented identity component of the isometry group (Lemma 59) +- Axiom 5 basis-set preservation (Lemma 60) **Covariance – Minkowski spacetime** -- Composition of covariance (Lemma 98) -- Uniqueness of the quasilocal covariance lift (Lemma 100); existence of the quasilocal covariance lift (Theorem 101); existence for the trivial net (Theorem 102) -- Group-action coherence of the covariance automorphism (Lemma 104) -- GNS-unitary implementation of an invariant state (Theorem 106) -- Irreducible covariant GNS representation of a pure invariant state (Theorem 107) -- Positive-Energy API: the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is strongly continuous (Theorem 109) -- No-Stone consequences of a vacuum state: invariance, and (for a pure state) irreducibility of the covariant GNS representation (Theorem 111) -- Purity is covariance-invariant: purity is preserved under pullback by any \*-automorphism, and in particular under the covariance automorphism $$\beta_L$$ (Theorem 114) -- Einstein Causality in a representation (Theorem 65) +- Composition of covariance (Lemma 114) +- Uniqueness of the quasilocal covariance lift (Lemma 116); existence of the quasilocal covariance lift (Theorem 117); existence for the trivial net (Theorem 118) +- Group-action coherence of the covariance automorphism (Lemma 120) +- GNS-unitary implementation of an invariant state (Theorem 122) +- Irreducible covariant GNS representation of a pure invariant state (Theorem 123) +- Positive-Energy API: the trivial group has positive energy, the witnessing generator is unique, positive energy is preserved under unitary conjugation, and a positive-energy group is strongly continuous (Theorem 125) +- No-Stone consequences of a vacuum state: invariance, and (for a pure state) irreducibility of the covariant GNS representation (Theorem 127) +- Purity is covariance-invariant: purity is preserved under pullback by any \*-automorphism, and in particular under the covariance automorphism $$\beta_L$$ (Theorem 130) +- Einstein Causality in a representation (Theorem 69) **Covariance – curved spacetime** -- Composition of covariance in curved spacetime (Lemma 154) -- The stabiliser action is a group action (Lemma 156) -- GNS unitary representation of the stabiliser (Theorem 157); strongly continuous stabiliser GNS unitary (Theorem 158) -- Irreducible covariant GNS representation of a pure invariant state on a local algebra (Theorem 159) -- Purity is invariant under the stabiliser action (Theorem 160) -- Einstein Causality in a representation, curved spacetime (Theorem 138) +- Composition of covariance in curved spacetime (Lemma 171) +- The stabiliser action is a group action (Lemma 173) +- GNS unitary representation of the stabiliser (Theorem 174); strongly continuous stabiliser GNS unitary (Theorem 175) +- Irreducible covariant GNS representation of a pure invariant state on a local algebra (Theorem 176) +- Purity is invariant under the stabiliser action (Theorem 177) +- Einstein Causality in a representation, curved spacetime (Theorem 154) **Local von Neumann algebras – Minkowski spacetime** -- $$R(\mathbf{B})$$ as a von Neumann algebra (Definition 67) -- Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 68) -- Isotony of the von Neumann net (Theorem 69) -- Bundled von Neumann microcausality and isotony (Theorem 70) -- The net of von Neumann algebras as an order-preserving map on the poset of regions (Definition 71) -- Statistical Independence (Schlieder Property): the cyclic vector of one region is separating for the local von Neumann algebra of any spacelike-separated region (Theorems 72–73) -- Geometric Covariance of the von Neumann net: conjugation by the implementing unitary carries the local von Neumann algebra of a region onto that of the transformed region (Theorem 74); orbit-invariance of factoriality along the symmetry orbit (Theorem 75); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 76) -- Topological Schur Lemma for cyclic representations (Theorem 78) -- Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 79) -- Pure state implies irreducible GNS representation (Theorem 81) -- GNS Radon–Nikodym form is bounded (Theorem 82); GNS Radon–Nikodym operator exists and commutes with the representation (Theorem 83) -- Pure state $$\iff$$ irreducible GNS representation (Theorem 84) -- An irreducible representation generates a von Neumann algebra with trivial centre, i.e. a factor (Theorem 85); more sharply, an irreducible representation generates the whole of $$\mathcal{B}(H)$$ (Theorem 86); bundled density form on Mathlib's `VonNeumannAlgebra` type (Theorem 87) -- The GNS representation of a pure state generates a factor (Theorem 88); more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 89) -- Norm of a positive linear functional equals its value on the unit (Theorem 90) -- Pure state $$\iff$$ extreme point of the state space (Theorem 92); state-space convexity and the extreme-point bridge (Theorem 93); weak-\* compactness of the state space (Theorem 94) -- Pure state $$\iff$$ extreme point of the state space of the quasilocal algebra (Theorem 95) -- Pure state $$\iff$$ irreducible GNS representation on the quasilocal algebra (Theorem 96) +- Microcausality: spacelike-separated local von Neumann algebras commute (Theorem 72) +- Isotony of the von Neumann net (Theorem 73) +- Bundled von Neumann microcausality and isotony (Theorem 74) +- Statistical Independence (Schlieder Property): the cyclic vector of one region is separating for the local von Neumann algebra of any spacelike-separated region (Theorems 76–77) +- Geometric Covariance of the von Neumann net: conjugation by the implementing unitary carries the local von Neumann algebra of a region onto that of the transformed region (Theorem 78); orbit-invariance of factoriality along the symmetry orbit (Theorem 79); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 80) +- Topological Schur Lemma for cyclic representations (Theorem 82) +- Commutant operator is scalar iff its diagonal coefficient is proportional to the state (Theorem 83) +- Pure state implies irreducible GNS representation (Theorem 85) +- GNS Radon–Nikodym form is bounded (Theorem 86); GNS Radon–Nikodym operator exists and commutes with the representation (Theorem 87) +- Pure state $$\iff$$ irreducible GNS representation (Theorem 88) +- An irreducible representation generates a von Neumann algebra with trivial centre, i.e. a factor (Theorem 89); more sharply, an irreducible representation generates the whole of $$\mathcal{B}(H)$$ (Theorem 90); bundled density form on Mathlib's `VonNeumannAlgebra` type (Theorem 91) +- The GNS representation of a pure state generates a factor (Theorem 92); more sharply, generates the whole of $$\mathcal{B}(H)$$ (Theorem 93) +- Norm of a positive linear functional equals its value on the unit (Theorem 94) +- Pure state $$\iff$$ extreme point of the state space (Theorem 96); state-space convexity and the extreme-point bridge (Theorem 97); weak-\* compactness of the state space (Theorem 98) +- Pure state $$\iff$$ extreme point of the state space of the quasilocal algebra (Theorem 99) +- Pure state $$\iff$$ irreducible GNS representation on the quasilocal algebra (Theorem 100) **Local von Neumann algebras – curved spacetime** -- $$R(\mathbf{B}')$$ as a von Neumann algebra in curved spacetime (Definition 140) -- Microcausality relative to a containing local algebra (Theorem 141) -- Isotony of the curved von Neumann net (Theorem 142) -- Bundled von Neumann microcausality and isotony, curved spacetime (Theorem 143) -- The net of von Neumann algebras in curved spacetime, relative to a containing region (Definition 144) -- Statistical Independence (Schlieder Property) in curved spacetime (Theorems 145–146) -- Geometric Covariance of the von Neumann net in curved spacetime, via the stabiliser GNS representation (Theorem 147); orbit-invariance of factoriality along the stabiliser orbit (Theorem 148); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 149) -- Pure state $$\iff$$ extreme point of the state space of a local algebra (Theorem 150) -- Pure state $$\iff$$ irreducible GNS representation on a local algebra (Theorem 151) -- The GNS representation of a pure state on a local algebra generates a factor and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 152) +- Microcausality relative to a containing local algebra (Theorem 157) +- Isotony of the curved von Neumann net (Theorem 158) +- Bundled von Neumann microcausality and isotony, curved spacetime (Theorem 159) +- Statistical Independence (Schlieder Property) in curved spacetime (Theorems 161–162) +- Geometric Covariance of the von Neumann net in curved spacetime, via the stabiliser GNS representation (Theorem 163); orbit-invariance of factoriality along the stabiliser orbit (Theorem 164); upgrade to a \*-algebra isomorphism of the bundled local von Neumann algebras (Theorem 165) +- Pure state $$\iff$$ extreme point of the state space of a local algebra (Theorem 166) +- Pure state $$\iff$$ irreducible GNS representation on a local algebra (Theorem 167) +- The GNS representation of a pure state on a local algebra generates a factor and, more sharply, the whole of $$\mathcal{B}(H)$$ (Theorem 168) +- The irreducible dichotomy (Theorem 105) specialised to curved local algebras (Theorem 169) + +**Unitary equivalence and superselection theory** +- Irreducibility and factoriality are unitary invariants (Theorem 102) +- Schur's Lemma and the Irreducible Dichotomy: two irreducible representations are disjoint or unitarily equivalent (Theorem 105) +- Schur multiplicity: the intertwiner space between two irreducible representations is at most one-dimensional (Lemma 106) +- The endomorphism algebra of an irreducible representation is $$\mathbb{C} \cdot 1$$ (Lemma 107) +- The Pure-State Dichotomy: the GNS representations of two pure states are disjoint or unitarily equivalent (Theorem 108) + +**Direct sums, amplification, and reducibility** +- Subrepresentations and commutant of a direct sum (Theorem 110) +- Reducibility of a direct sum with at least two nonzero summands, hence of any multiply-amplified representation (Theorem 112) **Separating vectors and faithful states** -- Separating vector of a faithful state (Theorem 115) +- Separating vector of a faithful state (Theorem 131) **KMS condition** -- The KMS state set is convex (Theorem 118) -- Boundary coincidence for $$a = 1$$ (Lemma 119) -- $$i\beta$$-periodic entire extension / strip Schwarz reflection (Theorem 121) -- Strip-Liouville holds for $$\beta > 0$$ (Theorem 122) -- KMS states are invariant (Theorem 123) -- Uniqueness on the strip from boundary values (Theorem 124) -- Uniqueness of the KMS correlation function (Theorem 125) -- A Lorentz one-parameter subgroup induces a one-parameter automorphism group on the quasilocal algebra (Lemma 127) -- Convexity of the covariance-flow KMS states – Minkowski spacetime (Theorem 129) -- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 162) -- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 164) -- Convexity of the Killing-flow KMS states – curved spacetime (Theorem 165) +- The KMS state set is convex (Theorem 134) +- Boundary coincidence for $$a = 1$$ (Lemma 135) +- $$i\beta$$-periodic entire extension / strip Schwarz reflection (Theorem 137) +- Strip-Liouville holds for $$\beta > 0$$ (Theorem 138) +- KMS states are invariant (Theorem 139) +- Uniqueness on the strip from boundary values (Theorem 140) +- Uniqueness of the KMS correlation function (Theorem 141) +- A Lorentz one-parameter subgroup induces a one-parameter automorphism group on the quasilocal algebra (Lemma 143) +- Convexity of the covariance-flow KMS states – Minkowski spacetime (Theorem 145) +- A Killing flow induces a one-parameter automorphism group on the local algebra (Lemma 179) +- The Killing-Flow KMS Thermal Representation: a KMS state for a Killing flow at positive inverse temperature carries a strongly continuous one-parameter unitary group on its GNS Hilbert space implementing the flow (Theorem 181) +- Convexity of the Killing-flow KMS states – curved spacetime (Theorem 182) ### Axioms -**Minkowski spacetime:** Local Algebras (Definition 57), Isotony (Definition 58), Local Commutativity (Definition 60), Quasilocal Completeness (Definition 62), Lorentz Covariance (Definition 63). +Axiom 6 (Primitivity) from the original 1964 Haag–Kastler paper is not carried into the sharpened axiom set—see Chapter 8 for the discussion of why it is dropped. The five sharpened axioms below, bundled together as a `HaagKastlerNet`, are what is actually formalised. -**Curved spacetime:** Local Algebras (Definition 131), Isotony (Definition 132), Local Commutativity (Definition 133), Local Completeness (Definition 135), Isometric Covariance (Definition 136). +**Minkowski spacetime:** Local Algebras (Definition 61), Isotony (Definition 62), Local Commutativity (Definition 64), Quasilocal Completeness (Definition 66), Lorentz Covariance (Definition 67). + +**Curved spacetime:** Local Algebras (Definition 147), Isotony (Definition 148), Local Commutativity (Definition 149), Local Completeness (Definition 151), Isometric Covariance (Definition 152). ## Contributing diff --git a/images/readme/picasso.png b/images/readme/picasso.png index b02a01a..f1aaab1 100644 Binary files a/images/readme/picasso.png and b/images/readme/picasso.png differ