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 Mathlib.Analysis.InnerProductSpace.PiL2Euclidean group
This file defines the Euclidean group as translations composed with orthogonal maps, together with the special Euclidean group, translation subgroup, and rotation subgroups.
The affine group, together with the inclusion of the Euclidean group into it, is defined in
Physlib.SpaceAndTime.Space.EuclideanGroup.AffineGroup.
@[expose] public section
An n-dimensional Euclidean group is a group of
rotations, reflections, and translations.
The translation part of a Euclidean transformation.
The orthogonal linear part of a Euclidean transformation.
@[ext]
structure EuclideanGroup (n : ℕ) where translation : EuclideanSpace ℝ (Fin n) linear : Matrix.orthogonalGroup (Fin n) ℝ
One/Mul projection lemmas
These expose the semidirect-product formulas behind the Group instance so that simp can
reduce the translation/linear components of 1 and A * B.
@[simp] lemma one_translation : (1 : EuclideanGroup n).translation = 0 := rfl@[simp] lemma one_linear : (1 : EuclideanGroup n).linear = 1 := rfl@[simp] lemma mul_translation (A B : EuclideanGroup n) :
(A * B).translation = A.translation + A.linear • B.translation := rfl@[simp] lemma mul_linear (A B : EuclideanGroup n) :
(A * B).linear = A.linear * B.linear := rflAll goals completed! 🐙All goals completed! 🐙Special Euclidean Group is the subgroup with det(Q) = 1 where Q ∈ O(n)
All goals completed! 🐙Translation is the subgroup with Q = 1.
All goals completed! 🐙MonoidHom including a translation vector into the Euclidean Group.
def translationVector.incl (n : ℕ) :
Multiplicative (EuclideanSpace ℝ (Fin n)) →* EuclideanGroup n where
toFun v := ⟨v.toAdd, 1⟩
map_one' := n:ℕ⊢ { translation := Multiplicative.toAdd 1, linear := 1 } = 1 All goals completed! 🐙
map_mul' x y := n:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ { translation := Multiplicative.toAdd (x * y), linear := 1 } =
{ translation := Multiplicative.toAdd x, linear := 1 } * { translation := Multiplicative.toAdd y, linear := 1 }
n:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ { translation := Multiplicative.toAdd (x * y), linear := 1 }.translation =
({ translation := Multiplicative.toAdd x, linear := 1 } *
{ translation := Multiplicative.toAdd y, linear := 1 }).translationn:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ { translation := Multiplicative.toAdd (x * y), linear := 1 }.linear =
({ translation := Multiplicative.toAdd x, linear := 1 } *
{ translation := Multiplicative.toAdd y, linear := 1 }).linear
n:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ { translation := Multiplicative.toAdd (x * y), linear := 1 }.translation =
({ translation := Multiplicative.toAdd x, linear := 1 } *
{ translation := Multiplicative.toAdd y, linear := 1 }).translation n:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ Multiplicative.toAdd (x * y) = Multiplicative.toAdd x + 1 • Multiplicative.toAdd y
All goals completed! 🐙
n:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ { translation := Multiplicative.toAdd (x * y), linear := 1 }.linear =
({ translation := Multiplicative.toAdd x, linear := 1 } *
{ translation := Multiplicative.toAdd y, linear := 1 }).linear n:ℕx:Multiplicative (EuclideanSpace ℝ (Fin n))y:Multiplicative (EuclideanSpace ℝ (Fin n))⊢ 1 = 1 * 1
All goals completed! 🐙
An API feature: the translation vector inclusion image is the TranslationGroup carrier.
n:ℕg:EuclideanGroup nh:g ∈ ↑(TranslationGroup n)⊢ ∃ y, (incl n) y = g
n:ℕg:EuclideanGroup nh:g ∈ ↑(TranslationGroup n)⊢ (incl n) g.translation = g
n:ℕg:EuclideanGroup nh:g ∈ ↑(TranslationGroup n)⊢ { translation := g.translation, linear := 1 } = g
n:ℕg:EuclideanGroup nh:g ∈ ↑(TranslationGroup n)⊢ { translation := g.translation, linear := 1 }.linear = g.linear
n:ℕg:EuclideanGroup nh:g ∈ ↑(TranslationGroup n)⊢ ↑{ translation := g.translation, linear := 1 }.linear = ↑g.linear
All goals completed! 🐙The translation by the zero vector is the identity of the Euclidean group.
lemma translation_zero : translationVector.incl n
(Multiplicative.ofAdd (0 : EuclideanSpace ℝ (Fin n))) = 1 := n:ℕ⊢ (translationVector.incl n) (Multiplicative.ofAdd 0) = 1
All goals completed! 🐙
The subgroup of EuclideanGroup n whose elements fix the origin
(translation = 0). This is the copy of O(n) sitting inside E(n).
All goals completed! 🐙
RotationsAbout.toOrigin p followed by RotationsAbout.fromOrigin p is the identity; the
forward leg of the isomorphism RotationsAboutEquiv.
lemma RotationsAbout.fromOrigin_comp_toOrigin :
(RotationsAbout.fromOrigin p).comp (RotationsAbout.toOrigin p) =
MonoidHom.id (RotationsAbout p) := n:ℕp:EuclideanSpace ℝ (Fin n)⊢ (fromOrigin p).comp (toOrigin p) = MonoidHom.id ↥(RotationsAbout p)
n:ℕp:EuclideanSpace ℝ (Fin n)⊢ ∀ (x : ↥(RotationsAbout p)), ((fromOrigin p).comp (toOrigin p)) x = (MonoidHom.id ↥(RotationsAbout p)) x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationsAbout p)⊢ ((fromOrigin p).comp (toOrigin p)) x = (MonoidHom.id ↥(RotationsAbout p)) x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationsAbout p)⊢ ↑(((fromOrigin p).comp (toOrigin p)) x) = ↑((MonoidHom.id ↥(RotationsAbout p)) x)
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationsAbout p)⊢ (fromOrigin p) ((toOrigin p) x) = x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationsAbout p)⊢ (fromOrigin p)
({
toFun := fun g =>
⟨(translationVector.incl n) (Multiplicative.ofAdd (-p)) * ↑g *
(translationVector.incl n) (Multiplicative.ofAdd p),
⋯⟩,
map_one' := ⋯, map_mul' := ⋯ }
x) =
x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationsAbout p)⊢ {
toFun := fun g =>
⟨(translationVector.incl n) (Multiplicative.ofAdd p) * ↑g *
(translationVector.incl n) (Multiplicative.ofAdd (-p)),
⋯⟩,
map_one' := ⋯, map_mul' := ⋯ }
({
toFun := fun g =>
⟨(translationVector.incl n) (Multiplicative.ofAdd (-p)) * ↑g *
(translationVector.incl n) (Multiplicative.ofAdd p),
⋯⟩,
map_one' := ⋯, map_mul' := ⋯ }
x) =
x
All goals completed! 🐙
RotationsAbout.fromOrigin p followed by RotationsAbout.toOrigin p is the identity; the
backward leg of the isomorphism RotationsAboutEquiv.
lemma RotationsAbout.toOrigin_comp_fromOrigin :
(RotationsAbout.toOrigin p).comp (RotationsAbout.fromOrigin p) =
MonoidHom.id (RotationGroup n) := n:ℕp:EuclideanSpace ℝ (Fin n)⊢ (toOrigin p).comp (fromOrigin p) = MonoidHom.id ↥(RotationGroup n)
n:ℕp:EuclideanSpace ℝ (Fin n)⊢ ∀ (x : ↥(RotationGroup n)), ((toOrigin p).comp (fromOrigin p)) x = (MonoidHom.id ↥(RotationGroup n)) x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationGroup n)⊢ ((toOrigin p).comp (fromOrigin p)) x = (MonoidHom.id ↥(RotationGroup n)) x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationGroup n)⊢ ↑(((toOrigin p).comp (fromOrigin p)) x) = ↑((MonoidHom.id ↥(RotationGroup n)) x)
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationGroup n)⊢ (toOrigin p) ((fromOrigin p) x) = x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationGroup n)⊢ {
toFun := fun g =>
⟨(translationVector.incl n) (Multiplicative.ofAdd (-p)) * ↑g *
(translationVector.incl n) (Multiplicative.ofAdd p),
⋯⟩,
map_one' := ⋯, map_mul' := ⋯ }
((fromOrigin p) x) =
x
n:ℕp:EuclideanSpace ℝ (Fin n)x:↥(RotationGroup n)⊢ {
toFun := fun g =>
⟨(translationVector.incl n) (Multiplicative.ofAdd (-p)) * ↑g *
(translationVector.incl n) (Multiplicative.ofAdd p),
⋯⟩,
map_one' := ⋯, map_mul' := ⋯ }
({
toFun := fun g =>
⟨(translationVector.incl n) (Multiplicative.ofAdd p) * ↑g *
(translationVector.incl n) (Multiplicative.ofAdd (-p)),
⋯⟩,
map_one' := ⋯, map_mul' := ⋯ }
x) =
x
All goals completed! 🐙
API feature: the degenerate identity that RotationsAbout 0 = RotationGroup n
n:ℕg:EuclideanGroup ng1:↥(RotationGroup n)hg1:g = ↑g1⊢ ↑g1 ∈ RotationGroup n
All goals completed! 🐙
n:ℕg:EuclideanGroup n⊢ g ∈ RotationGroup n → g ∈ RotationsAbout 0 n:ℕg:EuclideanGroup nhg:g ∈ RotationGroup n⊢ g ∈ RotationsAbout 0
n:ℕg:EuclideanGroup nhg:g ∈ RotationGroup n⊢ g =
(translationVector.incl n) (Multiplicative.ofAdd 0) * ↑⟨g, hg⟩ *
(translationVector.incl n) (Multiplicative.ofAdd (-0))
All goals completed! 🐙Rotations are members of special orthogonal groups and can be viewed as members of orthogonal groups.
def specialOrthogonal.incl (n : ℕ) :
Matrix.specialOrthogonalGroup (Fin n) ℝ →* Matrix.orthogonalGroup (Fin n) ℝ :=
Submonoid.inclusion Matrix.specialUnitaryGroup_le_unitaryGroupThe Euclidean group element given by a rotation about the origin (zero translation).
def ofRotation (Q : Matrix.specialOrthogonalGroup (Fin n) ℝ) :
EuclideanGroup n := ⟨0, specialOrthogonal.incl n Q⟩Specialization to a group element from a rotation and a translation.
def ofRotationTranslation (Q : Matrix.specialOrthogonalGroup (Fin n) ℝ)
(t : EuclideanSpace ℝ (Fin n)) : EuclideanGroup n :=
⟨t, specialOrthogonal.incl n Q⟩The specialization projects back to the translation component.
@[simp]
lemma ofRotationTranslation_translation (Q : Matrix.specialOrthogonalGroup (Fin n) ℝ)
(t : EuclideanSpace ℝ (Fin n)) :
(ofRotationTranslation Q t).translation = t := rflThe specialization projects back to the linear (rotation) component.
@[simp]
lemma ofRotationTranslation_linear (Q : Matrix.specialOrthogonalGroup (Fin n) ℝ)
(t : EuclideanSpace ℝ (Fin n)) :
(ofRotationTranslation Q t).linear = specialOrthogonal.incl n Q := rflAPI feature: the inclusion image decomposes as group product.
All goals completed! 🐙
specialOrthogonal.toRotation n followed by specialOrthogonal.fromRotation n is the identity;
the forward leg of the isomorphism specialOrthogonalEquiv.
lemma specialOrthogonal.fromRotation_comp_toRotation :
(specialOrthogonal.fromRotation n).comp (specialOrthogonal.toRotation n) =
MonoidHom.id (Matrix.specialOrthogonalGroup (Fin n) ℝ) := n:ℕ⊢ (fromRotation n).comp (toRotation n) = MonoidHom.id ↥(Matrix.specialOrthogonalGroup (Fin n) ℝ)
n:ℕ⊢ ∀ (x : ↥(Matrix.specialOrthogonalGroup (Fin n) ℝ)),
((fromRotation n).comp (toRotation n)) x = (MonoidHom.id ↥(Matrix.specialOrthogonalGroup (Fin n) ℝ)) x
n:ℕx:↥(Matrix.specialOrthogonalGroup (Fin n) ℝ)⊢ ((fromRotation n).comp (toRotation n)) x = (MonoidHom.id ↥(Matrix.specialOrthogonalGroup (Fin n) ℝ)) x
All goals completed! 🐙
specialOrthogonal.fromRotation n followed by specialOrthogonal.toRotation n is the identity;
the backward leg of the isomorphism specialOrthogonalEquiv.
All goals completed! 🐙
n:ℕx:↥(RotationGroup n)⊢ (↑(((toRotation n).comp (fromRotation n)) x)).linear = (↑((MonoidHom.id ↥(RotationGroup n)) x)).linear All goals completed! 🐙