The real Clifford algebras Cliff(p, q) and the base entries of the Bott table

Over ℂ a nondegenerate quadratic form is determined by its rank, so there is one Clifford algebra in each dimension. Over ℝ this fails: a nondegenerate real form is classified by its signature (p, q), and the resulting algebras Cliff(p, q) run through matrix algebras over ℝ, ℂ and ℍ, and products of two copies of such a matrix algebra, in a pattern periodic modulo 8. This file introduces the family of forms that the pattern is indexed by, the coordinate isometries for switching signatures, and the four small entries that fix the indexing convention.

TauCeti.realCliffordForm p q is the diagonal form on Fin (p + q) → ℝ with +1 in the first p coordinates and -1 in the last q, written as a QuadraticMap.weightedSumSquares against the sign vector TauCeti.realCliffordWeight p q. It is nondegenerate (TauCeti.nondegenerate_realCliffordForm), and its Clifford algebra has dimension 2 ^ (p + q) (TauCeti.finrank_cliffordAlgebra_realCliffordForm). The compact form realCliffordForm n 0 is positive definite (TauCeti.posDef_realCliffordForm_zero) and equals the standard sum-of-squares form (TauCeti.realCliffordForm_zero_eq_weightedSumSquares_one). Negating the form swaps the two signature indices through TauCeti.realCliffordFormNegIsometry; its coordinate action is given by TauCeti.realCliffordFormNegIsometry_apply_castAdd and TauCeti.realCliffordFormNegIsometry_apply_natAdd.

The sign convention — generators of the first p coordinates square to +1 — is not universal: sources that make the first generators square to -1 index the periodicity table by (p - q) mod 8 where this one uses (q - p) mod 8. The convention is therefore fixed here by four explicit small identifications:

• Cliff(1,0) ≅ ℝ × ℝ — TauCeti.realCliffordOneZeroEquivProd;
• Cliff(0,1) ≅ ℂ — TauCeti.realCliffordZeroOneEquivComplex;
• Cliff(0,2) ≅ ℍ — TauCeti.realCliffordZeroTwoEquivQuaternion;
• Cliff(1,1) ≅ M₂(ℝ) — TauCeti.realCliffordOneOneEquivMatrix.

The middle two are Mathlib's CliffordAlgebraComplex.equiv and CliffordAlgebraQuaternion.equiv transported along an isometry, since the forms Mathlib uses there are exactly the (0,1) and (0,2) signature forms in disguise. The last is the same transport for the split quaternions ℍ[ℝ,1,-1], followed by their splitting TauCeti.QuaternionAlgebra.oneEquivMatrix. The first is built here from the universal property: a single generator squaring to +1 splits the algebra into two copies of ℝ.

Implementation notes

Cliff(p, q) is spelled CliffordAlgebra (realCliffordForm p q) throughout rather than being given an abbreviation, so that every lemma about a general CliffordAlgebra applies to it without unfolding.

Main definitions

• TauCeti.realCliffordWeight and TauCeti.realCliffordForm: the signature (p, q) sign vector and the diagonal real quadratic form it weights.
• TauCeti.realCliffordFormNegIsometry: the isometry from the negated (p, q) form to the (q, p) form, with coordinate equations ..._pos_of_neg and ..._neg_of_pos.
• TauCeti.CliffordAlgebra.realCliffordEvenToNeg p q: the even-algebra comparison into the Clifford algebra of the negated signature.
• TauCeti.realCliffordSplitIsometry: the shared splitter into two standard signature blocks.
• TauCeti.realCliffordFormCongr: the coordinate isometry between equal signatures.
• TauCeti.realCliffordBlockIsometry: the splitting of the (p, q) form into its positive-definite (p, 0) and negative-definite (0, q) blocks.
• TauCeti.realCliffordPositiveSplitIsometry: the isometry which separates the last positive coordinate from a standard signature form.
• TauCeti.realBottSplitIsometry: the two-coordinate specialization of the same signature splitter, separating a hyperbolic plane.
• TauCeti.realCliffordSignSwitchStandardIsometry: the isometry which puts a sign-switched form with one positive line back into standard signature coordinates.
• TauCeti.realCliffordZeroOneIsometry and TauCeti.realCliffordZeroTwoIsometry: the coordinate isometries used in the complex and quaternion base entries.
• TauCeti.realCliffordOneZeroEquivProd, TauCeti.realCliffordZeroOneEquivComplex, TauCeti.realCliffordZeroTwoEquivQuaternion, TauCeti.realCliffordOneOneEquivMatrix: the four base entries of the Bott table, each with a ..._ι lemma computing it on a generator.

