# Quaternions as a normed algebra #

In this file we define the following structures on the space ℍ := ℍ[ℝ] of quaternions:

• inner product space;
• normed ring;
• normed space over ℝ.

We show that the norm on ℍ[ℝ] agrees with the euclidean norm of its components.

## Notation #

The following notation is available with open Quaternion or open scoped Quaternion:

• ℍ : quaternions

## Tags #

quaternion, normed ring, normed space, normed algebra

Space of quaternions over a type. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Equations
Instances For
Equations
theorem Quaternion.inner_self (a : ) :
a, a⟫_ = Quaternion.normSq a
theorem Quaternion.inner_def (a : ) (b : ) :
a, b⟫_ = (a * star b).re
Equations
noncomputable instance Quaternion.instInnerProductSpaceReal :
Equations
• One or more equations did not get rendered due to their size.
theorem Quaternion.normSq_eq_norm_mul_self (a : ) :
Quaternion.normSq a = a * a
Equations
@[simp]
theorem Quaternion.norm_coe (a : ) :
@[simp]
noncomputable instance Quaternion.instNormedAlgebraReal :
Equations

Coercion from ℂ to ℍ.

Equations
• z = { re := z.re, imI := z.im, imJ := 0, imK := 0 }
Instances For
@[simp]
theorem Quaternion.coeComplex_re (z : ) :
(z).re = z.re
@[simp]
theorem Quaternion.coeComplex_imI (z : ) :
(z).imI = z.im
@[simp]
theorem Quaternion.coeComplex_imJ (z : ) :
(z).imJ = 0
@[simp]
theorem Quaternion.coeComplex_imK (z : ) :
(z).imK = 0
@[simp]
theorem Quaternion.coeComplex_add (z : ) (w : ) :
(z + w) = z + w
@[simp]
theorem Quaternion.coeComplex_mul (z : ) (w : ) :
(z * w) = z * w
@[simp]
@[simp]
@[simp]
theorem Quaternion.coe_real_complex_mul (r : ) (z : ) :
r z = r * z
@[simp]
theorem Quaternion.coeComplex_coe (r : ) :
r = r

Coercion ℂ →ₐ[ℝ] ℍ as an algebra homomorphism.

Equations
• One or more equations did not get rendered due to their size.
Instances For
@[simp]

The norm of the components as a euclidean vector equals the norm of the quaternion.

@[simp]
theorem Quaternion.linearIsometryEquivTuple_apply (a : ) :
Quaternion.linearIsometryEquivTuple a = (WithLp.equiv 2 (Fin 4)).symm ![a.re, a.imI, a.imJ, a.imK]
@[simp]
theorem Quaternion.linearIsometryEquivTuple_symm_apply (a : ) :
= { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }

QuaternionAlgebra.linearEquivTuple as a LinearIsometryEquiv.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Quaternion.continuous_normSq :
Continuous Quaternion.normSq
theorem Quaternion.continuous_re :
Continuous fun (q : ) => q.re
theorem Quaternion.continuous_imI :
Continuous fun (q : ) => q.imI
theorem Quaternion.continuous_imJ :
Continuous fun (q : ) => q.imJ
theorem Quaternion.continuous_imK :
Continuous fun (q : ) => q.imK
theorem Quaternion.continuous_im :
Continuous fun (q : ) => q.im
Equations
@[simp]
theorem Quaternion.hasSum_coe {α : Type u_1} {f : α} {r : } :
HasSum (fun (a : α) => (f a)) r HasSum f r
@[simp]
theorem Quaternion.summable_coe {α : Type u_1} {f : α} :
(Summable fun (a : α) => (f a))
theorem Quaternion.tsum_coe {α : Type u_1} (f : α) :
∑' (a : α), (f a) = (∑' (a : α), f a)