Physlib.SpaceAndTime.GalileanGroup.Basic

Imports

/-
Copyright (c) 2026 Rob Sneiderman. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Rob Sneiderman
-/
module

public import Physlib.SpaceAndTime.Space.EuclideanGroup.Basic
public import Physlib.SpaceAndTime.Space.Origin
public import Physlib.SpaceAndTime.Time.Basic

The Galilean group

This file defines Galilean transformations in d spatial dimensions, together with their group law and their action on Time × Space d.

An element consists of a spatial orthogonal transformation R, a boost velocity v, a spatial translation a, and a time translation b. We use the active convention (t, x) ↦ (t + b, R x + v t + a).

@[expose] public section

A Galilean transformation in d spatial dimensions. The fields are, in order, the spatial orthogonal part, boost velocity, spatial translation, and time translation.

The spatial orthogonal part.

The boost velocity.

The spatial translation.

The time translation.

              @[ext]
structure GalileanGroup (d : ℕ := 3) where  rotation : Matrix.orthogonalGroup (Fin d) ℝ  velocity : EuclideanSpace ℝ (Fin d)  spaceTranslation : EuclideanSpace ℝ (Fin d)  timeTranslation : Time

A. Basic support lemmas



lemma orthogonal_smul_smul (R : Matrix.orthogonalGroup (Fin d) ℝ) (c : ℝ)
    (v : EuclideanSpace ℝ (Fin d)) :
    R • (c • v) = c • (R • v) := byd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)c:ℝv:EuclideanSpace ℝ (Fin d)⊢ R • c • v = c • R • v
  change (DistribMulAction.toLinearEquiv ℝ (EuclideanSpace ℝ (Fin d)) R) (c • v) =
    c • ((DistribMulAction.toLinearEquiv ℝ (EuclideanSpace ℝ (Fin d)) R) v)d:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)c:ℝv:EuclideanSpace ℝ (Fin d)⊢ (DistribMulAction.toLinearEquiv ℝ (EuclideanSpace ℝ (Fin d)) R) (c • v) =
  c • (DistribMulAction.toLinearEquiv ℝ (EuclideanSpace ℝ (Fin d)) R) v
  rw [map_smuld:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)c:ℝv:EuclideanSpace ℝ (Fin d)⊢ c • (DistribMulAction.toLinearEquiv ℝ (EuclideanSpace ℝ (Fin d)) R) v =
  c • (DistribMulAction.toLinearEquiv ℝ (EuclideanSpace ℝ (Fin d)) R) vAll goals completed! 🐙]All goals completed! 🐙

B. Group operations

The identity Galilean transformation.

instance : One (GalileanGroup d) where
  one := ⟨1, 0, 0, 0⟩

              @[simp]
lemma one_rotation : (1 : GalileanGroup d).rotation = 1 := rfl@[simp]
lemma one_velocity : (1 : GalileanGroup d).velocity = 0 := rfl@[simp]
lemma one_spaceTranslation : (1 : GalileanGroup d).spaceTranslation = 0 := rfl@[simp]
lemma one_timeTranslation : (1 : GalileanGroup d).timeTranslation = 0 := rfl

The product whose action is composition: (g * h) • tx = g • h • tx.

instance : Mul (GalileanGroup d) where
  mul g h :=
    ⟨g.rotation * h.rotation,
      g.rotation • h.velocity + g.velocity,
      g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity,
      g.timeTranslation + h.timeTranslation⟩

              @[simp]
lemma mul_rotation (g h : GalileanGroup d) :
    (g * h).rotation = g.rotation * h.rotation := rfl@[simp]
lemma mul_velocity (g h : GalileanGroup d) :
    (g * h).velocity = g.rotation • h.velocity + g.velocity := rfl@[simp]
lemma mul_spaceTranslation (g h : GalileanGroup d) :
    (g * h).spaceTranslation =
      g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity :=
  rfl@[simp]
lemma mul_timeTranslation (g h : GalileanGroup d) :
    (g * h).timeTranslation = g.timeTranslation + h.timeTranslation := rfl

The inverse Galilean transformation.

instance : Inv (GalileanGroup d) where
  inv g :=
    ⟨g.rotation⁻¹,
      -(g.rotation⁻¹ • g.velocity),
      -(g.rotation⁻¹ • g.spaceTranslation) + g.timeTranslation.val • (g.rotation⁻¹ • g.velocity),
      -g.timeTranslation⟩

