From 8f9d99b4e06a0e27e3622fb5a7679e3be0898565 Mon Sep 17 00:00:00 2001 From: George Date: Wed, 20 May 2026 21:54:57 +0100 Subject: [PATCH 1/2] feat(SpaceAndTime): add basic GalileanGroup type and coordinate action MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit First-step API for Galilean transformations: the `GalileanGroup d` structure bundling rotation/velocity/space-translation/time-translation, four pure constructors, `id`, `Inhabited`, and the action on `Time × Space d` with core simp lemmas. Group/Lie/Newtonian-action structure is intentionally deferred to follow-up PRs. --- Physlib.lean | 1 + Physlib/SpaceAndTime/GalileanGroup/Basic.lean | 352 ++++++++++++++++++ 2 files changed, 353 insertions(+) create mode 100644 Physlib/SpaceAndTime/GalileanGroup/Basic.lean diff --git a/Physlib.lean b/Physlib.lean index 13a94d958..906721d90 100644 --- a/Physlib.lean +++ b/Physlib.lean @@ -348,6 +348,7 @@ public import Physlib.Relativity.Tensors.RealTensor.Velocity.Basic public import Physlib.Relativity.Tensors.TensorSpecies.Basic public import Physlib.Relativity.Tensors.Tensorial public import Physlib.Relativity.Tensors.UnitTensor +public import Physlib.SpaceAndTime.GalileanGroup.Basic public import Physlib.SpaceAndTime.Space.Basic public import Physlib.SpaceAndTime.Space.ConstantSliceDist public import Physlib.SpaceAndTime.Space.CrossProduct diff --git a/Physlib/SpaceAndTime/GalileanGroup/Basic.lean b/Physlib/SpaceAndTime/GalileanGroup/Basic.lean new file mode 100644 index 000000000..724f45ddf --- /dev/null +++ b/Physlib/SpaceAndTime/GalileanGroup/Basic.lean @@ -0,0 +1,352 @@ +/- +Copyright (c) 2026 Zuo Zhidong. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Zuo Zhidong +-/ +module + +public import Mathlib.LinearAlgebra.UnitaryGroup +public import Physlib.SpaceAndTime.Space.Basic +public import Physlib.SpaceAndTime.Time.Basic +/-! +# The Galilean group + +## i. Overview + +In this module we define the type `GalileanGroup d`, whose elements are +Galilean transformations in `d` spatial dimensions. A Galilean transformation +is a kinematic symmetry of non-relativistic spacetime, built from four +independent pieces: + +* a spatial rotation (or reflection) `R ∈ O(d)`, +* a boost velocity `v` (the relative velocity between two inertial frames), +* a spatial translation `a`, +* a time translation `b`. + +On coordinates it acts as +``` +t' = t + b +x' = R x + v t + a +``` +so the action on `Time × Space d` reads +`(t, x) ↦ (t + b, R x + v t + a)`. + +This file is the **first-step** API: it provides only the data type, four +"pure" constructors, the identity, and the coordinate action together with +its core `simp` lemmas. Subsequent PRs will add the group law, the inverse, +the smooth/Lie-group structure, subgroup inclusions, and actions on fields. +The current API is designed so those additions are non-breaking. + +## ii. Key results + +- `GalileanGroup` : The type of Galilean transformations in `d` spatial + dimensions. +- `GalileanGroup.apply` : The action of a Galilean transformation on a + point `(t, x) : Time × Space d`. +- `GalileanGroup.pureRotation`, `pureBoost`, `pureSpaceTranslation`, + `pureTimeTranslation` : Smart constructors for the four kinematic + building blocks. +- `GalileanGroup.id` : The identity Galilean transformation. + +## iii. Table of contents + +- A. The type `GalileanGroup` +- B. The identity and basic constructors + - B.1. The identity + - B.2. Pure rotations + - B.3. Pure boosts + - B.4. Pure spatial translations + - B.5. Pure time translations +- C. The action on `Time × Space d` + - C.1. The coordinate formulas + - C.2. Action of the identity + - C.3. Action of pure rotations + - C.4. Action of pure boosts + - C.5. Action of pure spatial translations + - C.6. Action of pure time translations + +## iv. References + +- *Classical Mechanics*, Goldstein, Poole, Safko — §1.7 (Galilean + transformations as a kinematic symmetry). +- *Foundations of Mechanics*, Abraham–Marsden — Ch. 4 (the Galilean group + as the symmetry group of Newtonian spacetime). + +-/ + +@[expose] public section + +noncomputable section + +/-! + +## A. The type `GalileanGroup` + +-/ + +/-- A `Galilean transformation` in `d` spatial dimensions. It bundles +the four independent pieces of data +`(rotation, boost velocity, spatial translation, time translation)`, and +acts on `(t, x) : Time × Space d` by +`(t, x) ↦ (t + b, R x + v t + a)`. + +The default value of `d` is `3`, so `GalileanGroup = GalileanGroup 3`. -/ +structure GalileanGroup (d : ℕ := 3) where + /-- The spatial rotation (or reflection): an element of the full + orthogonal group `O(d)`. Using `O(d)` rather than `SO(d)` so that + parity transformations are included in the first-version API. -/ + rotation : Matrix.orthogonalGroup (Fin d) ℝ + /-- The boost velocity (the relative velocity between two inertial + frames). -/ + velocity : EuclideanSpace ℝ (Fin d) + /-- The spatial translation. -/ + spaceTranslation : EuclideanSpace ℝ (Fin d) + /-- The time translation. -/ + timeTranslation : Time + +namespace GalileanGroup + +variable {d : ℕ} + +/-! + +## B. The identity and basic constructors + +-/ + +/-! + +### B.1. The identity + +-/ + +/-- The identity Galilean transformation: no rotation, no boost, +no spatial translation, no time translation. -/ +def id : GalileanGroup d := + ⟨1, 0, 0, 0⟩ + +instance : Inhabited (GalileanGroup d) := ⟨id⟩ + +@[simp] +lemma id_rotation : (id : GalileanGroup d).rotation = 1 := rfl + +@[simp] +lemma id_velocity : (id : GalileanGroup d).velocity = 0 := rfl + +@[simp] +lemma id_spaceTranslation : (id : GalileanGroup d).spaceTranslation = 0 := rfl + +@[simp] +lemma id_timeTranslation : (id : GalileanGroup d).timeTranslation = 0 := rfl + +/-! + +### B.2. Pure rotations + +-/ + +/-- The Galilean transformation that is a pure rotation by `R`. -/ +def pureRotation (R : Matrix.orthogonalGroup (Fin d) ℝ) : GalileanGroup d := + ⟨R, 0, 0, 0⟩ + +@[simp] +lemma pureRotation_rotation (R : Matrix.orthogonalGroup (Fin d) ℝ) : + (pureRotation R).rotation = R := rfl + +@[simp] +lemma pureRotation_velocity (R : Matrix.orthogonalGroup (Fin d) ℝ) : + (pureRotation R).velocity = 0 := rfl + +@[simp] +lemma pureRotation_spaceTranslation (R : Matrix.orthogonalGroup (Fin d) ℝ) : + (pureRotation R).spaceTranslation = 0 := rfl + +@[simp] +lemma pureRotation_timeTranslation (R : Matrix.orthogonalGroup (Fin d) ℝ) : + (pureRotation R).timeTranslation = 0 := rfl + +/-! + +### B.3. Pure boosts + +-/ + +/-- The Galilean transformation that is a pure boost of velocity `v`. -/ +def pureBoost (v : EuclideanSpace ℝ (Fin d)) : GalileanGroup d := + ⟨1, v, 0, 0⟩ + +@[simp] +lemma pureBoost_rotation (v : EuclideanSpace ℝ (Fin d)) : + (pureBoost v).rotation = 1 := rfl + +@[simp] +lemma pureBoost_velocity (v : EuclideanSpace ℝ (Fin d)) : + (pureBoost v).velocity = v := rfl + +@[simp] +lemma pureBoost_spaceTranslation (v : EuclideanSpace ℝ (Fin d)) : + (pureBoost v).spaceTranslation = 0 := rfl + +@[simp] +lemma pureBoost_timeTranslation (v : EuclideanSpace ℝ (Fin d)) : + (pureBoost v).timeTranslation = 0 := rfl + +/-! + +### B.4. Pure spatial translations + +-/ + +/-- The Galilean transformation that is a pure spatial translation by `a`. -/ +def pureSpaceTranslation (a : EuclideanSpace ℝ (Fin d)) : GalileanGroup d := + ⟨1, 0, a, 0⟩ + +@[simp] +lemma pureSpaceTranslation_rotation (a : EuclideanSpace ℝ (Fin d)) : + (pureSpaceTranslation a).rotation = 1 := rfl + +@[simp] +lemma pureSpaceTranslation_velocity (a : EuclideanSpace ℝ (Fin d)) : + (pureSpaceTranslation a).velocity = 0 := rfl + +@[simp] +lemma pureSpaceTranslation_spaceTranslation (a : EuclideanSpace ℝ (Fin d)) : + (pureSpaceTranslation a).spaceTranslation = a := rfl + +@[simp] +lemma pureSpaceTranslation_timeTranslation (a : EuclideanSpace ℝ (Fin d)) : + (pureSpaceTranslation a).timeTranslation = 0 := rfl + +/-! + +### B.5. Pure time translations + +-/ + +/-- The Galilean transformation that is a pure time translation by `b`. -/ +def pureTimeTranslation (b : Time) : GalileanGroup d := + ⟨1, 0, 0, b⟩ + +@[simp] +lemma pureTimeTranslation_rotation (b : Time) : + (pureTimeTranslation (d := d) b).rotation = 1 := rfl + +@[simp] +lemma pureTimeTranslation_velocity (b : Time) : + (pureTimeTranslation (d := d) b).velocity = 0 := rfl + +@[simp] +lemma pureTimeTranslation_spaceTranslation (b : Time) : + (pureTimeTranslation (d := d) b).spaceTranslation = 0 := rfl + +@[simp] +lemma pureTimeTranslation_timeTranslation (b : Time) : + (pureTimeTranslation (d := d) b).timeTranslation = b := rfl + +/-! + +## C. The action on `Time × Space d` + +-/ + +/-- The action of a Galilean transformation `g` on a point `(t, x)` in +`Time × Space d`: +``` +(t, x) ↦ (t + b, R x + v t + a) +``` +where `R, v, a, b` are the four pieces of data of `g`. -/ +def apply (g : GalileanGroup d) (tx : Time × Space d) : Time × Space d := + (tx.1 + g.timeTranslation, + ⟨fun i => g.rotation.1.mulVec tx.2.val i + + tx.1.val * g.velocity i + + g.spaceTranslation i⟩) + +/-! + +### C.1. The coordinate formulas + +-/ + +@[simp] +lemma apply_fst (g : GalileanGroup d) (t : Time) (x : Space d) : + (g.apply (t, x)).1 = t + g.timeTranslation := rfl + +@[simp] +lemma apply_snd_apply (g : GalileanGroup d) (t : Time) (x : Space d) (i : Fin d) : + (g.apply (t, x)).2 i = + g.rotation.1.mulVec x.val i + t.val * g.velocity i + g.spaceTranslation i := + rfl + +/-! + +### C.2. Action of the identity + +-/ + +@[simp] +lemma id_apply (tx : Time × Space d) : id.apply tx = tx := by + obtain ⟨t, x⟩ := tx + ext + · simp [apply] + · simp [apply, Matrix.one_mulVec] + +/-! + +### C.3. Action of pure rotations + +-/ + +@[simp] +lemma pureRotation_apply (R : Matrix.orthogonalGroup (Fin d) ℝ) + (t : Time) (x : Space d) : + (pureRotation R).apply (t, x) = (t, ⟨fun i => R.1.mulVec x.val i⟩) := by + ext + · simp [apply] + · simp [apply] + +/-! + +### C.4. Action of pure boosts + +-/ + +@[simp] +lemma pureBoost_apply (v : EuclideanSpace ℝ (Fin d)) + (t : Time) (x : Space d) : + (pureBoost v).apply (t, x) = + (t, ⟨fun i => x i + t.val * v i⟩) := by + ext + · simp [apply] + · simp [apply, Matrix.one_mulVec] + +/-! + +### C.5. Action of pure spatial translations + +-/ + +@[simp] +lemma pureSpaceTranslation_apply (a : EuclideanSpace ℝ (Fin d)) + (t : Time) (x : Space d) : + (pureSpaceTranslation a).apply (t, x) = + (t, ⟨fun i => x i + a i⟩) := by + ext + · simp [apply] + · simp [apply, Matrix.one_mulVec] + +/-! + +### C.6. Action of pure time translations + +-/ + +@[simp] +lemma pureTimeTranslation_apply (b : Time) (t : Time) (x : Space d) : + (pureTimeTranslation b).apply (t, x) = (t + b, x) := by + ext + · simp [apply] + · simp [apply, Matrix.one_mulVec] + +end GalileanGroup + +end From 7d5fe0445d251600943183987f4be3d84ff723af Mon Sep 17 00:00:00 2001 From: George Date: Wed, 20 May 2026 22:21:03 +0100 Subject: [PATCH 2/2] docs(SpaceAndTime/GalileanGroup): clarify conventions per reviewer feedback Three documentation improvements and one small rename, in response to a physicist-style review of the first-step GalileanGroup API: - Add an explicit active-vs-passive sign-convention note in the module header. A pure boost by v sends a point x to x + v t (the point is dragged along the velocity). The passive change-of-frame interpretation would use the opposite sign x - v t. - Explain in both the module header and the structure docstring that the fields velocity and spaceTranslation are spatial vectors of type EuclideanSpace R (Fin d), while Space d is the type of spatial positions. This makes it clear to a physicist user why the constructors take Euclidean vectors rather than Space d points. - Update the docstring of pureRotation to make explicit that the rotation field has type Matrix.orthogonalGroup (Fin d) R, so R may be a proper rotation OR a reflection. The function name pureRotation follows the common physics shorthand; restricting to SO(d) is left to a follow-up PR. - Add a per-constructor one-line summary of the action (e.g. "It sends (t, x) to (t, x + v t)") in pureRotation, pureBoost, pureSpaceTranslation, pureTimeTranslation. - Rename apply_snd_apply to apply_snd_coord. The original name read as "apply second apply", which obscured that the lemma states the closed form of the i-th spatial coordinate of g.apply (t, x). No definitional changes; all proofs still discharged by simp/rfl. Build verified. --- Physlib/SpaceAndTime/GalileanGroup/Basic.lean | 42 +++++++++++++++---- 1 file changed, 35 insertions(+), 7 deletions(-) diff --git a/Physlib/SpaceAndTime/GalileanGroup/Basic.lean b/Physlib/SpaceAndTime/GalileanGroup/Basic.lean index 724f45ddf..9a86d7107 100644 --- a/Physlib/SpaceAndTime/GalileanGroup/Basic.lean +++ b/Physlib/SpaceAndTime/GalileanGroup/Basic.lean @@ -31,6 +31,18 @@ x' = R x + v t + a so the action on `Time × Space d` reads `(t, x) ↦ (t + b, R x + v t + a)`. +**Sign convention.** This is the *active* convention: a pure boost by `v` sends +`x` to `x + v t` (the point itself is dragged along the velocity). The *passive* +change-of-frame interpretation, where one re-expresses the same point in a frame +moving with velocity `v`, would use the opposite sign — `x' = x - v t`. + +**Spatial positions vs. spatial vectors.** The type `Space d` represents spatial +positions, while `velocity` and `spaceTranslation` are spatial vectors, represented +by `EuclideanSpace ℝ (Fin d)`. This file works at the coordinate level: the formula +`R x + v t + a` is implemented using the coordinate representation of `x`. The +vector terms `v t` and `a` should be read as displacements added to the transformed +spatial position. + This file is the **first-step** API: it provides only the data type, four "pure" constructors, the identity, and the coordinate action together with its core `simp` lemmas. Subsequent PRs will add the group law, the inverse, @@ -88,7 +100,12 @@ noncomputable section the four independent pieces of data `(rotation, boost velocity, spatial translation, time translation)`, and acts on `(t, x) : Time × Space d` by -`(t, x) ↦ (t + b, R x + v t + a)`. +`(t, x) ↦ (t + b, R x + v t + a)` in the active convention. + +The fields `velocity` and `spaceTranslation` are spatial *vectors* and live in +`EuclideanSpace ℝ (Fin d)`, whereas `Space d` is the type of spatial *positions*. +In this first-step API, the action is implemented in coordinates: the transformed +spatial point has coordinates `R x + v t + a`. The default value of `d` is `3`, so `GalileanGroup = GalileanGroup 3`. -/ structure GalileanGroup (d : ℕ := 3) where @@ -145,7 +162,10 @@ lemma id_timeTranslation : (id : GalileanGroup d).timeTranslation = 0 := rfl -/ -/-- The Galilean transformation that is a pure rotation by `R`. -/ +/-- The Galilean transformation that is a pure orthogonal spatial transformation `R`. + +It sends `(t, x)` to `(t, R x)`. Since `R` lies in `O(d)`, this includes both +ordinary proper rotations and reflections. -/ def pureRotation (R : Matrix.orthogonalGroup (Fin d) ℝ) : GalileanGroup d := ⟨R, 0, 0, 0⟩ @@ -171,7 +191,10 @@ lemma pureRotation_timeTranslation (R : Matrix.orthogonalGroup (Fin d) ℝ) : -/ -/-- The Galilean transformation that is a pure boost of velocity `v`. -/ +/-- The Galilean transformation that is a pure boost of velocity `v`. + +With the active convention used in this file, it sends `(t, x)` to +`(t, x + v t)`. -/ def pureBoost (v : EuclideanSpace ℝ (Fin d)) : GalileanGroup d := ⟨1, v, 0, 0⟩ @@ -197,7 +220,9 @@ lemma pureBoost_timeTranslation (v : EuclideanSpace ℝ (Fin d)) : -/ -/-- The Galilean transformation that is a pure spatial translation by `a`. -/ +/-- The Galilean transformation that is a pure spatial translation by `a`. + +It sends `(t, x)` to `(t, x + a)`. -/ def pureSpaceTranslation (a : EuclideanSpace ℝ (Fin d)) : GalileanGroup d := ⟨1, 0, a, 0⟩ @@ -223,7 +248,9 @@ lemma pureSpaceTranslation_timeTranslation (a : EuclideanSpace ℝ (Fin d)) : -/ -/-- The Galilean transformation that is a pure time translation by `b`. -/ +/-- The Galilean transformation that is a pure time translation by `b`. + +It sends `(t, x)` to `(t + b, x)`. -/ def pureTimeTranslation (b : Time) : GalileanGroup d := ⟨1, 0, 0, b⟩ @@ -254,7 +281,8 @@ lemma pureTimeTranslation_timeTranslation (b : Time) : ``` (t, x) ↦ (t + b, R x + v t + a) ``` -where `R, v, a, b` are the four pieces of data of `g`. -/ +where `R, v, a, b` are the four pieces of data of `g`. This uses the active +convention for boosts. -/ def apply (g : GalileanGroup d) (tx : Time × Space d) : Time × Space d := (tx.1 + g.timeTranslation, ⟨fun i => g.rotation.1.mulVec tx.2.val i @@ -272,7 +300,7 @@ lemma apply_fst (g : GalileanGroup d) (t : Time) (x : Space d) : (g.apply (t, x)).1 = t + g.timeTranslation := rfl @[simp] -lemma apply_snd_apply (g : GalileanGroup d) (t : Time) (x : Space d) (i : Fin d) : +lemma apply_snd_coord (g : GalileanGroup d) (t : Time) (x : Space d) (i : Fin d) : (g.apply (t, x)).2 i = g.rotation.1.mulVec x.val i + t.val * g.velocity i + g.spaceTranslation i := rfl