From 2348d3e2a7453ce74ef137f02814f1728de07bc4 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Wed, 16 Sep 2026 19:23:11 +0200 Subject: [PATCH 1/4] feat(PhyslibAlpha/ClassicalMechanics): Souriau moment map, cocycle and Noether on a symplectic vector space Co-authored-by: Claude Fable 5.1 --- PhyslibAlpha.lean | 1 + .../ClassicalMechanics/MomentMap.lean | 510 ++++++++++++++++++ docs/references.bib | 9 + 3 files changed, 520 insertions(+) create mode 100644 PhyslibAlpha/ClassicalMechanics/MomentMap.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index 1218c1030..cd74d47c2 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -27,6 +27,7 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell +public import PhyslibAlpha.ClassicalMechanics.MomentMap public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism public import PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMap.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap.lean new file mode 100644 index 000000000..5f9bbbfc0 --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap.lean @@ -0,0 +1,510 @@ +/- +Copyright (c) 2026 Philippe Kevorkian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Philippe Kevorkian +-/ +module + +public import Mathlib.LinearAlgebra.BilinearForm.Properties +public import Mathlib.LinearAlgebra.BilinearMap +public import Mathlib.LinearAlgebra.Dual.Defs +public import Mathlib.Algebra.Lie.Basic +public import Mathlib.Algebra.Lie.OfAssociative +public import Mathlib.Topology.Algebra.Module.FiniteDimension +public import Mathlib.Analysis.Calculus.FDeriv.CompCLM +public import Mathlib.Analysis.Calculus.FDeriv.Mul +public import Mathlib.Analysis.Calculus.FDeriv.Symmetric +public import Mathlib.Analysis.Calculus.Deriv.Comp +public import Mathlib.Analysis.Calculus.MeanValue +/-! + +# Souriau's moment map on a symplectic vector space + +## i. Overview + +Souriau (Structure des systèmes dynamiques, Dunod 1970, chapter 11) attaches to a Lie group `G` +acting on a symplectic manifold `V` by symplectomorphisms (a *dynamical group*) a *moment* +`μ : V → 𝔤*`, defined by `σ(Z_V(x)) = -∇[μ.Z]` for every `Z` in the Lie algebra (11.7). Two moments +differ by a constant (11.8 a); the moment is constant along the motions (Noether's theorem, 11.12); +and the moment fails to be equivariant for the coadjoint action by a *symplectic cocycle* `θ` whose +derivative `f` is a 2-form on `𝔤` satisfying `σ(Z_V)(Z'_V) = μ[Z, Z'] + f(Z)(Z')` (11.17 d) and the +cyclic identity (11.33). The cohomology class of `θ` is an invariant of the dynamical group; it is +zero when a `G`-invariant potential of `σ` exists (11.21) and for semisimple groups (11.27). + +This file states and proves these results in the setting of Souriau's example (11.2): a real +finite-dimensional symplectic vector space `E` on which a real Lie algebra `𝔤` acts by *affine* +infinitesimally symplectic vector fields `Z_E(x) = A Z x + b Z` (the infinitesimal version of the +affine symplectomorphisms `x ↦ B x + C` of (10.12)). No manifold is involved: the moment is given +explicitly by `μ.Z (x) = -½ σ(A Z x, x) - σ(b Z, x)`, the cocycle by `f(Z)(Z') = σ(b Z, b Z')`, and +Noether's theorem is stated for a Hamiltonian flow on `E`. + +All signs follow Souriau's printed conventions: the bracket of the Lie algebra is the one for which +`Z ↦ Z_E` is a homomorphism for the bracket `[Z, Z']_E = Z'_E ∘ Z_E - Z_E ∘ Z'_E` of (11.22 a) +(opposite to the usual commutator), `Ad(Z)(Z') = [Z, Z']` (6.13 b), and the coadjoint vector +field is `Z_{𝔤*}(ν) = ν ∘ Ad(Z)` (11.16). + +## ii. Key results + +- `AffineSymplecticAction.hasFDerivAt_moment`: (11.7), `σ(Z_E(x)) = -∇[μ.Z]`. +- `AffineSymplecticAction.moment_unique`: (11.8 a), two moments differ by a constant torsor; this is + proved without the alternation of `σ`, from the symmetry of the second derivative of the given + moment. +- `AffineSymplecticAction.sigma_vectorField_vectorField`: (11.17 d), + `σ(Z_E)(Z'_E) = μ[Z, Z'] + f(Z)(Z')`. +- `AffineSymplecticAction.cocycle_cyclic`: (11.33), the cyclic identity of the symplectic cocycle. +- `AffineSymplecticAction.equivariant_of_coboundary`: (11.27) in this setting, a coboundary cocycle + can be absorbed in the moment. +- `AffineSymplecticAction.noether`: (11.12), `μ.Z` is a first integral of every `Z_E`-invariant + Hamiltonian flow. +- `planeTranslations_not_coboundary`: the translations of the plane have a non-zero cohomology class + (the simplest instance of Souriau's "mass" cocycle). + +## iii. Table of contents + +- A. Symplectic forms +- B. Affine symplectic actions of a Lie algebra +- C. The Souriau cocycle +- D. The moment map +- E. Noether's theorem +- F. The plane: translations and a non-trivial cohomology class + +## iv. References + +- J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970, chapter 11 (Groupes + dynamiques), pp. 104-117; English translation: Structure of Dynamical Systems, Birkhäuser, 1997 + (same equation numbers). + +## References + +* J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, + Paris, 1970, chapter 11 "Groupes dynamiques", pp. 104-117. The equation numbers (11.7), + (11.8), (11.12), (11.17), (11.22), (11.27), (11.33) refer to this edition. [ref: Souriau1970] + +-/ + +@[expose] public section + +noncomputable section + +namespace ClassicalMechanics + +open Module + +/-! + +## A. Symplectic forms + +Souriau's "forme de Lagrange" `σ` is an alternating non-degenerate bilinear form. + +-/ + +/-- A symplectic form on a real vector space: an alternating non-degenerate bilinear form. -/ +structure IsSymplecticForm {E : Type} [AddCommGroup E] [Module ℝ E] (σ : LinearMap.BilinForm ℝ E) : + Prop where + /-- `σ` is alternating: `σ v v = 0`. -/ + alt : LinearMap.BilinForm.IsAlt σ + /-- `σ` is non-degenerate. -/ + nondeg : LinearMap.BilinForm.Nondegenerate σ + +/-! + +## B. Affine symplectic actions of a Lie algebra + +The infinitesimal version of Souriau's example (11.2) with the affine symplectomorphisms of (10.12): +each `Z` of the Lie algebra acts on `E` by the affine vector field `Z_E(x) = A Z x + b Z`, with +`A Z` infinitesimally symplectic ((10.28)-(10.32)), and the bracket is Souriau's (6.12 b), +(11.22 a): `[Z, Z']_E = Z'_E ∘ Z_E - Z_E ∘ Z'_E`, extended to affine vector fields by the formula +`[X, X'](x) = DX'(x)(X(x)) - DX(x)(X'(x))`. + +-/ + +/-- An affine infinitesimally symplectic action of a Lie algebra `g` on `E`, in Souriau's +conventions: `Z_E(x) = A Z x + b Z`. -/ +structure AffineSymplecticAction {E : Type} [AddCommGroup E] [Module ℝ E] + (σ : LinearMap.BilinForm ℝ E) (g : Type) [LieRing g] [LieAlgebra ℝ g] where + /-- The linear part `Z ↦ A Z` of the vector fields. -/ + A : g →ₗ[ℝ] (E →ₗ[ℝ] E) + /-- The constant part `Z ↦ b Z` of the vector fields. -/ + b : g →ₗ[ℝ] E + /-- Each `A Z` is infinitesimally symplectic: `σ (A Z v) w + σ v (A Z w) = 0`. -/ + infinitesimallySymplectic : ∀ Z v w, σ (A Z v) w + σ v (A Z w) = 0 + /-- Souriau's bracket (11.22 a) on the linear parts: `A [Z, Z'] = A Z' ∘ A Z - A Z ∘ A Z'`. -/ + map_bracket_A : ∀ Z Z', A ⁅Z, Z'⁆ = A Z' ∘ₗ A Z - A Z ∘ₗ A Z' + /-- Souriau's bracket on the constant parts: `b [Z, Z'] = A Z' (b Z) - A Z (b Z')`. -/ + map_bracket_b : ∀ Z Z', b ⁅Z, Z'⁆ = A Z' (b Z) - A Z (b Z') + +/-- (11.16) with (6.13 b): the coadjoint vector field `Z_{𝔤*}(ν) = ν ∘ Ad(Z)`, +`Ad(Z)(Z') = [Z, Z']`, for a torsor `ν` given as a function; this is also the coboundary +`δ(ν)(Z)` of (11.24). -/ +def coadjoint {g : Type} [LieRing g] (Z : g) (ν : g → ℝ) (Z' : g) : ℝ := ν ⁅Z, Z'⁆ + +namespace AffineSymplecticAction + +variable {E : Type} [AddCommGroup E] [Module ℝ E] +variable {g : Type} [LieRing g] [LieAlgebra ℝ g] {σ : LinearMap.BilinForm ℝ E} +variable (ρ : AffineSymplecticAction σ g) + +/-- (6.11): the affine vector field `Z_E` associated with `Z`. -/ +def vectorField (Z : g) (x : E) : E := ρ.A Z x + ρ.b Z + +/-- The moment (11.7), (11.9) of the action, as a function of the point `x` and of `Z`: +`μ.Z (x) = -½ σ(A Z x, x) - σ(b Z, x)`. Its sign is fixed by (11.7). -/ +def moment (x : E) (Z : g) : ℝ := -(1 / 2 : ℝ) * σ (ρ.A Z x) x - σ (ρ.b Z) x + +/-- (11.17 c): Souriau's cocycle `f(Z)(Z') = σ(b Z, b Z')`, a 2-form on `g`. -/ +def cocycle (Z Z' : g) : ℝ := σ (ρ.b Z) (ρ.b Z') + +/-- `infinitesimallySymplectic` in the form `σ (A Z v) w = -σ v (A Z w)`. -/ +lemma sigma_A_left (Z : g) (v w : E) : σ (ρ.A Z v) w = -σ v (ρ.A Z w) := + eq_neg_of_add_eq_zero_left (ρ.infinitesimallySymplectic Z v w) + +/-- `infinitesimallySymplectic` in the form `σ v (A Z w) = -σ (A Z v) w`. -/ +lemma sigma_A_right (Z : g) (v w : E) : σ v (ρ.A Z w) = -σ (ρ.A Z v) w := by + rw [ρ.sigma_A_left Z v w, neg_neg] + +/-- For an alternating `σ`, `σ (A Z v) w` is symmetric in `v`, `w`. -/ +lemma sigma_A_symm (hσ : IsSymplecticForm σ) (Z : g) (v w : E) : + σ (ρ.A Z v) w = σ (ρ.A Z w) v := by + rw [ρ.sigma_A_left Z v w, hσ.alt.neg_eq] + +/-- The moment is a torsor: `μ.(Z + Z') = μ.Z + μ.Z'`. -/ +lemma moment_add (x : E) (Z Z' : g) : ρ.moment x (Z + Z') = ρ.moment x Z + ρ.moment x Z' := by + simp only [moment, map_add, LinearMap.add_apply] + ring + +/-- The moment is a torsor: `μ.(c Z) = c μ.Z`. -/ +lemma moment_smul (x : E) (c : ℝ) (Z : g) : ρ.moment x (c • Z) = c * ρ.moment x Z := by + simp only [moment, map_smul, LinearMap.smul_apply, smul_eq_mul] + ring + +/-! + +## C. The Souriau cocycle + +(11.17 d, ♯), (11.30), (11.33), the Lie algebra cocycle identity (11.22)/(11.24), the change of +moment (11.18), the coboundary case (11.27) and the linear case (11.21). Everything here is algebra: +only the bilinearity and the alternation of `σ` and the axioms of the action are used. + +-/ + +/-- (11.17 d, ♯): `σ(Z_E(x))(Z'_E(x)) = μ[Z, Z'](x) + f(Z)(Z')`. -/ +lemma sigma_vectorField_vectorField (hσ : IsSymplecticForm σ) (Z Z' : g) (x : E) : + σ (ρ.vectorField Z x) (ρ.vectorField Z' x) = ρ.moment x ⁅Z, Z'⁆ + ρ.cocycle Z Z' := by + unfold vectorField moment cocycle + rw [ρ.map_bracket_A Z Z', ρ.map_bracket_b Z Z'] + simp only [LinearMap.sub_apply, LinearMap.comp_apply, map_add, map_sub, LinearMap.add_apply] + have h1 : σ (ρ.A Z' (ρ.A Z x)) x = -σ (ρ.A Z x) (ρ.A Z' x) := ρ.sigma_A_left Z' _ _ + have h2 : σ (ρ.A Z (ρ.A Z' x)) x = σ (ρ.A Z x) (ρ.A Z' x) := by + rw [ρ.sigma_A_left Z, hσ.alt.neg_eq] + have h3 : σ (ρ.A Z' (ρ.b Z)) x = -σ (ρ.b Z) (ρ.A Z' x) := ρ.sigma_A_left Z' _ _ + have h4 : σ (ρ.A Z (ρ.b Z')) x = σ (ρ.A Z x) (ρ.b Z') := by + rw [ρ.sigma_A_left Z, hσ.alt.neg_eq] + rw [h1, h2, h3, h4] + ring + +/-- (11.30): the cocycle is antisymmetric. -/ +lemma cocycle_antisymm (hσ : IsSymplecticForm σ) (Z Z' : g) : + ρ.cocycle Z' Z = -ρ.cocycle Z Z' := by + unfold cocycle + exact (hσ.alt.neg_eq _ _).symm + +/-- (11.33): the cyclic identity `f(Z)([Z', Z'']) + f(Z')([Z'', Z]) + f(Z'')([Z, Z']) = 0`. -/ +lemma cocycle_cyclic (hσ : IsSymplecticForm σ) (Z Z' Z'' : g) : + ρ.cocycle Z ⁅Z', Z''⁆ + ρ.cocycle Z' ⁅Z'', Z⁆ + ρ.cocycle Z'' ⁅Z, Z'⁆ = 0 := by + unfold cocycle + rw [ρ.map_bracket_b Z' Z'', ρ.map_bracket_b Z'' Z, ρ.map_bracket_b Z Z'] + simp only [map_sub] + rw [ρ.sigma_A_right Z'' (ρ.b Z) (ρ.b Z'), ρ.sigma_A_right Z' (ρ.b Z) (ρ.b Z''), + ρ.sigma_A_right Z (ρ.b Z') (ρ.b Z''), ρ.sigma_A_right Z'' (ρ.b Z') (ρ.b Z), + ρ.sigma_A_right Z' (ρ.b Z'') (ρ.b Z), ρ.sigma_A_right Z (ρ.b Z'') (ρ.b Z')] + have e1 := ρ.sigma_A_symm hσ Z'' (ρ.b Z') (ρ.b Z) + have e2 := ρ.sigma_A_symm hσ Z' (ρ.b Z'') (ρ.b Z) + have e3 := ρ.sigma_A_symm hσ Z (ρ.b Z'') (ρ.b Z') + linarith + +/-- (11.22)/(11.24) for the coadjoint representation: `f` is a Lie algebra cocycle, +`f([Z, Z']) = Z'_{𝔤*}(f(Z)) - Z_{𝔤*}(f(Z'))`, evaluated on `Z''`. -/ +lemma cocycle_lie (hσ : IsSymplecticForm σ) (Z Z' Z'' : g) : + ρ.cocycle ⁅Z, Z'⁆ Z'' = ρ.cocycle Z ⁅Z', Z''⁆ - ρ.cocycle Z' ⁅Z, Z''⁆ := by + unfold cocycle + rw [ρ.map_bracket_b Z Z', ρ.map_bracket_b Z' Z'', ρ.map_bracket_b Z Z''] + simp only [map_sub, LinearMap.sub_apply] + rw [ρ.sigma_A_right Z'' (ρ.b Z) (ρ.b Z'), ρ.sigma_A_right Z' (ρ.b Z) (ρ.b Z''), + ρ.sigma_A_right Z'' (ρ.b Z') (ρ.b Z), ρ.sigma_A_right Z (ρ.b Z') (ρ.b Z'')] + have e1 := ρ.sigma_A_symm hσ Z'' (ρ.b Z') (ρ.b Z) + linarith + +/-- (11.18): changing the moment into `μ - μ₀` (`μ₀` a constant torsor) keeps (11.17 d) with the +cocycle `f + Z_{𝔤*}(μ₀)`, i.e. `f(Z)(Z') + μ₀ [Z, Z']`. -/ +lemma sigma_vectorField_vectorField_shift (hσ : IsSymplecticForm σ) (μ₀ : Dual ℝ g) (Z Z' : g) + (x : E) : + σ (ρ.vectorField Z x) (ρ.vectorField Z' x) = + (ρ.moment x ⁅Z, Z'⁆ - μ₀ ⁅Z, Z'⁆) + (ρ.cocycle Z Z' + coadjoint Z μ₀ Z') := by + rw [ρ.sigma_vectorField_vectorField hσ Z Z' x] + unfold coadjoint + ring + +/-- (11.27) in this setting: if the cocycle is a coboundary, `f(Z)(Z') = μ₀ [Z, Z']`, then the +moment `μ + μ₀` is exactly equivariant. -/ +lemma equivariant_of_coboundary (hσ : IsSymplecticForm σ) (μ₀ : Dual ℝ g) + (h : ∀ Z Z', ρ.cocycle Z Z' = coadjoint Z μ₀ Z') (Z Z' : g) (x : E) : + σ (ρ.vectorField Z x) (ρ.vectorField Z' x) = ρ.moment x ⁅Z, Z'⁆ + μ₀ ⁅Z, Z'⁆ := by + rw [ρ.sigma_vectorField_vectorField hσ Z Z' x, h Z Z'] + rfl + +/-- (11.21) in this setting: a linear action (`b = 0`, the case (11.2) of `Sp(E)`) has a zero +cocycle. -/ +lemma cocycle_eq_zero_of_linear (hb : ρ.b = 0) (Z Z' : g) : ρ.cocycle Z Z' = 0 := by + simp [cocycle, hb] + +end AffineSymplecticAction + +/-- The symplectic gradient (9.16) in the convention of (11.7) and (10.32): `X` is the symplectic +gradient of `u` when `σ (X x) v = -Du(x)(v)` for all `x`, `v`. -/ +def IsSymplecticGradient {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] + (σ : LinearMap.BilinForm ℝ E) (u : E → ℝ) (X : E → E) : Prop := + ∀ x v, σ (X x) v = -(fderiv ℝ u x v) + +/-! + +## D. The moment map + +(11.7), (11.9) and (11.8 a), then the infinitesimal equivariance (11.17 d, ♠) and the identity +(11.8 c). The derivative of `y ↦ σ (A y) y` is computed by viewing `y ↦ σ (A y)` as a continuous +linear map into `E →L[ℝ] ℝ`. + +-/ + +namespace AffineSymplecticAction + +variable {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] +variable {g : Type} [LieRing g] [LieAlgebra ℝ g] {σ : LinearMap.BilinForm ℝ E} +variable (ρ : AffineSymplecticAction σ g) + +/-- `y ↦ σ (A Z y)` as a continuous linear map from `E` to `E →L[ℝ] ℝ`. -/ +def sigmaA (Z : g) : E →L[ℝ] (E →L[ℝ] ℝ) := + LinearMap.toContinuousLinearMap + ((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] (E →L[ℝ] ℝ)).toLinearMap ∘ₗ σ ∘ₗ ρ.A Z) + +@[simp] +lemma sigmaA_apply (Z : g) (y v : E) : ρ.sigmaA Z y v = σ (ρ.A Z y) v := by + simp [sigmaA] + +/-- The constant linear form `σ (b Z)` as a continuous linear map. -/ +def sigmaB (Z : g) : E →L[ℝ] ℝ := LinearMap.toContinuousLinearMap (σ (ρ.b Z)) + +@[simp] +lemma sigmaB_apply (Z : g) (v : E) : ρ.sigmaB Z v = σ (ρ.b Z) v := by + simp [sigmaB] + +/-- The derivative of `y ↦ σ (A Z y) y` at `x` is `v ↦ σ (A Z v) x + σ (A Z x) v`. -/ +lemma hasFDerivAt_quad (Z : g) (x : E) : + HasFDerivAt (fun y => σ (ρ.A Z y) y) + ((ρ.sigmaA Z x).comp (ContinuousLinearMap.id ℝ E) + (ρ.sigmaA Z).flip x) x := by + have h := (ρ.sigmaA Z).hasFDerivAt (x := x) + have h2 := hasFDerivAt_id (𝕜 := ℝ) x + have h3 := h.clm_apply h2 + refine h3.congr_of_eventuallyEq (Filter.Eventually.of_forall fun y => ?_) + simp + +/-- (11.7) under the sole symmetry `σ (A Z v) w = σ (A Z w) v`. -/ +lemma hasFDerivAt_moment_of_symm (Z : g) (hsym : ∀ v w, σ (ρ.A Z v) w = σ (ρ.A Z w) v) (x : E) : + HasFDerivAt (fun y => ρ.moment y Z) + (-(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z x)))) x := by + have hq := ρ.hasFDerivAt_quad Z x + have hl : HasFDerivAt (fun y => σ (ρ.b Z) y) (LinearMap.toContinuousLinearMap (σ (ρ.b Z))) x := + (LinearMap.toContinuousLinearMap (σ (ρ.b Z))).hasFDerivAt + have h := (hq.const_mul (-(1 / 2 : ℝ))).sub hl + refine h.congr_fderiv ?_ + ext v + simp [vectorField] + rw [hsym v x] + ring + +/-- (11.7): `σ(Z_E(x)) = -∇[μ.Z]`, the derivative of `x ↦ μ.Z` at `x` is `v ↦ -σ (Z_E x) v`. -/ +lemma hasFDerivAt_moment (hσ : IsSymplecticForm σ) (Z : g) (x : E) : + HasFDerivAt (fun y => ρ.moment y Z) + (-(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z x)))) x := + ρ.hasFDerivAt_moment_of_symm Z (ρ.sigma_A_symm hσ Z) x + +/-- (11.9): `Z_E` is the symplectic gradient of `μ.Z`. -/ +lemma vectorField_isSymplecticGradient (hσ : IsSymplecticForm σ) (Z : g) : + IsSymplecticGradient σ (fun y => ρ.moment y Z) (ρ.vectorField Z) := by + intro x v + rw [(ρ.hasFDerivAt_moment hσ Z x).fderiv] + simp + +/-- The derivative of the affine map `x ↦ -σ (Z_E x)` (with values in `E →L[ℝ] ℝ`) is `-sigmaA`. -/ +lemma hasFDerivAt_negSigmaVectorField (Z : g) (x : E) : + HasFDerivAt (fun y => -(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z y)))) + (-(ρ.sigmaA Z)) x := by + have h : HasFDerivAt (fun y => ρ.sigmaA Z y + ρ.sigmaB Z) (ρ.sigmaA Z) x := + (ρ.sigmaA Z).hasFDerivAt.add_const _ + refine (h.neg).congr_of_eventuallyEq (Filter.Eventually.of_forall fun y => ?_) + ext v + simp [vectorField] + +/-- (11.8 a): two moments of the same action differ by a constant torsor (`E` is connected). Any `ψ` +satisfying (11.7) equals `μ + c`, `Z` by `Z`. No alternation of `σ` is needed: the symmetry of the +second derivative of `ψ` gives `σ (A Z v) w = σ (A Z w) v`. -/ +lemma moment_unique (ψ : E → g → ℝ) + (hψ : ∀ Z x, HasFDerivAt (fun y => ψ y Z) + (-(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z x)))) x) (Z : g) : + ∃ c : ℝ, ∀ x, ψ x Z = ρ.moment x Z + c := by + have hsym : ∀ v w, σ (ρ.A Z v) w = σ (ρ.A Z w) v := by + intro v w + have h := second_derivative_symmetric (f := fun y => ψ y Z) + (f' := fun y => -(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z y)))) (hψ Z) + (ρ.hasFDerivAt_negSigmaVectorField Z 0) v w + simpa using h + have hd : ∀ x, HasFDerivAt (fun y => ψ y Z - ρ.moment y Z) 0 x := fun x => by + have h := (hψ Z x).sub (ρ.hasFDerivAt_moment_of_symm Z hsym x) + rw [sub_self] at h + exact h + refine ⟨ψ 0 Z - ρ.moment 0 Z, fun x => ?_⟩ + have hc : ψ x Z - ρ.moment x Z = ψ 0 Z - ρ.moment 0 Z := + is_const_of_fderiv_eq_zero (f := fun y => ψ y Z - ρ.moment y Z) + (fun y => (hd y).differentiableAt) (fun y => (hd y).fderiv) x 0 + linarith + +/-- (11.17 d, ♠): `D(ψ)(x)(Z_E(x)) = ψ(x).ad(Z) + f(Z)`, evaluated on `Z'`: the infinitesimal +equivariance of the moment, up to the cocycle. -/ +lemma fderiv_moment_vectorField (hσ : IsSymplecticForm σ) (Z Z' : g) (x : E) : + fderiv ℝ (fun y => ρ.moment y Z') x (ρ.vectorField Z x) = + coadjoint Z (ρ.moment x) Z' + ρ.cocycle Z Z' := by + rw [(ρ.hasFDerivAt_moment hσ Z' x).fderiv] + have e : (-(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z' x)))) (ρ.vectorField Z x) = + -(σ (ρ.vectorField Z' x) (ρ.vectorField Z x)) := by simp + rw [e, hσ.alt.neg_eq, ρ.sigma_vectorField_vectorField hσ Z Z' x] + rfl + +/-- (11.8 c): `σ([Z, Z']_E(x)) = -∇[σ(Z_E(x))(Z'_E(x))]`, an identity valid for every dynamical +group. -/ +lemma sigma_vectorField_bracket (hσ : IsSymplecticForm σ) (Z Z' : g) (x v : E) : + σ (ρ.vectorField ⁅Z, Z'⁆ x) v = + -(fderiv ℝ (fun y => σ (ρ.vectorField Z y) (ρ.vectorField Z' y)) x v) := by + have hc : HasFDerivAt (fun y => ρ.sigmaA Z y + ρ.sigmaB Z) (ρ.sigmaA Z) x := + (ρ.sigmaA Z).hasFDerivAt.add_const _ + have hu : HasFDerivAt (fun y => LinearMap.toContinuousLinearMap (ρ.A Z') y + ρ.b Z') + (LinearMap.toContinuousLinearMap (ρ.A Z')) x := + (LinearMap.toContinuousLinearMap (ρ.A Z')).hasFDerivAt.add_const _ + have h := hc.clm_apply hu + have h' : HasFDerivAt (fun y => σ (ρ.vectorField Z y) (ρ.vectorField Z' y)) + ((ρ.sigmaA Z x + ρ.sigmaB Z).comp (LinearMap.toContinuousLinearMap (ρ.A Z')) + + (ρ.sigmaA Z).flip (LinearMap.toContinuousLinearMap (ρ.A Z') x + ρ.b Z')) x := by + refine h.congr_of_eventuallyEq (Filter.Eventually.of_forall fun y => ?_) + simp [vectorField] + rw [h'.fderiv] + simp only [vectorField, ρ.map_bracket_A, ρ.map_bracket_b, add_apply, + ContinuousLinearMap.comp_apply, ContinuousLinearMap.flip_apply, sigmaA_apply, sigmaB_apply, + LinearMap.coe_toContinuousLinearMap', LinearMap.sub_apply, LinearMap.comp_apply, map_add, + map_sub, LinearMap.add_apply] + have e1 : σ (ρ.A Z x + ρ.b Z) (ρ.A Z' v) = -σ (ρ.A Z' (ρ.A Z x + ρ.b Z)) v := by + rw [ρ.sigma_A_left Z' (ρ.A Z x + ρ.b Z) v, neg_neg] + have e2 : σ (ρ.A Z v) (ρ.A Z' x + ρ.b Z') = σ (ρ.A Z (ρ.A Z' x + ρ.b Z')) v := by + rw [ρ.sigma_A_left Z, hσ.alt.neg_eq] + simp only [map_add, LinearMap.add_apply] at e1 e2 + linarith + +/-! + +## E. Noether's theorem + +(11.12) states that a moment is constant on each leaf of the presymplectic evolution space. On `E`, +for a Hamiltonian flow `γ' = X ∘ γ` with `X` the symplectic gradient of an `H` invariant under +`Z_E`, this says that `μ.Z ∘ γ` is constant. + +-/ + +/-- (11.12), Noether's theorem: along a motion of a Hamiltonian `H` invariant under `Z_E`, the +component `μ.Z` of the moment has zero derivative. -/ +lemma noether (hσ : IsSymplecticForm σ) (H : E → ℝ) (X : E → E) (hX : IsSymplecticGradient σ H X) + (Z : g) (hinv : ∀ x, fderiv ℝ H x (ρ.vectorField Z x) = 0) + (γ : ℝ → E) (hγ : ∀ t, HasDerivAt γ (X (γ t)) t) (t : ℝ) : + HasDerivAt (fun s => ρ.moment (γ s) Z) 0 t := by + have h := (ρ.hasFDerivAt_moment hσ Z (γ t)).comp_hasDerivAt t (hγ t) + have e : σ (X (γ t)) (ρ.vectorField Z (γ t)) = 0 := by + rw [hX (γ t) (ρ.vectorField Z (γ t)), hinv (γ t), neg_zero] + have e2 : (-(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z (γ t))))) (X (γ t)) = 0 := by + have e3 : (-(LinearMap.toContinuousLinearMap (σ (ρ.vectorField Z (γ t))))) (X (γ t)) = + -(σ (ρ.vectorField Z (γ t)) (X (γ t))) := by simp + rw [e3, hσ.alt.neg_eq, e] + rw [e2] at h + exact h + +/-- (11.12) as a conservation law: `μ.Z` takes the same value at any two instants of a motion. -/ +lemma noether_const (hσ : IsSymplecticForm σ) (H : E → ℝ) (X : E → E) + (hX : IsSymplecticGradient σ H X) (Z : g) (hinv : ∀ x, fderiv ℝ H x (ρ.vectorField Z x) = 0) + (γ : ℝ → E) (hγ : ∀ t, HasDerivAt γ (X (γ t)) t) (t s : ℝ) : + ρ.moment (γ t) Z = ρ.moment (γ s) Z := + is_const_of_deriv_eq_zero (f := fun s => ρ.moment (γ s) Z) + (fun u => (ρ.noether hσ H X hX Z hinv γ hγ u).differentiableAt) + (fun u => (ρ.noether hσ H X hX Z hinv γ hγ u).deriv) t s + +end AffineSymplecticAction + +/-! + +## F. The plane: translations and a non-trivial cohomology class + +The standard symplectic form of `ℝ × ℝ` and the translations `Z_E(x) = x + Z`: their cocycle is +`σ(Z, Z')` itself, which is not a coboundary (the Lie algebra is abelian, so every coboundary +vanishes). This is the simplest instance of (11.20)-(11.21): no invariant potential exists, and no +moment of the translations is equivariant. + +-/ + +/-- `ℝ × ℝ` as an abelian Lie ring (the commutator bracket of the product ring, which vanishes). -/ +instance instLieRingPlane : LieRing (ℝ × ℝ) := LieRing.ofAssociativeRing + +/-- `ℝ × ℝ` as an abelian real Lie algebra. -/ +instance instLieAlgebraPlane : LieAlgebra ℝ (ℝ × ℝ) := LieAlgebra.ofAssociativeAlgebra + +/-- The standard symplectic form of the plane, `σ((a, b), (c, d)) = a d - b c`. -/ +def planeForm : LinearMap.BilinForm ℝ (ℝ × ℝ) := + LinearMap.mk₂ ℝ (fun v w => v.1 * w.2 - v.2 * w.1) + (by intros; simp only [Prod.fst_add, Prod.snd_add]; ring) + (by intros; simp only [Prod.smul_fst, Prod.smul_snd, smul_eq_mul]; ring) + (by intros; simp only [Prod.fst_add, Prod.snd_add]; ring) + (by intros; simp only [Prod.smul_fst, Prod.smul_snd, smul_eq_mul]; ring) + +/-- The translations of the plane: `A = 0`, `b = id`, `Z_E(x) = x + Z`. -/ +def planeTranslations : AffineSymplecticAction planeForm (ℝ × ℝ) where + A := 0 + b := LinearMap.id + infinitesimallySymplectic := by intros; simp [planeForm] + map_bracket_A := by intros; simp + map_bracket_b := by intros; simp [LieRing.of_associative_ring_bracket, mul_comm] + +/-- `planeForm` is symplectic. -/ +lemma isSymplecticForm_planeForm : IsSymplecticForm planeForm := by + refine ⟨fun v => ?_, ?_⟩ + · simp [planeForm] + ring + · refine ⟨fun v hv => ?_, fun w hw => ?_⟩ + · have h1 := hv (0, 1) + have h2 := hv (1, 0) + simp [planeForm] at h1 h2 + exact Prod.ext (by simpa using h1) (by simpa using h2) + · have h1 := hw (0, 1) + have h2 := hw (1, 0) + simp [planeForm] at h1 h2 + exact Prod.ext (by simpa using h1) (by simpa using h2) + +/-- (11.17 c), (11.20): for the translations of the plane the cocycle is `σ(Z, Z')`, so +`f((1, 0))((0, 1)) = 1`. -/ +lemma planeTranslations_cocycle : planeTranslations.cocycle (1, 0) (0, 1) = 1 := by + simp [AffineSymplecticAction.cocycle, planeTranslations, planeForm] + +/-- (11.21): the cocycle of the translations is not a coboundary: the cohomology class of the +translations of the plane is not zero. -/ +lemma planeTranslations_not_coboundary : + ¬ ∃ μ₀ : Dual ℝ (ℝ × ℝ), ∀ Z Z', planeTranslations.cocycle Z Z' = coadjoint Z μ₀ Z' := by + rintro ⟨μ₀, h⟩ + have := h (1, 0) (0, 1) + rw [planeTranslations_cocycle] at this + simp [coadjoint, LieRing.of_associative_ring_bracket] at this + +end ClassicalMechanics + +end diff --git a/docs/references.bib b/docs/references.bib index ded357f7d..08f5bb397 100644 --- a/docs/references.bib +++ b/docs/references.bib @@ -634,6 +634,15 @@ @article{snyder_toberer_2008 year = {2008} } +@book{Souriau1970, + author = {Souriau, Jean-Marie}, + title = {Structure des syst{\`e}mes dynamiques}, + series = {Ma{\^i}trises de math{\'e}matiques}, + publisher = {Dunod}, + address = {Paris}, + year = {1970} +} + @misc{stackexchange_qc_12953, title = {Quantum Computing Stack Exchange answer 12953}, howpublished = {}, From 4bd5dd64f70388d1879d8cb75ca6a18be9fdf48e Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 17 Sep 2026 22:07:45 +0200 Subject: [PATCH 2/4] feat(PhyslibAlpha/ClassicalMechanics): the cohomology class of the affine symplectic group MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit The group level of Souriau's chapter 11 (SDS, Dunod 1970, pp. 108-115) for his example (10.12): the affine symplectic group Sp(E) x E of a real symplectic vector space, acting by x -> B x + C. Adds AffineSymplecticGroup (Group and MulAction instances), its Lie algebra affineSymplecticAlgebra of pairs (A, b) acting by the affine vector fields of MomentMap.lean, the adjoint action (6.24) characterised by (6.25) (vectorField_adjoint, vectorField_injective), the coadjoint action (11.15) as SMul/MulAction/DistribMulAction on the dual, and the moment (11.7). Results: (11.17 a) in closed form, the defect mu(a_E(x)) - a_g*(mu(x)) is independent of x and equals mu(C) (moment_smul_sub_smul_moment); (11.17 b) it is a groupCohomology.IsCocycle₁ of the coadjoint action; (11.17 c) its derivative at the identity is the Lie algebra cocycle sigma(b Z', b Z) of the previous file; and the class is NOT a coboundary as soon as E is non-zero, so by (11.21) no invariant potential of sigma exists. The cocycle vocabulary is Mathlib's: no new cohomology definition. Co-Authored-By: Claude Opus 5 --- PhyslibAlpha.lean | 1 + .../MomentMapCohomology.lean | 486 ++++++++++++++++++ 2 files changed, 487 insertions(+) create mode 100644 PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index cd74d47c2..6efbdc5cb 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -28,6 +28,7 @@ public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidCylinder public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SolidSphere public import PhyslibAlpha.SpaceAndTime.Space.Surfaces.SphericalShell public import PhyslibAlpha.ClassicalMechanics.MomentMap +public import PhyslibAlpha.ClassicalMechanics.MomentMapCohomology public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism public import PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean b/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean new file mode 100644 index 000000000..f0cdf3751 --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean @@ -0,0 +1,486 @@ +/- +Copyright (c) 2026 Philippe Kevorkian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Philippe Kevorkian +-/ +module + +public import PhyslibAlpha.ClassicalMechanics.MomentMap +public import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree +/-! + +# The cohomology class of the affine symplectic group + +## i. Overview + +Souriau (Structure des systemes dynamiques, Dunod 1970, chapter 11) attaches to a dynamical group +`G` acting on a connected symplectic (or presymplectic) manifold `V` with moment `μ` a map +`θ : G → 𝔤*`, `θ(a) = μ(a_V(x)) - a_{𝔤*}(μ(x))` (11.17 a), which by connectedness does not depend +on `x` and satisfies the cocycle identity `θ(a × b) = θ(a) + a_{𝔤*}(θ(b))` (11.17 b). Its +cohomology class does not depend on the choice of the moment (11.18), (11.20), and it vanishes +when a `G`-invariant potential exists (11.21). + +This file proves the following for the group of Souriau's example (10.12), the affine symplectic +group `Sp(E) ⋉ E` of a real symplectic vector space `E`, acting by `x ↦ B x + C`, with the moment +`moment` of (11.7): the defect `θ(a)` does not depend on `x` and equals `μ(C)` (a computation here, +not a consequence of connectedness), `θ` is a 1-cocycle of the coadjoint action, its derivative +at the identity along a curve is the Lie algebra cocycle of +`PhyslibAlpha.ClassicalMechanics.MomentMap`, and its cohomology class is not zero. It does NOT +prove (11.18), (11.20) or (11.21): by (11.21) the non-zero class means that no potential of `σ` is +invariant under this group, but that implication is Souriau's and is not formalised here. + +The Lie algebra is the space of pairs `(A, b)` with `A` infinitesimally symplectic, acting by the +affine vector fields `Z_E(x) = A x + b`; only its module structure is used, and no Lean term +relates it to `AffineSymplecticAction` (the link with its cocycle is by formula). The adjoint +action is given by the formula of `adjoint` and characterised by the identity `vectorField_adjoint` +of (6.25); the coadjoint action `a_{𝔤*}(μ) = μ ∘ Ad(a⁻¹)` of (11.15) is a `MulAction` on the +dual. + +The cocycle notions are Mathlib's: `θ` is a `groupCohomology.IsCocycle₁` for the coadjoint action, +and "the class is non-zero" is `¬ groupCohomology.IsCoboundary₁`. Souriau's differentiability +requirement on `θ` is not formalised: the group here carries no manifold structure, and `θ` is +given by a closed formula. + +## ii. Key results + +- `vectorField_adjoint`: (6.25), `(Ad(a) Z)_E (a_E x) = B (Z_E x)`, which characterises `adjoint` + together with `vectorField_injective`. +- `moment_smul_sub_smul_moment`: (11.17 a) in closed form, `μ(a_E(x)) - a_{𝔤*}(μ(x)) = μ(C)`: the + defect `θ(a)` does not depend on `x`, and is the moment at the point `a_E(0) = C`. +- `isCocycle₁_moment_translation`: (11.17 b), `θ` is a 1-cocycle of the coadjoint action. +- `hasDerivAt_moment_translation`: part of (11.17 c), the derivative of `θ` at the identity along a + curve whose translation part has velocity `b'` is `σ (b', b Z)`, the value of + `AffineSymplecticAction.cocycle` (the 2-form property and ♣ of (11.17 c) are not proved here). +- `not_isCoboundary₁_moment_translation`: the cohomology class of the affine symplectic group is + non-zero as soon as `E ≠ 0`. + +## iii. Table of contents + +- A. The affine symplectic group +- B. Its Lie algebra and the adjoint action +- C. The coadjoint action and the moment +- D. The cohomology class +- E. The plane + +## iv. References + +- J.-M. Souriau, Structure des systemes dynamiques, Dunod, Paris, 1970: chapter 11 (Groupes + dynamiques), pp. 104-117, for (11.7), (11.15)-(11.21) and (11.28); (6.24)-(6.25) and (10.12), + (10.28)-(10.32) for the adjoint action and the affine symplectic group. + +## References + +* J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, + Paris, 1970, chapter 11 "Groupes dynamiques", pp. 104-117, and (6.24)-(6.25), (10.12). The + equation numbers refer to this edition. [ref: Souriau1970] + +-/ + +@[expose] public section + +noncomputable section + +namespace ClassicalMechanics + +open Module + +/-! + +## A. The affine symplectic group + +The affine symplectomorphisms `x ↦ B x + C` of (10.12), with `B` linear symplectic. + +-/ + +/-- The affine symplectic group of a bilinear form `σ` on `E`: the affine maps `x ↦ B x + C` with +`B` a linear equivalence preserving `σ` (Souriau (10.12)). -/ +structure AffineSymplecticGroup {E : Type} [AddCommGroup E] [Module ℝ E] + (σ : LinearMap.BilinForm ℝ E) where + /-- The linear part `B`. -/ + linear : E ≃ₗ[ℝ] E + /-- The translation part `C`. -/ + translation : E + /-- The linear part preserves `σ`. -/ + map_symplecticForm : ∀ v w, σ (linear v) (linear w) = σ v w + +namespace AffineSymplecticGroup + +variable {E : Type} [AddCommGroup E] [Module ℝ E] {σ : LinearMap.BilinForm ℝ E} + +instance : Mul (AffineSymplecticGroup σ) := + ⟨fun a b => ⟨b.linear.trans a.linear, a.linear b.translation + a.translation, fun v w => by + simp only [LinearEquiv.trans_apply, a.map_symplecticForm, b.map_symplecticForm]⟩⟩ + +instance : One (AffineSymplecticGroup σ) := ⟨⟨LinearEquiv.refl ℝ E, 0, fun _ _ => rfl⟩⟩ + +instance : Inv (AffineSymplecticGroup σ) := + ⟨fun a => ⟨a.linear.symm, -(a.linear.symm a.translation), fun v w => by + have h := a.map_symplecticForm (a.linear.symm v) (a.linear.symm w) + simpa using h.symm⟩⟩ + +@[simp] +lemma mul_linear (a b : AffineSymplecticGroup σ) : (a * b).linear = b.linear.trans a.linear := rfl + +@[simp] +lemma mul_translation (a b : AffineSymplecticGroup σ) : + (a * b).translation = a.linear b.translation + a.translation := rfl + +@[simp] +lemma one_linear : (1 : AffineSymplecticGroup σ).linear = LinearEquiv.refl ℝ E := rfl + +@[simp] +lemma one_translation : (1 : AffineSymplecticGroup σ).translation = 0 := rfl + +@[simp] +lemma inv_linear (a : AffineSymplecticGroup σ) : a⁻¹.linear = a.linear.symm := rfl + +@[simp] +lemma inv_translation (a : AffineSymplecticGroup σ) : + a⁻¹.translation = -(a.linear.symm a.translation) := rfl + +/-- Two elements with the same linear and translation parts are equal. -/ +@[ext] +lemma ext {a b : AffineSymplecticGroup σ} (hl : a.linear = b.linear) + (ht : a.translation = b.translation) : a = b := by + cases a + cases b + simp_all + +instance : Group (AffineSymplecticGroup σ) where + mul_assoc a b c := by + refine ext (by rfl) ?_ + simp only [mul_translation, mul_linear, LinearEquiv.trans_apply, map_add, add_assoc] + one_mul a := by + refine ext (by rfl) ?_ + simp + mul_one a := by + refine ext (by rfl) ?_ + simp + inv_mul_cancel a := by + refine ext ?_ ?_ + · ext v + simp + · simp + +/-- The affine symplectic group acts on `E` by `a_E(x) = B x + C` (10.12). -/ +instance : MulAction (AffineSymplecticGroup σ) E where + smul a x := a.linear x + a.translation + one_smul x := by + change (1 : AffineSymplecticGroup σ).linear x + (1 : AffineSymplecticGroup σ).translation = x + simp + mul_smul a b x := by + change (a * b).linear x + (a * b).translation + = a.linear (b.linear x + b.translation) + a.translation + simp only [mul_linear, mul_translation, LinearEquiv.trans_apply, map_add, add_assoc] + +lemma smul_def (a : AffineSymplecticGroup σ) (x : E) : a • x = a.linear x + a.translation := rfl + +end AffineSymplecticGroup + +/-! + +## B. Its Lie algebra and the adjoint action + +The pairs `(A, b)` with `A` infinitesimally symplectic, acting by the affine vector fields +`Z_E(x) = A x + b` of `AffineSymplecticAction`; the adjoint action of (6.24) is characterised by +(6.25). Only the module structure is used here: the Lie bracket of Souriau's (11.22 a) lives on +the abstract Lie algebra of `AffineSymplecticAction`. + +-/ + +variable {E : Type} [AddCommGroup E] [Module ℝ E] + +/-- The Lie algebra of the affine symplectic group: the pairs `(A, b)` with `A` infinitesimally +symplectic ((10.28)-(10.32)). -/ +def affineSymplecticAlgebra (σ : LinearMap.BilinForm ℝ E) : Submodule ℝ ((E →ₗ[ℝ] E) × E) where + carrier := {Z | ∀ v w, σ (Z.1 v) w + σ v (Z.1 w) = 0} + add_mem' := by + intro Z Z' hZ hZ' v w + have h1 := hZ v w + have h2 := hZ' v w + simp only [Prod.fst_add, LinearMap.add_apply, map_add] + linarith + zero_mem' := by + intro v w + simp + smul_mem' := by + intro c Z hZ v w + have h := hZ v w + simp only [Prod.smul_fst, LinearMap.smul_apply, map_smul, smul_eq_mul] + rw [← mul_add, h, mul_zero] + +variable {σ : LinearMap.BilinForm ℝ E} + +lemma mem_affineSymplecticAlgebra {Z : (E →ₗ[ℝ] E) × E} : + Z ∈ affineSymplecticAlgebra σ ↔ ∀ v w, σ (Z.1 v) w + σ v (Z.1 w) = 0 := Iff.rfl + +/-- The affine vector field `Z_E(x) = A x + b` of `Z = (A, b)`, as in `AffineSymplecticAction`. -/ +def vectorField (Z : affineSymplecticAlgebra σ) (x : E) : E := Z.1.1 x + Z.1.2 + +/-- The adjoint action (6.24): `Ad(a)(A, b) = (B A B⁻¹, B b - B A B⁻¹ C)` for `a = (B, C)`. -/ +def adjoint (a : AffineSymplecticGroup σ) : + affineSymplecticAlgebra σ →ₗ[ℝ] affineSymplecticAlgebra σ where + toFun Z := ⟨(a.linear.toLinearMap ∘ₗ Z.1.1 ∘ₗ a.linear.symm.toLinearMap, + a.linear Z.1.2 - a.linear (Z.1.1 (a.linear.symm a.translation))), by + rw [mem_affineSymplecticAlgebra] + intro v w + have h := Z.2 (a.linear.symm v) (a.linear.symm w) + rw [← a.map_symplecticForm (Z.1.1 (a.linear.symm v)) (a.linear.symm w), + ← a.map_symplecticForm (a.linear.symm v) (Z.1.1 (a.linear.symm w))] at h + simpa using h⟩ + map_add' Z Z' := by + refine Subtype.ext (Prod.ext (LinearMap.ext fun v => ?_) ?_) + · simp + · simp only [Submodule.coe_add, Prod.fst_add, Prod.snd_add, map_add, LinearMap.add_apply] + abel + map_smul' c Z := by + refine Subtype.ext (Prod.ext (LinearMap.ext fun v => ?_) ?_) + · simp + · simp only [Submodule.coe_smul, Prod.smul_fst, Prod.smul_snd, map_smul, LinearMap.smul_apply, + RingHom.id_apply, smul_sub] + +@[simp] +lemma adjoint_one : adjoint (1 : AffineSymplecticGroup σ) = LinearMap.id := by + refine LinearMap.ext fun Z => Subtype.ext (Prod.ext (LinearMap.ext fun v => rfl) ?_) + change Z.1.2 - Z.1.1 0 = Z.1.2 + simp + +lemma adjoint_mul (a b : AffineSymplecticGroup σ) : + adjoint (a * b) = adjoint a ∘ₗ adjoint b := by + refine LinearMap.ext fun Z => Subtype.ext (Prod.ext (LinearMap.ext fun v => rfl) ?_) + change (b.linear.trans a.linear) Z.1.2 + - (b.linear.trans a.linear) (Z.1.1 ((b.linear.trans a.linear).symm + (a.linear b.translation + a.translation))) + = a.linear (b.linear Z.1.2 - b.linear (Z.1.1 (b.linear.symm b.translation))) + - a.linear (b.linear (Z.1.1 (b.linear.symm (a.linear.symm a.translation)))) + simp only [LinearEquiv.trans_apply, LinearEquiv.symm_trans_apply, map_add, + LinearEquiv.symm_apply_apply, map_sub] + abel + +/-- (6.25): the adjoint action is the one for which `(Ad(a) Z)_E (a_E x) = B (Z_E x)`. With +`vectorField_injective` this characterises `adjoint`. -/ +lemma vectorField_adjoint (a : AffineSymplecticGroup σ) (Z : affineSymplecticAlgebra σ) (x : E) : + vectorField (adjoint a Z) (a • x) = a.linear (vectorField Z x) := by + dsimp only [vectorField] + have hA : (adjoint a Z).1.1 + = a.linear.toLinearMap ∘ₗ Z.1.1 ∘ₗ a.linear.symm.toLinearMap := rfl + have hb : (adjoint a Z).1.2 + = a.linear Z.1.2 - a.linear (Z.1.1 (a.linear.symm a.translation)) := rfl + rw [hA, hb, AffineSymplecticGroup.smul_def, LinearMap.comp_apply, LinearMap.comp_apply, + LinearEquiv.coe_toLinearMap, LinearEquiv.coe_toLinearMap] + have hsym : a.linear.symm (a.linear x + a.translation) = x + a.linear.symm a.translation := by + rw [map_add, LinearEquiv.symm_apply_apply] + rw [hsym, map_add, map_add, map_add] + abel + +/-- An element of the Lie algebra is determined by its vector field. -/ +lemma vectorField_injective {Z Z' : affineSymplecticAlgebra σ} + (h : ∀ x, vectorField Z x = vectorField Z' x) : Z = Z' := by + have h0 : Z.1.2 = Z'.1.2 := by + have := h 0 + simpa [vectorField] using this + refine Subtype.ext (Prod.ext (LinearMap.ext fun x => ?_) h0) + have hx := h x + rw [vectorField, vectorField, h0] at hx + exact add_right_cancel hx + +/-! + +## C. The coadjoint action and the moment + +The coadjoint action of (11.15), `a_{𝔤*}(μ) = μ ∘ Ad(a⁻¹)`, and the moment of (11.7), which is the +moment of `AffineSymplecticAction` read on the pairs `(A, b)`. + +-/ + +/-- (11.15): the coadjoint action `a_{𝔤*}(μ) = μ.a_𝔤⁻¹`, that is `μ ∘ Ad(a⁻¹)`. -/ +instance : SMul (AffineSymplecticGroup σ) (Dual ℝ (affineSymplecticAlgebra σ)) := + ⟨fun a μ => μ ∘ₗ adjoint a⁻¹⟩ + +@[simp] +lemma coadjoint_smul_apply (a : AffineSymplecticGroup σ) (μ : Dual ℝ (affineSymplecticAlgebra σ)) + (Z : affineSymplecticAlgebra σ) : (a • μ) Z = μ (adjoint a⁻¹ Z) := rfl + +instance : MulAction (AffineSymplecticGroup σ) (Dual ℝ (affineSymplecticAlgebra σ)) where + one_smul μ := by + refine LinearMap.ext fun Z => ?_ + simp + mul_smul a b μ := by + refine LinearMap.ext fun Z => ?_ + simp [mul_inv_rev, adjoint_mul] + +instance : DistribMulAction (AffineSymplecticGroup σ) (Dual ℝ (affineSymplecticAlgebra σ)) where + smul_zero a := by + refine LinearMap.ext fun Z => ?_ + simp + smul_add a μ ν := by + refine LinearMap.ext fun Z => ?_ + simp + +/-- (11.7): the moment of the affine symplectic action, `μ(x)(A, b) = -½ σ(A x, x) - σ(b, x)`, the +moment of `AffineSymplecticAction` read on the pairs `(A, b)`. -/ +def moment (σ : LinearMap.BilinForm ℝ E) (x : E) : Dual ℝ (affineSymplecticAlgebra σ) where + toFun Z := -(1 / 2 : ℝ) * σ (Z.1.1 x) x - σ Z.1.2 x + map_add' Z Z' := by + simp only [Submodule.coe_add, Prod.fst_add, Prod.snd_add, LinearMap.add_apply, map_add] + ring + map_smul' c Z := by + simp only [Submodule.coe_smul, Prod.smul_fst, Prod.smul_snd, LinearMap.smul_apply, map_smul, + smul_eq_mul, RingHom.id_apply] + ring + +@[simp] +lemma moment_apply (x : E) (Z : affineSymplecticAlgebra σ) : + moment σ x Z = -(1 / 2 : ℝ) * σ (Z.1.1 x) x - σ Z.1.2 x := rfl + +@[simp] +lemma moment_zero : moment σ (0 : E) = 0 := by + refine LinearMap.ext fun Z => ?_ + simp + +/-! + +## D. The cohomology class + +(11.17 a) in closed form, (11.17 b), (11.17 c) and the non-vanishing of the class. + +-/ + +/-- (11.17 a) in closed form: for this moment, the defect `θ(a) = μ(a_E(x)) - a_{𝔤*}(μ(x))` does +not depend on the point `x`, and equals the moment at `a_E(0) = C`. The terms in `x` cancel by the +infinitesimal symplecticity of `A` and the alternation of `σ`. -/ +lemma moment_smul_sub_smul_moment (hσ : IsSymplecticForm σ) (x : E) + (a : AffineSymplecticGroup σ) : + moment σ (a • x) - a • moment σ x = moment σ a.translation := by + refine LinearMap.ext fun Z => ?_ + have alt (u v : E) : σ u v = -σ v u := (hσ.alt.neg_eq v u).symm + have hB : ∀ u v, σ (a.linear.symm u) v = σ u (a.linear v) := by + intro u v + rw [← a.map_symplecticForm (a.linear.symm u) v, LinearEquiv.apply_symm_apply] + have h1 : σ (Z.1.1 (a.linear x)) a.translation + + σ (a.linear x) (Z.1.1 a.translation) = 0 := Z.2 (a.linear x) a.translation + have h1' : σ (Z.1.1 (a.linear x)) a.translation = σ (Z.1.1 a.translation) (a.linear x) := by + rw [alt (a.linear x) (Z.1.1 a.translation)] at h1 + exact sub_eq_zero.mp h1 + simp only [LinearMap.sub_apply, coadjoint_smul_apply, moment_apply, + AffineSymplecticGroup.smul_def] + simp [adjoint, map_add] + rw [hB (Z.1.1 (a.linear x)) x, hB Z.1.2 x, hB (Z.1.1 a.translation) x, h1'] + ring + +/-- (11.17 b): `θ(a) = μ(C)` is a 1-cocycle of the coadjoint action, +`θ(a × b) = θ(a) + a_{𝔤*}(θ(b))`. -/ +lemma isCocycle₁_moment_translation (hσ : IsSymplecticForm σ) : + groupCohomology.IsCocycle₁ (fun a : AffineSymplecticGroup σ => moment σ a.translation) := by + intro a b + show moment σ (a * b).translation + = a • moment σ b.translation + moment σ a.translation + have h := moment_smul_sub_smul_moment hσ b.translation a + have hab : (a * b).translation = a • b.translation := by + rw [AffineSymplecticGroup.smul_def] + rfl + rw [hab, ← h] + abel + +/-- `y ↦ σ (A y)` as a continuous linear map from `E` to `E →L[ℝ] ℝ`, used to differentiate the +quadratic part of the moment. -/ +def sigmaLinear {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] + (σ : LinearMap.BilinForm ℝ E) (A : E →ₗ[ℝ] E) : E →L[ℝ] (E →L[ℝ] ℝ) := + LinearMap.toContinuousLinearMap + ((LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] (E →L[ℝ] ℝ)).toLinearMap ∘ₗ σ ∘ₗ A) + +@[simp] +lemma sigmaLinear_apply {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] (σ : LinearMap.BilinForm ℝ E) (A : E →ₗ[ℝ] E) (y v : E) : + sigmaLinear σ A y v = σ (A y) v := by + simp [sigmaLinear] + +/-- The derivative of `y ↦ σ (A y) y` at `x` is `v ↦ σ (A v) x + σ (A x) v`. -/ +lemma hasFDerivAt_quad {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] (σ : LinearMap.BilinForm ℝ E) (A : E →ₗ[ℝ] E) (x : E) : + HasFDerivAt (fun y => σ (A y) y) + ((sigmaLinear σ A x).comp (ContinuousLinearMap.id ℝ E) + (sigmaLinear σ A).flip x) x := by + have h := (sigmaLinear σ A).hasFDerivAt (x := x) + have h2 := hasFDerivAt_id (𝕜 := ℝ) x + refine (h.clm_apply h2).congr_of_eventuallyEq (Filter.Eventually.of_forall fun y => ?_) + simp + +/-- (11.7) for the affine symplectic group: `σ(Z_E(x)) = -∇[μ.Z]`. -/ +lemma hasFDerivAt_moment {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] {σ : LinearMap.BilinForm ℝ E} (hσ : IsSymplecticForm σ) + (Z : affineSymplecticAlgebra σ) (x : E) : + HasFDerivAt (fun y => moment σ y Z) + (-(LinearMap.toContinuousLinearMap (σ (vectorField Z x)))) x := by + have hsym : ∀ v w : E, σ (Z.1.1 v) w = σ (Z.1.1 w) v := by + intro v w + rw [eq_neg_of_add_eq_zero_left (Z.2 v w), hσ.alt.neg_eq] + have hlin : HasFDerivAt (fun y => σ Z.1.2 y) + (LinearMap.toContinuousLinearMap (σ Z.1.2)) x := + (LinearMap.toContinuousLinearMap (σ Z.1.2)).hasFDerivAt + refine (((hasFDerivAt_quad σ Z.1.1 x).const_mul (-(1 / 2 : ℝ))).sub hlin).congr_fderiv ?_ + ext v + simp [vectorField] + rw [hsym v x] + ring + +/-- Part of (11.17 c): along any curve of the group issued from the identity whose translation part +has velocity `b'`, the derivative of `θ = μ(C)` at the identity is `σ (b', b Z)`, which is the value +of `AffineSymplecticAction.cocycle` on the corresponding pairs (a relation by formula: no Lean term +relates the two Lie algebras). -/ +lemma hasDerivAt_moment_translation {E : Type} [NormedAddCommGroup E] [NormedSpace ℝ E] + [FiniteDimensional ℝ E] {σ : LinearMap.BilinForm ℝ E} (hσ : IsSymplecticForm σ) + (γ : ℝ → AffineSymplecticGroup σ) (hγ : γ 0 = 1) (b' : E) + (hC : HasDerivAt (fun t => (γ t).translation) b' 0) (Z : affineSymplecticAlgebra σ) : + HasDerivAt (fun t => moment σ (γ t).translation Z) (σ b' Z.1.2) 0 := by + have h0 : (γ 0).translation = 0 := by rw [hγ]; rfl + refine ((hasFDerivAt_moment hσ Z ((γ 0).translation)).comp_hasDerivAt 0 hC).congr_deriv ?_ + simp only [neg_apply, LinearMap.coe_toContinuousLinearMap'] + rw [h0] + have hv : vectorField Z (0 : E) = Z.1.2 := by simp [vectorField] + rw [hv, hσ.alt.neg_eq] + +/-- The cohomology class of the affine symplectic group of a non-zero symplectic vector space is +NOT zero: `θ` is not a coboundary. On the translations `(id, C)` the coadjoint action fixes the +elements `(0, b)` of the Lie algebra, so every coboundary vanishes on them, whereas +`θ((id, C))(0, b) = -σ (b, C)`, which is non-zero for a suitable `b` by non-degeneracy. (By +Souriau's (11.21) this forbids a potential of `σ` invariant under the group; that implication is +not formalised here.) -/ +lemma not_isCoboundary₁_moment_translation (hσ : IsSymplecticForm σ) (hE : ∃ v : E, v ≠ 0) : + ¬ groupCohomology.IsCoboundary₁ + (fun a : AffineSymplecticGroup σ => moment σ a.translation) := by + rintro ⟨μ, hμ⟩ + obtain ⟨v, hv⟩ := hE + obtain ⟨w, hsw⟩ : ∃ w : E, σ v w ≠ 0 := by + by_contra h + push Not at h + exact hv (hσ.nondeg.1 v h) + let a : AffineSymplecticGroup σ := ⟨LinearEquiv.refl ℝ E, w, fun _ _ => rfl⟩ + let Z : affineSymplecticAlgebra σ := ⟨(0, v), by simp [mem_affineSymplecticAlgebra]⟩ + have hZ : adjoint a⁻¹ Z = Z := by + refine Subtype.ext (Prod.ext (LinearMap.ext fun u => ?_) ?_) + · show a.linear.symm (Z.1.1 (a.linear.symm.symm u)) = Z.1.1 u + simp [a, Z] + · show a.linear.symm Z.1.2 + - a.linear.symm (Z.1.1 (a.linear.symm.symm a⁻¹.translation)) = Z.1.2 + simp [a, Z] + have hk := congrArg (fun φ : Dual ℝ (affineSymplecticAlgebra σ) => φ Z) (hμ a) + simp only [LinearMap.sub_apply, coadjoint_smul_apply, hZ, sub_self] at hk + rw [show moment σ a.translation Z = -σ v w by simp [a, Z]] at hk + exact hsw (neg_eq_zero.mp hk.symm) + +/-! + +## E. The plane + +The simplest instance: the standard symplectic plane, whose affine symplectic group has a non-zero +cohomology class. This is the group-level counterpart of `planeTranslations_not_coboundary`. + +-/ + +/-- The affine symplectic group of the symplectic plane has a non-zero cohomology class. -/ +lemma planeForm_not_isCoboundary₁ : + ¬ groupCohomology.IsCoboundary₁ + (fun a : AffineSymplecticGroup planeForm => moment planeForm a.translation) := + not_isCoboundary₁_moment_translation isSymplecticForm_planeForm ⟨(1, 0), by simp⟩ + +end ClassicalMechanics From ce9565bc29f771cde2e700eb03c808a3b5bf84b4 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Wed, 23 Sep 2026 14:44:52 +0200 Subject: [PATCH 3/4] docs(PhyslibAlpha): drop the French chapter title from the references of MomentMap codespell reads "Groupes" as a misspelling of "Groups"; the chapter number and the pages are enough to locate the reference. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha/ClassicalMechanics/MomentMap.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMap.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap.lean index 5f9bbbfc0..1b3b776ab 100644 --- a/PhyslibAlpha/ClassicalMechanics/MomentMap.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap.lean @@ -70,14 +70,14 @@ field is `Z_{𝔤*}(ν) = ν ∘ Ad(Z)` (11.16). ## iv. References -- J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970, chapter 11 (Groupes - dynamiques), pp. 104-117; English translation: Structure of Dynamical Systems, Birkhäuser, 1997 +- J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970, chapter 11, + pp. 104-117; English translation: Structure of Dynamical Systems, Birkhäuser, 1997 (same equation numbers). ## References * J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, - Paris, 1970, chapter 11 "Groupes dynamiques", pp. 104-117. The equation numbers (11.7), + Paris, 1970, chapter 11, pp. 104-117. The equation numbers (11.7), (11.8), (11.12), (11.17), (11.22), (11.27), (11.33) refer to this edition. [ref: Souriau1970] -/ From 29b085124f5ea4aab31e26ff5db87c075df36364 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Wed, 23 Sep 2026 14:44:52 +0200 Subject: [PATCH 4/4] docs(PhyslibAlpha): drop the French chapter title from the references of MomentMapCohomology Same codespell fix as on moment-map-1, merged in above. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean b/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean index f0cdf3751..f8c53914c 100644 --- a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean @@ -64,14 +64,14 @@ given by a closed formula. ## iv. References -- J.-M. Souriau, Structure des systemes dynamiques, Dunod, Paris, 1970: chapter 11 (Groupes - dynamiques), pp. 104-117, for (11.7), (11.15)-(11.21) and (11.28); (6.24)-(6.25) and (10.12), +- J.-M. Souriau, Structure des systemes dynamiques, Dunod, Paris, 1970: chapter 11, + pp. 104-117, for (11.7), (11.15)-(11.21) and (11.28); (6.24)-(6.25) and (10.12), (10.28)-(10.32) for the adjoint action and the affine symplectic group. ## References * J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, - Paris, 1970, chapter 11 "Groupes dynamiques", pp. 104-117, and (6.24)-(6.25), (10.12). The + Paris, 1970, chapter 11, pp. 104-117, and (6.24)-(6.25), (10.12). The equation numbers refer to this edition. [ref: Souriau1970] -/