Real Spin groups in the Clifford algebra of the negated signature

Negating the coordinate form realCliffordForm p q gives, up to the coordinate isometry realCliffordFormNegIsometry p q, the form realCliffordForm q p. This file transports the Spin group of signature (p, q) into the Clifford algebra of signature (q, p).

The main case is the compact Spin group Spin(n), which is realCliffordSpinGroup n 0, the Spin group of the positive-definite form realCliffordForm n 0. Geometric Clifford multiplication instead uses the negative-definite form, for which c(v)² = -|v|²; its coordinate model is realCliffordForm 0 n. Taking p = n and q = 0 transports Spin(n) into the Clifford algebra of that model.

The isomorphism CliffordAlgebra.realCliffordSpinGroupEquivNeg p q is CliffordAlgebra.spinGroupEquivNeg, followed by the coordinate isometry realCliffordFormNegIsometry p q from -realCliffordForm p q to realCliffordForm q p. It sends a bivector ι a * ι b to minus the corresponding bivector of the negated signature. It intertwines the two vector actions through the coordinate isometry, and it sends -1 to -1.

The same construction compares Spin(n) with the Spin group of a form Q v = -‖v‖² on a real inner product space V, along an orthonormal basis b of V: the coordinate isometry is replaced by the coordinates OrthonormalBasis.negRealCliffordFormIsometryEquiv b hQ of b. This gives the frame comparison OrthonormalBasis.realSpinGroupEquiv b hQ, which on even parts is the even Clifford algebra equivalence OrthonormalBasis.realEvenCliffordEquiv b hQ of TauCeti.LinearAlgebra.CliffordAlgebra.RealForm.OrthonormalBasis. The comparison depends on the frame.

Main definitions

• OrthonormalBasis.realSpinGroupEquiv b hQ: the comparison of the compact Spin group spinGroup (realCliffordForm n 0) with spinGroup Q along b.

Main results

• CliffordAlgebra.realCliffordSpinGroupEquivNeg: the isomorphism realCliffordSpinGroup p q ≃* realCliffordSpinGroup q p.
• CliffordAlgebra.coe_realCliffordSpinGroupEquivNeg_apply_of_coe_eq_ι_mul_ι: the bivector sign.
• CliffordAlgebra.spinVectorAction_realCliffordSpinGroupEquivNeg: the vector actions agree under the coordinate isometry.
• CliffordAlgebra.realCliffordSpinGroupEquivNeg_negOne: the central element -1 goes to -1.
• OrthonormalBasis.spinVectorAction_realSpinGroupEquiv: the frame comparison intertwines the vector actions through the coordinates of b.
• OrthonormalBasis.spinGroupToEven_realSpinGroupEquiv: on even parts, the Spin frame comparison is the even frame comparison OrthonormalBasis.realEvenCliffordEquiv b hQ.

References

• H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §§1–3.

noncomputable def CliffordAlgebra.realCliffordSpinGroupEquivNeg (p q : ℕ) : ↥(realCliffordSpinGroup p q) ≃* ↥(realCliffordSpinGroup q p)

The Spin group of signature (p, q), transported into the Clifford algebra of the negated signature (q, p). For p = n and q = 0 this is the compact Spin group Spin(n) in the Clifford algebra of the negative-definite coordinate form realCliffordForm 0 n.

theorem CliffordAlgebra.coe_realCliffordSpinGroupEquivNeg_apply (p q : ℕ) (x : ↥(realCliffordSpinGroup p q)) : ↑((realCliffordSpinGroupEquivNeg p q) x) = (TauCeti.CliffordAlgebra.realCliffordEvenToNeg p q) ((spinGroupToEven (TauCeti.realCliffordForm p q)) x)

The Clifford value of realCliffordSpinGroupEquivNeg p q x is the even comparison TauCeti.CliffordAlgebra.realCliffordEvenToNeg p q applied to its even Clifford value.