@[simp]
lemma inv_rotation (g : GalileanGroup d) :
    g⁻¹.rotation = g.rotation⁻¹ := rfl

The inverse boost velocity formula.

@[simp]
lemma inv_velocity (g : GalileanGroup d) :
    g⁻¹.velocity = -(g.rotation⁻¹ • g.velocity) := rfl

@[simp]
lemma inv_spaceTranslation (g : GalileanGroup d) :
    g⁻¹.spaceTranslation =
      -(g.rotation⁻¹ • g.spaceTranslation) +
        g.timeTranslation.val • (g.rotation⁻¹ • g.velocity) := rfl

@[simp]
lemma inv_timeTranslation (g : GalileanGroup d) :
    g⁻¹.timeTranslation = -g.timeTranslation := rfl

The Galilean transformations form a group under composition.


instance : Group (GalileanGroup d) where
  mul_assoc g h k := byd:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g * h * k = g * (h * k)
    refine GalileanGroup.ext ?_ ?_ ?_ ?_refine_1d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).rotation = (g * (h * k)).rotationrefine_2d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).velocity = (g * (h * k)).velocityrefine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).spaceTranslation = (g * (h * k)).spaceTranslationrefine_4d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).timeTranslation = (g * (h * k)).timeTranslation
    ·refine_1d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).rotation = (g * (h * k)).rotation simpa using (mul_assoc g.rotation h.rotation k.rotation)All goals completed! 🐙
    ·refine_2d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).velocity = (g * (h * k)).velocity simp [mul_smul, smul_add, add_assoc]All goals completed! 🐙
    ·refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).spaceTranslation = (g * (h * k)).spaceTranslation simp only [mul_spaceTranslation, mul_rotation, mul_velocity, mul_timeTranslation,
        Time.add_val]refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      (g.rotation * h.rotation) • k.spaceTranslation +
    k.timeTranslation.val • (g.rotation • h.velocity + g.velocity) =
  g.spaceTranslation +
      g.rotation • (h.spaceTranslation + h.rotation • k.spaceTranslation + k.timeTranslation.val • h.velocity) +
    (h.timeTranslation.val + k.timeTranslation.val) • g.velocity
      rw [mul_smul,refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    k.timeTranslation.val • (g.rotation • h.velocity + g.velocity) =
  g.spaceTranslation +
      g.rotation • (h.spaceTranslation + h.rotation • k.spaceTranslation + k.timeTranslation.val • h.velocity) +
    (h.timeTranslation.val + k.timeTranslation.val) • g.velocityrefine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity) smul_add,refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      g.rotation • (h.spaceTranslation + h.rotation • k.spaceTranslation + k.timeTranslation.val • h.velocity) +
    (h.timeTranslation.val + k.timeTranslation.val) • g.velocityrefine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity) smul_add,refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • (h.spaceTranslation + h.rotation • k.spaceTranslation) +
        g.rotation • k.timeTranslation.val • h.velocity) +
    (h.timeTranslation.val + k.timeTranslation.val) • g.velocityrefine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity) add_smul,refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • (h.spaceTranslation + h.rotation • k.spaceTranslation) +
        g.rotation • k.timeTranslation.val • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity)refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity) smul_add,refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        g.rotation • k.timeTranslation.val • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity)refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity) orthogonal_smul_smulrefine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity)refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity)]refine_3d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ g.spaceTranslation + g.rotation • h.spaceTranslation + h.timeTranslation.val • g.velocity +
      g.rotation • h.rotation • k.spaceTranslation +
    (k.timeTranslation.val • g.rotation • h.velocity + k.timeTranslation.val • g.velocity) =
  g.spaceTranslation +
      (g.rotation • h.spaceTranslation + g.rotation • h.rotation • k.spaceTranslation +
        k.timeTranslation.val • g.rotation • h.velocity) +
    (h.timeTranslation.val • g.velocity + k.timeTranslation.val • g.velocity)
      abelAll goals completed! 🐙
    ·refine_4d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).timeTranslation = (g * (h * k)).timeTranslation extrefine_4d:ℕg:GalileanGroup dh:GalileanGroup dk:GalileanGroup d⊢ (g * h * k).timeTranslation.val = (g * (h * k)).timeTranslation.val
      simp [Time.add_val, add_assoc]All goals completed! 🐙
  one_mul g := byd:ℕg:GalileanGroup d⊢ 1 * g = g
    refine GalileanGroup.ext ?_ ?_ ?_ ?_refine_1d:ℕg:GalileanGroup d⊢ (1 * g).rotation = g.rotationrefine_2d:ℕg:GalileanGroup d⊢ (1 * g).velocity = g.velocityrefine_3d:ℕg:GalileanGroup d⊢ (1 * g).spaceTranslation = g.spaceTranslationrefine_4d:ℕg:GalileanGroup d⊢ (1 * g).timeTranslation = g.timeTranslation
    ·refine_1d:ℕg:GalileanGroup d⊢ (1 * g).rotation = g.rotation simpAll goals completed! 🐙
    ·refine_2d:ℕg:GalileanGroup d⊢ (1 * g).velocity = g.velocity simpAll goals completed! 🐙
    ·refine_3d:ℕg:GalileanGroup d⊢ (1 * g).spaceTranslation = g.spaceTranslation simpAll goals completed! 🐙
    ·refine_4d:ℕg:GalileanGroup d⊢ (1 * g).timeTranslation = g.timeTranslation extrefine_4d:ℕg:GalileanGroup d⊢ (1 * g).timeTranslation.val = g.timeTranslation.val
      simpAll goals completed! 🐙
  mul_one g := byd:ℕg:GalileanGroup d⊢ g * 1 = g
    refine GalileanGroup.ext ?_ ?_ ?_ ?_refine_1d:ℕg:GalileanGroup d⊢ (g * 1).rotation = g.rotationrefine_2d:ℕg:GalileanGroup d⊢ (g * 1).velocity = g.velocityrefine_3d:ℕg:GalileanGroup d⊢ (g * 1).spaceTranslation = g.spaceTranslationrefine_4d:ℕg:GalileanGroup d⊢ (g * 1).timeTranslation = g.timeTranslation
    ·refine_1d:ℕg:GalileanGroup d⊢ (g * 1).rotation = g.rotation simpAll goals completed! 🐙
    ·refine_2d:ℕg:GalileanGroup d⊢ (g * 1).velocity = g.velocity simpAll goals completed! 🐙
    ·refine_3d:ℕg:GalileanGroup d⊢ (g * 1).spaceTranslation = g.spaceTranslation simpAll goals completed! 🐙
    ·refine_4d:ℕg:GalileanGroup d⊢ (g * 1).timeTranslation = g.timeTranslation extrefine_4d:ℕg:GalileanGroup d⊢ (g * 1).timeTranslation.val = g.timeTranslation.val
      simpAll goals completed! 🐙
  inv_mul_cancel g := byd:ℕg:GalileanGroup d⊢ g⁻¹ * g = 1
    refine GalileanGroup.ext ?_ ?_ ?_ ?_refine_1d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).rotation = rotation 1refine_2d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).velocity = velocity 1refine_3d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).spaceTranslation = spaceTranslation 1refine_4d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).timeTranslation = timeTranslation 1
    ·refine_1d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).rotation = rotation 1 simpAll goals completed! 🐙
    ·refine_2d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).velocity = velocity 1 simpAll goals completed! 🐙
    ·refine_3d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).spaceTranslation = spaceTranslation 1 simp [smul_neg, add_comm, add_left_comm]All goals completed! 🐙
    ·refine_4d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).timeTranslation = timeTranslation 1 extrefine_4d:ℕg:GalileanGroup d⊢ (g⁻¹ * g).timeTranslation.val = (timeTranslation 1).val
      simpAll goals completed! 🐙

