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. Implemented as a structure with four fields: re, im_i, im_j, and im_k.

Equations

• Quaternion.termℍ = Lean.ParserDescr.node `Quaternion.termℍ 1024 (Lean.ParserDescr.symbol "ℍ")

instance Quaternion.instInnerReal : Inner ℝ (Quaternion ℝ)

Equations

• Quaternion.instInnerReal = { inner := fun (a b : Quaternion ℝ) => (a * star b).re }

theorem Quaternion.inner_self (a : Quaternion ℝ) : ⟪a, a⟫_ℝ = Quaternion.normSq a

theorem Quaternion.inner_def (a : Quaternion ℝ) (b : Quaternion ℝ) : ⟪a, b⟫_ℝ = (a * star b).re

noncomputable instance Quaternion.instNormedAddCommGroupReal : NormedAddCommGroup (Quaternion ℝ)

Equations

• Quaternion.instNormedAddCommGroupReal = InnerProductSpace.Core.toNormedAddCommGroup

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

Equations

• One or more equations did not get rendered due to their size.

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

instance Quaternion.instNormOneClassReal : NormOneClass (Quaternion ℝ)

Equations

• Quaternion.instNormOneClassReal = ⋯

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

noncomputable instance Quaternion.instNormedDivisionRingReal : NormedDivisionRing (Quaternion ℝ)

Equations

• Quaternion.instNormedDivisionRingReal = NormedDivisionRing.mk Quaternion.instNormedDivisionRingReal.proof_1 Quaternion.instNormedDivisionRingReal.proof_2

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

Equations

• Quaternion.instNormedAlgebraReal = NormedAlgebra.mk Quaternion.instNormedAlgebraReal.proof_1

instance Quaternion.instCstarRingReal : CstarRing (Quaternion ℝ)

Equations

• Quaternion.instCstarRingReal = ⋯

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

Coercion from ℂ to ℍ.

Equations

• ↑z = { re := z.re, imI := z.im, imJ := 0, imK := 0 }

instance Quaternion.instCoeComplexReal : Coe ℂ (Quaternion ℝ)

Equations

• Quaternion.instCoeComplexReal = { coe := Quaternion.coeComplex }

@[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]

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.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem Quaternion.coe_ofComplex : ⇑Quaternion.ofComplex = Quaternion.coeComplex

theorem Quaternion.norm_piLp_equiv_symm_equivTuple (x : Quaternion ℝ) : ‖(WithLp.equiv 2 (Fin 4 → ℝ)).symm ((Quaternion.equivTuple ℝ) x)‖ = ‖x‖

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

@[simp]

theorem Quaternion.linearIsometryEquivTuple_apply (a : Quaternion ℝ) : Quaternion.linearIsometryEquivTuple a = (WithLp.equiv 2 (Fin 4 → ℝ)).symm ![a.re, a.imI, a.imJ, a.imK]

@[simp]

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

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

QuaternionAlgebra.linearEquivTuple as a LinearIsometryEquiv.

Equations

• One or more equations did not get rendered due to their size.

theorem Quaternion.continuous_coe : Continuous Quaternion.coe

theorem Quaternion.continuous_normSq : Continuous ⇑Quaternion.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 ℝ)

Equations

• Quaternion.instCompleteSpaceReal = ⋯

@[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)) ↔ Summable f

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