Main results

• TauCeti.equivalent_realSignatureForm_realCliffordForm: the orthogonal-sum and coordinate presentations of the real normal form are isometric.
• TauCeti.nondegenerate_realCliffordForm: the signature forms are nondegenerate.
• TauCeti.isOrtho_realCliffordForm_single: distinct coordinate lines are orthogonal.
• TauCeti.realCliffordForm_zero_eq_weightedSumSquares_one: the compact signature form is the standard real sum-of-squares form.
• TauCeti.finrank_cliffordAlgebra_realCliffordForm: finrank ℝ (CliffordAlgebra (realCliffordForm p q)) = 2 ^ (p + q).

References

• H. B. Lawson, M.-L. Michelsohn, Spin Geometry, Princeton (1989), Chapter I, §4.

The real quadratic form of a signature

def TauCeti.realCliffordWeight (p q : ℕ) (i : Fin (p + q)) : ℝ

The sign vector of signature (p, q): +1 on the first p coordinates of Fin (p + q) and -1 on the last q.

def TauCeti.realCliffordForm (p q : ℕ) : QuadraticForm ℝ (Fin (p + q) → ℝ)

The real quadratic form of signature (p, q): the diagonal form x ↦ ∑ᵢ₌₀^{p-1} xᵢ² - ∑ᵢ₌ₚ^{p+q-1} xᵢ² on Fin (p + q) → ℝ. Its Clifford algebra is the real Clifford algebra Cliff(p, q).

theorem TauCeti.realCliffordForm_def (p q : ℕ) : realCliffordForm p q = QuadraticMap.weightedSumSquares ℝ (realCliffordWeight p q)

The coordinate signature form is the weighted sum of squares for realCliffordWeight.

@[simp]

theorem TauCeti.realCliffordWeight_of_lt {p q : ℕ} {i : Fin (p + q)} (hi : ↑i < p) : realCliffordWeight p q i = 1

@[simp]

theorem TauCeti.realCliffordWeight_of_le {p q : ℕ} {i : Fin (p + q)} (hi : p ≤ ↑i) : realCliffordWeight p q i = -1

theorem TauCeti.equivalent_realSignatureForm_realCliffordForm (p q : ℕ) : QuadraticMap.Equivalent (QuadraticForm.realSignatureForm p q) (realCliffordForm p q)

The orthogonal-sum and coordinate presentations of the real normal form of signature (p, q) are isometric.

@[simp]

theorem TauCeti.realCliffordWeight_mul_self (p q : ℕ) (i : Fin (p + q)) : realCliffordWeight p q i * realCliffordWeight p q i = 1

@[simp]

theorem TauCeti.realCliffordWeight_ne_zero (p q : ℕ) (i : Fin (p + q)) : realCliffordWeight p q i ≠ 0

@[simp]

theorem TauCeti.realCliffordForm_apply (p q : ℕ) (v : Fin (p + q) → ℝ) : (realCliffordForm p q) v = ∑ i : Fin (p + q), realCliffordWeight p q i * (v i * v i)

theorem TauCeti.realCliffordForm_zero_eq_weightedSumSquares_one (n : ℕ) : realCliffordForm n 0 = QuadraticMap.weightedSumSquares ℝ 1

The positive-definite signature form is the standard real sum-of-squares form.

theorem TauCeti.nondegenerate_realCliffordForm (p q : ℕ) : QuadraticMap.Nondegenerate

The signature forms are nondegenerate.

