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.EuclideanGroup.BasicThe inclusion of the Euclidean group into the affine automorphism group
This file has two parts.
Part 1: the inclusion. The abstract Euclidean group EuclideanGroup n = ℝⁿ ⋊ O(n) is
included into Mathlib's affine automorphism group as the composite of two monoid homomorphisms
EuclideanGroup n →* AffineIsometryEquiv ℝ (EuclideanSpace ℝ (Fin n)) _ →* AffineEquiv ℝ _ _.
EuclideanGroup.orthogonalToLinearIsometryEquiv : an orthogonal matrix as a linear isometry
equivalence of EuclideanSpace ℝ (Fin n); the linear ingredient of the first leg.
EuclideanGroup.toAffineIsometryHom : the first leg, ⟨t, Q⟩ ↦ (x ↦ Q x + t).
AffineIsometryEquiv.toAffineEquivHom : the second leg, AffineIsometryEquiv.toAffineEquiv
as a monoid homomorphism.
EuclideanGroup.toAffineEquiv : the composite of the two legs; the result intended for use
elsewhere.
Part 2: strengthening the first leg to an isomorphism. Every affine isometry of
EuclideanSpace ℝ (Fin n) is x ↦ Q x + t for a unique orthogonal Q and translation t, so
the first leg is in fact a group isomorphism. We record it as
EuclideanGroup.toAffineIsometryMulEquiv, a MulEquiv whose fields are supplied as follows:
toFun, map_mul' : reused from EuclideanGroup.toAffineIsometryHom in part 1;
invFun : built from EuclideanGroup.linearIsometryEquivToOrthogonal, the inverse of the
linear bridge orthogonalToLinearIsometryEquiv;
left_inv : from the round trip orthogonalToLinearIsometryEquiv_left_inv together with the
projection lemma linearIsometryEquiv_constVAdd_mul;
right_inv : from the round trip orthogonalToLinearIsometryEquiv_right_inv.
Part 2 is self-contained; nothing in part 1 depends on it.
@[expose] public sectionPart 1: the inclusion
The chain is: orthogonalToLinearIsometryEquiv (linear ingredient) → toAffineIsometryHom
(first leg) → AffineIsometryEquiv.toAffineEquivHom (second leg) → toAffineEquiv
(the composite).
@[simp] lemma orthogonalToLinearIsometryEquiv_apply
(Q : Matrix.orthogonalGroup (Fin n) ℝ) (x : EuclideanSpace ℝ (Fin n)) :
orthogonalToLinearIsometryEquiv Q x = Q • x := rfl
Unfolds toAffineIsometryHom into its translation and linear factors.
@[simp] lemma toAffineIsometryHom_apply (A : EuclideanGroup n) :
toAffineIsometryHom A =
AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin n)) A.translation *
(orthogonalToLinearIsometryEquiv A.linear).toAffineIsometryEquiv := rflPart 2: strengthening the first leg to an isomorphism
The first leg toAffineIsometryHom is in fact a group isomorphism: every affine isometry of
EuclideanSpace ℝ (Fin n) is x ↦ Q x + t for a unique orthogonal Q and translation t. The
declarations below supply the remaining fields of the MulEquiv toAffineIsometryMulEquiv, in
field order: the invFun ingredient, the two lemmas proving left_inv, and the lemma proving
right_inv. Nothing in part 1 depends on this section.
linearIsometryEquivToOrthogonal is a left inverse of orthogonalToLinearIsometryEquiv.
Together with linearIsometryEquiv_constVAdd_mul, this proves left_inv of
toAffineIsometryMulEquiv.
All goals completed! 🐙
The affine map x ↦ t +ᵥ L x, projected to its linear isometry component, is L.
Together with orthogonalToLinearIsometryEquiv_left_inv, this proves left_inv of
toAffineIsometryMulEquiv.
n:ℕt:EuclideanSpace ℝ (Fin n)L:EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)x:EuclideanSpace ℝ (Fin n)h:(AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin n)) t * L.toAffineIsometryEquiv).linearIsometryEquiv x =
(AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin n)) t * L.toAffineIsometryEquiv) x -ᵥ
(AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin n)) t * L.toAffineIsometryEquiv) 0⊢ (AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin n)) t * L.toAffineIsometryEquiv) x -ᵥ
(AffineIsometryEquiv.constVAdd ℝ (EuclideanSpace ℝ (Fin n)) t * L.toAffineIsometryEquiv) 0 =
L x
All goals completed! 🐙
linearIsometryEquivToOrthogonal is a right inverse of orthogonalToLinearIsometryEquiv;
this proves right_inv of toAffineIsometryMulEquiv.
n:ℕL:EuclideanSpace ℝ (Fin n) ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin n)x:EuclideanSpace ℝ (Fin n)⊢ ↑L.toLinearEquiv x = L x
All goals completed! 🐙
toAffineIsometryMulEquiv agrees with toAffineIsometryHom.
@[simp] lemma toAffineIsometryMulEquiv_apply (A : EuclideanGroup n) :
toAffineIsometryMulEquiv A = toAffineIsometryHom A := rfl