The Spin groups of a quadratic form and of its negative

Mathlib's CliffordAlgebra.evenEquivEvenNeg identifies the even Clifford algebras of Q and -Q; it sends a product of two vectors ι Q a * ι Q b to -(ι (-Q) a * ι (-Q) b). When 2 is invertible, this file restricts that equivalence to a group isomorphism CliffordAlgebra.spinGroupEquivNeg Q : spinGroup Q ≃* spinGroup (-Q). Both Spin groups act on the common underlying module, and the isomorphism preserves these actions on the nose. It also sends the central element -1 to -1.

Over the reals this compares a Spin group built from a positive-definite form with the Clifford algebra of the negative-definite form, in which vectors satisfy c(v)² = -|v|². There is no algebra isomorphism between the full Clifford algebras of Q and -Q in general, so the comparison necessarily passes through the even subalgebras. After extension of scalars to an algebra containing a square root u of -1, such as ℂ, the full algebras are identified by CliffordAlgebra.equivNeg, ι m ↦ u • ι m; on scalar-extended Spin elements it agrees with CliffordAlgebra.spinGroupEquivNeg.

A Spin element is a product of an even number of vectors of invertible norm (CliffordAlgebra.exists_even_length_list_of_spinGroup). The same vectors, read in the Clifford algebra of -Q, conjugate vectors in the same way, which is what identifies the two actions.

Main results

• CliffordAlgebra.spinGroupEquivNeg: the group isomorphism spinGroup Q ≃* spinGroup (-Q).
• CliffordAlgebra.coe_spinGroupEquivNeg_apply: its Clifford value is evenEquivEvenNeg.
• CliffordAlgebra.coe_spinGroupEquivNeg_apply_of_coe_eq_ι_mul_ι: a product of two vectors ι Q a * ι Q b goes to -(ι (-Q) a * ι (-Q) b).
• CliffordAlgebra.spinVectorAction_spinGroupEquivNeg: the isomorphism preserves the vector actions.
• CliffordAlgebra.spinGroupEquivNeg_negOne: the isomorphism sends -1 to -1.
• CliffordAlgebra.equivNeg_spinGroupBaseChange: after extension of scalars to an algebra containing u with u * u = -1, the full-algebra isomorphism CliffordAlgebra.equivNeg restricts on Spin elements to the scalar extension of spinGroupEquivNeg.

References

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

def CliffordAlgebra.spinGroupEquivNeg {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] : ↥(spinGroup Q) ≃* ↥(spinGroup (-Q))

The Spin groups of Q and -Q are isomorphic, through Mathlib's identification evenEquivEvenNeg of their even Clifford algebras. A product of two vectors ι Q a * ι Q b goes to -(ι (-Q) a * ι (-Q) b), and the vector actions agree.

@[simp]

theorem CliffordAlgebra.coe_spinGroupEquivNeg_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) : ↑((spinGroupEquivNeg Q) x) = ↑((evenEquivEvenNeg Q) ((spinGroupToEven Q) x))

The Clifford value of spinGroupEquivNeg Q x is the image of x under evenEquivEvenNeg.

@[simp]

theorem CliffordAlgebra.coe_spinGroupEquivNeg_symm_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (y : ↥(spinGroup (-Q))) : ↑((spinGroupEquivNeg Q).symm y) = ↑((evenEquivEvenNeg Q).symm ((spinGroupToEven (-Q)) y))

The Clifford value of the inverse isomorphism is given by the inverse of evenEquivEvenNeg.

@[simp]

theorem CliffordAlgebra.spinGroupToEven_spinGroupEquivNeg {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) : (spinGroupToEven (-Q)) ((spinGroupEquivNeg Q) x) = (evenEquivEvenNeg Q) ((spinGroupToEven Q) x)

On even parts, spinGroupEquivNeg is evenEquivEvenNeg.

theorem CliffordAlgebra.coe_spinGroupEquivNeg_apply_of_coe_eq_ι_mul_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {x : ↥(spinGroup Q)} {a b : M} (hx : ↑x = (ι Q) a * (ι Q) b) : ↑((spinGroupEquivNeg Q) x) = -((ι (-Q)) a * (ι (-Q)) b)

A Spin element that is a product of two vectors ι Q a * ι Q b goes to the negative of the corresponding product -(ι (-Q) a * ι (-Q) b).

@[simp]

theorem CliffordAlgebra.spinVectorAction_spinGroupEquivNeg {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] (x : ↥(spinGroup Q)) : spinVectorAction (-Q) ((spinGroupEquivNeg Q) x) = spinVectorAction Q x

The isomorphism spinGroupEquivNeg preserves the vector actions: the Spin elements of Q and of -Q that correspond act by the same linear automorphism of the common module.

@[simp]

theorem CliffordAlgebra.spinGroupEquivNeg_negOne {M : Type v} [AddCommGroup M] {K : Type u_1} [Field K] [Module K M] [Invertible 2] (Q : QuadraticForm K M) (hQ : Q ≠ 0) : (spinGroupEquivNeg Q) (spinGroup.negOne Q hQ) = spinGroup.negOne (-Q) ⋯

The isomorphism spinGroupEquivNeg sends the central element -1 to -1.

theorem CliffordAlgebra.equivNeg_spinGroupBaseChange {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) [Invertible 2] {A : Type u_1} [CommRing A] [Algebra R A] {u : A} (hu : u * u = -1) (x : ↥(spinGroup Q)) : (equivNeg (QuadraticForm.baseChange A Q) (QuadraticForm.baseChange A (-Q)) ⋯ hu) ↑((spinGroupBaseChange Q) x) = ↑((spinGroupBaseChange (-Q)) ((spinGroupEquivNeg Q) x))

After extension of scalars to an algebra A containing u with u * u = -1, the full-algebra isomorphism CliffordAlgebra.equivNeg of the extended Clifford algebras of Q and -Q, which sends ι m to u • ι m, restricts on scalar-extended Spin elements to the scalar extension of spinGroupEquivNeg. Over ℂ, this compares v ↦ i v with the real comparison of the Spin groups of Q and -Q; on a product of two vectors both carry the sign of coe_spinGroupEquivNeg_apply_of_coe_eq_ι_mul_ι.