theorem CliffordAlgebra.coe_realCliffordSpinGroupEquivNeg_apply_of_coe_eq_ι_mul_ι (p q : ℕ) {x : ↥(realCliffordSpinGroup p q)} {a b : Fin (p + q) → ℝ} (hx : ↑x = (ι (TauCeti.realCliffordForm p q)) a * (ι (TauCeti.realCliffordForm p q)) b) : ↑((realCliffordSpinGroupEquivNeg p q) x) = -((ι (TauCeti.realCliffordForm q p)) ((TauCeti.realCliffordFormNegIsometry p q) a) * (ι (TauCeti.realCliffordForm q p)) ((TauCeti.realCliffordFormNegIsometry p q) b))

A bivector ι a * ι b in the Spin group of signature (p, q) goes to minus the bivector of the transported vectors in signature (q, p).

@[simp]

theorem CliffordAlgebra.spinVectorAction_realCliffordSpinGroupEquivNeg (p q : ℕ) (x : ↥(realCliffordSpinGroup p q)) (v : Fin (p + q) → ℝ) : (spinVectorAction (TauCeti.realCliffordForm q p) ((realCliffordSpinGroupEquivNeg p q) x)) ((TauCeti.realCliffordFormNegIsometry p q) v) = (TauCeti.realCliffordFormNegIsometry p q) ((spinVectorAction (TauCeti.realCliffordForm p q) x) v)

Under realCliffordSpinGroupEquivNeg, the vector actions of the Spin groups of signatures (p, q) and (q, p) correspond through the coordinate isometry realCliffordFormNegIsometry p q.

@[simp]

theorem CliffordAlgebra.realCliffordSpinGroupEquivNeg_negOne (p q : ℕ) [NeZero (p + q)] : (realCliffordSpinGroupEquivNeg p q) (spinGroup.negOne (TauCeti.realCliffordForm p q) ⋯) = spinGroup.negOne (TauCeti.realCliffordForm q p) ⋯

In positive dimension, i.e. given NeZero (p + q), realCliffordSpinGroupEquivNeg sends the central element -1 to -1.

noncomputable def OrthonormalBasis.realSpinGroupEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) : ↥(spinGroup (TauCeti.realCliffordForm n 0)) ≃* ↥(spinGroup Q)

The comparison of the compact Spin group of the positive-definite coordinate form with the Spin group of a form Q v = -‖v‖², along the orthonormal basis b: the isomorphism CliffordAlgebra.spinGroupEquivNeg followed by the coordinates of b.

@[simp]

theorem OrthonormalBasis.spinVectorAction_realSpinGroupEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (s : ↥(spinGroup (TauCeti.realCliffordForm n 0))) (x : Fin (n + 0) → ℝ) : (CliffordAlgebra.spinVectorAction Q ((b.realSpinGroupEquiv hQ) s)) ((b.negRealCliffordFormIsometryEquiv hQ) x) = (b.negRealCliffordFormIsometryEquiv hQ) ((CliffordAlgebra.spinVectorAction (TauCeti.realCliffordForm n 0) s) x)

The Spin comparison OrthonormalBasis.realSpinGroupEquiv is compatible with the vector actions: a coordinate Spin element and its image rotate coordinates and vectors in the same way.

@[simp]

