Numina/aqft in lean

Physicslib4.lean

@@ -59,8 +59,12 @@ import Physicslib4.GNS.Separating
 import Physicslib4.GNS.Superselection
 import Physicslib4.GNS.UnitaryEquiv
 import Physicslib4.GNS.UnitaryRepresentation
+import Physicslib4.Geometry.PseudoRiemannian.Basic
+import Physicslib4.Geometry.PseudoRiemannian.Flat
+import Physicslib4.Geometry.PseudoRiemannian.LeviCivita
 import Physicslib4.Operators.Conjugation
 import Physicslib4.Operators.LpDiagonal
+import Physicslib4.Spacetime.AlongPath
 import Physicslib4.Spacetime.Basic
 import Physicslib4.Spacetime.CausalComplement
 import Physicslib4.Spacetime.CausalStructure

Physicslib4/Geometry/PseudoRiemannian/Basic.lean

@@ -0,0 +1,97 @@
+/-
+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.Geometry.Manifold.VectorBundle.Hom
+import Mathlib.Geometry.Manifold.VectorBundle.Tangent
+import Physicslib4.Spacetime.Basic
+
+/-!
+# Pseudo-Riemannian metrics
+
+A *pseudo-Riemannian metric* on a manifold `M` modelled on `(E, H)` with model `I` is a
+smooth family of symmetric, nondegenerate continuous bilinear forms on the tangent spaces.
+Unlike Mathlib's `Bundle.ContMDiffRiemannianMetric`, no positivity is required, so Lorentzian
+metrics are included. The smoothness condition has the same bundle-section shape as
+`Bundle.ContMDiffRiemannianMetric.contMDiff`.
+
+## Main definitions
+
+* `Physicslib4.Geometry.PseudoRiemannianMetric`: the structure.
+* `Physicslib4.Spacetime.toPseudoRiemannianMetric`: the metric of a spacetime.
+
+## Main results
+
+* `Physicslib4.Geometry.PseudoRiemannianMetric.bijective_val`: at each point, `v ↦ g_x(v, ·)` is
+  a linear isomorphism `T_xM → T_x*M` (the musical isomorphism).
+
+Blueprint reference: `def:pseudo-riemannian-metric`, `lmm:musical-isomorphism`.
+-/
+
+open Bundle
+open scoped Manifold ContDiff
+
+namespace Physicslib4
+
+namespace Geometry
+
+variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
+  {H : Type*} [TopologicalSpace H] (I : ModelWithCorners ℝ E H)
+  (M : Type*) [TopologicalSpace M] [ChartedSpace H M] [IsManifold I ∞ M]
+
+/-- A **pseudo-Riemannian metric** on `M`: a smooth section `g` of the bundle of continuous
+bilinear forms on `TM` that is symmetric and nondegenerate at every point. No positivity is
+required.
+
+Blueprint reference: `def:pseudo-riemannian-metric`. -/
+structure PseudoRiemannianMetric where
+  /-- The bilinear form `g_x` on `T_xM`. -/
+  val : ∀ x : M, TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ
+  /-- Symmetry: `g_x(v, w) = g_x(w, v)`. -/
+  symm : ∀ (x : M) (v w : TangentSpace I x), val x v w = val x w v
+  /-- Nondegeneracy: if `g_x(v, w) = 0` for all `w`, then `v = 0`. -/
+  nondegenerate : ∀ (x : M) (v : TangentSpace I x), (∀ w, val x v w = 0) → v = 0
+  /-- Smoothness of `g` as a section of the bundle of bilinear forms on `TM`. -/
+  contMDiff : ContMDiff I (I.prod 𝓘(ℝ, E →L[ℝ] E →L[ℝ] ℝ)) ∞
+    (fun x ↦ TotalSpace.mk' (E →L[ℝ] E →L[ℝ] ℝ)
+      (E := fun x ↦ TangentSpace I x →L[ℝ] TangentSpace I x →L[ℝ] ℝ) x (val x))
+
+namespace PseudoRiemannianMetric
+
+variable {I M}
+
+/-- **The musical isomorphism.** At each point `x`, the map `v ↦ g_x(v, ·)` from `T_xM` to its
+dual is bijective: injective by nondegeneracy and hence bijective since `T_xM` is
+finite-dimensional.
+
+Blueprint reference: `lmm:musical-isomorphism`. -/
+theorem bijective_val [FiniteDimensional ℝ E] (g : PseudoRiemannianMetric I M) (x : M) :
+    Function.Bijective (g.val x) := by
+  let A : E →L[ℝ] E →L[ℝ] ℝ := g.val x
+  change Function.Bijective A
+  have hinj : Function.Injective (A : E →ₗ[ℝ] E →L[ℝ] ℝ) := by
+    rw [← LinearMap.ker_eq_bot, LinearMap.ker_eq_bot']
+    exact fun v hv ↦ g.nondegenerate x v fun w ↦ DFunLike.congr_fun hv w
+  have hrank : Module.finrank ℝ E = Module.finrank ℝ (E →L[ℝ] ℝ) := by
+    rw [← (LinearMap.toContinuousLinearMap (𝕜 := ℝ) (E := E) (F' := ℝ)).finrank_eq]
+    exact (Subspace.dual_finrank_eq).symm
+  exact ⟨hinj, (LinearMap.injective_iff_surjective_of_finrank_eq_finrank hrank).1 hinj⟩
+
+end PseudoRiemannianMetric
+
+end Geometry
+
+attribute [local instance] Spacetime.topology Spacetime.chartedSpace Spacetime.isManifold
+
+/-- The metric of a spacetime is a pseudo-Riemannian metric on its manifold.
+
+Blueprint reference: `def:pseudo-riemannian-metric`. -/
+def Spacetime.toPseudoRiemannianMetric (M : Spacetime) :
+    Geometry.PseudoRiemannianMetric M.model M.Carrier where
+  val := M.val
+  symm := M.symm
+  nondegenerate := M.nondegenerate
+  contMDiff := M.contMDiff
+
+end Physicslib4

Physicslib4/Geometry/PseudoRiemannian/Flat.lean

@@ -0,0 +1,117 @@
+/-
+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.Geometry.PseudoRiemannian.LeviCivita
+
+/-!
+# The flat connection on a vector space
+
+On a finite-dimensional real vector space `E`, viewed as a manifold over itself, the tangent
+bundle is trivial and the ordinary directional derivative `∇_v σ = Dσ(v)` is a covariant
+derivative. For a pseudo-Riemannian metric that is constant (the same bilinear form at every
+point), it is the Levi-Civita connection. This is the flat case used for Minkowski spacetime.
+
+## Main definitions
+
+* `Physicslib4.Geometry.flatConnection`: `σ ↦ (x ↦ fderiv ℝ σ x)`.
+
+## Main results
+
+* `PseudoRiemannianMetric.isLeviCivitaFor_flatConnection`: for a constant metric, the flat
+  connection is a Levi-Civita connection.
+* `PseudoRiemannianMetric.leviCivita_apply_eq_fderiv`: hence the Levi-Civita connection of a
+  constant metric is the directional derivative on differentiable vector fields.
+
+Blueprint reference: `lmm:minkowski-directional-derivative-levi-civita`,
+`lmm:minkowski-levi-civita-flat`.
+-/
+
+open Bundle
+open scoped Manifold ContDiff
+
+namespace Physicslib4
+
+namespace Geometry
+
+variable (E : Type*) [NormedAddCommGroup E] [NormedSpace ℝ E]
+
+/-- The directional derivative is a covariant derivative on the tangent bundle of `E`.
+
+Blueprint reference: `lmm:minkowski-directional-derivative-levi-civita`. -/
+theorem isCovariantDerivativeOn_fderiv :
+    IsCovariantDerivativeOn E
+      (fun (σ : Π x : E, TangentSpace 𝓘(ℝ, E) x) (x : E) ↦
+        (fderiv ℝ (fun y ↦ (σ y : E)) x : TangentSpace 𝓘(ℝ, E) x →L[ℝ] TangentSpace 𝓘(ℝ, E) x))
+      Set.univ := by
+  have hd : ∀ {σ : Π x : E, TangentSpace 𝓘(ℝ, E) x} {x : E}, MDiffAt (T% σ) x →
+      DifferentiableAt ℝ (F := E) (fun y ↦ σ y) x := fun {σ x} h ↦
+    mdifferentiableAt_iff_differentiableAt.1 <|
+      ((contMDiff_snd_tangentBundle_modelSpace E 𝓘(ℝ, E) (n := 1)).mdifferentiable
+        one_ne_zero _).comp x h
+  refine ⟨fun {σ σ' x} hσ hσ' _ ↦ ?_, fun {σ g x} hσ hg _ ↦ ?_⟩
+  · have h := fderiv_add (F := E) (hd hσ) (hd hσ')
+    exact h
+  · have h := fderiv_smul (F := E) (mdifferentiableAt_iff_differentiableAt.1 hg) (hd hσ)
+    rw [← mfderiv_eq_fderiv (E := E) (E' := ℝ)] at h
+    exact h
+
+/-- The **flat connection** on `E`: `∇_v σ = Dσ(v)`.
+
+Blueprint reference: `lmm:minkowski-directional-derivative-levi-civita`. -/
+noncomputable def flatConnection :
+    _root_.CovariantDerivative 𝓘(ℝ, E) E (TangentSpace 𝓘(ℝ, E) : E → Type _) where
+  toFun σ x := fderiv ℝ (fun y ↦ (σ y : E)) x
+  isCovariantDerivativeOnUniv := isCovariantDerivativeOn_fderiv E
+
+theorem flatConnection_apply (σ : Π x : E, TangentSpace 𝓘(ℝ, E) x) (x : E)
+    (v : TangentSpace 𝓘(ℝ, E) x) :
+    flatConnection E σ x v = fderiv ℝ (fun y ↦ (σ y : E)) x v := rfl
+
+namespace PseudoRiemannianMetric
+
+variable {E} [FiniteDimensional ℝ E]
+
+/-- For a metric that is the same bilinear form `B` at every point, the flat connection is a
+Levi-Civita connection.
+
+Blueprint reference: `lmm:minkowski-directional-derivative-levi-civita`. -/
+theorem isLeviCivitaFor_flatConnection (g : PseudoRiemannianMetric 𝓘(ℝ, E) E)
+    (B : E →L[ℝ] E →L[ℝ] ℝ) (hg : ∀ x, g.val x = B) :
+    CovariantDerivative.IsLeviCivitaFor g (flatConnection E) := by
+  have hdiff : ∀ {V : Π x : E, TangentSpace 𝓘(ℝ, E) x} {x : E}, MDiffAt (T% V) x →
+      DifferentiableAt ℝ (fun y ↦ (V y : E)) x := fun {V x} h ↦
+    ((contMDiff_snd_tangentBundle_modelSpace E 𝓘(ℝ, E)).mdifferentiableAt one_ne_zero
+      |>.comp x h).differentiableAt
+  refine ⟨fun x X σ τ _ hσ hτ ↦ ?_, ?_⟩
+  · have h1 := hdiff hσ
+    have h2 := hdiff hτ
+    have hfun : (fun y ↦ g.val y (σ y) (τ y)) = fun y ↦ B (σ y) (τ y) :=
+      funext fun y ↦ by rw [hg]; rfl
+    simp only [hg, flatConnection_apply]
+    rw [hfun, mfderiv_eq_fderiv, (B.hasFDerivAt_of_bilinear h1.hasFDerivAt h2.hasFDerivAt).fderiv]
+    exact add_comm _ _
+  · rw [_root_.CovariantDerivative.torsion_eq_zero_iff]
+    intro X Y x _ _
+    rw [← VectorField.mlieBracketWithin_univ, VectorField.mlieBracketWithin_eq_lieBracketWithin]
+    have := VectorField.lieBracketWithin_univ (𝕜 := ℝ) (V := fun y ↦ (X y : E))
+      (W := fun y ↦ (Y y : E))
+    exact ((congrFun this x).trans (congrFun (VectorField.lieBracket_eq (𝕜 := ℝ)) x)).symm
+
+/-- **The Levi-Civita connection of a constant metric is flat**: on vector fields
+differentiable at `x`, it is the directional derivative.
+
+Blueprint reference: `lmm:minkowski-levi-civita-flat`. -/
+theorem leviCivita_apply_eq_fderiv (g : PseudoRiemannianMetric 𝓘(ℝ, E) E)
+    (B : E →L[ℝ] E →L[ℝ] ℝ) (hg : ∀ x, g.val x = B) {X : Π x : E, TangentSpace 𝓘(ℝ, E) x}
+    {x : E} (hX : MDiffAt (T% X) x) (v : TangentSpace 𝓘(ℝ, E) x) :
+    g.leviCivita X x v = fderiv ℝ (fun y ↦ (X y : E)) x v :=
+  (g.isLeviCivitaFor_leviCivita.uniqueness (g.isLeviCivitaFor_flatConnection B hg) hX v).trans
+    (flatConnection_apply E X x v)
+
+end PseudoRiemannianMetric
+
+end Geometry
+
+end Physicslib4