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

def Quaternion.termℍ : Lean.ParserDescr

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

instance Quaternion.instInnerReal : Inner ℝ (Quaternion ℝ)

theorem Quaternion.inner_self (a : Quaternion ℝ) : inner ℝ a a = normSq a

theorem Quaternion.inner_def (a b : Quaternion ℝ) : inner ℝ a b = (a * star b).re

noncomputable instance Quaternion.instNormedAddCommGroupReal : NormedAddCommGroup (Quaternion ℝ)

noncomputable instance Quaternion.instInnerProductSpaceReal : InnerProductSpace ℝ (Quaternion ℝ)

theorem Quaternion.normSq_eq_norm_mul_self (a : Quaternion ℝ) : normSq a = ‖a‖ * ‖a‖

instance Quaternion.instNormOneClassReal : NormOneClass (Quaternion ℝ)

@[simp]

theorem Quaternion.norm_coe (a : ℝ) : ‖↑a‖ = ‖a‖

@[simp]

theorem Quaternion.nnnorm_coe (a : ℝ) : ‖↑a‖₊ = ‖a‖₊

theorem Quaternion.norm_star (a : Quaternion ℝ) : ‖star a‖ = ‖a‖

theorem Quaternion.nnnorm_star (a : Quaternion ℝ) : ‖star a‖₊ = ‖a‖₊

noncomputable instance Quaternion.instNormedDivisionRingReal : NormedDivisionRing (Quaternion ℝ)

noncomputable instance Quaternion.instNormedAlgebraReal : NormedAlgebra ℝ (Quaternion ℝ)

instance Quaternion.instCStarRingReal : CStarRing (Quaternion ℝ)

def Quaternion.coeComplex (z : ℂ) : Quaternion ℝ

Coercion from ℂ to ℍ.

instance Quaternion.instCoeComplexReal : Coe ℂ (Quaternion ℝ)

@[simp]

theorem Quaternion.re_coeComplex (z : ℂ) : (↑z).re = z.re

@[deprecated Quaternion.re_coeComplex (since := "2025-08-31")]

theorem Quaternion.coeComplex_re (z : ℂ) : (↑z).re = z.re

Alias of Quaternion.re_coeComplex.

@[simp]

theorem Quaternion.imI_coeComplex (z : ℂ) : (↑z).imI = z.im

@[deprecated Quaternion.imI_coeComplex (since := "2025-08-31")]

theorem Quaternion.coeComplex_imI (z : ℂ) : (↑z).imI = z.im

Alias of Quaternion.imI_coeComplex.

@[simp]

theorem Quaternion.imJ_coeComplex (z : ℂ) : (↑z).imJ = 0

@[deprecated Quaternion.imJ_coeComplex (since := "2025-08-31")]

theorem Quaternion.coeComplex_imJ (z : ℂ) : (↑z).imJ = 0

Alias of Quaternion.imJ_coeComplex.

@[simp]

theorem Quaternion.imK_coeComplex (z : ℂ) : (↑z).imK = 0

@[deprecated Quaternion.imK_coeComplex (since := "2025-08-31")]

theorem Quaternion.coeComplex_imK (z : ℂ) : (↑z).imK = 0

Alias of Quaternion.imK_coeComplex.

@[simp]

theorem Quaternion.coeComplex_add (z w : ℂ) : ↑(z + w) = ↑z + ↑w

@[simp]

theorem Quaternion.coeComplex_mul (z w : ℂ) : ↑(z * w) = ↑z * ↑w

@[simp]

theorem Quaternion.coeComplex_zero : ↑0 = 0

@[simp]

theorem Quaternion.coeComplex_one : ↑1 = 1

@[simp]

theorem Quaternion.coe_real_complex_mul (r : ℝ) (z : ℂ) : r • ↑z = ↑r * ↑z

@[simp]

theorem Quaternion.coeComplex_coe (r : ℝ) : ↑↑r = ↑r

def Quaternion.ofComplex : ℂ →ₐ[ℝ] Quaternion ℝ

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

@[simp]

theorem Quaternion.coe_ofComplex : ⇑ofComplex = coeComplex

theorem Quaternion.norm_toLp_equivTuple (x : Quaternion ℝ) : ‖WithLp.toLp 2 ((equivTuple ℝ) x)‖ = ‖x‖

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

noncomputable def Quaternion.linearIsometryEquivTuple : Quaternion ℝ ≃ₗᵢ[ℝ] EuclideanSpace ℝ (Fin 4)

QuaternionAlgebra.linearEquivTuple as a LinearIsometryEquiv.

@[simp]

theorem Quaternion.linearIsometryEquivTuple_apply (a : Quaternion ℝ) : linearIsometryEquivTuple a = !₂[a.re, a.imI, a.imJ, a.imK]

@[simp]

theorem Quaternion.linearIsometryEquivTuple_symm_apply (a : EuclideanSpace ℝ (Fin 4)) : linearIsometryEquivTuple.symm a = { re := a.ofLp 0, imI := a.ofLp 1, imJ := a.ofLp 2, imK := a.ofLp 3 }

theorem Quaternion.continuous_coe : Continuous coe

theorem Quaternion.continuous_normSq : Continuous ⇑normSq

theorem Quaternion.continuous_re : Continuous fun (q : Quaternion ℝ) => q.re

theorem Quaternion.continuous_imI : Continuous fun (q : Quaternion ℝ) => q.imI

theorem Quaternion.continuous_imJ : Continuous fun (q : Quaternion ℝ) => q.imJ

theorem Quaternion.continuous_imK : Continuous fun (q : Quaternion ℝ) => q.imK

theorem Quaternion.continuous_im : Continuous fun (q : Quaternion ℝ) => q.im

instance Quaternion.instCompleteSpaceReal : CompleteSpace (Quaternion ℝ)

@[simp]

theorem Quaternion.hasSum_coe {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} {r : ℝ} : HasSum (fun (a : α) => ↑(f a)) (↑r) L ↔ HasSum f r L

@[simp]

theorem Quaternion.summable_coe {α : Type u_1} {L : SummationFilter α} {f : α → ℝ} : Summable (fun (a : α) => ↑(f a)) L ↔ Summable f L

theorem Quaternion.tsum_coe {α : Type u_1} {L : SummationFilter α} (f : α → ℝ) : ∑'[L] (a : α), ↑(f a) = ↑(∑'[L] (a : α), f a)