The negative-plane recurrence for real Clifford algebras

Adjoining a hyperbolic plane to a real quadratic module tensors its Clifford algebra with M₂(ℝ) and leaves the form alone (CliffordAlgebra.hyperbolicEquivTensor). This file proves the companion step for the negative definite plane: adjoining two generators which both square to -1 tensors the Clifford algebra with Cliff(0,2) ≅ ℍ and negates the form,

Cliff(Q ⊥ ⟨-1, -1⟩) ≅ Cliff(-Q) ⊗ᵣ ℍ.

The mechanism is the plane's volume element ω = e₀e₁. It squares to -1 — rather than to +1, as the hyperbolic volume element does — and it commutes with the old generators while anticommuting with the two new ones, so m ↦ ι m · ω turns the old generators into generators for the negated form. On the standard signature forms this reads

Cliff(p, q + 2) ≅ Cliff(q, p) ⊗ᵣ ℍ,

the negative-plane companion of TauCeti.realCliffordSignatureSwitchRecurrenceEquiv (Cliff(p + 2, q) ≅ Cliff(q, p) ⊗ᵣ M₂(ℝ)). The two recurrences are what the eightfold periodicity table of the real Clifford algebras is assembled from; composing them across four negative generators already gives the signature-preserving four-step recurrence

Cliff(p, q + 4) ≅ Cliff(p, q) ⊗ᵣ M₂(ℝ) ⊗ᵣ ℍ

proved at the end of the file.

Implementation notes

The generic statement is proved with Cliff(0,2) rather than ℍ on the right, and the quaternions are reached at the very end by transporting along TauCeti.realCliffordZeroTwoEquivQuaternion. That keeps the whole construction independent of the quaternion model; the model is used only for the two identities the volume element has to satisfy, which it inherits from the quaternion unit k it corresponds to.

The forward map is built from the universal property on the explicit generator (m, v) ↦ ι m ⊗ₜ ω + 1 ⊗ₜ ι v, and its inverse from the two commuting inclusions Cliff(-Q) → Cliff(Q ⊥ ⟨-1, -1⟩) and Cliff(0,2) → Cliff(Q ⊥ ⟨-1, -1⟩) through Algebra.TensorProduct.lift. The base inclusion carries a sign: it sends ι m to -(ι (m, 0) · ω) rather than to ι (m, 0) · ω. Either choice is a valid Clifford lift, since the square is unchanged, but only the signed one inverts the unsigned forward map, precisely because ω² = -1 here where the hyperbolic volume element satisfies ω² = 1.

Main definitions

• TauCeti.realCliffordZeroTwoVolume: the volume element e₀e₁ of Cliff(0,2), with its square and its anticommutation with the generators;
• TauCeti.realCliffordNegativePlaneSplitIsometry: the coordinate isometry separating the last two negative coordinates of a standard signature form;
• CliffordAlgebra.negativePlaneEquivTensor: Cliff(Q ⊥ ⟨-1, -1⟩) ≅ Cliff(-Q) ⊗ᵣ Cliff(0,2) for an arbitrary real quadratic module, and CliffordAlgebra.negativePlaneEquivQuaternion for its quaternionic form;
• TauCeti.realCliffordQuaternionRecurrenceEquiv: the standard-signature recurrence Cliff(p, q + 2) ≅ Cliff(q, p) ⊗ᵣ ℍ;
• TauCeti.realCliffordFourNegativeRecurrenceEquiv: Cliff(p, q + 4) ≅ Cliff(p, q) ⊗ᵣ M₂(ℝ) ⊗ᵣ ℍ.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, Proposition 4.2.

The volume element of the negative definite plane

noncomputable def TauCeti.realCliffordZeroTwoVolume : CliffordAlgebra (realCliffordForm 0 2)

The volume element of the negative definite plane: the product of the two coordinate generators of Cliff(0,2). It squares to -1 and anticommutes with every generator, which is what drives the negative-plane recurrence below.

theorem TauCeti.realCliffordZeroTwoVolume_def : realCliffordZeroTwoVolume = (CliffordAlgebra.ι (realCliffordForm 0 2)) (Pi.single 0 1) * (CliffordAlgebra.ι (realCliffordForm 0 2)) (Pi.single 1 1)

The defining equation of the volume element: it is the product of the two coordinate generators of Cliff(0,2). This is deliberately not a simp lemma — the volume element is the normal form, and the lemmas below which mention it do so in that form.

@[simp]

theorem TauCeti.realCliffordZeroTwoEquivQuaternion_volume : realCliffordZeroTwoEquivQuaternion realCliffordZeroTwoVolume = { re := 0, imI := 0, imJ := 0, imK := 1 }

Under Cliff(0,2) ≅ ℍ the volume element is the quaternion unit k = ij.

@[simp]

theorem TauCeti.realCliffordZeroTwoVolume_sq : realCliffordZeroTwoVolume * realCliffordZeroTwoVolume = -1