theorem TauCeti.posDef_realCliffordForm_zero (n : ℕ) : QuadraticMap.PosDef (realCliffordForm n 0)

The standard signature form with no negative coordinates is positive definite.

@[simp]

theorem TauCeti.realCliffordForm_apply_single (p q : ℕ) (i : Fin (p + q)) (x : ℝ) : (realCliffordForm p q) (Pi.single i x) = realCliffordWeight p q i * x ^ 2

A coordinate vector Pi.single i x takes the value w * x ^ 2, where w is the signature weight of its coordinate: 1 at the first p coordinates and -1 at the last q.

theorem TauCeti.isOrtho_realCliffordForm_single {p q : ℕ} {i j : Fin (p + q)} (hij : i ≠ j) (x y : ℝ) : QuadraticMap.IsOrtho (realCliffordForm p q) (Pi.single i x) (Pi.single j y)

Distinct coordinate lines are orthogonal for the signature form.

theorem TauCeti.isOrthoᵢ_associated_realCliffordForm (p q : ℕ) : LinearMap.IsOrthoᵢ (QuadraticMap.associated (realCliffordForm p q)) ⇑(Pi.basisFun ℝ (Fin (p + q)))

The coordinate basis is orthogonal for the polar form of the signature form.

@[simp]

theorem TauCeti.realCliffordForm_zero_single_one (n : ℕ) (i : Fin n) : (realCliffordForm n 0) (Pi.single i 1) = 1

Every coordinate unit vector has value one for the compact real Clifford form.

@[simp]

theorem TauCeti.finrank_cliffordAlgebra_realCliffordForm (p q : ℕ) : Module.finrank ℝ (CliffordAlgebra (realCliffordForm p q)) = 2 ^ (p + q)

The real Clifford algebra of signature (p, q) has dimension 2 ^ (p + q), as every Clifford algebra of a space of that dimension does. This is the count that forces the surjections built below to be isomorphisms.

def TauCeti.realCliffordFormNegIsometry (p q : ℕ) : QuadraticMap.IsometryEquiv (-realCliffordForm p q) (realCliffordForm q p)

Negating a real signature form swaps its positive and negative coordinates.

@[simp]

theorem TauCeti.realCliffordFormNegIsometry_apply (p q : ℕ) (x : Fin (p + q) → ℝ) (i : Fin (q + p)) : (realCliffordFormNegIsometry p q) x i = x (finAddFlip i)

realCliffordFormNegIsometry reads each coordinate through the block swap finAddFlip.

theorem TauCeti.realCliffordFormNegIsometry_apply_castAdd (p q : ℕ) (x : Fin (p + q) → ℝ) (i : Fin q) : (realCliffordFormNegIsometry p q) x (Fin.castAdd p i) = x (Fin.natAdd p i)

Negated negative coordinates become positive coordinates under realCliffordFormNegIsometry.

theorem TauCeti.realCliffordFormNegIsometry_apply_natAdd (p q : ℕ) (x : Fin (p + q) → ℝ) (i : Fin p) : (realCliffordFormNegIsometry p q) x (Fin.natAdd q i) = x (Fin.castAdd q i)

Negated positive coordinates become negative coordinates under realCliffordFormNegIsometry.

noncomputable def TauCeti.CliffordAlgebra.realCliffordEvenToNeg (p q : ℕ) : ↥(CliffordAlgebra.even (realCliffordForm p q)) →ₐ[ℝ] CliffordAlgebra (realCliffordForm q p)

The even Clifford algebra of signature (p, q) mapped into the Clifford algebra of signature (q, p), through negation and the signature-coordinate isometry.

theorem TauCeti.CliffordAlgebra.realCliffordEvenToNeg_apply (p q : ℕ) (x : ↥(CliffordAlgebra.even (realCliffordForm p q))) : (realCliffordEvenToNeg p q) x = (CliffordAlgebra.map (realCliffordFormNegIsometry p q).toIsometry) ↑((CliffordAlgebra.evenEquivEvenNeg (realCliffordForm p q)) x)

The even comparison applies negation followed by the signature-coordinate isometry.

