Documentation

TauCeti.Algebra.CayleyDickson.Quaternion

The octonions as the Cayley–Dickson double of the quaternions #

The Cayley–Dickson double CayleyDickson ℍ[R] of Hamilton's quaternions over a commutative ring R is a free R-module of rank eight with a bilinear, in general nonassociative, product ⟨a, b⟩ * ⟨c, d⟩ = ⟨a * c - star d * b, d * a + b * star c⟩ and the involution star ⟨a, b⟩ = ⟨star a, -b⟩. For R = ℝ it is the algebra of octonions, the eight-dimensional real division algebra, TauCeti.DivisionOctonionReal; this is its compact real form, unlike the split octonions TauCeti.Octonion ℝ.

This file proves the composition-algebra identities of the double over an arbitrary commutative ring; over a field of characteristic other than two, where the norm is nondegenerate, they make the double a composition algebra. Its norm N ⟨a, b⟩ = N a + N b, the sum of the quaternion norms, and its trace T ⟨a, b⟩ = 2 re a satisfy

Over a linearly ordered ring the norm is positive definite, so the double has no zero divisors, and over a linearly ordered field every nonzero x has the two-sided inverse x⁻¹ = (N x)⁻¹ • star x, for which both cancellation laws hold on either side.

Main definitions #

Main results #

Implementation notes #

The polynomial identities of the double are proved in coordinates: ext splits an equation into the four real and imaginary parts of each of the two quaternion coordinates, the quaternion product and conjugation are expanded by their simp lemmas, and ring closes the resulting polynomial identity over R. This works over every commutative ring, with no hypothesis on 2, and the inverse properties and the alternative laws are uniform instances of it.

References #

Scalars #

The instance SMulCommClass R (CayleyDickson A) (CayleyDickson A) of TauCeti.Algebra.CayleyDickson.Basic asks for a StarModule, which needs an involution on the scalars; a general commutative ring carries none, so the double of a quaternion algebra gets it here directly, from QuaternionAlgebra.star_smul.

source
instance TauCeti.CayleyDickson.instSMulCommClassQuaternionAlgebra {R : Type u_1} [CommRing R] {c₁ c₂ c₃ : R} :
SMulCommClass R (CayleyDickson (QuaternionAlgebra R c₁ c₂ c₃)) (CayleyDickson (QuaternionAlgebra R c₁ c₂ c₃))

Scalars commute with left multiplication in the double of a quaternion algebra over any commutative ring.

The norm and the trace #

source
def TauCeti.CayleyDickson.normSq {R : Type u_1} [CommRing R] :
CayleyDickson (Quaternion R) →*₀ R

The norm of the double of the quaternions, N ⟨a, b⟩ = N a + N b, the sum of the quaternion norms of the two coordinates. It is multiplicative over every commutative ring R; over a field of characteristic other than two it is also nondegenerate, so the double is a composition algebra.

