Hyperbolic Bott periodicity for real Clifford algebras

This file proves the (1, 1) periodicity step for Clifford algebras: adding one positive and one negative generator is equivalent to tensoring with two-by-two real matrices. It also derives the signature-switch recurrence Cliff(p + 2, q) ≅ Cliff(q, p) ⊗ M₂(ℝ) from CliffordAlgebra.signSwitchEquiv.

Main results

• CliffordAlgebra.hyperbolicEquivTensor: adjoining a hyperbolic plane to an arbitrary real quadratic module tensors its Clifford algebra with M₂(ℝ);
• TauCeti.realCliffordBottEquiv: the corresponding equivalence for the standard signature forms;
• TauCeti.realCliffordBottIterEquiv: the iterated standard-signature equivalence, with matrix size 2 ^ n after adjoining n hyperbolic planes;
• TauCeti.realCliffordSignatureSwitchRecurrenceEquiv: the recurrence which switches a real signature while adding two positive generators.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I. Their Cl(r, s) is CliffordAlgebra (realCliffordForm s r) here.

noncomputable def CliffordAlgebra.hyperbolicEquivTensor {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) : CliffordAlgebra (QuadraticMap.prod Q (TauCeti.realCliffordForm 1 1)) ≃ₐ[ℝ] TensorProduct ℝ (CliffordAlgebra Q) (Matrix (Fin 2) (Fin 2) ℝ)

Adjoining a hyperbolic plane to a real quadratic module tensors its Clifford algebra with two-by-two real matrices.

@[simp]

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

The image of a generator under hyperbolicEquivTensor, split into its original-module and hyperbolic-plane components.

@[simp]

theorem CliffordAlgebra.hyperbolicEquivTensor_symm_apply_ι_base {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (m : M) : (hyperbolicEquivTensor Q).symm ((ι Q) m ⊗ₜ[ℝ] !![0, 1; 1, 0]) = (ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 1 1))) (m, 0)

The inverse of hyperbolicEquivTensor on the tensor representing an original generator.

@[simp]

theorem CliffordAlgebra.hyperbolicEquivTensor_symm_apply_ι_hyperbolic {M : Type u_1} [AddCommGroup M] [Module ℝ M] (Q : QuadraticForm ℝ M) (v : Fin (1 + 1) → ℝ) : (hyperbolicEquivTensor Q).symm (1 ⊗ₜ[ℝ] !![v 0, v 1; -v 1, -v 0]) = (ι (QuadraticMap.prod Q (TauCeti.realCliffordForm 1 1))) (0, v)

The inverse of hyperbolicEquivTensor on a tensor representing a hyperbolic generator.

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

The hyperbolic Bott step for the standard real signature forms: Cliff(p + 1, q + 1) ≅ Cliff(p, q) ⊗ M₂(ℝ).

@[simp]

theorem TauCeti.realCliffordBottEquiv_ι (p q : ℕ) (v : Fin (p + 1 + (q + 1)) → ℝ) : (realCliffordBottEquiv p q) ((CliffordAlgebra.ι (realCliffordForm (p + 1) (q + 1))) v) = (CliffordAlgebra.ι (realCliffordForm p q)) ((realBottSplitIsometry p q) v).1 ⊗ₜ[ℝ] !![0, 1; 1, 0] + 1 ⊗ₜ[ℝ] !![((realBottSplitIsometry p q) v).2 0, ((realBottSplitIsometry p q) v).2 1; -((realBottSplitIsometry p q) v).2 1, -((realBottSplitIsometry p q) v).2 0]

realCliffordBottEquiv first separates the last positive and negative coordinates, then applies the hyperbolic-plane equivalence.

Iterated hyperbolic reduction

@[irreducible]

noncomputable def TauCeti.realCliffordBottIterEquiv (p q n : ℕ) : CliffordAlgebra (realCliffordForm (p + n) (q + n)) ≃ₐ[ℝ] TensorProduct ℝ (CliffordAlgebra (realCliffordForm p q)) (Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℝ)

Iterating the hyperbolic Bott step n times identifies Cliff(p + n, q + n) with Cliff(p, q) ⊗ M_(2 ^ n)(ℝ).

@[simp]

theorem TauCeti.realCliffordBottIterEquiv_zero_apply (p q : ℕ) (x : CliffordAlgebra (realCliffordForm p q)) : have e := realCliffordBottIterEquiv p q 0; e x = x ⊗ₜ[ℝ] 1

At zero iterations, realCliffordBottIterEquiv is the canonical identification with a one-by-one matrix tensor factor.

@[simp]

theorem TauCeti.realCliffordBottIterEquiv_succ (p q n : ℕ) : realCliffordBottIterEquiv p q (n + 1) = (realCliffordBottEquiv (p + n) (q + n)).trans ((Algebra.TensorProduct.congr (realCliffordBottIterEquiv p q n) AlgEquiv.refl).trans ((Algebra.TensorProduct.assoc ℝ ℝ ℝ (CliffordAlgebra (realCliffordForm p q)) (Matrix (Fin (2 ^ n)) (Fin (2 ^ n)) ℝ) (Matrix (Fin 2) (Fin 2) ℝ)).trans (Algebra.TensorProduct.congr AlgEquiv.refl (Matrix.kroneckerFinAlgEquiv (2 ^ n) 2 ℝ))))

The successor iteration first applies one hyperbolic Bott step, transports the previous iteration through the left tensor factor, and absorbs the two matrix factors by the Kronecker equivalence.

Signature-switch recurrence

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

One sign switch followed by the hyperbolic Bott step gives the signature-switch recurrence Cliff(p + 2, q) ≅ Cliff(q, p) ⊗ M₂(ℝ).

@[simp]

theorem TauCeti.realCliffordSignatureSwitchRecurrenceEquiv_ι (p q : ℕ) (v : Fin (p + 1 + 1 + q) → ℝ) : (realCliffordSignatureSwitchRecurrenceEquiv p q) ((CliffordAlgebra.ι (realCliffordForm (p + 1 + 1) q)) v) = (realCliffordBottEquiv q p) ((CliffordAlgebra.ι (realCliffordForm (q + 1) (p + 1))) ((realCliffordSignSwitchStandardIsometry (p + 1) q) (0, 1))) * (realCliffordBottEquiv q p) ((CliffordAlgebra.ι (realCliffordForm (q + 1) (p + 1))) ((realCliffordSignSwitchStandardIsometry (p + 1) q) (((realCliffordPositiveSplitIsometry (p + 1) q) v).1, 0))) + ((realCliffordPositiveSplitIsometry (p + 1) q) v).2 • (realCliffordBottEquiv q p) ((CliffordAlgebra.ι (realCliffordForm (q + 1) (p + 1))) ((realCliffordSignSwitchStandardIsometry (p + 1) q) (0, 1)))

The signature-switch recurrence sends a Clifford generator through its two coordinate isometries and the sign-switch generator formula, then transports the result through realCliffordBottEquiv q p.