@[simp]

theorem TauCeti.CliffordAlgebra.realCliffordEvenToNeg_ι (p q : ℕ) (a b : Fin (p + q) → ℝ) : (realCliffordEvenToNeg p q) (((CliffordAlgebra.even.ι (realCliffordForm p q)).bilin a) b) = -((CliffordAlgebra.ι (realCliffordForm q p)) ((realCliffordFormNegIsometry p q) a) * (CliffordAlgebra.ι (realCliffordForm q p)) ((realCliffordFormNegIsometry p q) b))

An even generator maps to minus the product of the transported vectors.

Standard signature coordinate isometries

def TauCeti.realCliffordSplitIsometry (p₁ p₂ q₁ q₂ : ℕ) : QuadraticMap.IsometryEquiv (realCliffordForm (p₁ + p₂) (q₁ + q₂)) (QuadraticMap.prod (realCliffordForm p₁ q₁) (realCliffordForm p₂ q₂))

Splits a standard real signature form into two standard signature blocks.

@[simp]

theorem TauCeti.realCliffordSplitIsometry_fst_pos (p₁ p₂ q₁ q₂ : ℕ) (x : Fin (p₁ + p₂ + (q₁ + q₂)) → ℝ) (i : Fin p₁) : ((realCliffordSplitIsometry p₁ p₂ q₁ q₂) x).1 (Fin.castAdd q₁ i) = x (Fin.castAdd (q₁ + q₂) (Fin.castAdd p₂ i))

The first output block receives the first positive-coordinate block.

@[simp]

theorem TauCeti.realCliffordSplitIsometry_fst_neg (p₁ p₂ q₁ q₂ : ℕ) (x : Fin (p₁ + p₂ + (q₁ + q₂)) → ℝ) (i : Fin q₁) : ((realCliffordSplitIsometry p₁ p₂ q₁ q₂) x).1 (Fin.natAdd p₁ i) = x (Fin.natAdd (p₁ + p₂) (Fin.castAdd q₂ i))

The first output block receives the first negative-coordinate block.

@[simp]

theorem TauCeti.realCliffordSplitIsometry_snd_pos (p₁ p₂ q₁ q₂ : ℕ) (x : Fin (p₁ + p₂ + (q₁ + q₂)) → ℝ) (i : Fin p₂) : ((realCliffordSplitIsometry p₁ p₂ q₁ q₂) x).2 (Fin.castAdd q₂ i) = x (Fin.castAdd (q₁ + q₂) (Fin.natAdd p₁ i))

The second output block receives the second positive-coordinate block.

@[simp]

theorem TauCeti.realCliffordSplitIsometry_snd_neg (p₁ p₂ q₁ q₂ : ℕ) (x : Fin (p₁ + p₂ + (q₁ + q₂)) → ℝ) (i : Fin q₂) : ((realCliffordSplitIsometry p₁ p₂ q₁ q₂) x).2 (Fin.natAdd p₂ i) = x (Fin.natAdd (p₁ + p₂) (Fin.natAdd q₁ i))

The second output block receives the second negative-coordinate block.

def TauCeti.realCliffordFormCongr {p q p' q' : ℕ} (hp : p = p') (hq : q = q') : QuadraticMap.IsometryEquiv (realCliffordForm p q) (realCliffordForm p' q')

The coordinate isometry between two presentations of the same signature, relabelling the coordinates along Fin.cast.

@[simp]

theorem TauCeti.realCliffordFormCongr_apply {p q p' q' : ℕ} (hp : p = p') (hq : q = q') (x : Fin (p + q) → ℝ) (i : Fin (p' + q')) : (realCliffordFormCongr hp hq) x i = x (Fin.cast ⋯ i)

realCliffordFormCongr reads each coordinate through Fin.cast.

def TauCeti.realCliffordBlockIsometry (p q : ℕ) : QuadraticMap.IsometryEquiv (realCliffordForm p q) (QuadraticMap.prod (realCliffordForm p 0) (realCliffordForm 0 q))

