The semidirect product of translations and linear isometries

The affine isometry group of a seminormed space is the semidirect product of its additive translation group and its linear isometry group. The action is the usual evaluation action, and the multiplication convention is (v, L) (w, K) = (v + L w, L K). The pair (v, L) acts on a point x as v + L x.

AffineIsometryEquiv.semidirectProductMulEquiv extracts the image of zero and the linear part. Its inverse constructs the corresponding affine isometry. The two factor inclusions are respectively translations and linear isometries. Over a real inner product space this is the Euclidean group decomposition into translations and orthogonal transformations.

This uses Mathlib's affine isometry and semidirect product carriers, without introducing a second rigid-motion group.

References

• J. M. Lee, Introduction to Riemannian Manifolds, 2nd ed., Chapter 3: Euclidean isometries and the Euclidean group.

def AffineIsometryEquiv.semidirectProductMulEquiv {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] : (E ≃ᵃⁱ[𝕜] E) ≃* Multiplicative E ⋊[LinearIsometryEquiv.multiplicativeAutHom] (E ≃ₗᵢ[𝕜] E)

The affine isometry group is the semidirect product of translations and linear isometries. The coordinates of f are (f 0, f.linearIsometryEquiv).

@[simp]

theorem AffineIsometryEquiv.semidirectProductMulEquiv_left {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (f : E ≃ᵃⁱ[𝕜] E) : (semidirectProductMulEquiv f).left = Multiplicative.ofAdd (f 0)

The translation coordinate is the image of zero.

@[simp]

theorem AffineIsometryEquiv.semidirectProductMulEquiv_right {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (f : E ≃ᵃⁱ[𝕜] E) : (semidirectProductMulEquiv f).right = f.linearIsometryEquiv

The linear coordinate is the linear part.

@[simp]

theorem AffineIsometryEquiv.semidirectProductMulEquiv_symm_apply {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (p : Multiplicative E ⋊[LinearIsometryEquiv.multiplicativeAutHom] (E ≃ₗᵢ[𝕜] E)) (x : E) : (semidirectProductMulEquiv.symm p) x = Multiplicative.toAdd p.left + p.right x

The rigid motion represented by (v, L) sends x to v + L x.

@[simp]

theorem AffineIsometryEquiv.semidirectProductMulEquiv_constVAdd {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (v : E) : semidirectProductMulEquiv (constVAdd 𝕜 E v) = SemidirectProduct.inl (Multiplicative.ofAdd v)

The first factor is the translation subgroup.

@[simp]

theorem AffineIsometryEquiv.semidirectProductMulEquiv_toAffineIsometryEquiv {𝕜 : Type u_1} {E : Type u_2} [NormedField 𝕜] [SeminormedAddCommGroup E] [NormedSpace 𝕜 E] (L : E ≃ₗᵢ[𝕜] E) : semidirectProductMulEquiv L.toAffineIsometryEquiv = SemidirectProduct.inr L

The second factor is the linear isometry subgroup.