English
There exists a real-linear isometry between the quaternions ℍ and the Euclidean space ℝ^4, given by identifying ℍ with ℝ^4 via the coordinate map a0 + a1 i + a2 j + a3 k ↦ (a0, a1, a2, a3) with inverse extracting the four coordinates.
Русский
Существует линейная изометрия между кватернионами ℍ и евклидовым пространством ℝ^4, заданная идентификацией ℍ с ℝ^4 по координатной карте a0 + a1 i + a2 j + a3 k ↦ (a0, a1, a2, a3) с обратной связью возвращающей четыре коэффициента.
LaTeX
$$$\mathbb{H} \cong_{\mathrm{LinIso}} \mathbb{R}^4$$$
Lean4
/-- `QuaternionAlgebra.linearEquivTuple` as a `LinearIsometryEquiv`. -/
@[simps apply symm_apply]
noncomputable def linearIsometryEquivTuple : ℍ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4) :=
{
(QuaternionAlgebra.linearEquivTuple (-1 : ℝ) (0 : ℝ) (-1 : ℝ)).trans
(WithLp.linearEquiv 2 ℝ
(Fin 4 → ℝ)).symm with
toFun := fun a => !₂[a.1, a.2, a.3, a.4]
invFun := fun a => ⟨a 0, a 1, a 2, a 3⟩
norm_map' := norm_toLp_equivTuple }
