diff --git a/PhyslibAlpha.lean b/PhyslibAlpha.lean index c170fca38..90cdd3742 100644 --- a/PhyslibAlpha.lean +++ b/PhyslibAlpha.lean @@ -27,8 +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.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.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/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/MomentMap/GalileanMass.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean new file mode 100644 index 000000000..50baaccfa --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMass.lean @@ -0,0 +1,481 @@ +/- +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 +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`; 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 (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 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 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.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 + +- `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.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, 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] + +-/ + +@[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), (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⟩ + +/-- 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 `μ₀` ((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 + 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), (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 + = 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 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, + (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`, 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 + +/-- (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] + +/-- 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] + 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 diff --git a/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean new file mode 100644 index 000000000..ea7559d5c --- /dev/null +++ b/PhyslibAlpha/ClassicalMechanics/MomentMap/GalileanMassCocycle.lean @@ -0,0 +1,838 @@ +/- +Copyright (c) 2026 Philippe Kevorkian. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Philippe Kevorkian +-/ +module + +public import PhyslibAlpha.ClassicalMechanics.MomentMap.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.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. + +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, 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 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.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. + +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⁻¹` (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); +- (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); `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 + +- 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.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 + +* 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, in components: with +`ω* = det R • R ω`, `a • (ω, β, γ, ε) = (ω*, R β - ω* × b, R γ + ε b - e R β - ω* × (c - e b), ε)`. +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, + 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 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 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 + +/-! + +## 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): `θ₀` 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 => ?_ + 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 + +/-- 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⟩ + exact eq_zero_of_smul_massCocycle_boost M μ₀ (h _) + · rintro rfl + exact ⟨0, fun a => by simp⟩ + +/-- `θ₀` 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) 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 => ?_ + 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.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₁ + (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 + +/-- (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 + +/-! + +## 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