The volume element of the negative definite plane squares to -1.

theorem TauCeti.realCliffordZeroTwoVolume_anticomm (v : Fin (0 + 2) → ℝ) : realCliffordZeroTwoVolume * (CliffordAlgebra.ι (realCliffordForm 0 2)) v + (CliffordAlgebra.ι (realCliffordForm 0 2)) v * realCliffordZeroTwoVolume = 0

The volume element of the negative definite plane anticommutes with every generator.

The negative-plane coordinate splitter

def TauCeti.realCliffordNegativePlaneSplitIsometry (p q : ℕ) : QuadraticMap.IsometryEquiv (realCliffordForm p (q + 1 + 1)) (QuadraticMap.prod (realCliffordForm p q) (realCliffordForm 0 2))

The coordinate isometry which separates the last two negative coordinates of a standard signature form as a negative definite plane.

@[simp]

theorem TauCeti.realCliffordNegativePlaneSplitIsometry_fst_pos (p q : ℕ) (v : Fin (p + (q + 1 + 1)) → ℝ) (i : Fin p) : ((realCliffordNegativePlaneSplitIsometry p q) v).1 (Fin.castAdd q i) = v (Fin.castAdd (q + 1 + 1) i)

The positive coordinates retained by realCliffordNegativePlaneSplitIsometry.

@[simp]

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

The negative coordinates retained by realCliffordNegativePlaneSplitIsometry.

@[simp]

theorem TauCeti.realCliffordNegativePlaneSplitIsometry_snd_zero (p q : ℕ) (v : Fin (p + (q + 1 + 1)) → ℝ) : ((realCliffordNegativePlaneSplitIsometry p q) v).2 0 = v (Fin.natAdd p (Fin.last q).castSucc)

The first of the two negative coordinates extracted by realCliffordNegativePlaneSplitIsometry.

@[simp]

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

The second of the two negative coordinates extracted by realCliffordNegativePlaneSplitIsometry.

The forward map

The two inclusions into Cliff(Q ⊥ ⟨-1, -1⟩)

The two composites

noncomputable def CliffordAlgebra.negativePlaneEquivTensor {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : CliffordAlgebra (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2)) ≃ₐ[ℝ] TensorProduct ℝ (CliffordAlgebra (-Q)) (CliffordAlgebra (TauCeti.realCliffordForm 0 2))

The negative-plane recurrence. Adjoining two generators which square to -1 to a real quadratic module tensors its Clifford algebra with Cliff(0,2) and negates the form.

@[simp]

theorem CliffordAlgebra.negativePlaneEquivTensor_ι {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x : M × (Fin (0 + 2) → ℝ)) : (negativePlaneEquivTensor Q) ((ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2))) x) = (ι (-Q)) x.1 ⊗ₜ[ℝ] TauCeti.realCliffordZeroTwoVolume + 1 ⊗ₜ[ℝ] (ι (TauCeti.realCliffordForm 0 2)) x.2

negativePlaneEquivTensor sends an old generator to ι m ⊗ ω and a new one to 1 ⊗ ι v.

@[simp]

theorem CliffordAlgebra.negativePlaneEquivTensor_symm_apply_ι_base {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (m : M) : (negativePlaneEquivTensor Q).symm ((ι (-Q)) m ⊗ₜ[ℝ] TauCeti.realCliffordZeroTwoVolume) = (ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2))) (m, 0)

The inverse of negativePlaneEquivTensor on the tensor representing an old generator.

@[simp]

theorem CliffordAlgebra.negativePlaneEquivTensor_symm_apply_ι_plane {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (v : Fin (0 + 2) → ℝ) : (negativePlaneEquivTensor Q).symm (1 ⊗ₜ[ℝ] (ι (TauCeti.realCliffordForm 0 2)) v) = (ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2))) (0, v)

The inverse of negativePlaneEquivTensor on the tensor representing a new generator.

noncomputable def CliffordAlgebra.negativePlaneEquivQuaternion {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : CliffordAlgebra (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2)) ≃ₐ[ℝ] TensorProduct ℝ (CliffordAlgebra (-Q)) (Quaternion ℝ)

The negative-plane recurrence, quaternionic form: adjoining a negative definite plane tensors the Clifford algebra with the quaternions and negates the form.

@[simp]

theorem CliffordAlgebra.negativePlaneEquivQuaternion_ι {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (x : M × (Fin (0 + 2) → ℝ)) : (negativePlaneEquivQuaternion Q) ((ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2))) x) = (ι (-Q)) x.1 ⊗ₜ[ℝ] TauCeti.realCliffordZeroTwoEquivQuaternion TauCeti.realCliffordZeroTwoVolume + 1 ⊗ₜ[ℝ] TauCeti.realCliffordZeroTwoEquivQuaternion ((ι (TauCeti.realCliffordForm 0 2)) x.2)

