Quaternions #
In this file we define quaternions ℍ[R] over a commutative ring R, and define some
algebraic structures on ℍ[R].
Main definitions #
quaternion_algebra R a b,ℍ[R, a, b]: quaternion algebra with coefficientsa,bquaternion R,ℍ[R]: the space of quaternions, a.k.a.quaternion_algebra R (-1) (-1);quaternion.norm_sq: square of the norm of a quaternion;quaternion.conj: conjugate of a quaternion;
We also define the following algebraic structures on ℍ[R]:
ring ℍ[R, a, b]andalgebra R ℍ[R, a, b]: for any commutative ringR;ring ℍ[R]andalgebra R ℍ[R]: for any commutative ringR;domain ℍ[R]: for a linear ordered commutative ringR;division_algebra ℍ[R]: for a linear ordered fieldR.
Notation #
The following notation is available with open_locale quaternion.
ℍ[R, c₁, c₂]:quaternion_algebra R c₁ c₂ℍ[R]: quaternions overR.
Implementation notes #
We define quaternions over any ring R, not just ℝ to be able to deal with, e.g., integer
or rational quaternions without using real numbers. In particular, all definitions in this file
are computable.
Tags #
quaternion
@[nolint, ext]
- re : R
- im_i : R
- im_j : R
- im_k : R
Quaternion algebra over a type with fixed coefficients $a=i^2$ and $b=j^2$.
Implemented as a structure with four fields: re, im_i, im_j, and im_k.
@[simp]
@[simp]
@[simp]
@[simp]
@[simp, norm_cast]
@[simp]
@[simp]
@[simp]
@[simp]
@[simp, norm_cast]
@[protected, instance]
Multiplication is given by
1 * x = x * 1 = x;i * i = c₁;j * j = c₂;i * j = k,j * i = -k;k * k = -c₁ * c₂;i * k = c₁ * j,k * i =-c₁ * j`;j * k = -c₂ * i, `k * j = c₂ * i`.
Equations
- quaternion_algebra.has_mul = {mul := λ (a b : ℍ[R,c₁,c₂]), {re := (a.re) * b.re + (c₁ * a.im_i) * b.im_i + (c₂ * a.im_j) * b.im_j - ((c₁ * c₂) * a.im_k) * b.im_k, im_i := (a.re) * b.im_i + (a.im_i) * b.re - (c₂ * a.im_j) * b.im_k + (c₂ * a.im_k) * b.im_j, im_j := (a.re) * b.im_j + (c₁ * a.im_i) * b.im_k + (a.im_j) * b.re - (c₁ * a.im_k) * b.im_i, im_k := (a.re) * b.im_k + (a.im_i) * b.im_j - (a.im_j) * b.im_i + (a.im_k) * b.re}}
@[simp]
theorem
quaternion_algebra.mk_mul_mk
{R : Type u_1}
[comm_ring R]
{c₁ c₂ : R}
(a₁ a₂ a₃ a₄ b₁ b₂ b₃ b₄ : R) :
{re := a₁, im_i := a₂, im_j := a₃, im_k := a₄} * {re := b₁, im_i := b₂, im_j := b₃, im_k := b₄} = {re := a₁ * b₁ + (c₁ * a₂) * b₂ + (c₂ * a₃) * b₃ - ((c₁ * c₂) * a₄) * b₄, im_i := a₁ * b₂ + a₂ * b₁ - (c₂ * a₃) * b₄ + (c₂ * a₄) * b₃, im_j := a₁ * b₃ + (c₁ * a₂) * b₄ + a₃ * b₁ - (c₁ * a₄) * b₂, im_k := a₁ * b₄ + a₂ * b₃ - a₃ * b₂ + a₄ * b₁}
@[protected, instance]
Equations
- quaternion_algebra.ring = {add := has_add.add quaternion_algebra.has_add, add_assoc := _, zero := 0, zero_add := _, add_zero := _, nsmul := nsmul_rec {add := has_add.add quaternion_algebra.has_add}, nsmul_zero' := _, nsmul_succ' := _, neg := has_neg.neg quaternion_algebra.has_neg, sub := has_sub.sub quaternion_algebra.has_sub, sub_eq_add_neg := _, gsmul := gsmul_rec {neg := has_neg.neg quaternion_algebra.has_neg}, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := has_mul.mul quaternion_algebra.has_mul, mul_assoc := _, one := 1, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul quaternion_algebra.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
@[protected, instance]
Equations
Quaternion conjugate.
theorem
quaternion_algebra.conj_conj_mul
{R : Type u_1}
[comm_ring R]
{c₁ c₂ : R}
(a b : ℍ[R,c₁,c₂]) :
⇑quaternion_algebra.conj ((⇑quaternion_algebra.conj a) * b) = (⇑quaternion_algebra.conj b) * a
@[simp]
theorem
quaternion_algebra.conj_smul
{R : Type u_1}
[comm_ring R]
{c₁ c₂ : R}
(r : R)
(a : ℍ[R,c₁,c₂]) :
⇑quaternion_algebra.conj (r • a) = r • ⇑quaternion_algebra.conj a
@[simp]
@[protected, instance]
Equations
- quaternion_algebra.star_ring = {to_star_monoid := {to_has_involutive_star := {to_has_star := {star := ⇑quaternion_algebra.conj}, star_involutive := _}, star_mul := _}, star_add := _}
Quaternion conjugate as an alg_equiv to the opposite ring.
Equations
- quaternion_algebra.conj_alg_equiv = {to_fun := opposite.op ∘ ⇑quaternion_algebra.conj, inv_fun := ⇑quaternion_algebra.conj ∘ opposite.unop, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
@[simp]
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[protected, instance]
Equations
@[protected, instance]
@[simp]
Quaternion conjugate.
Equations
@[simp]
@[simp]
@[simp]
theorem
quaternion.conj_add
{R : Type u_1}
[comm_ring R]
(a b : ℍ[R]) :
⇑quaternion.conj (a + b) = ⇑quaternion.conj a + ⇑quaternion.conj b
@[simp]
theorem
quaternion.conj_mul
{R : Type u_1}
[comm_ring R]
(a b : ℍ[R]) :
⇑quaternion.conj (a * b) = (⇑quaternion.conj b) * ⇑quaternion.conj a
theorem
quaternion.conj_conj_mul
{R : Type u_1}
[comm_ring R]
(a b : ℍ[R]) :
⇑quaternion.conj ((⇑quaternion.conj a) * b) = (⇑quaternion.conj b) * a
theorem
quaternion.conj_mul_conj
{R : Type u_1}
[comm_ring R]
(a b : ℍ[R]) :
⇑quaternion.conj (a * ⇑quaternion.conj b) = b * ⇑quaternion.conj a
theorem
quaternion.commute_conj_self
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
commute (⇑quaternion.conj a) a
theorem
quaternion.commute_self_conj
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
commute a (⇑quaternion.conj a)
theorem
quaternion.commute_conj_conj
{R : Type u_1}
[comm_ring R]
{a b : ℍ[R]}
(h : commute a b) :
commute (⇑quaternion.conj a) (⇑quaternion.conj b)
theorem
commute.quaternion_conj
{R : Type u_1}
[comm_ring R]
{a b : ℍ[R]}
(h : commute a b) :
commute (⇑quaternion.conj a) (⇑quaternion.conj b)
Alias of commute_conj_conj.
@[simp]
@[simp]
theorem
quaternion.conj_smul
{R : Type u_1}
[comm_ring R]
(r : R)
(a : ℍ[R]) :
⇑quaternion.conj (r • a) = r • ⇑quaternion.conj a
@[simp]
theorem
quaternion.conj_fixed
{R : Type u_1}
[comm_ring R]
[no_zero_divisors R]
[char_zero R]
{a : ℍ[R]} :
theorem
quaternion.conj_mul_eq_coe
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
(⇑quaternion.conj a) * a = ↑(((⇑quaternion.conj a) * a).re)
theorem
quaternion.mul_conj_eq_coe
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
a * ⇑quaternion.conj a = ↑((a * ⇑quaternion.conj a).re)
@[simp]
@[simp]
theorem
quaternion.conj_sub
{R : Type u_1}
[comm_ring R]
(a b : ℍ[R]) :
⇑quaternion.conj (a - b) = ⇑quaternion.conj a - ⇑quaternion.conj b
Quaternion conjugate as an alg_equiv to the opposite ring.
@[simp]
Square of the norm.
theorem
quaternion.norm_sq_def
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
⇑quaternion.norm_sq a = (a * ⇑quaternion.conj a).re
theorem
quaternion.norm_sq_coe
{R : Type u_1}
[comm_ring R]
(x : R) :
⇑quaternion.norm_sq ↑x = x ^ 2
@[simp]
theorem
quaternion.self_mul_conj
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
a * ⇑quaternion.conj a = ↑(⇑quaternion.norm_sq a)
theorem
quaternion.conj_mul_self
{R : Type u_1}
[comm_ring R]
(a : ℍ[R]) :
(⇑quaternion.conj a) * a = ↑(⇑quaternion.norm_sq a)
theorem
quaternion.coe_norm_sq_add
{R : Type u_1}
[comm_ring R]
(a b : ℍ[R]) :
↑(⇑quaternion.norm_sq (a + b)) = ↑(⇑quaternion.norm_sq a) + a * ⇑quaternion.conj b + b * ⇑quaternion.conj a + ↑(⇑quaternion.norm_sq b)
@[simp]
theorem
quaternion.norm_sq_eq_zero
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : ℍ[R]} :
⇑quaternion.norm_sq a = 0 ↔ a = 0
theorem
quaternion.norm_sq_ne_zero
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : ℍ[R]} :
⇑quaternion.norm_sq a ≠ 0 ↔ a ≠ 0
@[simp]
theorem
quaternion.norm_sq_nonneg
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : ℍ[R]} :
0 ≤ ⇑quaternion.norm_sq a
@[simp]
theorem
quaternion.norm_sq_le_zero
{R : Type u_1}
[linear_ordered_comm_ring R]
{a : ℍ[R]} :
⇑quaternion.norm_sq a ≤ 0 ↔ a = 0
@[protected, instance]
Equations
- quaternion.domain = {add := ring.add quaternion.ring, add_assoc := _, zero := ring.zero quaternion.ring, zero_add := _, add_zero := _, nsmul := ring.nsmul quaternion.ring, nsmul_zero' := _, nsmul_succ' := _, neg := ring.neg quaternion.ring, sub := ring.sub quaternion.ring, sub_eq_add_neg := _, gsmul := ring.gsmul quaternion.ring, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := ring.mul quaternion.ring, mul_assoc := _, one := ring.one quaternion.ring, one_mul := _, mul_one := _, npow := ring.npow quaternion.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, exists_pair_ne := _, eq_zero_or_eq_zero_of_mul_eq_zero := _}
@[protected, instance]
Equations
- quaternion.has_inv = {inv := λ (a : ℍ[R]), (⇑quaternion.norm_sq a)⁻¹ • ⇑quaternion.conj a}
theorem
quaternion.has_inv_inv
{R : Type u_1}
[linear_ordered_field R]
(a : ℍ[R]) :
a⁻¹ = (⇑quaternion.norm_sq a)⁻¹ • ⇑quaternion.conj a
@[protected, instance]
Equations
- quaternion.division_ring = {add := domain.add quaternion.domain, add_assoc := _, zero := domain.zero quaternion.domain, zero_add := _, add_zero := _, nsmul := domain.nsmul quaternion.domain, nsmul_zero' := _, nsmul_succ' := _, neg := domain.neg quaternion.domain, sub := domain.sub quaternion.domain, sub_eq_add_neg := _, gsmul := domain.gsmul quaternion.domain, gsmul_zero' := _, gsmul_succ' := _, gsmul_neg' := _, add_left_neg := _, add_comm := _, mul := domain.mul quaternion.domain, mul_assoc := _, one := domain.one quaternion.domain, one_mul := _, mul_one := _, npow := domain.npow quaternion.domain, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := has_inv.inv quaternion.has_inv, div := div_inv_monoid.div._default domain.mul quaternion.division_ring._proof_19 domain.one quaternion.division_ring._proof_20 quaternion.division_ring._proof_21 domain.npow quaternion.division_ring._proof_22 quaternion.division_ring._proof_23 has_inv.inv, div_eq_mul_inv := _, gpow := div_inv_monoid.gpow._default domain.mul quaternion.division_ring._proof_25 domain.one quaternion.division_ring._proof_26 quaternion.division_ring._proof_27 domain.npow quaternion.division_ring._proof_28 quaternion.division_ring._proof_29 has_inv.inv, gpow_zero' := _, gpow_succ' := _, gpow_neg' := _, exists_pair_ne := _, mul_inv_cancel := _, inv_zero := _}
@[simp]
@[simp]
theorem
quaternion.norm_sq_div
{R : Type u_1}
[linear_ordered_field R]
(a b : ℍ[R]) :
⇑quaternion.norm_sq (a / b) = ⇑quaternion.norm_sq a / ⇑quaternion.norm_sq b