Imports
/-
Copyright (c) 2026 Shaopeng Zhu. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Shaopeng Zhu
-/
module
public import Physlib.SpaceAndTime.Space.Origin
public import Physlib.SpaceAndTime.Space.EuclideanGroup.AffineGroup
The action of the Euclidean group on Space
The Euclidean group EuclideanGroup d = ℝᵈ ⋊ O(d) (Space/EuclideanGroup/Basic.lean) is the group
of rigid motions of d-dimensional space. This file makes that geometric meaning literal: it
endows the affine space of points Space d (Space/Basic.lean) with a MulAction of
EuclideanGroup d by isometries, and specialises it to the rotations.
Main results
EuclideanGroup.smul_vsub_smul — displacements transform by the linear part alone.
EuclideanGroup.dist_smul — the action preserves distance.
EuclideanGroup.rotation_smul_origin / rotation_smul_vsub_origin — rotations fix the origin
and act about it by their orthogonal part.
EuclideanGroup.chartEuclidean_smul — agreement with the affine-isometry model
(AffineGroup.lean); the rest of the file does not depend on it.
Implementation notes
Space d is an affine space (NormedAddTorsor) with no canonical origin, so the action uses its
vector-space zero (0 : Space d) as the basepoint:
g • p = (g.linear • (p -ᵥ (0 : Space d)) + g.translation) +ᵥ (0 : Space d).
The Zero instance and the chart Space.chartEuclidean are defined in Space/Origin.lean.
@[expose] public section
Part 1: the action of the Euclidean group on Space
The motion g = ⟨t, Q⟩ acts by g • p = (Q • (p -ᵥ origin) + t) +ᵥ origin. The MulAction laws
reduce to the semidirect-product group law of EuclideanGroup.
Coordinate formula for the action: (g • p) i = (Q • (p -ᵥ origin)) i + t i.
@[simp] lemma smul_apply (g : EuclideanGroup d) (p : Space d) (i : Fin d) :
(g • p) i = (g.linear • (p -ᵥ (0 : Space d))) i + g.translation i := d:ℕg:EuclideanGroup dp:Space di:Fin d⊢ (g • p).val i = (g.linear • (p -ᵥ 0)).ofLp i + g.translation.ofLp i
d:ℕg:EuclideanGroup dp:Space di:Fin d⊢ ((g.linear • (p -ᵥ 0) + g.translation) +ᵥ 0).val i = (g.linear • (p -ᵥ 0)).ofLp i + g.translation.ofLp i
All goals completed! 🐙
The displacement between two points transforms by the orthogonal part alone: the
translation cancels. This is the key lemma behind dist_smul.
All goals completed! 🐙
The Euclidean group acts on Space d by isometries: every rigid motion preserves distance.
d:ℕg:EuclideanGroup dp:Space dq:Space d⊢ ‖g.linear • (p -ᵥ q)‖ = ‖p -ᵥ q‖
All goals completed! 🐙Part 2: specialisation to rotations
The RotationGroup d action is the restriction of the Euclidean action along
RotationGroup d ≤ EuclideanGroup d (RotationGroup elements have zero translation). The lemmas
below record that rotations fix the origin, act by their orthogonal part about the origin, and
preserve distance.
The rotation-group action is the restriction of the Euclidean action: r • p = ↑r • p
(definitional).
@[simp] lemma rotation_smul_eq (r : RotationGroup d) (p : Space d) :
r • p = (r : EuclideanGroup d) • p := rfl
A rotation fixes the origin: its translation part vanishes
(RotationGroup ≤ OriginStabilizer), so ↑r • 0 = 0. Stated in the ↑r form (the simp normal
form of r • _, via rotation_smul_eq) so it is a well-formed simp lemma.
d:ℕr:↥(RotationGroup d)h_trans:(↑r).translation = 0h_rot:↑r • 0 = ((↑r).linear • 0 + 0) +ᵥ 0⊢ ↑r • 0 = 0
All goals completed! 🐙
A rotation acts on the displacement from the origin by its orthogonal part, for every p:
(r • p) -ᵥ origin = Q • (p -ᵥ origin).
All goals completed! 🐙
The rotation group acts on Space d by isometries (inherited from dist_smul).
lemma rotation_dist_smul (r : RotationGroup d) (p q : Space d) :
dist (r • p) (r • q) = dist p q :=
dist_smul (r : EuclideanGroup d) p qPart 3: relation to the affine isometry action (optional bridge)
chartEuclidean_smul records that, under the chart Space.chartEuclidean (Space/Origin.lean),
p ↦ p -ᵥ origin, the Part 1 action is the transport of toAffineIsometryMulEquiv
(AffineGroup.lean) from EuclideanSpace to Space. Nothing in Parts 1–2 depends on it.
Under the standard chart, the Euclidean action on Space d is the
transport of toAffineIsometryMulEquiv acting on EuclideanSpace:
chart (g • p) = (toAffineIsometryMulEquiv g) (chart p).
d:ℕg:EuclideanGroup dp:Space dh_left:g • p -ᵥ 0 = g.linear • (p -ᵥ 0) + g.translation⊢ g • p -ᵥ 0 =
(AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin d)) g.translation *
(orthogonalToLinearIsometryEquiv g.linear).toAffineIsometryEquiv)
((Space.chartEuclidean d) p)
d:ℕg:EuclideanGroup dp:Space dh_left:g • p -ᵥ 0 = g.linear • (p -ᵥ 0) + g.translation⊢ g.linear • (p -ᵥ 0) + g.translation = g.translation + g.linear • (p -ᵥ 0)
All goals completed! 🐙