negativePlaneEquivQuaternion sends an old generator to ι m ⊗ ω and a new one to the imaginary quaternion v 0 · i + v 1 · j, both read through Cliff(0,2) ≅ ℍ.

@[simp]

theorem CliffordAlgebra.negativePlaneEquivQuaternion_symm_apply_ι_base {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (m : M) : (negativePlaneEquivQuaternion Q).symm ((ι (-Q)) m ⊗ₜ[ℝ] { re := 0, imI := 0, imJ := 0, imK := 1 }) = (ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2))) (m, 0)

The inverse of negativePlaneEquivQuaternion on the tensor representing an old generator: the quaternion factor is the unit k, the image of the plane's volume element.

@[simp]

theorem CliffordAlgebra.negativePlaneEquivQuaternion_symm_apply_ι_plane {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (v : Fin (0 + 2) → ℝ) : (negativePlaneEquivQuaternion Q).symm (1 ⊗ₜ[ℝ] { re := 0, imI := v 0, imJ := v 1, imK := 0 }) = (ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 0 2))) (0, v)

The inverse of negativePlaneEquivQuaternion on the tensor representing a new generator: the quaternion factor is the imaginary quaternion v 0 * i + v 1 * j.

Negative-plane recurrences on standard signatures

noncomputable def TauCeti.realCliffordQuaternionRecurrenceEquiv (p q : ℕ) : CliffordAlgebra (realCliffordForm p (q + 1 + 1)) ≃ₐ[ℝ] TensorProduct ℝ (CliffordAlgebra (realCliffordForm q p)) (Quaternion ℝ)

The negative-plane signature recurrence Cliff(p, q + 2) ≅ Cliff(q, p) ⊗ ℍ: two extra negative generators switch the signature and tensor with the quaternions. This is the companion of TauCeti.realCliffordSignatureSwitchRecurrenceEquiv, which does the same with two extra positive generators and a factor of M₂(ℝ).

@[simp]

theorem TauCeti.realCliffordQuaternionRecurrenceEquiv_ι (p q : ℕ) (v : Fin (p + (q + 1 + 1)) → ℝ) : (realCliffordQuaternionRecurrenceEquiv p q) ((CliffordAlgebra.ι (realCliffordForm p (q + 1 + 1))) v) = (CliffordAlgebra.ι (realCliffordForm q p)) ((realCliffordFormNegIsometry p q) ((realCliffordNegativePlaneSplitIsometry p q) v).1) ⊗ₜ[ℝ] realCliffordZeroTwoEquivQuaternion realCliffordZeroTwoVolume + 1 ⊗ₜ[ℝ] realCliffordZeroTwoEquivQuaternion ((CliffordAlgebra.ι (realCliffordForm 0 2)) ((realCliffordNegativePlaneSplitIsometry p q) v).2)

The negative-plane signature recurrence on a Clifford generator: the coordinate isometry splits off the last two negative coordinates, the generic recurrence multiplies the remaining generator by the plane's volume element, and the negation isometry restores standard signature coordinates.

noncomputable def TauCeti.realCliffordFourNegativeRecurrenceEquiv (p q : ℕ) : CliffordAlgebra (realCliffordForm p (q + 1 + 1 + 1 + 1)) ≃ₐ[ℝ] TensorProduct ℝ (TensorProduct ℝ (CliffordAlgebra (realCliffordForm p q)) (Matrix (Fin 2) (Fin 2) ℝ)) (Quaternion ℝ)

The four-negative-generator recurrence Cliff(p, q + 4) ≅ Cliff(p, q) ⊗ M₂(ℝ) ⊗ ℍ, obtained by composing the negative-plane recurrence with the positive-plane one: four extra negative generators restore the original signature.

@[simp]

theorem TauCeti.realCliffordFourNegativeRecurrenceEquiv_ι (p q : ℕ) (v : Fin (p + (q + 1 + 1 + 1 + 1)) → ℝ) : (realCliffordFourNegativeRecurrenceEquiv p q) ((CliffordAlgebra.ι (realCliffordForm p (q + 1 + 1 + 1 + 1))) v) = (realCliffordSignatureSwitchRecurrenceEquiv q p) ((CliffordAlgebra.ι (realCliffordForm (q + 1 + 1) p)) ((realCliffordFormNegIsometry p (q + 1 + 1)) ((realCliffordNegativePlaneSplitIsometry p (q + 1 + 1)) v).1)) ⊗ₜ[ℝ] realCliffordZeroTwoEquivQuaternion realCliffordZeroTwoVolume + 1 ⊗ₜ[ℝ] realCliffordZeroTwoEquivQuaternion ((CliffordAlgebra.ι (realCliffordForm 0 2)) ((realCliffordNegativePlaneSplitIsometry p (q + 1 + 1)) v).2)

The four-negative-generator recurrence on a Clifford generator: the negative-plane recurrence splits off two of the four new coordinates, and the signature-switch recurrence transports the remaining generator back to the original signature.