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
,b
quaternion 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
- 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
.
Instances for quaternion_algebra
- quaternion_algebra.has_sizeof_inst
- quaternion_algebra.has_coe_t
- quaternion_algebra.has_zero
- quaternion_algebra.inhabited
- quaternion_algebra.has_one
- quaternion_algebra.has_add
- quaternion_algebra.has_neg
- quaternion_algebra.has_sub
- quaternion_algebra.has_mul
- quaternion_algebra.add_comm_group
- quaternion_algebra.add_group_with_one
- quaternion_algebra.ring
- quaternion_algebra.algebra
- quaternion_algebra.star_ring
The equivalence between a quaternion algebra over R and R × R × R × R.
Equations
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 : quaternion_algebra 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}}
Equations
- quaternion_algebra.add_comm_group = {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 := _, zsmul := zsmul_rec {neg := has_neg.neg quaternion_algebra.has_neg}, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _}
Equations
- quaternion_algebra.add_group_with_one = {int_cast := λ (n : ℤ), ↑↑n, add := add_comm_group.add quaternion_algebra.add_comm_group, add_assoc := _, zero := add_comm_group.zero quaternion_algebra.add_comm_group, zero_add := _, add_zero := _, nsmul := add_comm_group.nsmul quaternion_algebra.add_comm_group, nsmul_zero' := _, nsmul_succ' := _, neg := add_comm_group.neg quaternion_algebra.add_comm_group, sub := add_comm_group.sub quaternion_algebra.add_comm_group, sub_eq_add_neg := _, zsmul := add_comm_group.zsmul quaternion_algebra.add_comm_group, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, nat_cast := λ (n : ℕ), ↑↑n, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _}
Equations
- quaternion_algebra.ring = {add := has_add.add quaternion_algebra.has_add, add_assoc := _, zero := add_group_with_one.zero quaternion_algebra.add_group_with_one, zero_add := _, add_zero := _, nsmul := add_group_with_one.nsmul quaternion_algebra.add_group_with_one, nsmul_zero' := _, nsmul_succ' := _, neg := add_group_with_one.neg quaternion_algebra.add_group_with_one, sub := add_group_with_one.sub quaternion_algebra.add_group_with_one, sub_eq_add_neg := _, zsmul := add_group_with_one.zsmul quaternion_algebra.add_group_with_one, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := add_group_with_one.int_cast quaternion_algebra.add_group_with_one, nat_cast := add_group_with_one.nat_cast quaternion_algebra.add_group_with_one, one := 1, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := has_mul.mul quaternion_algebra.has_mul, mul_assoc := _, one_mul := _, mul_one := _, npow := npow_rec {mul := has_mul.mul quaternion_algebra.has_mul}, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _}
Equations
- quaternion_algebra.algebra = {to_has_smul := {smul := λ (r : R) (a : quaternion_algebra R c₁ c₂), {re := r * a.re, im_i := r * a.im_i, im_j := r * a.im_j, im_k := r * a.im_k}}, to_ring_hom := {to_fun := coe coe_to_lift, map_one' := _, map_mul' := _, map_zero' := _, map_add' := _}, commutes' := _, smul_def' := _}
quaternion_algebra.re
as a linear_map
Equations
- quaternion_algebra.re_lm R c₁ c₂ = {to_fun := quaternion_algebra.re c₂, map_add' := _, map_smul' := _}
quaternion_algebra.im_i
as a linear_map
Equations
- quaternion_algebra.im_i_lm R c₁ c₂ = {to_fun := quaternion_algebra.im_i c₂, map_add' := _, map_smul' := _}
quaternion_algebra.im_j
as a linear_map
Equations
- quaternion_algebra.im_j_lm R c₁ c₂ = {to_fun := quaternion_algebra.im_j c₂, map_add' := _, map_smul' := _}
quaternion_algebra.im_k
as a linear_map
Equations
- quaternion_algebra.im_k_lm R c₁ c₂ = {to_fun := quaternion_algebra.im_k c₂, map_add' := _, map_smul' := _}
Quaternion conjugate.
Equations
- quaternion_algebra.star_ring = {to_star_semigroup := {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_ae = {to_fun := mul_opposite.op ∘ ⇑quaternion_algebra.conj, inv_fun := ⇑quaternion_algebra.conj ∘ mul_opposite.unop, left_inv := _, right_inv := _, map_mul' := _, map_add' := _, commutes' := _}
Space of quaternions over a type. Implemented as a structure with four fields:
re
, im_i
, im_j
, and im_k
.
Equations
- quaternion R = quaternion_algebra R (-1) (-1)
Instances for quaternion
- quaternion.has_coe_t
- quaternion.ring
- quaternion.inhabited
- quaternion.algebra
- quaternion.star_ring
- quaternion.nontrivial
- quaternion.is_domain
- quaternion.has_inv
- quaternion.division_ring
- quaternion.has_inner
- quaternion.inner_product_space
- quaternion.norm_one_class
- quaternion.normed_division_ring
- quaternion.normed_algebra
- quaternion.has_coe
The equivalence between the quaternions over R and R × R × R × R.
Equations
- quaternion.equiv_prod R = quaternion_algebra.equiv_prod (-1) (-1)
Equations
Equations
Quaternion conjugate.
Equations
Alias of quaternion.commute_conj_conj
.
Quaternion conjugate as an alg_equiv
to the opposite ring.
Equations
Square of the norm.
Equations
- quaternion.norm_sq = {to_fun := λ (a : quaternion R), (a * ⇑quaternion.conj a).re, map_zero' := _, map_one' := _, map_mul' := _}
Equations
- quaternion.has_inv = {inv := λ (a : quaternion R), (⇑quaternion.norm_sq a)⁻¹ • ⇑quaternion.conj a}
Equations
- quaternion.division_ring = {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 := _, zsmul := ring.zsmul quaternion.ring, zsmul_zero' := _, zsmul_succ' := _, zsmul_neg' := _, add_left_neg := _, add_comm := _, int_cast := ring.int_cast quaternion.ring, nat_cast := ring.nat_cast quaternion.ring, one := ring.one quaternion.ring, nat_cast_zero := _, nat_cast_succ := _, int_cast_of_nat := _, int_cast_neg_succ_of_nat := _, mul := ring.mul quaternion.ring, mul_assoc := _, one_mul := _, mul_one := _, npow := ring.npow quaternion.ring, npow_zero' := _, npow_succ' := _, left_distrib := _, right_distrib := _, inv := has_inv.inv quaternion.has_inv, div := div_inv_monoid.div._default ring.mul quaternion.division_ring._proof_23 ring.one quaternion.division_ring._proof_24 quaternion.division_ring._proof_25 ring.npow quaternion.division_ring._proof_26 quaternion.division_ring._proof_27 has_inv.inv, div_eq_mul_inv := _, zpow := div_inv_monoid.zpow._default ring.mul quaternion.division_ring._proof_29 ring.one quaternion.division_ring._proof_30 quaternion.division_ring._proof_31 ring.npow quaternion.division_ring._proof_32 quaternion.division_ring._proof_33 has_inv.inv, zpow_zero' := _, zpow_succ' := _, zpow_neg' := _, exists_pair_ne := _, rat_cast := rat.cast_rec (div_inv_monoid.to_has_inv (quaternion R)), mul_inv_cancel := _, inv_zero := _, rat_cast_mk := _, qsmul := qsmul_rec rat.cast_rec (distrib.to_has_mul (quaternion R)), qsmul_eq_mul' := _}
The cardinality of a quaternion algebra, as a type.
The cardinality of a quaternion algebra, as a set.
The cardinality of the quaternions, as a type.
The cardinality of the quaternions, as a set.