The coordinate isometry which splits a real signature form into its positive-definite block, the first p coordinates, and its negative-definite block, the last q coordinates.

@[simp]

theorem TauCeti.realCliffordBlockIsometry_apply_fst (p q : ℕ) (x : Fin (p + q) → ℝ) (i : Fin p) : ((realCliffordBlockIsometry p q) x).1 i = x (Fin.castAdd q i)

The positive block of realCliffordBlockIsometry consists of the first p coordinates.

@[simp]

theorem TauCeti.realCliffordBlockIsometry_apply_snd (p q : ℕ) (x : Fin (p + q) → ℝ) (i : Fin (0 + q)) : ((realCliffordBlockIsometry p q) x).2 i = x (Fin.natAdd p (Fin.cast ⋯ i))

The negative block of realCliffordBlockIsometry consists of the last q coordinates.

def TauCeti.realCliffordPositiveSplitIsometry (p q : ℕ) : QuadraticMap.IsometryEquiv (realCliffordForm (p + 1) q) (QuadraticMap.prod (realCliffordForm p q) QuadraticMap.sq)

The coordinate isometry which splits the last positive coordinate from a real signature.

@[simp]

theorem TauCeti.realCliffordPositiveSplitIsometry_fst_pos (p q : ℕ) (v : Fin (p + 1 + q) → ℝ) (i : Fin p) : ((realCliffordPositiveSplitIsometry p q) v).1 (Fin.castAdd q i) = v (Fin.castAdd q i.castSucc)

The positive coordinates retained by realCliffordPositiveSplitIsometry.

@[simp]

theorem TauCeti.realCliffordPositiveSplitIsometry_fst_neg (p q : ℕ) (v : Fin (p + 1 + q) → ℝ) (i : Fin q) : ((realCliffordPositiveSplitIsometry p q) v).1 (Fin.natAdd p i) = v (Fin.natAdd (p + 1) i)

The negative coordinates retained by realCliffordPositiveSplitIsometry.

@[simp]

theorem TauCeti.realCliffordPositiveSplitIsometry_snd (p q : ℕ) (v : Fin (p + 1 + q) → ℝ) : ((realCliffordPositiveSplitIsometry p q) v).2 = v (Fin.castAdd q (Fin.last p))

The last positive coordinate extracted by realCliffordPositiveSplitIsometry.

def TauCeti.realBottSplitIsometry (p q : ℕ) : QuadraticMap.IsometryEquiv (realCliffordForm (p + 1) (q + 1)) (QuadraticMap.prod (realCliffordForm p q) (realCliffordForm 1 1))

The coordinate isometry which separates the last positive and negative coordinates of the signature form as a hyperbolic plane.

@[simp]

theorem TauCeti.realBottSplitIsometry_fst_pos (p q : ℕ) (v : Fin (p + 1 + (q + 1)) → ℝ) (i : Fin p) : ((realBottSplitIsometry p q) v).1 (Fin.castAdd q i) = v (Fin.castAdd (q + 1) i.castSucc)

The positive coordinates retained by realBottSplitIsometry.

@[simp]

theorem TauCeti.realBottSplitIsometry_fst_neg (p q : ℕ) (v : Fin (p + 1 + (q + 1)) → ℝ) (i : Fin q) : ((realBottSplitIsometry p q) v).1 (Fin.natAdd p i) = v (Fin.natAdd (p + 1) i.castSucc)

The negative coordinates retained by realBottSplitIsometry.

@[simp]

theorem TauCeti.realBottSplitIsometry_snd_zero (p q : ℕ) (v : Fin (p + 1 + (q + 1)) → ℝ) : ((realBottSplitIsometry p q) v).2 0 = v (Fin.castAdd (q + 1) (Fin.last p))

The last positive coordinate extracted by realBottSplitIsometry.

@[simp]

theorem TauCeti.realBottSplitIsometry_snd_one (p q : ℕ) (v : Fin (p + 1 + (q + 1)) → ℝ) : ((realBottSplitIsometry p q) v).2 1 = v (Fin.natAdd (p + 1) (Fin.last q))