Instances For
    source
    theorem TauCeti.CayleyDickson.normSq_def {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
    normSq x = Quaternion.normSq x.fst + Quaternion.normSq x.snd
    source
    theorem TauCeti.CayleyDickson.normSq_mul {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
    normSq (x * y) = normSq x * normSq y

    The norm is multiplicative: this is Degen's eight-square identity.

    source
    @[simp]
    theorem TauCeti.CayleyDickson.normSq_star {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
    normSq (star x) = normSq x
    source
    @[simp]
    theorem TauCeti.CayleyDickson.normSq_neg {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
    normSq (-x) = normSq x
    source
    theorem TauCeti.CayleyDickson.normSq_smul {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) (r : R) :
    normSq (r • x) = r ^ 2 * normSq x
    source
    def TauCeti.CayleyDickson.trace {R : Type u_1} [CommRing R] :
    CayleyDickson (Quaternion R) →ₗ[R] R

    The trace of the double of the quaternions, T ⟨a, b⟩ = 2 re a.

    Instances For
      source
      @[simp]
      theorem TauCeti.CayleyDickson.trace_apply {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      trace x = 2 * x.fst.re
      source
      theorem TauCeti.CayleyDickson.trace_one {R : Type u_1} [CommRing R] :
      trace 1 = 2

      The trace of 1 is 2. Not a simp lemma, because TauCeti.CayleyDickson.trace_apply already takes its left-hand side apart.

      source
      theorem TauCeti.CayleyDickson.trace_star {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      trace (star x) = trace x

      Conjugation preserves the trace. Not a simp lemma, for the same reason as TauCeti.CayleyDickson.trace_one.

      source
      theorem TauCeti.CayleyDickson.trace_surjective {R : Type u_1} [CommRing R] [Invertible 2] :
      Function.Surjective ⇑trace

      When 2 is invertible, the trace is onto: T (r • ⅟2 • 1) = r.

      source
      theorem TauCeti.CayleyDickson.trace_mul_comm {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      trace (x * y) = trace (y * x)

      The trace is symmetric in a product: T (x * y) = T (y * x).

      source
      theorem TauCeti.CayleyDickson.trace_mul_assoc {R : Type u_1} [CommRing R] (x y z : CayleyDickson (Quaternion R)) :
      trace (x * y * z) = trace (x * (y * z))

      The trace is associative in a triple product: T ((x * y) * z) = T (x * (y * z)), so the trace of a product of three octonions does not depend on how it is bracketed.

      source
      theorem TauCeti.CayleyDickson.trace_mul_cycle {R : Type u_1} [CommRing R] (x y z : CayleyDickson (Quaternion R)) :
      trace (x * y * z) = trace (z * x * y)

      The trace is invariant under cyclic permutation of a triple product.

      source
      theorem TauCeti.CayleyDickson.star_smul {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) (r : R) :
      star (r • x) = r • star x

      Scalars pass through the involution of the double. This is the StarModule law, which cannot be an instance here because a general commutative ring carries no involution.

      The norm and the trace as products and sums with the involution #

      source
      theorem TauCeti.CayleyDickson.self_mul_star {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      x * star x = normSq x • 1

      An element times its conjugate is its norm.

      source
      theorem TauCeti.CayleyDickson.trace_mul_star_comm {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      trace (x * star y) = trace (y * star x)

      The trace pairing T (x * star y) is symmetric, since conjugation reverses products and preserves the trace.

      source
      theorem TauCeti.CayleyDickson.trace_mul_star_self {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      trace (x * star x) = 2 * normSq x

      The trace of an element times its conjugate is twice its norm.

      source
      theorem TauCeti.CayleyDickson.star_mul_self {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      star x * x = normSq x • 1

      The conjugate of an element times the element is its norm.

      source
      theorem TauCeti.CayleyDickson.self_add_star {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      x + star x = trace x • 1

      An element plus its conjugate is its trace.

      source
      theorem TauCeti.CayleyDickson.star_add_self {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      star x + x = trace x • 1

      The conjugate of an element plus the element is its trace.

      source
      theorem TauCeti.CayleyDickson.star_eq_trace_smul_one_sub {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      star x = trace x • 1 - x

      Conjugation is x ↦ T x • 1 - x.

      source
      theorem TauCeti.CayleyDickson.mul_self {R : Type u_1} [CommRing R] (x : CayleyDickson (Quaternion R)) :
      x * x = trace x • x - normSq x • 1

      The rank-two equation x * x = T x • x - N x • 1: every element of the double is a root of the quadratic polynomial X ^ 2 - T x * X + N x.

      source
      theorem TauCeti.CayleyDickson.mul_add_mul_comm {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * y + y * x = trace y • x + trace x • y + (normSq x + normSq y - normSq (x + y)) • 1

      The polarization of the rank-two equation a * a = T a • a - N a • 1 at x and y: the symmetrized product x * y + y * x lies in the span of 1, x and y.

      source
      theorem TauCeti.CayleyDickson.star_mem_of_one_mem {R : Type u_1} [CommRing R] {S : Type u_2} [SetLike S (CayleyDickson (Quaternion R))] [AddSubgroupClass S (CayleyDickson (Quaternion R))] [SMulMemClass S R (CayleyDickson (Quaternion R))] {s : S} {a : CayleyDickson (Quaternion R)} (h₁ : 1 ∈ s) (ha : a ∈ s) :
      star a ∈ s

      A submodule of the double of the quaternions that contains 1 is closed under conjugation, as star a = T a • 1 - a.

      The inverse properties #

      source
      theorem TauCeti.CayleyDickson.star_mul_mul_left {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      star x * (x * y) = normSq x • y

      Multiplying on the left by an element and then by its conjugate is multiplication by its norm.

      source
      theorem TauCeti.CayleyDickson.mul_star_mul_left {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * (star x * y) = normSq x • y

      Multiplying on the left by the conjugate of an element and then by the element is multiplication by its norm.

      source
      theorem TauCeti.CayleyDickson.mul_mul_star_right {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * y * star y = normSq y • x

      Multiplying on the right by an element and then by its conjugate is multiplication by its norm.

      source
      theorem TauCeti.CayleyDickson.mul_star_mul_right {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * star y * y = normSq y • x

      Multiplying on the right by the conjugate of an element and then by the element is multiplication by its norm.

      The alternative and flexible laws #

      source
      theorem TauCeti.CayleyDickson.left_alternative {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * x * y = x * (x * y)

      The left alternative law of the octonions.

      source
      theorem TauCeti.CayleyDickson.right_alternative {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * y * y = x * (y * y)

      The right alternative law of the octonions.

      source
      theorem TauCeti.CayleyDickson.flexible {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      x * y * x = x * (y * x)

      The flexible law of the octonions.

      Real parts of products #

      source
      theorem TauCeti.CayleyDickson.re_mul_comm {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      (x * y).fst.re = (y * x).fst.re

      The real part of a product does not depend on the order of the factors.

      source
      theorem TauCeti.CayleyDickson.re_mul_mul {R : Type u_1} [CommRing R] (x y z : CayleyDickson (Quaternion R)) :
      (x * y * z).fst.re = (x * (y * z)).fst.re

      The real part of a triple product does not depend on how it is bracketed.

      source
      theorem TauCeti.CayleyDickson.normSq_add {R : Type u_1} [CommRing R] (x y : CayleyDickson (Quaternion R)) :
      normSq (x + y) = normSq x + normSq y + 2 * (x * star y).fst.re

      The norm of a sum is the sum of the norms plus twice the real part of x * star y.

      Definiteness of the norm #

      source
      theorem TauCeti.CayleyDickson.normSq_nonneg {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} :
      0 ≤ normSq x
      source
      @[simp]
      theorem TauCeti.CayleyDickson.normSq_eq_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} :
      normSq x = 0 ↔ x = 0

      The norm is definite: only 0 has norm zero.

      source
      theorem TauCeti.CayleyDickson.normSq_ne_zero {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} :
      normSq x ≠ 0 ↔ x ≠ 0
      source
      @[simp]
      theorem TauCeti.CayleyDickson.normSq_pos {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} :
      0 < normSq x ↔ x ≠ 0
      source
      instance TauCeti.CayleyDickson.instNoZeroDivisorsQuaternion {R : Type u_1} [CommRing R] [LinearOrder R] [IsStrictOrderedRing R] :
      NoZeroDivisors (CayleyDickson (Quaternion R))

      Over a linearly ordered ring the double of the quaternions has no zero divisors, the norm being multiplicative and definite.

      Inverses #

      source
      @[instance_reducible]
      instance TauCeti.CayleyDickson.instInvQuaternion {R : Type u_1} [Field R] :
      Inv (CayleyDickson (Quaternion R))

      The inverse x⁻¹ = (N x)⁻¹ • star x of an element of the double of the quaternions over a field, a two-sided inverse of every nonzero element over a linearly ordered field.

      source
      theorem TauCeti.CayleyDickson.inv_def {R : Type u_1} [Field R] (x : CayleyDickson (Quaternion R)) :
      x⁻¹ = (normSq x)⁻¹ • star x
      source
      @[simp]
      theorem TauCeti.CayleyDickson.inv_zero {R : Type u_1} [Field R] :
      0⁻¹ = 0
      source
      @[simp]
      theorem TauCeti.CayleyDickson.mul_inv_cancel₀ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} (hx : x ≠ 0) :
      x * x⁻¹ = 1

      Over a linearly ordered field, the inverse of a nonzero element is a right inverse.

      source
      @[simp]
      theorem TauCeti.CayleyDickson.inv_mul_cancel₀ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} (hx : x ≠ 0) :
      x⁻¹ * x = 1

      Over a linearly ordered field, the inverse of a nonzero element is a left inverse.

      source
      @[simp]
      theorem TauCeti.CayleyDickson.inv_mul_cancel_left₀ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} (y : CayleyDickson (Quaternion R)) (hx : x ≠ 0) :
      x⁻¹ * (x * y) = y

      Left multiplication by a nonzero element is undone by left multiplication by its inverse.

      source
      @[simp]
      theorem TauCeti.CayleyDickson.mul_inv_cancel_left₀ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} (y : CayleyDickson (Quaternion R)) (hx : x ≠ 0) :
      x * (x⁻¹ * y) = y

      Left multiplication by the inverse of a nonzero element is undone by left multiplication by the element.

      source
      @[simp]
      theorem TauCeti.CayleyDickson.mul_inv_cancel_right₀ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} (y : CayleyDickson (Quaternion R)) (hx : x ≠ 0) :
      y * x * x⁻¹ = y

      Right multiplication by a nonzero element is undone by right multiplication by its inverse.

      source
      @[simp]
      theorem TauCeti.CayleyDickson.inv_mul_cancel_right₀ {R : Type u_1} [Field R] [LinearOrder R] [IsStrictOrderedRing R] {x : CayleyDickson (Quaternion R)} (y : CayleyDickson (Quaternion R)) (hx : x ≠ 0) :
      y * x⁻¹ * x = y

      Right multiplication by the inverse of a nonzero element is undone by right multiplication by the element.

      source
      @[reducible, inline]
      abbrev TauCeti.DivisionOctonionReal :
      Type

      The real octonions, the eight-dimensional real division algebra, realized as the Cayley–Dickson double of the quaternions ℍ[ℝ]. Its involution star ⟨a, b⟩ = ⟨star a, -b⟩ is positive: x * star x = normSq x • 1, with 0 < normSq x for every nonzero x. It is the compact real form of the octonions, not the split form TauCeti.Octonion ℝ.

      Instances For
        source
        theorem TauCeti.DivisionOctonionReal.finrank_eq_eight :
        Module.finrank ℝ DivisionOctonionReal = 8

        The real octonions are eight-dimensional.

        source
        theorem TauCeti.DivisionOctonionReal.exists_mul_mul_ne :
        ∃ (x : DivisionOctonionReal) (y : DivisionOctonionReal) (z : DivisionOctonionReal), x * y * z ≠ x * (y * z)

        The real octonions are not associative: for the quaternion units i and j and the doubling unit l = ⟨0, 1⟩, the products (i * j) * l = ⟨0, k⟩ and i * (j * l) = ⟨0, -k⟩ differ.