instance : Inhabited (GalileanGroup d) where
  default := 1

C. Action on time and space

              @[simp]
lemma smul_fst (g : GalileanGroup d) (tx : Time × Space d) :
    (g • tx).1 = tx.1 + g.timeTranslation := rfl@[simp]
lemma smul_snd (g : GalileanGroup d) (tx : Time × Space d) :
    (g • tx).2 = g.actSpace tx.1 tx.2 := rfl@[simp]
lemma smul_mk (g : GalileanGroup d) (t : Time) (x : Space d) :
    g • ((t, x) : Time × Space d) = (t + g.timeTranslation, g.actSpace t x) := rfl@[simp]
lemma actSpace_apply (g : GalileanGroup d) (t : Time) (x : Space d) (i : Fin d) :
    g.actSpace t x i =
      (g.rotation • (x -ᵥ (0 : Space d))) i + t.val * g.velocity i + g.spaceTranslation i := byd:ℕg:GalileanGroup dt:Timex:Space di:Fin d⊢ (g.actSpace t x).val i = (g.rotation • (x -ᵥ 0)).ofLp i + t.val * g.velocity.ofLp i + g.spaceTranslation.ofLp i
  simp [actSpace, Space.vectorToSpace, add_assoc]All goals completed! 🐙

D. Subgroup inclusions