The last negative coordinate extracted by realBottSplitIsometry.

def TauCeti.realCliffordSignSwitchStandardIsometry (p q : ℕ) : (QuadraticMap.prod (-realCliffordForm p q) QuadraticMap.sq).IsometryEquiv (realCliffordForm (q + 1) p)

The coordinate isometry which turns the sign-switched form into the standard signature.

@[simp]

theorem TauCeti.realCliffordSignSwitchStandardIsometry_pos_of_neg (p q : ℕ) (x : Fin (p + q) → ℝ) (r : ℝ) (i : Fin q) : (realCliffordSignSwitchStandardIsometry p q) (x, r) (Fin.castAdd p i.castSucc) = x (Fin.natAdd p i)

Negated negative coordinates become positive coordinates under realCliffordSignSwitchStandardIsometry.

@[simp]

theorem TauCeti.realCliffordSignSwitchStandardIsometry_last_pos (p q : ℕ) (x : Fin (p + q) → ℝ) (r : ℝ) : (realCliffordSignSwitchStandardIsometry p q) (x, r) (Fin.castAdd p (Fin.last q)) = r

The new positive line is the last positive coordinate under realCliffordSignSwitchStandardIsometry.

@[simp]

theorem TauCeti.realCliffordSignSwitchStandardIsometry_neg_of_pos (p q : ℕ) (x : Fin (p + q) → ℝ) (r : ℝ) (i : Fin p) : (realCliffordSignSwitchStandardIsometry p q) (x, r) (Fin.natAdd (q + 1) i) = x (Fin.castAdd q i)

Negated positive coordinates become negative coordinates under realCliffordSignSwitchStandardIsometry.

The four base entries, in coordinates

@[simp]

theorem TauCeti.realCliffordForm_one_zero_apply (v : Fin (1 + 0) → ℝ) : (realCliffordForm 1 0) v = v 0 * v 0

The real Clifford form of signature (1, 0) in coordinates.

@[simp]

theorem TauCeti.realCliffordForm_zero_one_apply (v : Fin (0 + 1) → ℝ) : (realCliffordForm 0 1) v = -(v 0 * v 0)

The real Clifford form of signature (0, 1) in coordinates.

@[simp]

theorem TauCeti.realCliffordForm_zero_two_apply (v : Fin (0 + 2) → ℝ) : (realCliffordForm 0 2) v = -(v 0 * v 0) + -(v 1 * v 1)

The real Clifford form of signature (0, 2) in coordinates.

@[simp]

theorem TauCeti.realCliffordForm_one_one_apply (v : Fin (1 + 1) → ℝ) : (realCliffordForm 1 1) v = v 0 * v 0 - v 1 * v 1

The real Clifford form of signature (1, 1) in coordinates.

Cliff(1,0) ≅ ℝ × ℝ

noncomputable def TauCeti.realCliffordOneZeroEquivProd : CliffordAlgebra (realCliffordForm 1 0) ≃ₐ[ℝ] ℝ × ℝ

Cliff(1,0) ≅ ℝ × ℝ, the first base entry of the real periodicity table: a single generator squaring to +1 splits the algebra.

@[simp]

theorem TauCeti.realCliffordOneZeroEquivProd_ι (v : Fin (1 + 0) → ℝ) : realCliffordOneZeroEquivProd ((CliffordAlgebra.ι (realCliffordForm 1 0)) v) = (v 0, -v 0)

realCliffordOneZeroEquivProd sends the generator of the coordinate v to the pair (v 0, -v 0): the two characters of ℝ[e]/(e² - 1) read off the two components.

Cliff(0,1) ≅ ℂ

def TauCeti.realCliffordZeroOneIsometry : QuadraticMap.IsometryEquiv (realCliffordForm 0 1) CliffordAlgebraComplex.Q

The signature (0,1) form is Mathlib's CliffordAlgebraComplex.Q, r ↦ -r², read on the one-dimensional space Fin (0 + 1) → ℝ.

@[simp]

theorem TauCeti.realCliffordZeroOneIsometry_apply (v : Fin (0 + 1) → ℝ) : realCliffordZeroOneIsometry v = v 0

