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 ℝ (quaternion ℝ)

Equations

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

theorem quaternion.inner_self (a : quaternion ℝ) :

has_inner.inner a a = ⇑quaternion.norm_sq a

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

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

@[protected, instance]

noncomputable def quaternion.inner_product_space :

inner_product_space ℝ (quaternion ℝ)

Equations

quaternion.inner_product_space = inner_product_space.of_core {inner := has_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 ℝ) :

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

@[protected, instance]

def quaternion.norm_one_class :

norm_one_class (quaternion ℝ)

@[simp, norm_cast]

theorem quaternion.norm_coe (a : ℝ) :

∥↑a∥ = ∥a∥

@[simp, norm_cast]

theorem quaternion.nnnorm_coe (a : ℝ) :

∥↑a∥₊ = ∥a∥₊

@[protected, instance]

noncomputable def quaternion.normed_division_ring :

normed_division_ring (quaternion ℝ)

Equations

quaternion.normed_division_ring = {to_has_norm := normed_add_comm_group.to_has_norm (inner_product_space.to_normed_add_comm_group ℝ), to_division_ring := quaternion.division_ring real.linear_ordered_field, to_metric_space := normed_add_comm_group.to_metric_space (inner_product_space.to_normed_add_comm_group ℝ), dist_eq := quaternion.normed_division_ring._proof_1, norm_mul' := quaternion.normed_division_ring._proof_2}

@[protected, instance]

def quaternion.normed_algebra :

normed_algebra ℝ (quaternion ℝ)

Equations

quaternion.normed_algebra = {to_algebra := quaternion.algebra real.comm_ring, norm_smul_le := quaternion.normed_algebra._proof_1}

@[protected, instance]

def quaternion.has_coe :

has_coe ℂ (quaternion ℝ)

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 :

ℂ →ₐ[ℝ ] quaternion ℝ

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