theorem OrthonormalBasis.spinGroupToEven_realSpinGroupEquiv {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (s : ↥(spinGroup (TauCeti.realCliffordForm n 0))) : (CliffordAlgebra.spinGroupToEven Q) ((b.realSpinGroupEquiv hQ) s) = (b.realEvenCliffordEquiv hQ) ((CliffordAlgebra.spinGroupToEven (TauCeti.realCliffordForm n 0)) s)

On even parts, the Spin comparison OrthonormalBasis.realSpinGroupEquiv is the even Clifford algebra comparison OrthonormalBasis.realEvenCliffordEquiv.

@[simp]

theorem OrthonormalBasis.realSpinGroupEquiv_negOne {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) : (b.realSpinGroupEquiv hQ) (CliffordAlgebra.spinGroup.negOne (TauCeti.realCliffordForm n 0) hpos) = CliffordAlgebra.spinGroup.negOne Q hQ₀

The frame comparison preserves the central scalar -1.

noncomputable def OrthonormalBasis.realSpinCGroupHom {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) : CliffordAlgebra.spinCGroup (TauCeti.realCliffordForm n 0) hpos →* CliffordAlgebra.spinCGroup Q hQ₀

The frame comparison descended to Spinᶜ, leaving the circle factor unchanged.

@[simp]

theorem OrthonormalBasis.realSpinCGroupHom_mk {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) (p : ↥(spinGroup (TauCeti.realCliffordForm n 0)) × Circle) : (b.realSpinCGroupHom hQ hpos hQ₀) ((CliffordAlgebra.spinCGroup.mk (TauCeti.realCliffordForm n 0) hpos) p) = (CliffordAlgebra.spinCGroup.mk Q hQ₀) ((b.realSpinGroupEquiv hQ) p.1, p.2)

On representatives the Spinᶜ frame comparison applies the Spin comparison.

@[simp]

theorem OrthonormalBasis.realSpinCGroupHom_ofSpin {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) (s : ↥(spinGroup (TauCeti.realCliffordForm n 0))) : (b.realSpinCGroupHom hQ hpos hQ₀) ((CliffordAlgebra.spinCGroup.ofSpin (TauCeti.realCliffordForm n 0) hpos) s) = (CliffordAlgebra.spinCGroup.ofSpin Q hQ₀) ((b.realSpinGroupEquiv hQ) s)

The Spinᶜ comparison restricts to the frame comparison on Spin.

@[simp]

theorem OrthonormalBasis.realSpinCGroupHom_ofCircle {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) (z : Circle) : (b.realSpinCGroupHom hQ hpos hQ₀) ((CliffordAlgebra.spinCGroup.ofCircle (TauCeti.realCliffordForm n 0) hpos) z) = (CliffordAlgebra.spinCGroup.ofCircle Q hQ₀) z

The Spinᶜ frame comparison is the identity on the central circle.

@[simp]

theorem OrthonormalBasis.det_realSpinCGroupHom {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) (x : CliffordAlgebra.spinCGroup (TauCeti.realCliffordForm n 0) hpos) : (CliffordAlgebra.spinCGroup.det Q hQ₀) ((b.realSpinCGroupHom hQ hpos hQ₀) x) = (CliffordAlgebra.spinCGroup.det (TauCeti.realCliffordForm n 0) hpos) x

The Spinᶜ frame comparison preserves the determinant character.

theorem OrthonormalBasis.toSpecialOrthogonal_realSpinCGroupHom_apply {V : Type u_1} [NormedAddCommGroup V] [InnerProductSpace ℝ V] {Q : QuadraticForm ℝ V} {n : ℕ} (b : OrthonormalBasis (Fin n) ℝ V) (hQ : ∀ (v : V), Q v = -‖v‖ ^ 2) (hpos : TauCeti.realCliffordForm n 0 ≠ 0) (hQ₀ : Q ≠ 0) (x : CliffordAlgebra.spinCGroup (TauCeti.realCliffordForm n 0) hpos) (v : Fin (n + 0) → ℝ) : ↑((CliffordAlgebra.spinCGroup.toSpecialOrthogonal Q hQ₀) ((b.realSpinCGroupHom hQ hpos hQ₀) x)) ((b.negRealCliffordFormIsometryEquiv hQ) v) = (b.negRealCliffordFormIsometryEquiv hQ) (↑((CliffordAlgebra.spinCGroup.toSpecialOrthogonal (TauCeti.realCliffordForm n 0) hpos) x) v)

The Spinᶜ frame comparison intertwines the rotation projections.