A Euclidean spatial transformation as a Galilean transformation with zero boost and no time translation.

def ofEuclidean (g : EuclideanGroup d) : GalileanGroup d :=
  ⟨g.linear, 0, g.translation, 0⟩

              @[simp]
lemma ofEuclidean_rotation (g : EuclideanGroup d) :
    (ofEuclidean g).rotation = g.linear := rfl@[simp]
lemma ofEuclidean_velocity (g : EuclideanGroup d) :
    (ofEuclidean g).velocity = 0 := rfl@[simp]
lemma ofEuclidean_spaceTranslation (g : EuclideanGroup d) :
    (ofEuclidean g).spaceTranslation = g.translation := rfl@[simp]
lemma ofEuclidean_timeTranslation (g : EuclideanGroup d) :
    (ofEuclidean g).timeTranslation = 0 := rfl

Inclusion of the Euclidean group into the Galilean group.

def euclidean.incl : EuclideanGroup d →* GalileanGroup d where
  toFun := ofEuclidean
  map_one' := rfl
  map_mul' g h := byd:ℕg:EuclideanGroup dh:EuclideanGroup d⊢ ofEuclidean (g * h) = ofEuclidean g * ofEuclidean h
    ext irotationd:ℕg:EuclideanGroup dh:EuclideanGroup di:Fin dj✝:Fin d⊢ ↑(ofEuclidean (g * h)).rotation i j✝ = ↑(ofEuclidean g * ofEuclidean h).rotation i j✝velocityd:ℕg:EuclideanGroup dh:EuclideanGroup di:Fin d⊢ (ofEuclidean (g * h)).velocity.ofLp i = (ofEuclidean g * ofEuclidean h).velocity.ofLp ispaceTranslationd:ℕg:EuclideanGroup dh:EuclideanGroup di:Fin d⊢ (ofEuclidean (g * h)).spaceTranslation.ofLp i = (ofEuclidean g * ofEuclidean h).spaceTranslation.ofLp itimeTranslationd:ℕg:EuclideanGroup dh:EuclideanGroup d⊢ (ofEuclidean (g * h)).timeTranslation.val = (ofEuclidean g * ofEuclidean h).timeTranslation.val <;>rotationd:ℕg:EuclideanGroup dh:EuclideanGroup di:Fin dj✝:Fin d⊢ ↑(ofEuclidean (g * h)).rotation i j✝ = ↑(ofEuclidean g * ofEuclidean h).rotation i j✝velocityd:ℕg:EuclideanGroup dh:EuclideanGroup di:Fin d⊢ (ofEuclidean (g * h)).velocity.ofLp i = (ofEuclidean g * ofEuclidean h).velocity.ofLp ispaceTranslationd:ℕg:EuclideanGroup dh:EuclideanGroup di:Fin d⊢ (ofEuclidean (g * h)).spaceTranslation.ofLp i = (ofEuclidean g * ofEuclidean h).spaceTranslation.ofLp itimeTranslationd:ℕg:EuclideanGroup dh:EuclideanGroup d⊢ (ofEuclidean (g * h)).timeTranslation.val = (ofEuclidean g * ofEuclidean h).timeTranslation.val simp [ofEuclidean]All goals completed! 🐙

A pure orthogonal spatial transformation as a Galilean transformation.

def ofOrthogonal (R : Matrix.orthogonalGroup (Fin d) ℝ) : GalileanGroup d :=
  ⟨R, 0, 0, 0⟩

              @[simp]
lemma ofOrthogonal_rotation (R : Matrix.orthogonalGroup (Fin d) ℝ) :
    (ofOrthogonal R).rotation = R := rfl@[simp]
lemma ofOrthogonal_velocity (R : Matrix.orthogonalGroup (Fin d) ℝ) :
    (ofOrthogonal R).velocity = 0 := rfl@[simp]
lemma ofOrthogonal_spaceTranslation (R : Matrix.orthogonalGroup (Fin d) ℝ) :
    (ofOrthogonal R).spaceTranslation = 0 := rfl@[simp]