realCliffordZeroOneIsometry reads off the single coordinate.

def TauCeti.realCliffordZeroOneEquivComplex : CliffordAlgebra (realCliffordForm 0 1) ≃ₐ[ℝ] ℂ

Cliff(0,1) ≅ ℂ, the second base entry of the real periodicity table: a single generator squaring to -1 is a square root of -1.

@[simp]

theorem TauCeti.realCliffordZeroOneEquivComplex_ι (v : Fin (0 + 1) → ℝ) : realCliffordZeroOneEquivComplex ((CliffordAlgebra.ι (realCliffordForm 0 1)) v) = v 0 • Complex.I

realCliffordZeroOneEquivComplex sends the generator of the coordinate v to the purely imaginary complex number v 0 • Complex.I.

Cliff(0,2) ≅ ℍ

def TauCeti.realCliffordZeroTwoIsometry : QuadraticMap.IsometryEquiv (realCliffordForm 0 2) (CliffordAlgebraQuaternion.Q (-1) (-1))

The signature (0,2) form is Mathlib's CliffordAlgebraQuaternion.Q (-1) (-1) read on Fin (0 + 2) → ℝ instead of on ℝ × ℝ.

@[simp]

theorem TauCeti.realCliffordZeroTwoIsometry_apply (v : Fin (0 + 2) → ℝ) : realCliffordZeroTwoIsometry v = (v 0, v 1)

realCliffordZeroTwoIsometry reads off the two coordinates.

def TauCeti.realCliffordZeroTwoEquivQuaternion : CliffordAlgebra (realCliffordForm 0 2) ≃ₐ[ℝ] Quaternion ℝ

Cliff(0,2) ≅ ℍ, the third base entry of the real periodicity table: two anticommuting generators squaring to -1 are the quaternion units i and j.

@[simp]

theorem TauCeti.realCliffordZeroTwoEquivQuaternion_ι (v : Fin (0 + 2) → ℝ) : realCliffordZeroTwoEquivQuaternion ((CliffordAlgebra.ι (realCliffordForm 0 2)) v) = { re := 0, imI := v 0, imJ := v 1, imK := 0 }

realCliffordZeroTwoEquivQuaternion sends the generator of the coordinate v to the imaginary quaternion v 0 * i + v 1 * j.

@[simp]

theorem TauCeti.realCliffordZeroTwoEquivQuaternion_star (x : CliffordAlgebra (realCliffordForm 0 2)) : realCliffordZeroTwoEquivQuaternion (star x) = star (realCliffordZeroTwoEquivQuaternion x)

The (0,2) real Clifford-algebra equivalence identifies Clifford conjugation with quaternion conjugation.

Cliff(1,1) ≅ M₂(ℝ)

noncomputable def TauCeti.realCliffordOneOneEquivMatrix : CliffordAlgebra (realCliffordForm 1 1) ≃ₐ[ℝ] Matrix (Fin 2) (Fin 2) ℝ

Cliff(1,1) ≅ M₂(ℝ), the fourth base entry of the real periodicity table and the seed of the periodicity step Cliff(p+1, q+1) ≅ Cliff(p, q) ⊗ M₂(ℝ): Mathlib's CliffordAlgebraQuaternion.equiv onto the split quaternions ℍ[ℝ,1,-1], transported along realCliffordOneOneIsometry and followed by the splitting TauCeti.QuaternionAlgebra.oneEquivMatrix.

@[simp]

theorem TauCeti.realCliffordOneOneEquivMatrix_ι (v : Fin (1 + 1) → ℝ) : realCliffordOneOneEquivMatrix ((CliffordAlgebra.ι (realCliffordForm 1 1)) v) = !![v 0, v 1; -v 1, -v 0]

realCliffordOneOneEquivMatrix sends the generator of the coordinate v to !![v 0, v 1; -v 1, -v 0], the combination v 0 • !![1, 0; 0, -1] + v 1 • !![0, 1; -1, 0] of the images of the +1 and -1 generators.