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

source

def Quaternion.termℍ :

Lean.ParserDescr

Instances For

source

instance Quaternion.instInnerRealQuaternionInstOneRealInstNegReal :

Inner ℝ (Quaternion ℝ)

source

theorem Quaternion.inner_self (a : Quaternion ℝ) :

inner a a = ↑Quaternion.normSq a

source

theorem Quaternion.inner_def (a : Quaternion ℝ) (b : Quaternion ℝ) :

inner a b = (a * star b).re

source

noncomputable instance Quaternion.instNormedAddCommGroupQuaternionRealInstOneRealInstNegReal :

NormedAddCommGroup (Quaternion ℝ)

source

noncomputable instance Quaternion.instInnerProductSpaceRealQuaternionInstOneRealInstNegRealIsROrCInstNormedAddCommGroupQuaternionRealInstOneRealInstNegReal :

InnerProductSpace ℝ (Quaternion ℝ)

source

theorem Quaternion.normSq_eq_norm_mul_self (a : Quaternion ℝ) :

↑Quaternion.normSq a = ‖a‖ * ‖a‖

source

instance Quaternion.instNormOneClassQuaternionRealInstOneRealInstNegRealToNormInstNormedAddCommGroupQuaternionRealInstOneRealInstNegRealToOneToSemiringToDivisionSemiringInstDivisionRingQuaternionToOneToSemiringToStrictOrderedSemiringToLinearOrderedSemiringToLinearOrderedCommSemiringToLinearOrderedSemifieldToNegToRingToStrictOrderedRingToLinearOrderedRingToLinearOrderedCommRingInstLinearOrderedFieldReal :

NormOneClass (Quaternion ℝ)

source

@[simp]

theorem Quaternion.norm_coe (a : ℝ) :

‖↑a‖ = ‖a‖

source

@[simp]

theorem Quaternion.nnnorm_coe (a : ℝ) :

‖↑a‖₊ = ‖a‖₊

source

@[simp]

theorem Quaternion.norm_star (a : Quaternion ℝ) :

‖star a‖ = ‖a‖

source

@[simp]

theorem Quaternion.nnnorm_star (a : Quaternion ℝ) :

‖star a‖₊ = ‖a‖₊

source

noncomputable instance Quaternion.instNormedDivisionRingQuaternionRealInstOneRealInstNegReal :

NormedDivisionRing (Quaternion ℝ)

source

noncomputable instance Quaternion.instNormedAlgebraRealQuaternionInstOneRealInstNegRealNormedFieldToSeminormedRingToNormedRingInstNormedDivisionRingQuaternionRealInstOneRealInstNegReal :

NormedAlgebra ℝ (Quaternion ℝ)

source

instance Quaternion.instCstarRingQuaternionRealInstOneRealInstNegRealToNonUnitalNormedRingToNormedRingInstNormedDivisionRingQuaternionRealInstOneRealInstNegRealInstStarRingQuaternionToOneToSemiringToCommSemiringToNegToRingToNonUnitalNonAssocSemiringToNonUnitalNonAssocRingToNonAssocRingInstRingCommRing :

CstarRing (Quaternion ℝ)

source

def Quaternion.coeComplex (z : ℂ) :

Quaternion ℝ

Coercion from ℂ to ℍ.

Instances For

source

instance Quaternion.instCoeComplexQuaternionRealInstOneRealInstNegReal :

Coe ℂ (Quaternion ℝ)

source

@[simp]

theorem Quaternion.coeComplex_re (z : ℂ) :

(↑z).re = z.re

source

@[simp]

theorem Quaternion.coeComplex_imI (z : ℂ) :

(↑z).imI = z.im

source

@[simp]

theorem Quaternion.coeComplex_imJ (z : ℂ) :

(↑z).imJ = 0

source

@[simp]

theorem Quaternion.coeComplex_imK (z : ℂ) :

(↑z).imK = 0

source

@[simp]

theorem Quaternion.coeComplex_add (z : ℂ) (w : ℂ) :

↑(z + w) = ↑z + ↑w

source

@[simp]

theorem Quaternion.coeComplex_mul (z : ℂ) (w : ℂ) :

↑(z * w) = ↑z * ↑w

source

@[simp]

theorem Quaternion.coeComplex_zero :

↑0 = 0

source

@[simp]

theorem Quaternion.coeComplex_one :

↑1 = 1

source

@[simp]

theorem Quaternion.coe_real_complex_mul (r : ℝ) (z : ℂ) :

↑(r • z) = ↑r * ↑z

source

@[simp]

theorem Quaternion.coeComplex_coe (r : ℝ) :

↑↑r = ↑r

source

def Quaternion.ofComplex :

ℂ →ₐ[ℝ ] Quaternion ℝ

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

Instances For

source

@[simp]

theorem Quaternion.coe_ofComplex :

↑Quaternion.ofComplex = Quaternion.coeComplex

source

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.

source

@[simp]

theorem Quaternion.linearIsometryEquivTuple_apply (a : Quaternion ℝ) :

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

source

@[simp]

theorem Quaternion.linearIsometryEquivTuple_symm_apply (a : EuclideanSpace ℝ (Fin 4)) :

↑(LinearIsometryEquiv.symm Quaternion.linearIsometryEquivTuple) a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }

source

noncomputable def Quaternion.linearIsometryEquivTuple :

Quaternion ℝ ≃ₗᵢ[ℝ ] EuclideanSpace ℝ (Fin 4)

QuaternionAlgebra.linearEquivTuple as a LinearIsometryEquiv.

Instances For

source

theorem Quaternion.continuous_coe :

Continuous Quaternion.coe

source

theorem Quaternion.continuous_normSq :

Continuous ↑Quaternion.normSq

source

theorem Quaternion.continuous_re :

Continuous fun q => q.re

source

theorem Quaternion.continuous_imI :

Continuous fun q => q.imI

source

theorem Quaternion.continuous_imJ :

Continuous fun q => q.imJ

source

theorem Quaternion.continuous_imK :

Continuous fun q => q.imK

source

theorem Quaternion.continuous_im :

Continuous fun q => Quaternion.im q

source

instance Quaternion.instCompleteSpaceQuaternionRealInstOneRealInstNegRealToUniformSpaceToPseudoMetricSpaceToSeminormedRingToNormedRingInstNormedDivisionRingQuaternionRealInstOneRealInstNegReal :

CompleteSpace (Quaternion ℝ)

source

@[simp]

theorem Quaternion.hasSum_coe {α : Type u_1} {f : α → ℝ} {r : ℝ} :

HasSum (fun a => ↑(f a)) ↑r ↔ HasSum f r

source

@[simp]

theorem Quaternion.summable_coe {α : Type u_1} {f : α → ℝ} :

(Summable fun a => ↑(f a)) ↔ Summable f

source

theorem Quaternion.tsum_coe {α : Type u_1} (f : α → ℝ) :

∑' (a : α), ↑(f a) = ↑(∑' (a : α), f a)