lemma ofOrthogonal_timeTranslation (R : Matrix.orthogonalGroup (Fin d) ℝ) :
    (ofOrthogonal R).timeTranslation = 0 := rfl

Inclusion of the orthogonal group into the Galilean group.

def orthogonal.incl : Matrix.orthogonalGroup (Fin d) ℝ →* GalileanGroup d where
  toFun := ofOrthogonal
  map_one' := rfl
  map_mul' R S := byd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)⊢ ofOrthogonal (R * S) = ofOrthogonal R * ofOrthogonal S
    ext irotationd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)i:Fin dj✝:Fin d⊢ ↑(ofOrthogonal (R * S)).rotation i j✝ = ↑(ofOrthogonal R * ofOrthogonal S).rotation i j✝velocityd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)i:Fin d⊢ (ofOrthogonal (R * S)).velocity.ofLp i = (ofOrthogonal R * ofOrthogonal S).velocity.ofLp ispaceTranslationd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)i:Fin d⊢ (ofOrthogonal (R * S)).spaceTranslation.ofLp i = (ofOrthogonal R * ofOrthogonal S).spaceTranslation.ofLp itimeTranslationd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)⊢ (ofOrthogonal (R * S)).timeTranslation.val = (ofOrthogonal R * ofOrthogonal S).timeTranslation.val <;>rotationd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)i:Fin dj✝:Fin d⊢ ↑(ofOrthogonal (R * S)).rotation i j✝ = ↑(ofOrthogonal R * ofOrthogonal S).rotation i j✝velocityd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)i:Fin d⊢ (ofOrthogonal (R * S)).velocity.ofLp i = (ofOrthogonal R * ofOrthogonal S).velocity.ofLp ispaceTranslationd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)i:Fin d⊢ (ofOrthogonal (R * S)).spaceTranslation.ofLp i = (ofOrthogonal R * ofOrthogonal S).spaceTranslation.ofLp itimeTranslationd:ℕR:↥(Matrix.orthogonalGroup (Fin d) ℝ)S:↥(Matrix.orthogonalGroup (Fin d) ℝ)⊢ (ofOrthogonal (R * S)).timeTranslation.val = (ofOrthogonal R * ofOrthogonal S).timeTranslation.val simp [ofOrthogonal]All goals completed! 🐙

A pure spatial translation as a Galilean transformation.

def ofSpaceTranslation (a : EuclideanSpace ℝ (Fin d)) : GalileanGroup d :=
  ⟨1, 0, a, 0⟩

              @[simp]
lemma ofSpaceTranslation_rotation (a : EuclideanSpace ℝ (Fin d)) :
    (ofSpaceTranslation a).rotation = 1 := rfl@[simp]
lemma ofSpaceTranslation_velocity (a : EuclideanSpace ℝ (Fin d)) :
    (ofSpaceTranslation a).velocity = 0 := rfl@[simp]
lemma ofSpaceTranslation_spaceTranslation (a : EuclideanSpace ℝ (Fin d)) :
    (ofSpaceTranslation a).spaceTranslation = a := rfl@[simp]
lemma ofSpaceTranslation_timeTranslation (a : EuclideanSpace ℝ (Fin d)) :
    (ofSpaceTranslation a).timeTranslation = 0 := rfl

Inclusion of spatial translations into the Galilean group.

