mathlib3 documentation

analysis.quaternion

Quaternions as a normed algebra #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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_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 * has_star.star 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 * has_star.star b).re

@[protected, instance]

noncomputable def quaternion.normed_add_comm_group :

normed_add_comm_group (quaternion ℝ)

Equations

quaternion.normed_add_comm_group = inner_product_space.core.to_normed_add_comm_group

@[protected, instance]

noncomputable def quaternion.inner_product_space :

inner_product_space ℝ (quaternion ℝ)

Equations

quaternion.inner_product_space = inner_product_space.of_core {to_has_inner := infer_instance quaternion.has_inner, conj_symm := quaternion.normed_add_comm_group._proof_1, nonneg_re := quaternion.normed_add_comm_group._proof_2, definite := quaternion.normed_add_comm_group._proof_3, add_left := quaternion.normed_add_comm_group._proof_4, smul_left := quaternion.normed_add_comm_group._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‖₊

@[simp]

theorem quaternion.norm_star (a : quaternion ℝ) :

‖has_star.star a‖ = ‖a‖

@[simp]

theorem quaternion.nnnorm_star (a : quaternion ℝ) :

‖has_star.star 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 quaternion.normed_add_comm_group, to_division_ring := quaternion.division_ring real.linear_ordered_field, to_metric_space := normed_add_comm_group.to_metric_space quaternion.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 (algebra.id ℝ), norm_smul_le := quaternion.normed_algebra._proof_1}

@[protected, instance]

def quaternion.cstar_ring :

cstar_ring (quaternion ℝ)

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

theorem quaternion.norm_pi_Lp_equiv_symm_equiv_tuple (x : quaternion ℝ) :

‖⇑((pi_Lp.equiv 2 (λ (_x : fin 4), ℝ)).symm) (⇑(quaternion.equiv_tuple ℝ) x)‖ = ‖x‖

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

@[simp]

theorem quaternion.linear_isometry_equiv_tuple_symm_apply (a : euclidean_space ℝ (fin 4)) :

⇑(quaternion.linear_isometry_equiv_tuple.symm) a = {re := a 0, im_i := a 1, im_j := a 2, im_k := a 3}

@[simp]

theorem quaternion.linear_isometry_equiv_tuple_apply (a : quaternion ℝ) :

⇑quaternion.linear_isometry_equiv_tuple a = ⇑((pi_Lp.equiv 2 (λ (_x : fin 4), ℝ)).symm) ![a.re, a.im_i, a.im_j, a.im_k]

noncomputable def quaternion.linear_isometry_equiv_tuple :

quaternion ℝ ≃ₗᵢ[ℝ ] euclidean_space ℝ (fin 4)

quaternion_algebra.linear_equiv_tuple as a linear_isometry_equiv.

Equations

quaternion.linear_isometry_equiv_tuple = {to_linear_equiv := {to_fun := λ (a : quaternion ℝ), ⇑((pi_Lp.equiv 2 (λ (_x : fin 4), ℝ)).symm) ![a.re, a.im_i, a.im_j, a.im_k], map_add' := quaternion.linear_isometry_equiv_tuple._proof_1, map_smul' := quaternion.linear_isometry_equiv_tuple._proof_2, inv_fun := λ (a : euclidean_space ℝ (fin 4)), {re := a 0, im_i := a 1, im_j := a 2, im_k := a 3}, left_inv := quaternion.linear_isometry_equiv_tuple._proof_5, right_inv := quaternion.linear_isometry_equiv_tuple._proof_6}, norm_map' := quaternion.norm_pi_Lp_equiv_symm_equiv_tuple}

@[continuity]

theorem quaternion.continuous_coe :

@[continuity]

theorem quaternion.continuous_norm_sq :

continuous ⇑quaternion.norm_sq

@[continuity]

theorem quaternion.continuous_re :

continuous (λ (q : quaternion ℝ), q.re)

@[continuity]

theorem quaternion.continuous_im_i :

continuous (λ (q : quaternion ℝ), q.im_i)

@[continuity]

theorem quaternion.continuous_im_j :

continuous (λ (q : quaternion ℝ), q.im_j)

@[continuity]

theorem quaternion.continuous_im_k :

continuous (λ (q : quaternion ℝ), q.im_k)

@[continuity]

theorem quaternion.continuous_im :

continuous (λ (q : quaternion ℝ), q.im)

@[protected, instance]

def quaternion.complete_space :

complete_space (quaternion ℝ)

@[simp, norm_cast]

theorem quaternion.has_sum_coe {α : Type u_1} {f : α → ℝ} {r : ℝ} :

has_sum (λ (a : α), ↑(f a)) ↑r ↔ has_sum f r

@[simp, norm_cast]

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

summable (λ (a : α), ↑(f a)) ↔ summable f

@[norm_cast]

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

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