From c7d4f8bc9c5bcbdca80acde645b7f07fda80c8c2 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 24 Sep 2026 14:57:20 +0200 Subject: [PATCH 1/6] feat(PhyslibAlpha/ClassicalMechanics): the mass as a cohomology class of the Galilean Lie algebra Souriau's chapter 12 (SDS, Dunod 1970, pp. 132-153) at the level of the Lie algebra, for N free material points in Fin 3 -> R. Adds GalileanAlgebra (omega, beta, gamma, epsilon) with Souriau's bracket, GalileanTorsor {l, g, p, E} with the pairing (12.122), the 2-form f0 (12.130), and EvolutionSpace N with the vector fields (12.119), the Lagrange form (12.40) without forces and the moment (12.135). Results: the Jacobi identity; (12.129); M f0 is a coboundary of the algebra iff M = 0; (12.124) as a derivative along lines; (12.121) along the free motions; (12.134) with m = sum of the m_j; (12.136) at the level of the algebra; (12.141) g = m R - p t and the uniform motion of the centre of gravity of free points. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 1 + .../ClassicalMechanics/GalileanMass.lean | 460 ++++++++++++++++++ 2 files changed, 461 insertions(+) create mode 100644 PhyslibAlpha/ClassicalMechanics/GalileanMass.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index e5b26955d..192cb991c 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.GalileanMass public import PhyslibAlpha.ClassicalMechanics.MomentMap public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean new file mode 100644 index 000000000..a86a7b76d --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean @@ -0,0 +1,460 @@ +/- +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.CrossProduct +public import Mathlib.Analysis.Calculus.Deriv.Add +public import Mathlib.Analysis.Calculus.Deriv.Mul +public import Mathlib.Analysis.Calculus.Deriv.Pow +/-! + +# The mass as a cohomology class of the Galilean Lie algebra (Souriau) + +## i. Overview + +In chapter 12 of Structure des systèmes dynamiques (Dunod 1970), Souriau computes the moment of +the Galilean group acting on the evolution space of a system of material points. The moment is a +torsor `μ = {l, g, p, E}` (12.122)-(12.123): `l` is the angular momentum and `p` the momentum +(12.140), and `g = m R - p t` with `R` the centre of gravity (12.141). The Lagrange form `σ` of the +system satisfies (12.134), `σ(Z_V(y))(Z'_V(y)) = μ[Z, Z'] + m f₀(Z)(Z')`, where +`f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩` (12.130) and `m = Σ_j m_j` is the total mass (12.135). Souriau +concludes (12.136) that the total mass characterises the cohomology class of the system, and that +this class is never zero. + +This file proves these facts at the level of the Lie algebra for `N` free material points in +`ℝ³ = Fin 3 → ℝ` (no forces: `F_j = 0`, hence `E_j = B_j = 0` in (12.44)-(12.45)). An element +`Z = (ω, β, γ, ε)` of the Galilean Lie algebra (12.74), (12.118) is a rotation `ω` (an axial +vector), a change of velocity `β`, a space translation `γ` and a time translation `ε`; it acts on +the evolution space, whose points are `y = (t, r_j, v_j)` (12.76), by the affine vector field +(12.119). The bracket is Souriau's, `[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)` ((6.12 b), (11.22 a)), +opposite to the usual commutator (`EvolutionSpace.vectorField_bracket`). + +What is not formalised here: +- the Galilean group itself, its action (12.73), (12.76) and its cocycle `θ₀` (12.126)-(12.128), + hence the passage from the algebra to the group used on p. 151 and in (12.136). The Galilean group + is `GalileanGroup` in `Physlib.SpaceAndTime.GalileanGroup.Basic`; this file works with its Lie + algebra in dimension `3`, in Souriau's parametrisation, and does not link the two; +- `GalileanAlgebra` has no vector space or `LieRing` structure here, only `Zero` and `Add`; the + Jacobi identity is proved as an equation; +- the dimension `1` of (12.131), the second half of (12.136) (Hamilton's Lagrangian is not + invariant), forces, the converse of (12.48), the invariance of `σ` (12.72), (12.76), and the + uniqueness of the moment up to a constant (the constant in `E` is a choice); +- the evolution space is only presymplectic (`EvolutionSpace.lagrangeForm_motion`), so the setting + of `PhyslibAlpha.ClassicalMechanics.MomentMap` is not used; the moment and the cocycle are + computed explicitly. + +## ii. Key results + +- `GalileanAlgebra.bracket_jacobi`: the Jacobi identity for Souriau's bracket. +- `GalileanAlgebra.cocycle_cyclic`: (12.129), `f₀` satisfies the cyclic identity. +- `GalileanAlgebra.smul_cocycle_isCoboundary_iff`: `M f₀` is an algebra coboundary, + `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀`, if and only if `M = 0`. +- `EvolutionSpace.hasDerivAt_moment`: (12.124), the moment of the free points. +- `EvolutionSpace.moment_motion`: (12.121), the moment is constant along the free motions. +- `EvolutionSpace.lagrangeForm_vectorField`: (12.134) with `m = Σ_j m_j` (12.135). +- `EvolutionSpace.totalMass_cocycle_not_coboundary`: (12.136) at the level of the algebra, for a + non-zero total mass the cocycle of the system is not a coboundary. +- `EvolutionSpace.moment_g`, `EvolutionSpace.centerOfMass_motion`: (12.141), `g = m R - p t`, and + the uniform motion of the centre of gravity of free points. + +## iii. Table of contents + +- A. The Galilean Lie algebra +- B. Torsors +- C. The cocycle `f₀` +- D. The evolution space of free material points +- E. The moment +- F. The cocycle of the system and the mass + +## iv. References + +- J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970: pp. 132-133 + (12.40)-(12.48), pp. 139-140 (12.72)-(12.76), pp. 150-153 (12.118)-(12.141); p. 50 (6.12 b) and + p. 113 (11.22 a) for the bracket; p. 116, note (1), for the coboundaries of the algebra. + +## References + +* J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, + Paris, 1970, chapter 12, pp. 132-153. The equation numbers refer to this edition. + [ref: Souriau1970] + +-/ + +@[expose] public section + +noncomputable section + +namespace ClassicalMechanics + +open Matrix + +local notation "ℝ³" => Fin 3 → ℝ + +/-! + +## A. The Galilean Lie algebra + +-/ + +/-- An element `Z = (ω, β, γ, ε)` of the Lie algebra of the Galilean group, in Souriau's +parametrisation (12.74), (12.118). -/ +@[ext] +structure GalileanAlgebra where + /-- The infinitesimal rotation, as an axial vector. -/ + ω : ℝ³ + /-- The change of velocity (infinitesimal boost). -/ + β : ℝ³ + /-- The space translation. -/ + γ : ℝ³ + /-- The time translation. -/ + ε : ℝ + +namespace GalileanAlgebra + +instance : Zero GalileanAlgebra := ⟨⟨0, 0, 0, 0⟩⟩ + +instance : Add GalileanAlgebra := ⟨fun Z Z' => ⟨Z.ω + Z'.ω, Z.β + Z'.β, Z.γ + Z'.γ, Z.ε + Z'.ε⟩⟩ + +/-- Souriau's bracket on the Galilean Lie algebra. It is the bracket of the vector fields (12.119) +in the convention (6.12 b), (11.22 a), see `EvolutionSpace.vectorField_bracket`. -/ +def bracket (Z Z' : GalileanAlgebra) : GalileanAlgebra := + ⟨Z'.ω ⨯₃ Z.ω, Z'.ω ⨯₃ Z.β - Z.ω ⨯₃ Z'.β, + Z'.ω ⨯₃ Z.γ - Z.ω ⨯₃ Z'.γ + Z.ε • Z'.β - Z'.ε • Z.β, 0⟩ + +/-- The bracket is antisymmetric. -/ +lemma bracket_antisymm (Z Z' : GalileanAlgebra) : bracket Z Z' + bracket Z' Z = 0 := by + apply GalileanAlgebra.ext + · change Z'.ω ⨯₃ Z.ω + Z.ω ⨯₃ Z'.ω = 0 + simp + · change (Z'.ω ⨯₃ Z.β - Z.ω ⨯₃ Z'.β) + (Z.ω ⨯₃ Z'.β - Z'.ω ⨯₃ Z.β) = 0 + abel + · change (Z'.ω ⨯₃ Z.γ - Z.ω ⨯₃ Z'.γ + Z.ε • Z'.β - Z'.ε • Z.β) + + (Z.ω ⨯₃ Z'.γ - Z'.ω ⨯₃ Z.γ + Z'.ε • Z.β - Z.ε • Z'.β) = 0 + abel + · change (0 : ℝ) + 0 = 0 + simp + +/-- The Jacobi identity for Souriau's bracket. -/ +lemma bracket_jacobi (Z Z' Z'' : GalileanAlgebra) : + bracket Z (bracket Z' Z'') + bracket Z' (bracket Z'' Z) + bracket Z'' (bracket Z Z') = 0 := by + apply GalileanAlgebra.ext + · change (bracket Z (bracket Z' Z'')).ω + (bracket Z' (bracket Z'' Z)).ω + + (bracket Z'' (bracket Z Z')).ω = 0 + funext i + fin_cases i <;> simp [bracket, cross_apply, vecHead, vecTail] <;> ring + · change (bracket Z (bracket Z' Z'')).β + (bracket Z' (bracket Z'' Z)).β + + (bracket Z'' (bracket Z Z')).β = 0 + funext i + fin_cases i <;> simp [bracket, cross_apply, vecHead, vecTail] <;> ring + · change (bracket Z (bracket Z' Z'')).γ + (bracket Z' (bracket Z'' Z)).γ + + (bracket Z'' (bracket Z Z')).γ = 0 + funext i + fin_cases i <;> simp [bracket, cross_apply, vecHead, vecTail] <;> ring + · change (0 : ℝ) + 0 + 0 = 0 + simp + +/-- A change of velocity and a space translation commute. -/ +lemma bracket_boost_translation (β γ : ℝ³) : bracket ⟨0, β, 0, 0⟩ ⟨0, 0, γ, 0⟩ = 0 := by + simp [bracket] + rfl + +end GalileanAlgebra + +/-! + +## B. Torsors + +-/ + +/-- A torsor `μ = {l, g, p, E}`, an element of the dual of the Galilean Lie algebra (12.123). -/ +@[ext] +structure GalileanTorsor where + /-- The angular momentum part. -/ + l : ℝ³ + /-- The part paired with the changes of velocity. -/ + g : ℝ³ + /-- The momentum part. -/ + p : ℝ³ + /-- The energy part. -/ + E : ℝ + +/-- The pairing (12.122) of a torsor with an element of the Lie algebra, +`μ(Z) = ⟨l, ω⟩ - ⟨g, β⟩ + ⟨p, γ⟩ - E ε`. -/ +def GalileanTorsor.pair (μ : GalileanTorsor) (Z : GalileanAlgebra) : ℝ := + μ.l ⬝ᵥ Z.ω - μ.g ⬝ᵥ Z.β + μ.p ⬝ᵥ Z.γ - μ.E * Z.ε + +/-! + +## C. The cocycle `f₀` + +-/ + +namespace GalileanAlgebra + +/-- The 2-form `f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩` of (12.130). -/ +def cocycle (Z Z' : GalileanAlgebra) : ℝ := Z.β ⬝ᵥ Z'.γ - Z'.β ⬝ᵥ Z.γ + +/-- `f₀` is antisymmetric. -/ +lemma cocycle_antisymm (Z Z' : GalileanAlgebra) : cocycle Z Z' = -cocycle Z' Z := by + simp only [cocycle] + ring + +/-- (12.129): `f₀(Z)([Z', Z'']) + f₀(Z')([Z'', Z]) + f₀(Z'')([Z, Z']) = 0`. -/ +lemma cocycle_cyclic (Z Z' Z'' : GalileanAlgebra) : + cocycle Z (bracket Z' Z'') + cocycle Z' (bracket Z'' Z) + cocycle Z'' (bracket Z Z') = 0 := by + rw [cocycle, cocycle, cocycle, add_assoc, bracket, bracket, bracket] + simp only [cross_apply, vec3_dotProduct] + simp only [Fin.isValue, Nat.succ_eq_add_one, Nat.reduceAdd, sub_cons, head_cons, tail_cons, + sub_self, zero_empty, cons_add, empty_add_empty, Pi.sub_apply, cons_val_zero, Pi.smul_apply, + smul_eq_mul, cons_val_one, cons_val] + ring_nf + simp only [vecHead, vecTail] + simp only [Fin.isValue, Pi.smul_apply, smul_eq_mul, Nat.succ_eq_add_one, Nat.reduceAdd, + Function.comp_apply, Fin.succ_zero_eq_one, Fin.succ_one_eq_two] + ring_nf + +/-- `f₀` is not zero: its value on a change of velocity and a space translation along the same +axis is `1`. -/ +lemma cocycle_boost_translation : + cocycle ⟨0, ![1, 0, 0], 0, 0⟩ ⟨0, 0, ![1, 0, 0], 0⟩ = 1 := by + rw [cocycle] + simp + +/-- `M f₀` is a coboundary of the algebra, `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀` +(p. 116, note (1)), if and only if `M = 0`. -/ +lemma smul_cocycle_isCoboundary_iff (M : ℝ) : + (∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, M * cocycle Z Z' = μ₀.pair (bracket Z Z')) + ↔ M = 0 := by + constructor + · rintro ⟨μ₀, h⟩ + have h1 := h ⟨0, ![1, 0, 0], 0, 0⟩ ⟨0, 0, ![1, 0, 0], 0⟩ + rw [bracket_boost_translation ![1, 0, 0] ![1, 0, 0]] at h1 + change M * cocycle ⟨0, ![1, 0, 0], 0, 0⟩ ⟨0, 0, ![1, 0, 0], 0⟩ = + μ₀.l ⬝ᵥ 0 - μ₀.g ⬝ᵥ 0 + μ₀.p ⬝ᵥ 0 - μ₀.E * 0 at h1 + simp only [dotProduct, Pi.zero_apply, mul_zero, Finset.sum_const_zero, sub_zero, + add_zero] at h1 + rw [cocycle_boost_translation] at h1 + simpa using h1 + · intro hM + refine ⟨⟨0, 0, 0, 0⟩, fun Z Z' => ?_⟩ + rw [hM, GalileanTorsor.pair] + simp + +/-- `f₀` is not a coboundary of the algebra: no torsor `μ₀` satisfies `f₀(Z)(Z') = μ₀[Z, Z']` for +all `Z`, `Z'`. -/ +lemma cocycle_not_coboundary : + ¬ ∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, cocycle Z Z' = μ₀.pair (bracket Z Z') := by + rintro ⟨μ₀, h⟩ + exact one_ne_zero <| (smul_cocycle_isCoboundary_iff 1).mp + ⟨μ₀, fun Z Z' => by rw [one_mul]; exact h Z Z'⟩ + +end GalileanAlgebra + +/-! + +## D. The evolution space of free material points + +-/ + +/-- A point, or a tangent vector, of the evolution space of `N` material points, +`y = (t, r_j, v_j)` (12.76). -/ +@[ext] +structure EvolutionSpace (N : ℕ) where + /-- The time. -/ + t : ℝ + /-- The positions. -/ + r : Fin N → ℝ³ + /-- The velocities. -/ + v : Fin N → ℝ³ + +namespace EvolutionSpace + +variable {N : ℕ} + +instance : Sub (EvolutionSpace N) := ⟨fun y y' => ⟨y.t - y'.t, y.r - y'.r, y.v - y'.v⟩⟩ + +open GalileanAlgebra + +/-- The vector field `Z_V` of `Z` on the evolution space (12.119): `δt = ε`, +`δr_j = ω × r_j + β t + γ`, `δv_j = ω × v_j + β`. -/ +def vectorField (Z : GalileanAlgebra) (y : EvolutionSpace N) : EvolutionSpace N := + ⟨Z.ε, fun j => Z.ω ⨯₃ y.r j + y.t • Z.β + Z.γ, fun j => Z.ω ⨯₃ y.v j + Z.β⟩ + +/-- The differential of the affine vector field `Z_V` (its linear part), applied to a tangent vector +`w`. -/ +def linearPart (Z : GalileanAlgebra) (w : EvolutionSpace N) : EvolutionSpace N := + ⟨0, fun j => Z.ω ⨯₃ w.r j + w.t • Z.β, fun j => Z.ω ⨯₃ w.v j⟩ + +/-- Souriau's bracket is the bracket of the vector fields in the convention (6.12 b), (11.22 a): +`[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)`. -/ +lemma vectorField_bracket (Z Z' : GalileanAlgebra) (y : EvolutionSpace N) : + vectorField (bracket Z Z') y + = linearPart Z' (vectorField Z y) - linearPart Z (vectorField Z' y) := by + apply EvolutionSpace.ext + · change (0 : ℝ) = 0 - 0 + simp + · funext j + change (bracket Z Z').ω ⨯₃ y.r j + y.t • (bracket Z Z').β + (bracket Z Z').γ = + (linearPart Z' (vectorField Z y)).r j - (linearPart Z (vectorField Z' y)).r j + funext i + fin_cases i <;> simp [bracket, linearPart, vectorField, cross_apply, vecHead, vecTail] <;> ring + · funext j + change (bracket Z Z').ω ⨯₃ y.v j + (bracket Z Z').β = + (linearPart Z' (vectorField Z y)).v j - (linearPart Z (vectorField Z' y)).v j + funext i + fin_cases i <;> simp [bracket, linearPart, vectorField, cross_apply, vecHead, vecTail] <;> ring + +/-- The Lagrange form of `N` free material points of masses `m j` at `y`, (12.40) with `F_j = 0`: +`σ(dy)(δy) = Σ_j ⟨m_j dv_j, δr_j - v_j δt⟩ - ⟨m_j δv_j, dr_j - v_j dt⟩`. -/ +def lagrangeForm (m : Fin N → ℝ) (y dy δy : EvolutionSpace N) : ℝ := + ∑ j, (m j * (dy.v j ⬝ᵥ (δy.r j - δy.t • y.v j)) - m j * (δy.v j ⬝ᵥ (dy.r j - dy.t • y.v j))) + +/-- `σ` is antisymmetric. -/ +lemma lagrangeForm_antisymm (m : Fin N → ℝ) (y dy δy : EvolutionSpace N) : + lagrangeForm m y dy δy = -lagrangeForm m y δy dy := by + simp [lagrangeForm] + +/-- (12.41)-(12.43): the velocity `(1, v_j, 0)` of the free motion through `y` lies in the kernel +of `σ` (one direction of (12.48)). -/ +lemma lagrangeForm_motion (m : Fin N → ℝ) (y δy : EvolutionSpace N) : + lagrangeForm m y ⟨1, y.v, 0⟩ δy = 0 := by + simp [lagrangeForm] + +/-! + +## E. The moment + +-/ + +/-- The moment of `N` free material points ((12.125) for one point, (12.135) for `N` points): +`l = Σ m_j r_j × v_j`, `g = Σ m_j (r_j - v_j t)`, `p = Σ m_j v_j`, `E = ½ Σ m_j ‖v_j‖²`. -/ +def moment (m : Fin N → ℝ) (y : EvolutionSpace N) : GalileanTorsor := + ⟨∑ j, m j • (y.r j ⨯₃ y.v j), ∑ j, m j • (y.r j - y.t • y.v j), ∑ j, m j • y.v j, + (1 / 2 : ℝ) * ∑ j, m j * (y.v j ⬝ᵥ y.v j)⟩ + +/-- The line `s ↦ y + s dy` of the evolution space. -/ +def line (y dy : EvolutionSpace N) (s : ℝ) : EvolutionSpace N := + ⟨y.t + s * dy.t, fun j => y.r j + s • dy.r j, fun j => y.v j + s • dy.v j⟩ + +/-- The free motion through `y`: `t + s`, `r_j + s v_j`, `v_j`. -/ +def motion (y : EvolutionSpace N) (s : ℝ) : EvolutionSpace N := + ⟨y.t + s, fun j => y.r j + s • y.v j, y.v⟩ + +/-- `μ(Z)` as a sum over the material points. -/ +lemma pair_moment (m : Fin N → ℝ) (y : EvolutionSpace N) (Z : GalileanAlgebra) : + (moment m y).pair Z = ∑ j, m j * ((y.r j ⨯₃ y.v j) ⬝ᵥ Z.ω - (y.r j - y.t • y.v j) ⬝ᵥ Z.β + + y.v j ⬝ᵥ Z.γ - (1 / 2 : ℝ) * Z.ε * (y.v j ⬝ᵥ y.v j)) := by + simp only [GalileanTorsor.pair, moment, sum_dotProduct, smul_dotProduct, smul_eq_mul] + rw [Finset.mul_sum, Finset.sum_mul, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib, + ← Finset.sum_sub_distrib] + refine Finset.sum_congr rfl (fun j _ => ?_) + ring + +/-- The `j`th term of `μ(Z)` along `y + s dy`, as a polynomial of degree two in `s`. -/ +private lemma pair_term_line (m t dt s : ℝ) (r v dr dv : ℝ³) (Z : GalileanAlgebra) : + m * (((r + s • dr) ⨯₃ (v + s • dv)) ⬝ᵥ Z.ω - ((r + s • dr) - (t + s * dt) • (v + s • dv)) ⬝ᵥ Z.β + + (v + s • dv) ⬝ᵥ Z.γ - (1 / 2 : ℝ) * Z.ε * ((v + s • dv) ⬝ᵥ (v + s • dv))) + = m * ((r ⨯₃ v) ⬝ᵥ Z.ω - (r - t • v) ⬝ᵥ Z.β + v ⬝ᵥ Z.γ - (1 / 2 : ℝ) * Z.ε * (v ⬝ᵥ v)) + + s * (m * (dv ⬝ᵥ ((Z.ω ⨯₃ r + t • Z.β + Z.γ) - Z.ε • v)) + - m * ((Z.ω ⨯₃ v + Z.β) ⬝ᵥ (dr - dt • v))) + + s ^ 2 * (m * ((dr ⨯₃ dv) ⬝ᵥ Z.ω + dt * (dv ⬝ᵥ Z.β) - (1 / 2 : ℝ) * Z.ε * (dv ⬝ᵥ dv))) := by + simp only [dotProduct, Fin.sum_univ_three, cross_apply, Pi.add_apply, Pi.sub_apply, + Pi.smul_apply, smul_eq_mul, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, + Matrix.head_cons, Matrix.tail_cons] + ring + +/-- The derivative at `0` of a polynomial of degree two. -/ +private lemma hasDerivAt_quadratic (a b c : ℝ) : + HasDerivAt (fun s : ℝ => a + s * b + s ^ 2 * c) b 0 := by + have h := (((hasDerivAt_id' (0 : ℝ)).mul_const b).const_add a).fun_add + ((hasDerivAt_pow 2 (0 : ℝ)).mul_const c) + simpa using h + +/-- (12.124): `σ(dy)(Z_V(y)) = dμ(Z)(dy)`, stated as the derivative at `s = 0` of +`s ↦ μ(y + s dy)(Z)`; `μ` is a moment of the action (12.120). -/ +lemma hasDerivAt_moment (m : Fin N → ℝ) (y dy : EvolutionSpace N) (Z : GalileanAlgebra) : + HasDerivAt (fun s => (moment m (line y dy s)).pair Z) (lagrangeForm m y dy (vectorField Z y)) + 0 := by + have hfun : (fun s => (moment m (line y dy s)).pair Z) = fun s => ∑ j, + (m j * ((y.r j ⨯₃ y.v j) ⬝ᵥ Z.ω - (y.r j - y.t • y.v j) ⬝ᵥ Z.β + y.v j ⬝ᵥ Z.γ + - (1 / 2 : ℝ) * Z.ε * (y.v j ⬝ᵥ y.v j)) + + s * (m j * (dy.v j ⬝ᵥ ((Z.ω ⨯₃ y.r j + y.t • Z.β + Z.γ) - Z.ε • y.v j)) + - m j * ((Z.ω ⨯₃ y.v j + Z.β) ⬝ᵥ (dy.r j - dy.t • y.v j))) + + s ^ 2 * (m j * ((dy.r j ⨯₃ dy.v j) ⬝ᵥ Z.ω + dy.t * (dy.v j ⬝ᵥ Z.β) + - (1 / 2 : ℝ) * Z.ε * (dy.v j ⬝ᵥ dy.v j)))) := by + funext s + rw [pair_moment] + refine Finset.sum_congr rfl (fun j _ => ?_) + exact pair_term_line (m j) y.t dy.t s (y.r j) (y.v j) (dy.r j) (dy.v j) Z + rw [hfun] + have hL : lagrangeForm m y dy (vectorField Z y) = ∑ j, + (m j * (dy.v j ⬝ᵥ ((Z.ω ⨯₃ y.r j + y.t • Z.β + Z.γ) - Z.ε • y.v j)) + - m j * ((Z.ω ⨯₃ y.v j + Z.β) ⬝ᵥ (dy.r j - dy.t • y.v j))) := rfl + rw [hL] + exact HasDerivAt.fun_sum (fun j _ => hasDerivAt_quadratic _ _ _) + +/-- (12.121): the moment is constant along every free motion. -/ +lemma moment_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : + moment m (motion y s) = moment m y := by + simp [moment, motion] + congr + ext j + simp [add_smul] + +/-! + +## F. The cocycle of the system and the mass + +-/ + +/-- The total mass `m = Σ_j m_j` (12.135). -/ +def totalMass (m : Fin N → ℝ) : ℝ := ∑ j, m j + +/-- The centre of gravity `R = (Σ_j m_j r_j) / m` of (12.141). -/ +def centerOfMass (m : Fin N → ℝ) (y : EvolutionSpace N) : ℝ³ := + (totalMass m)⁻¹ • ∑ j, m j • y.r j + +/-- (12.134) with `m = Σ_j m_j` (12.135): `σ(Z_V(y))(Z'_V(y)) = μ[Z, Z'] + m f₀(Z)(Z')`. -/ +lemma lagrangeForm_vectorField (m : Fin N → ℝ) (y : EvolutionSpace N) (Z Z' : GalileanAlgebra) : + lagrangeForm m y (vectorField Z y) (vectorField Z' y) + = (moment m y).pair (bracket Z Z') + totalMass m * cocycle Z Z' := by + simp [lagrangeForm, GalileanTorsor.pair, moment, cocycle, totalMass, bracket, vectorField, + sum_dotProduct, smul_dotProduct, vec3_dotProduct, cross_apply, vecHead, vecTail, + Finset.sum_mul, ← Finset.sum_sub_distrib, ← Finset.sum_add_distrib] + apply Finset.sum_congr rfl + intro j _ + ring + +/-- (12.136) at the level of the algebra: for a non-zero total mass, the cocycle `m f₀` of the +system is not a coboundary of the algebra. -/ +lemma totalMass_cocycle_not_coboundary (m : Fin N → ℝ) (hM : totalMass m ≠ 0) : + ¬ ∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, + totalMass m * cocycle Z Z' = μ₀.pair (bracket Z Z') := + fun h => hM ((smul_cocycle_isCoboundary_iff (totalMass m)).mp h) + +/-- (12.141): `g = m R - p t`, with `R` the centre of gravity, for a non-zero total mass. -/ +lemma moment_g (m : Fin N → ℝ) (hM : totalMass m ≠ 0) (y : EvolutionSpace N) : + (moment m y).g = totalMass m • centerOfMass m y - y.t • (moment m y).p := by + simp [moment, smul_sub] + simp only [centerOfMass, Finset.smul_sum] + congr 1 + all_goals simp [← mul_smul, mul_comm] + congr! with i + field_simp [hM] + +/-- (12.141) for free material points: along a free motion the centre of gravity moves uniformly +with velocity `p / m`. -/ +lemma centerOfMass_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : + centerOfMass m (motion y s) = centerOfMass m y + s • ((totalMass m)⁻¹ • (moment m y).p) := by + simp [centerOfMass, motion, smul_smul] + simp [moment, mul_smul, Finset.smul_sum, Finset.sum_add_distrib, smul_add] + congr + ext i + simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, mul_comm s] + +end EvolutionSpace + +end ClassicalMechanics From 1a8ee8c26156b124752bbd5d0b3840fa370e02ab Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 24 Sep 2026 16:12:41 +0200 Subject: [PATCH 2/6] feat(PhyslibAlpha/ClassicalMechanics): the mass cocycle of the Galilean group The group level of GalileanMass.lean (Souriau, SDS, Dunod 1970, chapter 12), built on Physlib's GalileanGroup 3. Adds the action of the Galilean group on the evolution space of N free material points (12.76) with its differential, the adjoint action on GalileanAlgebra (6.24) in components, a real vector space structure on GalileanTorsor and the coadjoint action (11.15), and Souriau's cocycle theta0 (12.127) as massCocycle. Results: the action is Physlib's action on Time x Space on each point; invariance of the Lagrange form (12.76); (6.25) and the injectivity of Z -> Z_V; (12.126)-(12.127) moment equivariance up to the total mass times theta0; theta0 is a groupCohomology.IsCocycle1 (12.128) and M theta0 is a coboundary iff M = 0 (p. 151, (12.136) at the group level); (12.130) the derivative of theta0 at the identity along curves is the algebra cocycle f0. GalileanGroup has rotations in O(3): the axial vector omega carries a factor det R, equal to 1 on SO(3). Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 1 + .../GalileanMassCocycle.lean | 749 ++++++++++++++++++ 2 files changed, 750 insertions(+) create mode 100644 PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index 192cb991c..69140c69e 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.GalileanMass +public import PhyslibAlpha.ClassicalMechanics.GalileanMassCocycle public import PhyslibAlpha.ClassicalMechanics.MomentMap public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean b/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean new file mode 100644 index 000000000..a4b8f923e --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean @@ -0,0 +1,749 @@ +/- +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.GalileanMass +public import Physlib.SpaceAndTime.GalileanGroup.Basic +public import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree +public import Mathlib.Algebra.Group.TransferInstance +public import Mathlib.Algebra.Module.TransferInstance +public import Mathlib.LinearAlgebra.Matrix.Adjugate +public import Mathlib.Analysis.Calculus.Deriv.Prod +/-! + +# The mass cocycle of the Galilean group (Souriau) + +## i. Overview + +This file is the group level of `PhyslibAlpha.ClassicalMechanics.GalileanMass`, which treats +chapter 12 of Souriau's Structure des systèmes dynamiques (Dunod 1970) at the level of the Lie +algebra. The group is Physlib's `GalileanGroup 3` (`Physlib.SpaceAndTime.GalileanGroup.Basic`), +`a = (R, b, c, e)` (rotation, velocity, space translation, time translation), whose action +`(t, x) ↦ (t + e, R x + b t + c)` is Souriau's (12.76); `EvolutionSpace.smul_time_position` shows +that the action on the evolution space below is that action on each material point. + +For `N` free material points, the file defines the action of the group on the evolution space +(12.76), the adjoint action on the Lie algebra (6.24) in components, and the coadjoint action on +the torsors (11.15). It proves that the group preserves the Lagrange form (12.76), that the +adjoint action satisfies (6.25), and that the moment of the free points is equivariant up to the +total mass times Souriau's cocycle `θ₀(a) = {c × b, c - b e, b, ½ ‖b‖²}` (12.126)-(12.127). +`θ₀` is a 1-cocycle (12.128) and is not a coboundary (p. 151), so the class of the system is not +zero for a non-zero total mass (12.136); its derivative at the identity is the 2-cocycle `f₀` of +`GalileanMass` (12.130). + +The rotation part of `GalileanGroup` ranges over `O(3)`, whereas Souriau's (12.73) takes it in +`SO(3)`. The results hold on the whole group once the rotation vector `ω`, an axial vector, is +transformed with the factor `det R` (conjugation of `j(ω)`, `orthogonal_mulVec_cross`); for a +rotation (`det R = 1`) all the formulas are Souriau's. + +The cohomology vocabulary is Mathlib's: `θ₀` is a `groupCohomology.IsCocycle₁` for the coadjoint +action, which is (11.19 ♡), and "the class is not zero" is `¬ groupCohomology.IsCoboundary₁`, +which is (11.19 ◇). As in `PhyslibAlpha.ClassicalMechanics.MomentMapCohomology`, Souriau's +requirement that a cocycle be differentiable is not part of these definitions. + +What is not formalised here: +- the identification of the law of `GalileanGroup` with the product of the matrices (12.73) (it + was checked numerically outside Lean); +- the identification of the adjoint action in components with the conjugation `a Z a⁻¹` of the + matrices (12.73), (12.74) (6.24); it is characterised instead by (6.25), `vectorField_smul`, + together with the injectivity of `Z ↦ Z_V` for `N ≥ 1`, `vectorField_injective`; +- the Lie group structure (12.75) and any manifold: the derivative (12.130) is taken along curves; +- that `θ₀` is a symplectic cocycle (11.30), the dimension `1` of (12.131), forces, and the second + half of (12.136) (Hamilton's Lagrangian is not invariant); +- (12.126) is printed for one point of unit mass; here it is proved for `N` points and the moment + of `GalileanMass`, whose additive constant is zero. + +## ii. Key results + +- `EvolutionSpace.lagrangeForm_smul`: (12.76), the group preserves the Lagrange form. +- `EvolutionSpace.vectorField_smul`: (6.25), `(a • Z)_V(a • y) = D(a_V)(y)(Z_V(y))`. +- `GalileanTorsor.coadjoint_pair`: (11.15), `(a • μ)(Z) = μ(a⁻¹ • Z)`. +- `EvolutionSpace.moment_smul_sub`: (12.126)-(12.127), `μ(a • y) - a • μ(y) = m θ₀(a)`. +- `isCocycle₁_massCocycle`: (12.128). +- `isCoboundary₁_smul_massCocycle_iff`, `not_isCoboundary₁_massCocycle`: `M θ₀` is a coboundary + if and only if `M = 0`. +- `EvolutionSpace.not_isCoboundary₁_moment_smul_sub`: (12.136) at the level of the group. +- `hasDerivAt_massCocycle`: (12.130), `f₀ = D(θ₀)(e)`. + +## iii. Table of contents + +- A. Orthogonal matrices and the cross product +- B. The action on the evolution space +- C. The adjoint action +- D. Torsors and the coadjoint action +- E. The cocycle `θ₀` and the mass +- F. The derivative of `θ₀` at the identity + +## iv. References + +- J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970: pp. 139-140 + (12.73)-(12.77), p. 151 (12.126)-(12.130), pp. 152-153 (12.135)-(12.136); pp. 52-53 + (6.24)-(6.25); p. 108 (11.15), p. 111 (the derivative of a cocycle), p. 112 (11.19). + +## References + +* J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, + Paris, 1970, chapters 6, 11 and 12. The equation numbers refer to this edition. + [ref: Souriau1970] + +-/ + +@[expose] public section + +noncomputable section + +namespace ClassicalMechanics + +open Matrix + +local notation "ℝ³" => Fin 3 → ℝ + +/-! + +## A. Orthogonal matrices and the cross product + +-/ + +section Orthogonal + +variable (R : Matrix.orthogonalGroup (Fin 3) ℝ) + +/-- On coordinates, the action of `O(3)` on `EuclideanSpace ℝ (Fin 3)` is the matrix product. -/ +lemma ofLp_orthogonal_smul (v : EuclideanSpace ℝ (Fin 3)) : + WithLp.ofLp (R • v) = R.1 *ᵥ WithLp.ofLp v := rfl + +/-- On coordinates, the real scalar multiplication of `EuclideanSpace ℝ (Fin 3)`. Stated apart +from `WithLp.ofLp_smul`, which would also rewrite the action of `O(3)`. -/ +lemma ofLp_real_smul (k : ℝ) (v : EuclideanSpace ℝ (Fin 3)) : + WithLp.ofLp (k • v) = k • WithLp.ofLp v := rfl + +/-- An orthogonal matrix satisfies `Rᵀ R = 1`. -/ +lemma orthogonal_transpose_mul_self : R.1ᵀ * R.1 = 1 := by + have h := R.2 + rw [Matrix.mem_orthogonalGroup_iff'] at h + simpa [Matrix.star_eq_conjTranspose] using h + +/-- An orthogonal matrix satisfies `R Rᵀ = 1`. -/ +lemma orthogonal_mul_transpose_self : R.1 * R.1ᵀ = 1 := by + have h := R.2 + rw [Matrix.mem_orthogonalGroup_iff] at h + simpa [Matrix.star_eq_conjTranspose] using h + +/-- The inverse of an orthogonal matrix is its transpose. -/ +lemma orthogonal_inv_val : (R⁻¹).1 = R.1ᵀ := by + have h : (R⁻¹).1 * R.1 = 1 := by + rw [← Submonoid.coe_mul, inv_mul_cancel, OneMemClass.coe_one] + calc (R⁻¹).1 = (R⁻¹).1 * (R.1 * R.1ᵀ) := by rw [orthogonal_mul_transpose_self, Matrix.mul_one] + _ = R.1ᵀ := by rw [← Matrix.mul_assoc, h, Matrix.one_mul] + +/-- The determinant of an orthogonal matrix is `1` or `-1`: its square is `1`. -/ +lemma orthogonal_det_mul_self : R.1.det * R.1.det = 1 := by + calc R.1.det * R.1.det = R.1ᵀ.det * R.1.det := by rw [Matrix.det_transpose] + _ = 1 := by rw [← Matrix.det_mul, orthogonal_transpose_mul_self, Matrix.det_one] + +/-- The inverse of an orthogonal matrix has the same determinant. -/ +lemma orthogonal_det_inv : (R⁻¹).1.det = R.1.det := by + rw [orthogonal_inv_val, Matrix.det_transpose] + +/-- An orthogonal matrix preserves the dot product. -/ +lemma orthogonal_mulVec_dotProduct (u v : ℝ³) : (R.1 *ᵥ u) ⬝ᵥ (R.1 *ᵥ v) = u ⬝ᵥ v := by + rw [Matrix.dotProduct_mulVec, ← Matrix.vecMul_transpose, Matrix.vecMul_vecMul, + orthogonal_transpose_mul_self, Matrix.vecMul_one] + +/-- Moving an orthogonal matrix to the other side of a dot product: `⟨x, Rᵀ y⟩ = ⟨R x, y⟩`. -/ +lemma dotProduct_transpose_mulVec (x y : ℝ³) : x ⬝ᵥ (R.1ᵀ *ᵥ y) = (R.1 *ᵥ x) ⬝ᵥ y := by + rw [Matrix.dotProduct_mulVec, Matrix.vecMul_transpose] + +/-- For any `3 × 3` matrix, `(M u) × (M v) = (adj M)ᵀ (u × v)`. -/ +private lemma mulVec_cross_mulVec (M : Matrix (Fin 3) (Fin 3) ℝ) (u v : ℝ³) : + (M *ᵥ u) ⨯₃ (M *ᵥ v) = (adjugate M)ᵀ *ᵥ (u ⨯₃ v) := by + funext i + fin_cases i <;> + simp [cross_apply, adjugate_fin_three, mulVec, dotProduct, Fin.sum_univ_three, + transpose_apply] <;> + ring + +/-- The adjugate of an orthogonal matrix is `det R • Rᵀ`. -/ +lemma orthogonal_adjugate : adjugate R.1 = R.1.det • R.1ᵀ := by + calc adjugate R.1 = (R.1ᵀ * R.1) * adjugate R.1 := by + rw [orthogonal_transpose_mul_self, Matrix.one_mul] + _ = R.1ᵀ * (R.1 * adjugate R.1) := by rw [Matrix.mul_assoc] + _ = R.1.det • R.1ᵀ := by rw [Matrix.mul_adjugate, Matrix.mul_smul, Matrix.mul_one] + +/-- An orthogonal matrix maps the cross product to `det R` times the cross product of the images: +`R (u × v) = det R • (R u × R v)`. A rotation (`det R = 1`) preserves the cross product. -/ +lemma orthogonal_mulVec_cross (u v : ℝ³) : + R.1 *ᵥ (u ⨯₃ v) = R.1.det • ((R.1 *ᵥ u) ⨯₃ (R.1 *ᵥ v)) := by + rw [mulVec_cross_mulVec, orthogonal_adjugate, transpose_smul, transpose_transpose, + Matrix.smul_mulVec, smul_smul, orthogonal_det_mul_self, one_smul] + +/-- The same for the transpose: `Rᵀ (u × v) = det R • (Rᵀ u × Rᵀ v)`. -/ +lemma orthogonal_transpose_mulVec_cross (u v : ℝ³) : + R.1ᵀ *ᵥ (u ⨯₃ v) = R.1.det • ((R.1ᵀ *ᵥ u) ⨯₃ (R.1ᵀ *ᵥ v)) := by + have h := orthogonal_mulVec_cross R⁻¹ u v + rwa [orthogonal_inv_val, Matrix.det_transpose] at h + +/-- `⟨u × v, det R • Rᵀ w⟩ = ⟨R u × R v, w⟩`: the angular momentum paired with an axial vector. -/ +lemma cross_dotProduct_det_smul_transpose_mulVec (u v w : ℝ³) : + (u ⨯₃ v) ⬝ᵥ (R.1.det • (R.1ᵀ *ᵥ w)) = ((R.1 *ᵥ u) ⨯₃ (R.1 *ᵥ v)) ⬝ᵥ w := by + rw [dotProduct_smul, dotProduct_transpose_mulVec, orthogonal_mulVec_cross, smul_dotProduct, + smul_smul, orthogonal_det_mul_self, one_smul] + +end Orthogonal + +/-! + +## B. The action on the evolution space + +-/ + +namespace EvolutionSpace + +variable {N : ℕ} + +/-- The action (12.76) of the Galilean group on the evolution space of `N` material points, +`t* = t + e`, `r_j* = R r_j + b t + c`, `v_j* = R v_j + b`, for +`a = (R, b, c, e)` (rotation, velocity, space translation, time translation). -/ +instance : SMul (GalileanGroup 3) (EvolutionSpace N) := + ⟨fun a y => ⟨y.t + a.timeTranslation.val, + fun j => a.rotation.1 *ᵥ y.r j + y.t • WithLp.ofLp a.velocity + + WithLp.ofLp a.spaceTranslation, + fun j => a.rotation.1 *ᵥ y.v j + WithLp.ofLp a.velocity⟩⟩ + +@[simp] +lemma smul_t (a : GalileanGroup 3) (y : EvolutionSpace N) : + (a • y).t = y.t + a.timeTranslation.val := rfl + +@[simp] +lemma smul_r (a : GalileanGroup 3) (y : EvolutionSpace N) (j : Fin N) : + (a • y).r j = a.rotation.1 *ᵥ y.r j + y.t • WithLp.ofLp a.velocity + + WithLp.ofLp a.spaceTranslation := rfl + +@[simp] +lemma smul_v (a : GalileanGroup 3) (y : EvolutionSpace N) (j : Fin N) : + (a • y).v j = a.rotation.1 *ᵥ y.v j + WithLp.ofLp a.velocity := rfl + +/-- The Galilean group acts on the evolution space (12.77). -/ +instance : MulAction (GalileanGroup 3) (EvolutionSpace N) where + one_smul y := by + apply EvolutionSpace.ext + · simp + · funext j + simp + · funext j + simp + mul_smul a a' y := by + apply EvolutionSpace.ext + · simp only [smul_t, GalileanGroup.mul_timeTranslation, Time.add_val] + ring + · funext j + simp only [smul_r, smul_t, GalileanGroup.mul_rotation, GalileanGroup.mul_velocity, + GalileanGroup.mul_spaceTranslation, Submonoid.coe_mul, WithLp.ofLp_add, + ofLp_orthogonal_smul, ofLp_real_smul, ← Matrix.mulVec_mulVec, Matrix.mulVec_add, + Matrix.mulVec_smul, add_smul, smul_add] + module + · funext j + simp only [smul_v, GalileanGroup.mul_rotation, GalileanGroup.mul_velocity, Submonoid.coe_mul, + WithLp.ofLp_add, ofLp_orthogonal_smul, ← Matrix.mulVec_mulVec, Matrix.mulVec_add] + abel + +/-- The differential of the affine map `y ↦ a • y`, applied to a tangent vector `dy`: +`(dt, R dr_j + b dt, R dv_j)`. -/ +def tangentSMul (a : GalileanGroup 3) (dy : EvolutionSpace N) : EvolutionSpace N := + ⟨dy.t, fun j => a.rotation.1 *ᵥ dy.r j + dy.t • WithLp.ofLp a.velocity, + fun j => a.rotation.1 *ᵥ dy.v j⟩ + +/-- The action is affine with linear part `tangentSMul a`: it maps the line `s ↦ y + s dy` to the +line `s ↦ a • y + s (tangentSMul a dy)`. -/ +lemma smul_line (a : GalileanGroup 3) (y dy : EvolutionSpace N) (s : ℝ) : + a • line y dy s = line (a • y) (tangentSMul a dy) s := by + apply EvolutionSpace.ext + · simp only [smul_t, line, tangentSMul] + ring + · funext j + simp only [smul_r, line, tangentSMul, Matrix.mulVec_add, Matrix.mulVec_smul] + module + · funext j + simp only [smul_v, line, tangentSMul, Matrix.mulVec_add, Matrix.mulVec_smul] + abel + +/-- On each material point, the action is Physlib's action of the Galilean group on +`Time × Space 3`: the time and the position of the `j`th point of `a • y` are the images of those +of `y`. -/ +lemma smul_time_position (a : GalileanGroup 3) (y : EvolutionSpace N) (j : Fin N) : + a • ((⟨y.t⟩ : Time), Space.vectorToSpace (WithLp.toLp 2 (y.r j))) + = ((⟨(a • y).t⟩ : Time), Space.vectorToSpace (WithLp.toLp 2 ((a • y).r j))) := by + refine Prod.ext (Time.ext ?_) (Space.eq_of_apply fun i => ?_) + · simp [Time.add_val] + · simp only [GalileanGroup.smul_snd, GalileanGroup.actSpace_apply, Space.vectorToSpace_vsub_zero, + Space.vectorToSpace_apply, smul_r] + rfl + +/-- (12.76 ♣): the Galilean group preserves the Lagrange form of free material points, +`σ(a • y)(a dy)(a δy) = σ(y)(dy)(δy)`. -/ +lemma lagrangeForm_smul (m : Fin N → ℝ) (a : GalileanGroup 3) (y dy δy : EvolutionSpace N) : + lagrangeForm m (a • y) (tangentSMul a dy) (tangentSMul a δy) = lagrangeForm m y dy δy := by + simp only [lagrangeForm, tangentSMul, smul_v] + refine Finset.sum_congr rfl fun j _ => ?_ + have h (s : ℝ) (r : ℝ³) : a.rotation.1 *ᵥ r + s • WithLp.ofLp a.velocity + - s • (a.rotation.1 *ᵥ y.v j + WithLp.ofLp a.velocity) + = a.rotation.1 *ᵥ (r - s • y.v j) := by + rw [Matrix.mulVec_sub, Matrix.mulVec_smul] + module + rw [h, h, orthogonal_mulVec_dotProduct, orthogonal_mulVec_dotProduct] + +/-! + +## C. The adjoint action + +-/ + +end EvolutionSpace + +namespace GalileanAlgebra + +/-- The adjoint action (6.24) of the Galilean group on its Lie algebra, the conjugation +`Z ↦ a Z a⁻¹` of the matrices (12.73), (12.74) written in components: with +`ω* = det R • R ω`, `a • (ω, β, γ, ε) = (ω*, R β - ω* × b, R γ + ε b - e R β - ω* × (c - e b), ε)`. +The factor `det R` is `1` for a rotation; it makes `ω` an axial vector under reflections. -/ +instance : SMul (GalileanGroup 3) GalileanAlgebra := + ⟨fun a Z => ⟨a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω), + a.rotation.1 *ᵥ Z.β - (a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω)) ⨯₃ WithLp.ofLp a.velocity, + a.rotation.1 *ᵥ Z.γ + Z.ε • WithLp.ofLp a.velocity + - a.timeTranslation.val • (a.rotation.1 *ᵥ Z.β) + - (a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω)) ⨯₃ + (WithLp.ofLp a.spaceTranslation - a.timeTranslation.val • WithLp.ofLp a.velocity), + Z.ε⟩⟩ + +@[simp] +lemma smul_ω (a : GalileanGroup 3) (Z : GalileanAlgebra) : + (a • Z).ω = a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω) := rfl + +@[simp] +lemma smul_β (a : GalileanGroup 3) (Z : GalileanAlgebra) : + (a • Z).β = a.rotation.1 *ᵥ Z.β + - (a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω)) ⨯₃ WithLp.ofLp a.velocity := rfl + +@[simp] +lemma smul_γ (a : GalileanGroup 3) (Z : GalileanAlgebra) : + (a • Z).γ = a.rotation.1 *ᵥ Z.γ + Z.ε • WithLp.ofLp a.velocity + - a.timeTranslation.val • (a.rotation.1 *ᵥ Z.β) + - (a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω)) ⨯₃ + (WithLp.ofLp a.spaceTranslation - a.timeTranslation.val • WithLp.ofLp a.velocity) := rfl + +@[simp] +lemma smul_ε (a : GalileanGroup 3) (Z : GalileanAlgebra) : (a • Z).ε = Z.ε := rfl + +/-- The adjoint action is an action of the Galilean group on its Lie algebra. -/ +instance : MulAction (GalileanGroup 3) GalileanAlgebra where + one_smul Z := by + apply GalileanAlgebra.ext <;> simp + mul_smul a a' Z := by + apply GalileanAlgebra.ext + · simp only [smul_ω, GalileanGroup.mul_rotation, Submonoid.coe_mul, Matrix.det_mul, + ← Matrix.mulVec_mulVec, Matrix.mulVec_smul, smul_smul] + · simp only [smul_ω, smul_β, GalileanGroup.mul_rotation, GalileanGroup.mul_velocity, + Submonoid.coe_mul, Matrix.det_mul, WithLp.ofLp_add, ofLp_orthogonal_smul, + ← Matrix.mulVec_mulVec, Matrix.mulVec_sub, Matrix.mulVec_smul, orthogonal_mulVec_cross, + smul_smul, map_add, map_smul, LinearMap.smul_apply] + module + · simp only [smul_ω, smul_β, smul_γ, smul_ε, GalileanGroup.mul_rotation, + GalileanGroup.mul_velocity, GalileanGroup.mul_spaceTranslation, + GalileanGroup.mul_timeTranslation, Time.add_val, Submonoid.coe_mul, Matrix.det_mul, + WithLp.ofLp_add, ofLp_orthogonal_smul, ofLp_real_smul, ← Matrix.mulVec_mulVec, + Matrix.mulVec_add, Matrix.mulVec_sub, Matrix.mulVec_smul, orthogonal_mulVec_cross, + smul_smul, map_add, map_sub, map_smul, LinearMap.smul_apply, add_smul, smul_add, smul_sub] + module + · rfl + +/-- The adjoint action of `a⁻¹` in closed form: +`a⁻¹ • Z = (det R • Rᵀ ω, Rᵀ (β + ω × b), Rᵀ (γ - ε b + e β + ω × c), ε)`. -/ +lemma inv_smul_eq (a : GalileanGroup 3) (Z : GalileanAlgebra) : + a⁻¹ • Z = ⟨a.rotation.1.det • (a.rotation.1ᵀ *ᵥ Z.ω), + a.rotation.1ᵀ *ᵥ (Z.β + Z.ω ⨯₃ WithLp.ofLp a.velocity), + a.rotation.1ᵀ *ᵥ (Z.γ - Z.ε • WithLp.ofLp a.velocity + a.timeTranslation.val • Z.β + + Z.ω ⨯₃ WithLp.ofLp a.spaceTranslation), Z.ε⟩ := by + apply GalileanAlgebra.ext + · simp only [smul_ω, GalileanGroup.inv_rotation, orthogonal_inv_val, Matrix.det_transpose] + · simp only [smul_β, GalileanGroup.inv_rotation, GalileanGroup.inv_velocity, + orthogonal_inv_val, Matrix.det_transpose, WithLp.ofLp_neg, ofLp_orthogonal_smul, + Matrix.mulVec_add, orthogonal_transpose_mulVec_cross, map_neg, map_smul, + LinearMap.smul_apply] + module + · simp only [smul_γ, GalileanGroup.inv_rotation, GalileanGroup.inv_velocity, + GalileanGroup.inv_spaceTranslation, GalileanGroup.inv_timeTranslation, Time.neg_val, + WithLp.ofLp_neg, WithLp.ofLp_add, ofLp_orthogonal_smul, ofLp_real_smul, orthogonal_inv_val, + Matrix.det_transpose, Matrix.mulVec_add, Matrix.mulVec_sub, Matrix.mulVec_smul, + orthogonal_transpose_mulVec_cross, map_add, map_sub, map_neg, map_smul, + LinearMap.smul_apply, smul_neg, neg_smul] + module + · rfl + +end GalileanAlgebra + +namespace EvolutionSpace + +variable {N : ℕ} + +/-- (6.25): the vector field of `a • Z` at `a • y` is the image of the vector field of `Z` at `y`, +`(a • Z)_V(a • y) = D(a_V)(y)(Z_V(y))`. -/ +lemma vectorField_smul (a : GalileanGroup 3) (Z : GalileanAlgebra) (y : EvolutionSpace N) : + vectorField (a • Z) (a • y) = tangentSMul a (vectorField Z y) := by + apply EvolutionSpace.ext + · rfl + · funext j + simp only [vectorField, tangentSMul, GalileanAlgebra.smul_ω, GalileanAlgebra.smul_β, + GalileanAlgebra.smul_γ, GalileanAlgebra.smul_ε, smul_r, smul_t, Matrix.mulVec_add, + Matrix.mulVec_smul, orthogonal_mulVec_cross, map_add, map_sub, map_smul, + LinearMap.smul_apply, add_smul, smul_sub] + module + · funext j + simp only [vectorField, tangentSMul, GalileanAlgebra.smul_ω, GalileanAlgebra.smul_β, smul_v, + Matrix.mulVec_add, orthogonal_mulVec_cross, map_add, map_smul, LinearMap.smul_apply] + abel + +/-- For `N ≥ 1` the map `Z ↦ Z_V` is injective, so (6.25) characterises the adjoint action. -/ +lemma vectorField_injective [NeZero N] {Z Z' : GalileanAlgebra} + (h : ∀ y : EvolutionSpace N, vectorField Z y = vectorField Z' y) : Z = Z' := by + have h0 := h ⟨0, 0, 0⟩ + have hβ : Z.β = Z'.β := by + simpa [vectorField] using congrFun (congrArg EvolutionSpace.v h0) 0 + have hω (u : ℝ³) : Z.ω ⨯₃ u = Z'.ω ⨯₃ u := by + have := congrFun (congrArg EvolutionSpace.v (h ⟨0, 0, fun _ => u⟩)) 0 + simp only [vectorField, hβ] at this + exact add_right_cancel this + have h1 := hω ![1, 0, 0] + have h2 := hω ![0, 1, 0] + apply GalileanAlgebra.ext + · have a1 := congrFun h1 1 + have a2 := congrFun h1 2 + have b2 := congrFun h2 2 + simp [cross_apply] at a1 a2 b2 + funext i + fin_cases i + · exact b2 + · exact a2 + · exact a1 + · exact hβ + · simpa [vectorField] using congrFun (congrArg EvolutionSpace.r h0) 0 + · exact congrArg EvolutionSpace.t h0 + +end EvolutionSpace + +/-! + +## D. Torsors and the coadjoint action + +-/ + +namespace GalileanTorsor + +/-- The torsors as `ℝ³ × ℝ³ × ℝ³ × ℝ`, to transfer the vector space structure. -/ +def equivProd : GalileanTorsor ≃ ℝ³ × ℝ³ × ℝ³ × ℝ where + toFun μ := (μ.l, μ.g, μ.p, μ.E) + invFun x := ⟨x.1, x.2.1, x.2.2.1, x.2.2.2⟩ + left_inv _ := rfl + right_inv _ := rfl + +/-- The torsors form an additive group, component by component. -/ +instance : AddCommGroup GalileanTorsor := equivProd.addCommGroup + +/-- The torsors form a real vector space, component by component. -/ +instance : Module ℝ GalileanTorsor := AddEquiv.module ℝ equivProd.addEquiv + +/-- The pairing is additive in the torsor. -/ +lemma pair_add (μ ν : GalileanTorsor) (Z : GalileanAlgebra) : + (μ + ν).pair Z = μ.pair Z + ν.pair Z := by + change (μ.l + ν.l) ⬝ᵥ Z.ω - (μ.g + ν.g) ⬝ᵥ Z.β + (μ.p + ν.p) ⬝ᵥ Z.γ - (μ.E + ν.E) * Z.ε = _ + simp only [pair, add_dotProduct] + ring + +/-- The pairing is additive in the torsor: subtraction. -/ +lemma pair_sub (μ ν : GalileanTorsor) (Z : GalileanAlgebra) : + (μ - ν).pair Z = μ.pair Z - ν.pair Z := by + change (μ.l - ν.l) ⬝ᵥ Z.ω - (μ.g - ν.g) ⬝ᵥ Z.β + (μ.p - ν.p) ⬝ᵥ Z.γ - (μ.E - ν.E) * Z.ε = _ + simp only [pair, sub_dotProduct] + ring + +/-- The zero torsor pairs to zero. -/ +lemma pair_zero (Z : GalileanAlgebra) : (0 : GalileanTorsor).pair Z = 0 := by + change (0 : ℝ³) ⬝ᵥ Z.ω - (0 : ℝ³) ⬝ᵥ Z.β + (0 : ℝ³) ⬝ᵥ Z.γ - (0 : ℝ) * Z.ε = 0 + simp + +/-- The pairing is linear in the torsor. -/ +lemma pair_smul (k : ℝ) (μ : GalileanTorsor) (Z : GalileanAlgebra) : + (k • μ).pair Z = k * μ.pair Z := by + change (k • μ.l) ⬝ᵥ Z.ω - (k • μ.g) ⬝ᵥ Z.β + (k • μ.p) ⬝ᵥ Z.γ - (k • μ.E) * Z.ε = _ + simp only [pair, smul_dotProduct, smul_eq_mul] + ring + +/-- A torsor is determined by its values on the Lie algebra. -/ +lemma ext_pair {μ ν : GalileanTorsor} (h : ∀ Z, μ.pair Z = ν.pair Z) : μ = ν := by + apply GalileanTorsor.ext + · funext i + simpa [pair] using h ⟨Pi.single i 1, 0, 0, 0⟩ + · funext i + simpa [pair] using h ⟨0, Pi.single i 1, 0, 0⟩ + · funext i + simpa [pair] using h ⟨0, 0, Pi.single i 1, 0⟩ + · simpa [pair] using h ⟨0, 0, 0, 1⟩ + +/-- The coadjoint action (11.15) of the Galilean group on the torsors, in closed form: +`a • {l, g, p, E} = {det R • R l - b × R g + c × R p, R g - e R p, R p, E + ⟨R p, b⟩}`. +It is characterised by `(a • μ)(Z) = μ(a⁻¹ • Z)` (`coadjoint_pair`). -/ +instance : SMul (GalileanGroup 3) GalileanTorsor := + ⟨fun a μ => ⟨a.rotation.1.det • (a.rotation.1 *ᵥ μ.l) + - WithLp.ofLp a.velocity ⨯₃ (a.rotation.1 *ᵥ μ.g) + + WithLp.ofLp a.spaceTranslation ⨯₃ (a.rotation.1 *ᵥ μ.p), + a.rotation.1 *ᵥ μ.g - a.timeTranslation.val • (a.rotation.1 *ᵥ μ.p), + a.rotation.1 *ᵥ μ.p, μ.E + (a.rotation.1 *ᵥ μ.p) ⬝ᵥ WithLp.ofLp a.velocity⟩⟩ + +/-- (11.15): `(a • μ)(Z) = μ(a⁻¹ • Z)`. -/ +lemma coadjoint_pair (a : GalileanGroup 3) (μ : GalileanTorsor) (Z : GalileanAlgebra) : + (a • μ).pair Z = μ.pair (a⁻¹ • Z) := by + rw [GalileanAlgebra.inv_smul_eq] + change (a.rotation.1.det • (a.rotation.1 *ᵥ μ.l) - WithLp.ofLp a.velocity ⨯₃ (a.rotation.1 *ᵥ μ.g) + + WithLp.ofLp a.spaceTranslation ⨯₃ (a.rotation.1 *ᵥ μ.p)) ⬝ᵥ Z.ω + - (a.rotation.1 *ᵥ μ.g - a.timeTranslation.val • (a.rotation.1 *ᵥ μ.p)) ⬝ᵥ Z.β + + (a.rotation.1 *ᵥ μ.p) ⬝ᵥ Z.γ + - (μ.E + (a.rotation.1 *ᵥ μ.p) ⬝ᵥ WithLp.ofLp a.velocity) * Z.ε + = μ.l ⬝ᵥ (a.rotation.1.det • (a.rotation.1ᵀ *ᵥ Z.ω)) + - μ.g ⬝ᵥ (a.rotation.1ᵀ *ᵥ (Z.β + Z.ω ⨯₃ WithLp.ofLp a.velocity)) + + μ.p ⬝ᵥ (a.rotation.1ᵀ *ᵥ (Z.γ - Z.ε • WithLp.ofLp a.velocity + a.timeTranslation.val • Z.β + + Z.ω ⨯₃ WithLp.ofLp a.spaceTranslation)) + - μ.E * Z.ε + rw [dotProduct_smul, dotProduct_transpose_mulVec, dotProduct_transpose_mulVec, + dotProduct_transpose_mulVec] + generalize a.rotation.1 *ᵥ μ.l = L + generalize a.rotation.1 *ᵥ μ.g = G + generalize a.rotation.1 *ᵥ μ.p = P + generalize a.rotation.1.det = d + simp only [dotProduct, Fin.sum_univ_three, cross_apply, Pi.add_apply, Pi.sub_apply, + Pi.smul_apply, smul_eq_mul, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, + Matrix.head_cons, Matrix.tail_cons] + ring + +/-- The coadjoint action is a linear action of the Galilean group on the torsors. -/ +instance : MulAction (GalileanGroup 3) GalileanTorsor where + one_smul μ := ext_pair fun Z => by rw [coadjoint_pair, inv_one, one_smul] + mul_smul a a' μ := ext_pair fun Z => by + rw [coadjoint_pair, coadjoint_pair, coadjoint_pair, _root_.mul_inv_rev, mul_smul] + +/-- The coadjoint action is linear. -/ +instance : DistribMulAction (GalileanGroup 3) GalileanTorsor where + smul_zero a := ext_pair fun Z => by rw [coadjoint_pair, pair_zero, pair_zero] + smul_add a μ ν := ext_pair fun Z => by + rw [coadjoint_pair, pair_add, pair_add, coadjoint_pair, coadjoint_pair] + +end GalileanTorsor + +/-! + +## E. The cocycle `θ₀` and the mass + +-/ + +/-- Souriau's cocycle `θ₀(a) = {c × b, c - b e, b, ½ ‖b‖²}` of the Galilean group (12.127), for +`a = (R, b, c, e)`. -/ +def massCocycle (a : GalileanGroup 3) : GalileanTorsor := + ⟨WithLp.ofLp a.spaceTranslation ⨯₃ WithLp.ofLp a.velocity, + WithLp.ofLp a.spaceTranslation - a.timeTranslation.val • WithLp.ofLp a.velocity, + WithLp.ofLp a.velocity, (1 / 2 : ℝ) * (WithLp.ofLp a.velocity ⬝ᵥ WithLp.ofLp a.velocity)⟩ + +/-- `θ₀(1) = 0`. -/ +lemma massCocycle_one : massCocycle 1 = 0 := by + apply GalileanTorsor.ext_pair + intro Z + rw [GalileanTorsor.pair_zero] + simp [massCocycle, GalileanTorsor.pair] + +/-- (12.128): `θ₀` is a 1-cocycle of the Galilean group for the coadjoint action, +`θ₀(a a') = a • θ₀(a') + θ₀(a)`. -/ +lemma isCocycle₁_massCocycle : groupCohomology.IsCocycle₁ massCocycle := by + intro a a' + refine GalileanTorsor.ext_pair fun Z => ?_ + rw [GalileanTorsor.pair_add, GalileanTorsor.coadjoint_pair, GalileanAlgebra.inv_smul_eq] + have hE : WithLp.ofLp a'.velocity ⬝ᵥ WithLp.ofLp a'.velocity + = (a.rotation.1 *ᵥ WithLp.ofLp a'.velocity) ⬝ᵥ (a.rotation.1 *ᵥ WithLp.ofLp a'.velocity) := + (orthogonal_mulVec_dotProduct _ _ _).symm + change (WithLp.ofLp (a * a').spaceTranslation ⨯₃ WithLp.ofLp (a * a').velocity) ⬝ᵥ Z.ω + - (WithLp.ofLp (a * a').spaceTranslation + - (a * a').timeTranslation.val • WithLp.ofLp (a * a').velocity) ⬝ᵥ Z.β + + WithLp.ofLp (a * a').velocity ⬝ᵥ Z.γ + - (1 / 2 : ℝ) * (WithLp.ofLp (a * a').velocity ⬝ᵥ WithLp.ofLp (a * a').velocity) * Z.ε + = ((WithLp.ofLp a'.spaceTranslation ⨯₃ WithLp.ofLp a'.velocity) + ⬝ᵥ (a.rotation.1.det • (a.rotation.1ᵀ *ᵥ Z.ω)) + - (WithLp.ofLp a'.spaceTranslation - a'.timeTranslation.val • WithLp.ofLp a'.velocity) + ⬝ᵥ (a.rotation.1ᵀ *ᵥ (Z.β + Z.ω ⨯₃ WithLp.ofLp a.velocity)) + + WithLp.ofLp a'.velocity ⬝ᵥ (a.rotation.1ᵀ *ᵥ (Z.γ - Z.ε • WithLp.ofLp a.velocity + + a.timeTranslation.val • Z.β + Z.ω ⨯₃ WithLp.ofLp a.spaceTranslation)) + - (1 / 2 : ℝ) * (WithLp.ofLp a'.velocity ⬝ᵥ WithLp.ofLp a'.velocity) * Z.ε) + + ((WithLp.ofLp a.spaceTranslation ⨯₃ WithLp.ofLp a.velocity) ⬝ᵥ Z.ω + - (WithLp.ofLp a.spaceTranslation - a.timeTranslation.val • WithLp.ofLp a.velocity) ⬝ᵥ Z.β + + WithLp.ofLp a.velocity ⬝ᵥ Z.γ + - (1 / 2 : ℝ) * (WithLp.ofLp a.velocity ⬝ᵥ WithLp.ofLp a.velocity) * Z.ε) + rw [cross_dotProduct_det_smul_transpose_mulVec, dotProduct_transpose_mulVec, + dotProduct_transpose_mulVec, hE, Matrix.mulVec_sub, Matrix.mulVec_smul] + simp only [GalileanGroup.mul_velocity, GalileanGroup.mul_spaceTranslation, + GalileanGroup.mul_timeTranslation, Time.add_val, WithLp.ofLp_add, ofLp_orthogonal_smul, + ofLp_real_smul] + generalize a.rotation.1 *ᵥ WithLp.ofLp a'.velocity = B' + generalize a.rotation.1 *ᵥ WithLp.ofLp a'.spaceTranslation = C' + generalize WithLp.ofLp a.velocity = b + generalize WithLp.ofLp a.spaceTranslation = c + simp only [dotProduct, Fin.sum_univ_three, cross_apply, Pi.add_apply, Pi.sub_apply, + Pi.smul_apply, smul_eq_mul, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, + Matrix.head_cons, Matrix.tail_cons] + ring + +/-- `M θ₀` is a coboundary, `M θ₀(a) = a • μ₀ - μ₀` for some torsor `μ₀` (11.19), if and only if +`M = 0`: the classes `M [θ₀]` are pairwise distinct. -/ +lemma isCoboundary₁_smul_massCocycle_iff (M : ℝ) : + groupCohomology.IsCoboundary₁ (fun a : GalileanGroup 3 => M • massCocycle a) ↔ M = 0 := by + constructor + · rintro ⟨μ₀, h⟩ + have hZ : (⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩ : GalileanGroup 3)⁻¹ • + (⟨0, 0, ![1, 0, 0], 0⟩ : GalileanAlgebra) = ⟨0, 0, ![1, 0, 0], 0⟩ := by + rw [GalileanAlgebra.inv_smul_eq] + apply GalileanAlgebra.ext <;> simp [Time.zero_val] + have hθ : (massCocycle ⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩).pair ⟨0, 0, ![1, 0, 0], 0⟩ = 1 := by + simp [massCocycle, GalileanTorsor.pair, Time.zero_val] + have h1 := congrArg (fun μ => μ.pair ⟨0, 0, ![1, 0, 0], 0⟩) + (h ⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩) + simp only [GalileanTorsor.pair_sub, GalileanTorsor.coadjoint_pair, hZ, sub_self, + GalileanTorsor.pair_smul, hθ, mul_one] at h1 + exact h1.symm + · rintro rfl + exact ⟨0, fun a => by simp⟩ + +/-- `θ₀` is not a coboundary (p. 151): it defines a non-zero cohomology class of the Galilean +group. -/ +lemma not_isCoboundary₁_massCocycle : ¬ groupCohomology.IsCoboundary₁ massCocycle := by + intro h + refine one_ne_zero ((isCoboundary₁_smul_massCocycle_iff 1).mp ?_) + simpa using h + +namespace EvolutionSpace + +variable {N : ℕ} + +/-- (12.126)-(12.127) with `m = Σ_j m_j` (12.135): the moment of free material points is +equivariant up to the total mass times `θ₀`, `μ(a • y) - a • μ(y) = m θ₀(a)`, independently of +`y`. -/ +lemma moment_smul_sub (m : Fin N → ℝ) (a : GalileanGroup 3) (y : EvolutionSpace N) : + moment m (a • y) - a • moment m y = totalMass m • massCocycle a := by + refine GalileanTorsor.ext_pair fun Z => ?_ + rw [GalileanTorsor.pair_sub, GalileanTorsor.coadjoint_pair, GalileanTorsor.pair_smul, + GalileanAlgebra.inv_smul_eq, pair_moment, pair_moment, totalMass, Finset.sum_mul, + ← Finset.sum_sub_distrib] + refine Finset.sum_congr rfl fun j _ => ?_ + rw [← mul_sub] + congr 1 + have hE : y.v j ⬝ᵥ y.v j = (a.rotation.1 *ᵥ y.v j) ⬝ᵥ (a.rotation.1 *ᵥ y.v j) := + (orthogonal_mulVec_dotProduct _ _ _).symm + simp only [smul_r, smul_v, smul_t, massCocycle, GalileanTorsor.pair] + rw [cross_dotProduct_det_smul_transpose_mulVec, dotProduct_transpose_mulVec, + dotProduct_transpose_mulVec, hE, Matrix.mulVec_sub, Matrix.mulVec_smul] + generalize a.rotation.1 *ᵥ y.r j = X + generalize a.rotation.1 *ᵥ y.v j = Y + generalize WithLp.ofLp a.velocity = b + generalize WithLp.ofLp a.spaceTranslation = c + simp only [dotProduct, Fin.sum_univ_three, cross_apply, Pi.add_apply, Pi.sub_apply, + Pi.smul_apply, smul_eq_mul, Matrix.cons_val_zero, Matrix.cons_val_one, Matrix.cons_val_two, + Matrix.head_cons, Matrix.tail_cons] + ring + +/-- (12.136) at the level of the group: for a non-zero total mass, the cocycle +`a ↦ μ(a • y) - a • μ(y)` of the system is not a coboundary. -/ +lemma not_isCoboundary₁_moment_smul_sub (m : Fin N → ℝ) (hM : totalMass m ≠ 0) + (y : EvolutionSpace N) : + ¬ groupCohomology.IsCoboundary₁ + (fun a : GalileanGroup 3 => moment m (a • y) - a • moment m y) := by + simp_rw [moment_smul_sub] + rw [isCoboundary₁_smul_massCocycle_iff] + exact hM + +end EvolutionSpace + +/-! + +## F. The derivative of `θ₀` at the identity + +-/ + +/-- Product rule for the dot product of two curves in `ℝ³`. -/ +private lemma hasDerivAt_dotProduct {u v : ℝ → ℝ³} {u' v' : ℝ³} {x : ℝ} (hu : HasDerivAt u u' x) + (hv : HasDerivAt v v' x) : HasDerivAt (fun s => u s ⬝ᵥ v s) (u' ⬝ᵥ v x + u x ⬝ᵥ v') x := by + have h := HasDerivAt.fun_sum (u := Finset.univ) + (fun i _ => ((hasDerivAt_pi.1 hu) i).fun_mul ((hasDerivAt_pi.1 hv) i)) + refine h.congr_deriv ?_ + simp only [dotProduct, Finset.sum_add_distrib] + +/-- Product rule for the cross product of two curves in `ℝ³`. -/ +private lemma hasDerivAt_cross {u v : ℝ → ℝ³} {u' v' : ℝ³} {x : ℝ} (hu : HasDerivAt u u' x) + (hv : HasDerivAt v v' x) : HasDerivAt (fun s => u s ⨯₃ v s) (u' ⨯₃ v x + u x ⨯₃ v') x := by + have hu' := hasDerivAt_pi.1 hu + have hv' := hasDerivAt_pi.1 hv + refine hasDerivAt_pi.2 fun i => ?_ + fin_cases i + · convert ((hu' 1).fun_mul (hv' 2)).fun_sub ((hu' 2).fun_mul (hv' 1)) using 1 + · funext t + simp [cross_apply] + · simp [cross_apply] + ring + · convert ((hu' 2).fun_mul (hv' 0)).fun_sub ((hu' 0).fun_mul (hv' 2)) using 1 + · funext t + simp [cross_apply] + · simp [cross_apply] + ring + · convert ((hu' 0).fun_mul (hv' 1)).fun_sub ((hu' 1).fun_mul (hv' 0)) using 1 + · funext t + simp [cross_apply] + · simp [cross_apply] + ring + +/-- (12.130), `f₀ = D(θ₀)(e)`: along a curve `s ↦ γ s` of the Galilean group through the identity +whose velocity, space translation and time translation are differentiable at `0`, with derivatives +`b'`, `c'` and `e'`, the derivative at `0` of `s ↦ θ₀(γ s)(Z)` is `f₀(Z')(Z)` with +`Z' = (0, b', c', 0)`. It depends neither on the rotation part of the curve nor on `e'`. -/ +lemma hasDerivAt_massCocycle (γ : ℝ → GalileanGroup 3) (hγ : γ 0 = 1) + {b' c' : EuclideanSpace ℝ (Fin 3)} {e' : ℝ} (hb : HasDerivAt (fun s => (γ s).velocity) b' 0) + (hc : HasDerivAt (fun s => (γ s).spaceTranslation) c' 0) + (he : HasDerivAt (fun s => (γ s).timeTranslation.val) e' 0) (Z : GalileanAlgebra) : + HasDerivAt (fun s => (massCocycle (γ s)).pair Z) + (GalileanAlgebra.cocycle ⟨0, WithLp.ofLp b', WithLp.ofLp c', 0⟩ Z) 0 := by + have hb' : HasDerivAt (fun s => WithLp.ofLp (γ s).velocity) (WithLp.ofLp b') 0 := + (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin 3 => ℝ)).hasFDerivAt.comp_hasDerivAt 0 hb + have hc' : HasDerivAt (fun s => WithLp.ofLp (γ s).spaceTranslation) (WithLp.ofLp c') 0 := + (PiLp.continuousLinearEquiv 2 ℝ (fun _ : Fin 3 => ℝ)).hasFDerivAt.comp_hasDerivAt 0 hc + have h0b : WithLp.ofLp (γ 0).velocity = 0 := by rw [hγ]; rfl + have h0c : WithLp.ofLp (γ 0).spaceTranslation = 0 := by rw [hγ]; rfl + have h0e : (γ 0).timeTranslation.val = 0 := by rw [hγ]; exact Time.zero_val + have h1 := hasDerivAt_dotProduct (hasDerivAt_cross hc' hb') (hasDerivAt_const (0 : ℝ) Z.ω) + have h2 := hasDerivAt_dotProduct (hc'.fun_sub (he.fun_smul hb')) (hasDerivAt_const (0 : ℝ) Z.β) + have h3 := hasDerivAt_dotProduct hb' (hasDerivAt_const (0 : ℝ) Z.γ) + have h4 := ((hasDerivAt_dotProduct hb' hb').const_mul (1 / 2 : ℝ)).mul_const Z.ε + refine (((h1.fun_sub h2).fun_add h3).fun_sub h4).congr_deriv ?_ + simp only [GalileanAlgebra.cocycle, h0b, h0c, h0e, map_zero, LinearMap.zero_apply, add_zero, + zero_smul, smul_zero, sub_zero, dotProduct_zero, zero_dotProduct, mul_zero, zero_mul] + rw [dotProduct_comm Z.β] + ring + +/-- (12.130) along the curve `s ↦ (1, s b', s c', s e')`, which satisfies the hypotheses of +`hasDerivAt_massCocycle`. -/ +lemma hasDerivAt_massCocycle_line (b' c' : EuclideanSpace ℝ (Fin 3)) (e' : ℝ) + (Z : GalileanAlgebra) : + HasDerivAt (fun s : ℝ => (massCocycle ⟨1, s • b', s • c', ⟨s * e'⟩⟩).pair Z) + (GalileanAlgebra.cocycle ⟨0, WithLp.ofLp b', WithLp.ofLp c', 0⟩ Z) 0 := by + refine hasDerivAt_massCocycle (fun s => ⟨1, s • b', s • c', ⟨s * e'⟩⟩) ?_ (b' := b') (c' := c') + (e' := e') ?_ ?_ ?_ Z + · refine GalileanGroup.ext rfl (zero_smul ℝ b') (zero_smul ℝ c') ?_ + exact Time.ext (by simp [Time.zero_val]) + · simpa using (hasDerivAt_id (0 : ℝ)).smul_const b' + · simpa using (hasDerivAt_id (0 : ℝ)).smul_const c' + · simpa using (hasDerivAt_id (0 : ℝ)).mul_const e' + +end ClassicalMechanics From 67c3d7f211bd45bfcf1ea65d1ca7cf047fb1f47e Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 24 Sep 2026 17:12:29 +0200 Subject: [PATCH 3/6] feat(PhyslibAlpha/ClassicalMechanics): state the mass cocycle results on Souriau's group SO(3) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit An independent read-back of GalileanMassCocycle.lean against the printed pages found that the non-coboundary statements were only stated on Physlib's GalileanGroup 3, whose rotations range over O(3). A non-coboundary statement on the larger group does not imply the one on Souriau's group (12.73), where the rotation is in SO(3). Adds properGalileanGroup (det R = 1), isCocycle₁_massCocycle_proper, isCoboundary₁_smul_massCocycle_proper_iff, not_isCoboundary₁_massCocycle_proper and EvolutionSpace.not_isCoboundary₁_moment_smul_sub_proper, with the shared witness eq_zero_of_smul_massCocycle_boost; adds coadjoint_smul_real (the coadjoint action is linear). Docstrings: the O(3) paragraph, the adjoint action as (6.28), the printed formula (12.119), the differentiability of (11.19), (12.132) for N points, references. Co-Authored-By: Claude Opus 5.5 --- .../GalileanMassCocycle.lean | 173 +++++++++++++----- 1 file changed, 131 insertions(+), 42 deletions(-) diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean b/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean index a4b8f923e..d1e45e730 100644 --- a/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean +++ b/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean @@ -30,26 +30,35 @@ For `N` free material points, the file defines the action of the group on the ev the torsors (11.15). It proves that the group preserves the Lagrange form (12.76), that the adjoint action satisfies (6.25), and that the moment of the free points is equivariant up to the total mass times Souriau's cocycle `θ₀(a) = {c × b, c - b e, b, ½ ‖b‖²}` (12.126)-(12.127). -`θ₀` is a 1-cocycle (12.128) and is not a coboundary (p. 151), so the class of the system is not -zero for a non-zero total mass (12.136); its derivative at the identity is the 2-cocycle `f₀` of -`GalileanMass` (12.130). +`θ₀` is a 1-cocycle (12.128) and is not a coboundary, on Souriau's group (`det R = 1`) as on the +whole group (p. 151), so the class of the system is not zero for a non-zero total mass (12.136); +its derivative at the identity is the 2-cocycle `f₀` of `GalileanMass` (12.130). The rotation part of `GalileanGroup` ranges over `O(3)`, whereas Souriau's (12.73) takes it in -`SO(3)`. The results hold on the whole group once the rotation vector `ω`, an axial vector, is -transformed with the factor `det R` (conjugation of `j(ω)`, `orthogonal_mulVec_cross`); for a -rotation (`det R = 1`) all the formulas are Souriau's. +`SO(3)`. The rotation vector `ω`, an axial vector, is then transformed with the factor `det R` +(`orthogonal_mulVec_cross`). The identities proved for all `a` ((12.76), (12.77), (6.25), (11.15), +(12.126)-(12.128)) restrict to Souriau's group `properGalileanGroup`, where `det R = 1` and the +factor disappears. A negative statement does not restrict: a cocycle that is not a coboundary of +the larger group could be one of the smaller, so the statements of p. 151 and (12.136) are also +proved on `properGalileanGroup`. The adjoint and coadjoint actions in components are not printed +in chapter 12; they are computed here from (6.24), (6.28) and (11.15). The cohomology vocabulary is Mathlib's: `θ₀` is a `groupCohomology.IsCocycle₁` for the coadjoint action, which is (11.19 ♡), and "the class is not zero" is `¬ groupCohomology.IsCoboundary₁`, which is (11.19 ◇). As in `PhyslibAlpha.ClassicalMechanics.MomentMapCohomology`, Souriau's -requirement that a cocycle be differentiable is not part of these definitions. +requirement that a cocycle be differentiable is not part of these definitions. This does not +weaken the non-coboundary statements: a coboundary `a ↦ a • μ₀ - μ₀` of (11.19 ◇) is polynomial in +the entries of `a`, hence differentiable. What is not formalised here: - the identification of the law of `GalileanGroup` with the product of the matrices (12.73) (it was checked numerically outside Lean); -- the identification of the adjoint action in components with the conjugation `a Z a⁻¹` of the - matrices (12.73), (12.74) (6.24); it is characterised instead by (6.25), `vectorField_smul`, +- the identification of the adjoint action in components with the conjugation `a Z a⁻¹` (6.28) of + the matrices (12.73), (12.74); it is characterised instead by (6.25), `vectorField_smul`, together with the injectivity of `Z ↦ Z_V` for `N ≥ 1`, `vectorField_injective`; +- that the vector field `Z_V` (12.119), taken as printed in `GalileanMass`, is the derivative at + the identity of the action in the direction `Z` (6.11); the characterisation of the adjoint + action by (6.25) rests on this printed formula; - the Lie group structure (12.75) and any manifold: the derivative (12.130) is taken along curves; - that `θ₀` is a symplectic cocycle (11.30), the dimension `1` of (12.131), forces, and the second half of (12.136) (Hamilton's Lagrangian is not invariant); @@ -62,10 +71,13 @@ What is not formalised here: - `EvolutionSpace.vectorField_smul`: (6.25), `(a • Z)_V(a • y) = D(a_V)(y)(Z_V(y))`. - `GalileanTorsor.coadjoint_pair`: (11.15), `(a • μ)(Z) = μ(a⁻¹ • Z)`. - `EvolutionSpace.moment_smul_sub`: (12.126)-(12.127), `μ(a • y) - a • μ(y) = m θ₀(a)`. -- `isCocycle₁_massCocycle`: (12.128). -- `isCoboundary₁_smul_massCocycle_iff`, `not_isCoboundary₁_massCocycle`: `M θ₀` is a coboundary - if and only if `M = 0`. -- `EvolutionSpace.not_isCoboundary₁_moment_smul_sub`: (12.136) at the level of the group. +- `isCocycle₁_massCocycle`: (12.128); `isCocycle₁_massCocycle_proper` on Souriau's group. +- `isCoboundary₁_smul_massCocycle_proper_iff`, `not_isCoboundary₁_massCocycle_proper`: p. 151 on + Souriau's group `properGalileanGroup`, `M θ₀` is a coboundary if and only if `M = 0`; + `isCoboundary₁_smul_massCocycle_iff`, `not_isCoboundary₁_massCocycle`: the same on the whole + group. +- `EvolutionSpace.not_isCoboundary₁_moment_smul_sub_proper`: (12.136) at the level of Souriau's + group; `EvolutionSpace.not_isCoboundary₁_moment_smul_sub` on the whole group. - `hasDerivAt_massCocycle`: (12.130), `f₀ = D(θ₀)(e)`. ## iii. Table of contents @@ -80,8 +92,9 @@ What is not formalised here: ## iv. References - J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970: pp. 139-140 - (12.73)-(12.77), p. 151 (12.126)-(12.130), pp. 152-153 (12.135)-(12.136); pp. 52-53 - (6.24)-(6.25); p. 108 (11.15), p. 111 (the derivative of a cocycle), p. 112 (11.19). + (12.73)-(12.77), p. 151 (12.126)-(12.130), pp. 152-153 (12.132)-(12.136); pp. 52-53 (6.24), + (6.25), (6.28); p. 108 (11.15), p. 109 (11.17), p. 111 (the order of the arguments of the + derivative of a cocycle), p. 112 (11.19), p. 113 (11.22 b). ## References @@ -305,10 +318,12 @@ end EvolutionSpace namespace GalileanAlgebra -/-- The adjoint action (6.24) of the Galilean group on its Lie algebra, the conjugation -`Z ↦ a Z a⁻¹` of the matrices (12.73), (12.74) written in components: with +/-- The adjoint action (6.24) of the Galilean group on its Lie algebra, in components: with `ω* = det R • R ω`, `a • (ω, β, γ, ε) = (ω*, R β - ω* × b, R γ + ε b - e R β - ω* × (c - e b), ε)`. -The factor `det R` is `1` for a rotation; it makes `ω` an axial vector under reflections. -/ +It is the conjugation `Z ↦ a Z a⁻¹` (6.28) of the matrices (12.73), (12.74) with `R` taken in +`O(3)`; this identification is not proved here, the action is characterised by (6.25) +(`EvolutionSpace.vectorField_smul`). The factor `det R` is `1` for a rotation; it makes `ω` an +axial vector under reflections. -/ instance : SMul (GalileanGroup 3) GalileanAlgebra := ⟨fun a Z => ⟨a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω), a.rotation.1 *ᵥ Z.β - (a.rotation.1.det • (a.rotation.1 *ᵥ Z.ω)) ⨯₃ WithLp.ofLp a.velocity, @@ -526,18 +541,24 @@ lemma coadjoint_pair (a : GalileanGroup 3) (μ : GalileanTorsor) (Z : GalileanAl Matrix.head_cons, Matrix.tail_cons] ring -/-- The coadjoint action is a linear action of the Galilean group on the torsors. -/ +/-- The coadjoint action is an action of the Galilean group on the torsors. -/ instance : MulAction (GalileanGroup 3) GalileanTorsor where one_smul μ := ext_pair fun Z => by rw [coadjoint_pair, inv_one, one_smul] mul_smul a a' μ := ext_pair fun Z => by rw [coadjoint_pair, coadjoint_pair, coadjoint_pair, _root_.mul_inv_rev, mul_smul] -/-- The coadjoint action is linear. -/ +/-- The coadjoint action is additive; it is linear by `coadjoint_smul_real`. -/ instance : DistribMulAction (GalileanGroup 3) GalileanTorsor where smul_zero a := ext_pair fun Z => by rw [coadjoint_pair, pair_zero, pair_zero] smul_add a μ ν := ext_pair fun Z => by rw [coadjoint_pair, pair_add, pair_add, coadjoint_pair, coadjoint_pair] +/-- The coadjoint action commutes with the real scalar multiplication: it is a linear +representation, as in (11.14)-(11.15). -/ +lemma coadjoint_smul_real (a : GalileanGroup 3) (k : ℝ) (μ : GalileanTorsor) : + a • (k • μ) = k • (a • μ) := + ext_pair fun Z => by rw [coadjoint_pair, pair_smul, pair_smul, coadjoint_pair] + end GalileanTorsor /-! @@ -560,8 +581,9 @@ lemma massCocycle_one : massCocycle 1 = 0 := by rw [GalileanTorsor.pair_zero] simp [massCocycle, GalileanTorsor.pair] -/-- (12.128): `θ₀` is a 1-cocycle of the Galilean group for the coadjoint action, -`θ₀(a a') = a • θ₀(a') + θ₀(a)`. -/ +/-- (12.128): `θ₀` satisfies the cocycle identity (11.19 ♡) for the coadjoint action, +`θ₀(a a') = a • θ₀(a') + θ₀(a)` (`groupCohomology.IsCocycle₁`). The differentiability also +required by (11.19) is not part of this statement. -/ lemma isCocycle₁_massCocycle : groupCohomology.IsCocycle₁ massCocycle := by intro a a' refine GalileanTorsor.ext_pair fun Z => ?_ @@ -599,40 +621,94 @@ lemma isCocycle₁_massCocycle : groupCohomology.IsCocycle₁ massCocycle := by Matrix.head_cons, Matrix.tail_cons] ring -/-- `M θ₀` is a coboundary, `M θ₀(a) = a • μ₀ - μ₀` for some torsor `μ₀` (11.19), if and only if -`M = 0`: the classes `M [θ₀]` are pairwise distinct. -/ +/-- The witness of p. 151: if `a • μ₀ - μ₀ = M θ₀(a)` for the pure boost `a = (1, e₁, 0, 0)`, +then `M = 0`. This boost has `R = 1`, so it lies in Souriau's group `properGalileanGroup`. -/ +lemma eq_zero_of_smul_massCocycle_boost (M : ℝ) (μ₀ : GalileanTorsor) + (h : (⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩ : GalileanGroup 3) • μ₀ - μ₀ + = M • massCocycle ⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩) : M = 0 := by + have hZ : (⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩ : GalileanGroup 3)⁻¹ • + (⟨0, 0, ![1, 0, 0], 0⟩ : GalileanAlgebra) = ⟨0, 0, ![1, 0, 0], 0⟩ := by + rw [GalileanAlgebra.inv_smul_eq] + apply GalileanAlgebra.ext <;> simp [Time.zero_val] + have hθ : (massCocycle ⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩).pair ⟨0, 0, ![1, 0, 0], 0⟩ = 1 := by + simp [massCocycle, GalileanTorsor.pair, Time.zero_val] + have h1 := congrArg (fun μ => μ.pair ⟨0, 0, ![1, 0, 0], 0⟩) h + simp only [GalileanTorsor.pair_sub, GalileanTorsor.coadjoint_pair, hZ, sub_self, + GalileanTorsor.pair_smul, hθ, mul_one] at h1 + exact h1.symm + +/-- `M θ₀` is a coboundary of Physlib's Galilean group (rotations in `O(3)`), +`M θ₀(a) = a • μ₀ - μ₀` for some torsor `μ₀` (11.19 ◇), if and only if `M = 0`. For Souriau's +group (12.73) see `isCoboundary₁_smul_massCocycle_proper_iff`, which this lemma does not +imply. -/ lemma isCoboundary₁_smul_massCocycle_iff (M : ℝ) : groupCohomology.IsCoboundary₁ (fun a : GalileanGroup 3 => M • massCocycle a) ↔ M = 0 := by constructor · rintro ⟨μ₀, h⟩ - have hZ : (⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩ : GalileanGroup 3)⁻¹ • - (⟨0, 0, ![1, 0, 0], 0⟩ : GalileanAlgebra) = ⟨0, 0, ![1, 0, 0], 0⟩ := by - rw [GalileanAlgebra.inv_smul_eq] - apply GalileanAlgebra.ext <;> simp [Time.zero_val] - have hθ : (massCocycle ⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩).pair ⟨0, 0, ![1, 0, 0], 0⟩ = 1 := by - simp [massCocycle, GalileanTorsor.pair, Time.zero_val] - have h1 := congrArg (fun μ => μ.pair ⟨0, 0, ![1, 0, 0], 0⟩) - (h ⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩) - simp only [GalileanTorsor.pair_sub, GalileanTorsor.coadjoint_pair, hZ, sub_self, - GalileanTorsor.pair_smul, hθ, mul_one] at h1 - exact h1.symm + exact eq_zero_of_smul_massCocycle_boost M μ₀ (h _) · rintro rfl exact ⟨0, fun a => by simp⟩ -/-- `θ₀` is not a coboundary (p. 151): it defines a non-zero cohomology class of the Galilean -group. -/ +/-- `θ₀` is not a coboundary of Physlib's Galilean group (rotations in `O(3)`). Souriau's +statement (p. 151) is on his group (12.73) and is `not_isCoboundary₁_massCocycle_proper`; it is +not implied by this one. -/ lemma not_isCoboundary₁_massCocycle : ¬ groupCohomology.IsCoboundary₁ massCocycle := by intro h refine one_ne_zero ((isCoboundary₁_smul_massCocycle_iff 1).mp ?_) simpa using h +/-- Souriau's Galilean group (12.73): the elements of `GalileanGroup 3` whose rotation part has +determinant `1`, that is `R ∈ SO(3)`. -/ +def properGalileanGroup : Subgroup (GalileanGroup 3) where + carrier := {a | a.rotation.1.det = 1} + mul_mem' {a b} ha hb := by + change a.rotation.1.det = 1 at ha + change b.rotation.1.det = 1 at hb + change (a.rotation.1 * b.rotation.1).det = 1 + rw [Matrix.det_mul, ha, hb, mul_one] + one_mem' := by + change (1 : GalileanGroup 3).rotation.1.det = 1 + simp + inv_mem' {a} ha := by + change a.rotation.1.det = 1 at ha + change (a.rotation⁻¹).1.det = 1 + rw [orthogonal_det_inv, ha] + +/-- (12.128) on Souriau's group (12.73): the restriction of `θ₀` to `properGalileanGroup` satisfies +the cocycle identity (11.19 ♡). -/ +lemma isCocycle₁_massCocycle_proper : + groupCohomology.IsCocycle₁ (fun a : properGalileanGroup => massCocycle a) := + fun a a' => isCocycle₁_massCocycle a a' + +/-- p. 151 on Souriau's group (12.73): `M θ₀` is a coboundary of `properGalileanGroup`, +`M θ₀(a) = a • μ₀ - μ₀` for some torsor `μ₀` (11.19 ◇), if and only if `M = 0`. -/ +lemma isCoboundary₁_smul_massCocycle_proper_iff (M : ℝ) : + groupCohomology.IsCoboundary₁ (fun a : properGalileanGroup => M • massCocycle a) ↔ + M = 0 := by + constructor + · rintro ⟨μ₀, h⟩ + refine eq_zero_of_smul_massCocycle_boost M μ₀ + (h ⟨⟨1, WithLp.toLp 2 ![1, 0, 0], 0, 0⟩, ?_⟩) + change (1 : GalileanGroup 3).rotation.1.det = 1 + simp + · rintro rfl + exact ⟨0, fun a => by simp⟩ + +/-- p. 151 on Souriau's group (12.73): `θ₀` is not a coboundary of `properGalileanGroup`, so it +defines a non-zero cohomology class of Souriau's Galilean group. -/ +lemma not_isCoboundary₁_massCocycle_proper : + ¬ groupCohomology.IsCoboundary₁ (fun a : properGalileanGroup => massCocycle a) := by + intro h + refine one_ne_zero ((isCoboundary₁_smul_massCocycle_proper_iff 1).mp ?_) + simpa using h + namespace EvolutionSpace variable {N : ℕ} -/-- (12.126)-(12.127) with `m = Σ_j m_j` (12.135): the moment of free material points is -equivariant up to the total mass times `θ₀`, `μ(a • y) - a • μ(y) = m θ₀(a)`, independently of -`y`. -/ +/-- (12.126)-(12.127) for `N` points: with the moment of `GalileanMass` (additive constant zero) +and `m = Σ_j m_j` (12.135), `μ(a • y) - a • μ(y) = m θ₀(a)`, independently of `y`. Souriau +prints (12.126) for one point of unit mass; for `N` points this is (12.132) with `μ₀ = 0`. -/ lemma moment_smul_sub (m : Fin N → ℝ) (a : GalileanGroup 3) (y : EvolutionSpace N) : moment m (a • y) - a • moment m y = totalMass m • massCocycle a := by refine GalileanTorsor.ext_pair fun Z => ?_ @@ -656,8 +732,10 @@ lemma moment_smul_sub (m : Fin N → ℝ) (a : GalileanGroup 3) (y : EvolutionSp Matrix.head_cons, Matrix.tail_cons] ring -/-- (12.136) at the level of the group: for a non-zero total mass, the cocycle -`a ↦ μ(a • y) - a • μ(y)` of the system is not a coboundary. -/ +/-- (12.132) and (12.136) at the level of the group, on Physlib's Galilean group (rotations in +`O(3)`): for a non-zero total mass, the cocycle `a ↦ μ(a • y) - a • μ(y)` of the system is not a +coboundary. For Souriau's group (12.73) see `not_isCoboundary₁_moment_smul_sub_proper`, which this +lemma does not imply. -/ lemma not_isCoboundary₁_moment_smul_sub (m : Fin N → ℝ) (hM : totalMass m ≠ 0) (y : EvolutionSpace N) : ¬ groupCohomology.IsCoboundary₁ @@ -666,6 +744,17 @@ lemma not_isCoboundary₁_moment_smul_sub (m : Fin N → ℝ) (hM : totalMass m rw [isCoboundary₁_smul_massCocycle_iff] exact hM +/-- (12.132) and (12.136) at the level of the group, on Souriau's group (12.73): for a non-zero +total mass, the cocycle `a ↦ μ(a • y) - a • μ(y)` of the system, restricted to +`properGalileanGroup`, is not a coboundary. -/ +lemma not_isCoboundary₁_moment_smul_sub_proper (m : Fin N → ℝ) (hM : totalMass m ≠ 0) + (y : EvolutionSpace N) : + ¬ groupCohomology.IsCoboundary₁ + (fun a : properGalileanGroup => moment m (a • y) - a • moment m y) := by + simp_rw [Subgroup.smul_def, moment_smul_sub] + rw [isCoboundary₁_smul_massCocycle_proper_iff] + exact hM + end EvolutionSpace /-! From d45d65cf4664727ed160bdb61eecc79e999179f8 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 24 Sep 2026 18:40:57 +0200 Subject: [PATCH 4/6] docs(PhyslibAlpha/ClassicalMechanics): GalileanMass docstrings after a read-back against the book An independent read-back of GalileanMass.lean against the printed pages found no error in the statements and corrects the docstrings: the bracket of vector fields in (6.12 b) is (2.45), the usual Lie bracket of vector fields; only on the matrices (12.74) is Souriau's bracket the opposite of the usual commutator. Physlib's GalileanGroup has rotations in O(3) while Souriau's group (12.73) has them in SO(3). F_j = 0 alone does not give B_j = 0, which is the choice (12.49). Also: p. 151 works at the level of the group, the algebra coboundary is (11.24) with (11.16), (6.13 b), the presymplectic evolution space is (12.114), two more items in what is not formalised, and fuller references. Co-Authored-By: Claude Opus 5.5 --- .../ClassicalMechanics/GalileanMass.lean | 63 ++++++++++++------- 1 file changed, 42 insertions(+), 21 deletions(-) diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean index a86a7b76d..cd848a8f5 100644 --- a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean +++ b/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean @@ -21,29 +21,44 @@ torsor `μ = {l, g, p, E}` (12.122)-(12.123): `l` is the angular momentum and `p (12.140), and `g = m R - p t` with `R` the centre of gravity (12.141). The Lagrange form `σ` of the system satisfies (12.134), `σ(Z_V(y))(Z'_V(y)) = μ[Z, Z'] + m f₀(Z)(Z')`, where `f₀(Z)(Z') = ⟨β, γ'⟩ - ⟨β', γ⟩` (12.130) and `m = Σ_j m_j` is the total mass (12.135). Souriau -concludes (12.136) that the total mass characterises the cohomology class of the system, and that -this class is never zero. +remarks (12.136) that the total mass can be interpreted as characterising the corresponding +cohomology class of the Galilean group, and that this class is never zero. This file proves these facts at the level of the Lie algebra for `N` free material points in -`ℝ³ = Fin 3 → ℝ` (no forces: `F_j = 0`, hence `E_j = B_j = 0` in (12.44)-(12.45)). An element +`ℝ³ = Fin 3 → ℝ` (no forces, `F_j = 0`; with the choice `B_j = 0` of (12.49), which (12.135) +imposes on an isolated system, (12.44) gives `E_j = 0` and (12.45) reduces to (12.40)). An element `Z = (ω, β, γ, ε)` of the Galilean Lie algebra (12.74), (12.118) is a rotation `ω` (an axial vector), a change of velocity `β`, a space translation `γ` and a time translation `ε`; it acts on the evolution space, whose points are `y = (t, r_j, v_j)` (12.76), by the affine vector field -(12.119). The bracket is Souriau's, `[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)` ((6.12 b), (11.22 a)), -opposite to the usual commutator (`EvolutionSpace.vectorField_bracket`). +(12.119). The bracket is Souriau's (6.12 b), `[Z, Z']_V = [Z_V, Z'_V]`, where the bracket of two +vector fields is (2.45), here `DZ'_V(Z_V) - DZ_V(Z'_V)` (`EvolutionSpace.vectorField_bracket`); +this is the usual Lie bracket of vector fields (Mathlib's `VectorField.lieBracket`). The matrices +(12.74) are not formalised; on them this bracket reads `[Z, Z'] = Z'Z - ZZ'`, as in (11.22 a), the +opposite of the usual matrix commutator. What is not formalised here: - the Galilean group itself, its action (12.73), (12.76) and its cocycle `θ₀` (12.126)-(12.128), - hence the passage from the algebra to the group used on p. 151 and in (12.136). The Galilean group - is `GalileanGroup` in `Physlib.SpaceAndTime.GalileanGroup.Basic`; this file works with its Lie - algebra in dimension `3`, in Souriau's parametrisation, and does not link the two; + hence the statement of p. 151 that `θ₀` is not a coboundary of the group (definition (11.19)), + used in (12.136). The algebra-level result of this file implies it, because the derivative of a + group coboundary `Δ(μ₀)` is `μ₀[Z, Z']` (p. 116, note (1)); this implication is not formalised. + Physlib has `GalileanGroup` in `Physlib.SpaceAndTime.GalileanGroup.Basic`, whose rotation part + ranges over the full orthogonal group; Souriau's group (12.73) takes `A ∈ SO(3)` and is + connected (p. 139). Both have the same Lie algebra, with which this file works in dimension `3`, + in Souriau's parametrisation; the file links it to neither group; - `GalileanAlgebra` has no vector space or `LieRing` structure here, only `Zero` and `Add`; the Jacobi identity is proved as an equation; +- that the vector field (12.119), taken as printed, is the derivative (6.11) of the action (12.76); +- the reading of (12.135) as the solution of the system (12.124), (12.134) for a general isolated + system (`B_j = 0`, `Σ_j E_j = 0`, `Σ_j r_j × E_j = 0`): for free points the explicit moment and + `m = Σ_j m_j` are verified, not derived; the uniqueness of `m` in (12.134) follows from + `lagrangeForm_vectorField` and `smul_cocycle_isCoboundary_iff` but is not stated; - the dimension `1` of (12.131), the second half of (12.136) (Hamilton's Lagrangian is not invariant), forces, the converse of (12.48), the invariance of `σ` (12.72), (12.76), and the uniqueness of the moment up to a constant (the constant in `E` is a choice); -- the evolution space is only presymplectic (`EvolutionSpace.lagrangeForm_motion`), so the setting - of `PhyslibAlpha.ClassicalMechanics.MomentMap` is not used; the moment and the cocycle are +- the evolution space is presymplectic, not symplectic (p. 148, (12.114)); + `EvolutionSpace.lagrangeForm_motion` shows that `σ` is degenerate, and `σ` depends on the point + `y` through the velocities. The setting of `PhyslibAlpha.ClassicalMechanics.MomentMap` (a constant + non-degenerate form on a vector space) therefore does not apply; the moment and the cocycle are computed explicitly. ## ii. Key results @@ -72,13 +87,15 @@ What is not formalised here: ## iv. References - J.-M. Souriau, Structure des systèmes dynamiques, Dunod, Paris, 1970: pp. 132-133 - (12.40)-(12.48), pp. 139-140 (12.72)-(12.76), pp. 150-153 (12.118)-(12.141); p. 50 (6.12 b) and - p. 113 (11.22 a) for the bracket; p. 116, note (1), for the coboundaries of the algebra. + (12.40)-(12.49), pp. 139-140 (12.72)-(12.76), p. 148 (12.114), pp. 150-153 (12.118)-(12.141); + p. 27 (2.45), p. 50 (6.12 b) and p. 113 (11.22 a) for the bracket; p. 50 (6.13 b), p. 109 + (11.16), p. 114 (11.24) and p. 116, note (1), for the coboundaries of the algebra. ## References * J.-M. Souriau, *Structure des systèmes dynamiques*, Maîtrises de mathématiques, Dunod, - Paris, 1970, chapter 12, pp. 132-153. The equation numbers refer to this edition. + Paris, 1970: chapter 12, pp. 132-153, and pp. 27, 50, 109, 113-116 for the conventions (2.45), + (6.12), (6.13), (11.16), (11.22), (11.24). The equation numbers refer to this edition. [ref: Souriau1970] -/ @@ -119,7 +136,7 @@ instance : Zero GalileanAlgebra := ⟨⟨0, 0, 0, 0⟩⟩ instance : Add GalileanAlgebra := ⟨fun Z Z' => ⟨Z.ω + Z'.ω, Z.β + Z'.β, Z.γ + Z'.γ, Z.ε + Z'.ε⟩⟩ /-- Souriau's bracket on the Galilean Lie algebra. It is the bracket of the vector fields (12.119) -in the convention (6.12 b), (11.22 a), see `EvolutionSpace.vectorField_bracket`. -/ +in the convention (6.12 b), (2.45), see `EvolutionSpace.vectorField_bracket`. -/ def bracket (Z Z' : GalileanAlgebra) : GalileanAlgebra := ⟨Z'.ω ⨯₃ Z.ω, Z'.ω ⨯₃ Z.β - Z.ω ⨯₃ Z'.β, Z'.ω ⨯₃ Z.γ - Z.ω ⨯₃ Z'.γ + Z.ε • Z'.β - Z'.ε • Z.β, 0⟩ @@ -223,8 +240,9 @@ lemma cocycle_boost_translation : rw [cocycle] simp -/-- `M f₀` is a coboundary of the algebra, `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀` -(p. 116, note (1)), if and only if `M = 0`. -/ +/-- `M f₀` is a coboundary of the algebra, `M f₀(Z)(Z') = μ₀[Z, Z']` for some torsor `μ₀` ((11.24) +with `Z_{g*}(μ) = μ ∘ Ad(Z)` (11.16) and `Ad(Z)(Z') = [Z, Z']` (6.13 b); by p. 116, note (1), this +is also the derivative of the group coboundary `Δ(μ₀)` of (11.19)), if and only if `M = 0`. -/ lemma smul_cocycle_isCoboundary_iff (M : ℝ) : (∃ μ₀ : GalileanTorsor, ∀ Z Z' : GalileanAlgebra, M * cocycle Z Z' = μ₀.pair (bracket Z Z')) ↔ M = 0 := by @@ -288,7 +306,7 @@ def vectorField (Z : GalileanAlgebra) (y : EvolutionSpace N) : EvolutionSpace N def linearPart (Z : GalileanAlgebra) (w : EvolutionSpace N) : EvolutionSpace N := ⟨0, fun j => Z.ω ⨯₃ w.r j + w.t • Z.β, fun j => Z.ω ⨯₃ w.v j⟩ -/-- Souriau's bracket is the bracket of the vector fields in the convention (6.12 b), (11.22 a): +/-- Souriau's bracket is the bracket of the vector fields in the convention (6.12 b), (2.45): `[Z, Z']_V = DZ'_V(Z_V) - DZ_V(Z'_V)`. -/ lemma vectorField_bracket (Z Z' : GalileanAlgebra) (y : EvolutionSpace N) : vectorField (bracket Z Z') y @@ -329,7 +347,8 @@ lemma lagrangeForm_motion (m : Fin N → ℝ) (y δy : EvolutionSpace N) : -/ -/-- The moment of `N` free material points ((12.125) for one point, (12.135) for `N` points): +/-- The moment of `N` free material points ((12.125) for one point of unit mass; (12.135) for `N` +points, with `E_j = 0` in its last line and the additive constant of `E` chosen to be `0`): `l = Σ m_j r_j × v_j`, `g = Σ m_j (r_j - v_j t)`, `p = Σ m_j v_j`, `E = ½ Σ m_j ‖v_j‖²`. -/ def moment (m : Fin N → ℝ) (y : EvolutionSpace N) : GalileanTorsor := ⟨∑ j, m j • (y.r j ⨯₃ y.v j), ∑ j, m j • (y.r j - y.t • y.v j), ∑ j, m j • y.v j, @@ -413,7 +432,8 @@ lemma moment_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : /-- The total mass `m = Σ_j m_j` (12.135). -/ def totalMass (m : Fin N → ℝ) : ℝ := ∑ j, m j -/-- The centre of gravity `R = (Σ_j m_j r_j) / m` of (12.141). -/ +/-- The centre of gravity `R = (Σ_j m_j r_j) / m`, named in (12.141) (the formula is the usual one, +not printed there); for `m = 0` the value is `0`, by the convention `0⁻¹ = 0`. -/ def centerOfMass (m : Fin N → ℝ) (y : EvolutionSpace N) : ℝ³ := (totalMass m)⁻¹ • ∑ j, m j • y.r j @@ -445,8 +465,9 @@ lemma moment_g (m : Fin N → ℝ) (hM : totalMass m ≠ 0) (y : EvolutionSpace congr! with i field_simp [hM] -/-- (12.141) for free material points: along a free motion the centre of gravity moves uniformly -with velocity `p / m`. -/ +/-- Along a free motion the centre of gravity moves uniformly with velocity `p / m` (p. 153, after +(12.141)). Souriau deduces this for any isolated system from the constancy of `g` and `p`; here it +is proved directly from the free motion. For `m = 0` both sides are `0`. -/ lemma centerOfMass_motion (m : Fin N → ℝ) (y : EvolutionSpace N) (s : ℝ) : centerOfMass m (motion y s) = centerOfMass m y + s • ((totalMass m)⁻¹ • (moment m y).p) := by simp [centerOfMass, motion, smul_smul] From ae21c037c3869b77d4764d5e4ae388904fdd0ab0 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 25 Sep 2026 11:30:24 +0200 Subject: [PATCH 5/6] refactor(PhyslibAlpha/ClassicalMechanics): move the moment map files into MomentMap/ As agreed in the review of this PR: MomentMap.lean becomes MomentMap/Basic.lean, MomentMapCohomology.lean becomes MomentMap/Cohomology.lean, and GalileanMass.lean moves to MomentMap/GalileanMass.lean. Only the imports and two docstring references to the module name change. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 6 +++--- .../{MomentMap.lean => MomentMap/Basic.lean} | 0 .../{MomentMapCohomology.lean => MomentMap/Cohomology.lean} | 4 ++-- .../ClassicalMechanics/{ => MomentMap}/GalileanMass.lean | 6 +++--- 4 files changed, 8 insertions(+), 8 deletions(-) rename PhyslibAlpha/ClassicalMechanics/{MomentMap.lean => MomentMap/Basic.lean} (100%) rename PhyslibAlpha/ClassicalMechanics/{MomentMapCohomology.lean => MomentMap/Cohomology.lean} (99%) rename PhyslibAlpha/ClassicalMechanics/{ => MomentMap}/GalileanMass.lean (99%) diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index c3a5ad605..4eb6c1447 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -27,9 +27,9 @@ 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.GalileanMass -public import PhyslibAlpha.ClassicalMechanics.MomentMap -public import PhyslibAlpha.ClassicalMechanics.MomentMapCohomology +public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic +public import PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology +public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass 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/Basic.lean similarity index 100% rename from PhyslibAlpha/ClassicalMechanics/MomentMap.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/Basic.lean diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/Cohomology.lean similarity index 99% rename from PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/Cohomology.lean index f8c53914c..34c0f3dba 100644 --- a/PhyslibAlpha/ClassicalMechanics/MomentMapCohomology.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/Cohomology.lean @@ -5,7 +5,7 @@ Authors: Philippe Kevorkian -/ module -public import PhyslibAlpha.ClassicalMechanics.MomentMap +public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic public import Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree /-! @@ -25,7 +25,7 @@ group `Sp(E) ⋉ E` of a real symplectic vector space `E`, acting by `x ↦ B x `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 +`PhyslibAlpha.ClassicalMechanics.MomentMap.Basic`, 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. diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean similarity index 99% rename from PhyslibAlpha/ClassicalMechanics/GalileanMass.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean index cd848a8f5..50baaccfa 100644 --- a/PhyslibAlpha/ClassicalMechanics/GalileanMass.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean @@ -57,9 +57,9 @@ What is not formalised here: uniqueness of the moment up to a constant (the constant in `E` is a choice); - the evolution space is presymplectic, not symplectic (p. 148, (12.114)); `EvolutionSpace.lagrangeForm_motion` shows that `σ` is degenerate, and `σ` depends on the point - `y` through the velocities. The setting of `PhyslibAlpha.ClassicalMechanics.MomentMap` (a constant - non-degenerate form on a vector space) therefore does not apply; the moment and the cocycle are - computed explicitly. + `y` through the velocities. The setting of `PhyslibAlpha.ClassicalMechanics.MomentMap.Basic` + (a constant non-degenerate form on a vector space) therefore does not apply; the moment and the + cocycle are computed explicitly. ## ii. Key results From 1e6c267fe1063e49ecea4b648a3bbca93b0bb61e Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 25 Sep 2026 13:45:07 +0200 Subject: [PATCH 6/6] refactor(PhyslibAlpha/ClassicalMechanics): move GalileanMassCocycle.lean into MomentMap/ Next to GalileanMass.lean, as agreed in the review of #1684. Only the import line in PhyslibAlpha.lean and two docstring references to module names change. Co-Authored-By: Claude Opus 5.5 --- PhyslibAlpha.lean | 2 +- .../{ => MomentMap}/GalileanMassCocycle.lean | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) rename PhyslibAlpha/ClassicalMechanics/{ => MomentMap}/GalileanMassCocycle.lean (99%) diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index f071fe9be..90cdd3742 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -27,10 +27,10 @@ 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.GalileanMassCocycle public import PhyslibAlpha.ClassicalMechanics.MomentMap.Basic public import PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass +public import PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMassCocycle public import PhyslibAlpha.ClassicalMechanics.NortonDome.Basic public import PhyslibAlpha.ClassicalMechanics.NortonDome.Determinism public import PhyslibAlpha.ClassicalMechanics.NortonDome.NewtonianSystem diff --git a/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean similarity index 99% rename from PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean rename to PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean index 3cbe77bd4..ea7559d5c 100644 --- a/PhyslibAlpha/ClassicalMechanics/GalileanMassCocycle.lean +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean @@ -18,9 +18,9 @@ public import Mathlib.Analysis.Calculus.Deriv.Prod ## i. Overview -This file is the group level of `PhyslibAlpha.ClassicalMechanics.GalileanMass`, which treats -chapter 12 of Souriau's Structure des systèmes dynamiques (Dunod 1970) at the level of the Lie -algebra. The group is Physlib's `GalileanGroup 3` (`Physlib.SpaceAndTime.GalileanGroup.Basic`), +This file is the group level of `PhyslibAlpha.ClassicalMechanics.MomentMap.GalileanMass`, which +treats chapter 12 of Souriau's Structure des systèmes dynamiques (Dunod 1970) at the level of the +Lie algebra. The group is Physlib's `GalileanGroup 3` (`Physlib.SpaceAndTime.GalileanGroup.Basic`), `a = (R, b, c, e)` (rotation, velocity, space translation, time translation), whose action `(t, x) ↦ (t + e, R x + b t + c)` is Souriau's (12.76); `EvolutionSpace.smul_time_position` shows that the action on the evolution space below is that action on each material point. @@ -45,7 +45,7 @@ in chapter 12; they are computed here from (6.24), (6.28) and (11.15). The cohomology vocabulary is Mathlib's: `θ₀` is a `groupCohomology.IsCocycle₁` for the coadjoint action, which is (11.19 ♡), and "the class is not zero" is `¬ groupCohomology.IsCoboundary₁`, -which is (11.19 ◇). As in `PhyslibAlpha.ClassicalMechanics.MomentMapCohomology`, Souriau's +which is (11.19 ◇). As in `PhyslibAlpha.ClassicalMechanics.MomentMap.Cohomology`, Souriau's requirement that a cocycle be differentiable is not part of these definitions. This does not weaken the non-coboundary statements: a coboundary `a ↦ a • μ₀ - μ₀` of (11.19 ◇) is polynomial in the entries of `a`, hence differentiable.