mathlib documentation

analysis.quaternion

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 ℝ.

Notation #

The following notation is available with open_locale quaternion:

ℍ : quaternions

Tags #

quaternion, normed ring, normed space, normed algebra

@[protected, instance]

def quaternion.has_inner :

has_inner ℝ ℍ[ℝ ]

Equations

quaternion.has_inner = {inner := λ (a b : ℍ[ℝ ]), (a * ⇑quaternion.conj b).re}

theorem quaternion.inner_self (a : ℍ[ℝ ]) :

inner a a = ⇑quaternion.norm_sq a

theorem quaternion.inner_def (a b : ℍ[ℝ ]) :

inner a b = (a * ⇑quaternion.conj b).re

@[protected, instance]

noncomputable def quaternion.inner_product_space :

inner_product_space ℝ ℍ[ℝ ]

Equations

quaternion.inner_product_space = inner_product_space.of_core {inner := inner quaternion.has_inner, conj_sym := quaternion.inner_product_space._proof_1, nonneg_re := quaternion.inner_product_space._proof_2, definite := quaternion.inner_product_space._proof_3, add_left := quaternion.inner_product_space._proof_4, smul_left := quaternion.inner_product_space._proof_5}

theorem quaternion.norm_sq_eq_norm_sq (a : ℍ[ℝ ]) :

⇑quaternion.norm_sq a = ∥a∥ * ∥a∥

@[protected, instance]

def quaternion.norm_one_class :

norm_one_class ℍ[ℝ ]

@[simp]

theorem quaternion.norm_mul (a b : ℍ[ℝ ]) :

∥a * b∥ = ∥a∥ * ∥b∥

@[simp, norm_cast]

theorem quaternion.norm_coe (a : ℝ) :

∥↑a∥ = ∥a∥

@[protected, instance]

noncomputable def quaternion.normed_ring :

normed_ring ℍ[ℝ ]

Equations

quaternion.normed_ring = {to_has_norm := normed_group.to_has_norm (inner_product_space.to_normed_group ℝ), to_ring := quaternion.ring real.comm_ring, to_metric_space := normed_group.to_metric_space (inner_product_space.to_normed_group ℝ), dist_eq := quaternion.normed_ring._proof_1, norm_mul := quaternion.normed_ring._proof_2}

@[protected, instance]

noncomputable def quaternion.normed_algebra :

normed_algebra ℝ ℍ[ℝ ]

Equations

quaternion.normed_algebra = {to_algebra := quaternion.algebra real.comm_ring, norm_algebra_map_eq := quaternion.norm_coe}

@[protected, instance]

def quaternion.has_coe :

has_coe ℂ ℍ[ℝ ]

Equations

quaternion.has_coe = {coe := λ (z : ℂ), {re := z.re, im_i := z.im, im_j := 0, im_k := 0}}

@[simp, norm_cast]

theorem quaternion.coe_complex_re (z : ℂ) :

@[simp, norm_cast]

theorem quaternion.coe_complex_im_i (z : ℂ) :

↑z.im_i = z.im

@[simp, norm_cast]

theorem quaternion.coe_complex_im_j (z : ℂ) :

@[simp, norm_cast]

theorem quaternion.coe_complex_im_k (z : ℂ) :

@[simp, norm_cast]

theorem quaternion.coe_complex_add (z w : ℂ) :

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

@[simp, norm_cast]

theorem quaternion.coe_complex_mul (z w : ℂ) :

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

@[simp, norm_cast]

theorem quaternion.coe_complex_zero :

↑0 = 0

@[simp, norm_cast]

theorem quaternion.coe_complex_one :

↑1 = 1

@[simp, norm_cast]

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

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

@[simp, norm_cast]

theorem quaternion.coe_complex_coe (r : ℝ) :

def quaternion.of_complex :

ℂ →ₐ[ℝ ] ℍ[ℝ ]

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

Equations

quaternion.of_complex = {to_fun := coe coe_to_lift, map_one' := quaternion.of_complex._proof_1, map_mul' := quaternion.coe_complex_mul, map_zero' := quaternion.of_complex._proof_2, map_add' := quaternion.coe_complex_add, commutes' := quaternion.of_complex._proof_3}

@[simp]

theorem quaternion.coe_of_complex :

⇑quaternion.of_complex = coe