def spaceTranslation.incl :
    Multiplicative (EuclideanSpace ℝ (Fin d)) →* GalileanGroup d where
  toFun a := ofSpaceTranslation a.toAdd
  map_one' := rfl
  map_mul' a b := byd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))⊢ ofSpaceTranslation (Multiplicative.toAdd (a * b)) =
  ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)
    ext irotationd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))i:Fin dj✝:Fin d⊢ ↑(ofSpaceTranslation (Multiplicative.toAdd (a * b))).rotation i j✝ =
  ↑(ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).rotation i j✝velocityd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))i:Fin d⊢ (ofSpaceTranslation (Multiplicative.toAdd (a * b))).velocity.ofLp i =
  (ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).velocity.ofLp ispaceTranslationd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))i:Fin d⊢ (ofSpaceTranslation (Multiplicative.toAdd (a * b))).spaceTranslation.ofLp i =
  (ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).spaceTranslation.ofLp itimeTranslationd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))⊢ (ofSpaceTranslation (Multiplicative.toAdd (a * b))).timeTranslation.val =
  (ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).timeTranslation.val <;>rotationd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))i:Fin dj✝:Fin d⊢ ↑(ofSpaceTranslation (Multiplicative.toAdd (a * b))).rotation i j✝ =
  ↑(ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).rotation i j✝velocityd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))i:Fin d⊢ (ofSpaceTranslation (Multiplicative.toAdd (a * b))).velocity.ofLp i =
  (ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).velocity.ofLp ispaceTranslationd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))i:Fin d⊢ (ofSpaceTranslation (Multiplicative.toAdd (a * b))).spaceTranslation.ofLp i =
  (ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).spaceTranslation.ofLp itimeTranslationd:ℕa:Multiplicative (EuclideanSpace ℝ (Fin d))b:Multiplicative (EuclideanSpace ℝ (Fin d))⊢ (ofSpaceTranslation (Multiplicative.toAdd (a * b))).timeTranslation.val =
  (ofSpaceTranslation (Multiplicative.toAdd a) * ofSpaceTranslation (Multiplicative.toAdd b)).timeTranslation.val simp [ofSpaceTranslation]All goals completed! 🐙

A pure time translation as a Galilean transformation.

def ofTimeTranslation (b : Time) : GalileanGroup d :=
  ⟨1, 0, 0, b⟩

              @[simp]
lemma ofTimeTranslation_rotation (b : Time) :
    (ofTimeTranslation (d := d) b).rotation = 1 := rfl@[simp]
lemma ofTimeTranslation_velocity (b : Time) :
    (ofTimeTranslation (d := d) b).velocity = 0 := rfl@[simp]
lemma ofTimeTranslation_spaceTranslation (b : Time) :
    (ofTimeTranslation (d := d) b).spaceTranslation = 0 := rfl@[simp]
lemma ofTimeTranslation_timeTranslation (b : Time) :
    (ofTimeTranslation (d := d) b).timeTranslation = b := rfl

Inclusion of time translations into the Galilean group.

def timeTranslation.incl : Multiplicative Time →* GalileanGroup d where
  toFun b := ofTimeTranslation b.toAdd
  map_one' := rfl
  map_mul' a b := byd:ℕa:Multiplicative Timeb:Multiplicative Time⊢ ofTimeTranslation (Multiplicative.toAdd (a * b)) =
  ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)
    ext irotationd:ℕa:Multiplicative Timeb:Multiplicative Timei:Fin dj✝:Fin d⊢ ↑(ofTimeTranslation (Multiplicative.toAdd (a * b))).rotation i j✝ =
  ↑(ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).rotation i j✝velocityd:ℕa:Multiplicative Timeb:Multiplicative Timei:Fin d⊢ (ofTimeTranslation (Multiplicative.toAdd (a * b))).velocity.ofLp i =
  (ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).velocity.ofLp ispaceTranslationd:ℕa:Multiplicative Timeb:Multiplicative Timei:Fin d⊢ (ofTimeTranslation (Multiplicative.toAdd (a * b))).spaceTranslation.ofLp i =
  (ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).spaceTranslation.ofLp itimeTranslationd:ℕa:Multiplicative Timeb:Multiplicative Time⊢ (ofTimeTranslation (Multiplicative.toAdd (a * b))).timeTranslation.val =
  (ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).timeTranslation.val <;>rotationd:ℕa:Multiplicative Timeb:Multiplicative Timei:Fin dj✝:Fin d⊢ ↑(ofTimeTranslation (Multiplicative.toAdd (a * b))).rotation i j✝ =
  ↑(ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).rotation i j✝velocityd:ℕa:Multiplicative Timeb:Multiplicative Timei:Fin d⊢ (ofTimeTranslation (Multiplicative.toAdd (a * b))).velocity.ofLp i =
  (ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).velocity.ofLp ispaceTranslationd:ℕa:Multiplicative Timeb:Multiplicative Timei:Fin d⊢ (ofTimeTranslation (Multiplicative.toAdd (a * b))).spaceTranslation.ofLp i =
  (ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).spaceTranslation.ofLp itimeTranslationd:ℕa:Multiplicative Timeb:Multiplicative Time⊢ (ofTimeTranslation (Multiplicative.toAdd (a * b))).timeTranslation.val =
  (ofTimeTranslation (Multiplicative.toAdd a) * ofTimeTranslation (Multiplicative.toAdd b)).timeTranslation.val simp [ofTimeTranslation]All goals completed! 🐙