Compact real Spin groups

For a positive-definite real quadratic form, every norm is a square. The spinor norm on the orthogonal group is therefore trivial, so the Spin action is surjective.

This file applies that argument to the positive-definite signature form realCliffordForm n 0 and packages its Spin double cover. Topology, connectedness, and the universal-cover theorem remain separate.

Main definitions and results

• CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef shows that the orthogonal spinor norm is trivial for a positive-definite real form.
• CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_posDef proves surjectivity for any finite-dimensional positive-definite real form.
• QuadraticMap.IsometryEquiv.exists_spinVectorAction_eq_iff_det_eq_one: two isometry equivalences into such a form differ by the vector action of a Spin element exactly when the transition between them has determinant one.
• CliffordAlgebra.realCliffordSpinGroup names the real Spin groups by signature.
• CliffordAlgebra.realCliffordSpinGroupZero names the compact real Spin group.
• CliffordAlgebra.realCliffordSpinDoubleCoverZero packages its double cover in positive dimension.
• CliffordAlgebra.card_fiber_realCliffordSpinDoubleCoverZero_rightHom proves that every fiber of the double cover contains exactly two points.
• CliffordAlgebra.finite_realCliffordSpinGroupZero_one shows that Spin(1) = {1, -1} is finite.

References

See H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I §2.

theorem CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_posDef {V : Type u} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticForm ℝ V) (hQ : QuadraticMap.PosDef Q) : orthogonalSpinorNorm Q ⋯ = 1

On a finite-dimensional positive-definite real quadratic space, the orthogonal spinor norm is trivial.

theorem CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_posDef {V : Type u} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] (Q : QuadraticForm ℝ V) (hQ : QuadraticMap.PosDef Q) : Function.Surjective ⇑(spinToSpecialOrthogonal Q)

The Spin action of a finite-dimensional positive-definite real quadratic space is onto its special orthogonal group.

theorem QuadraticMap.IsometryEquiv.exists_spinVectorAction_eq_iff_det_eq_one {V : Type u} [AddCommGroup V] [Module ℝ V] [FiniteDimensional ℝ V] {M : Type u_1} [AddCommGroup M] [Module ℝ M] {P : QuadraticForm ℝ M} {Q : QuadraticForm ℝ V} (hQ : PosDef Q) (e e' : IsometryEquiv P Q) : (∃ (s : ↥(spinGroup Q)), ∀ (m : M), (CliffordAlgebra.spinVectorAction Q s) (e m) = e' m) ↔ LinearEquiv.det (e.symm.trans e').toLinearEquiv = 1

Two isometry equivalences e and e' into a finite-dimensional positive-definite real form Q differ by the vector action of a Spin element exactly when the transition e.symm.trans e' has determinant one.

@[reducible, inline]

abbrev CliffordAlgebra.realCliffordSpinGroup (p q : ℕ) : Submonoid (CliffordAlgebra (TauCeti.realCliffordForm p q))

The real Spin group of signature (p, q).

@[reducible, inline]

abbrev CliffordAlgebra.realCliffordSpinGroupZero (n : ℕ) : Submonoid (CliffordAlgebra (TauCeti.realCliffordForm n 0))

The compact real Spin group Spin(n).

noncomputable def CliffordAlgebra.realCliffordSpinDoubleCoverZero (n : ℕ) [NeZero n] : GroupExtension (Multiplicative (ZMod 2)) ↥(realCliffordSpinGroupZero n) ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (TauCeti.realCliffordForm n 0))

The algebraic double cover from Spin(n) to the special orthogonal group in positive dimension.

@[simp]

theorem CliffordAlgebra.realCliffordSpinDoubleCoverZero_inl_ofAdd_one (n : ℕ) [NeZero n] : (realCliffordSpinDoubleCoverZero n).inl (Multiplicative.ofAdd 1) = spinGroup.negOne (TauCeti.realCliffordForm n 0) ⋯

The inclusion in the compact real Spin double cover sends the generator to the distinguished element -1 of the Spin group.

@[simp]

theorem CliffordAlgebra.realCliffordSpinDoubleCoverZero_rightHom (n : ℕ) [NeZero n] : (realCliffordSpinDoubleCoverZero n).rightHom = spinToSpecialOrthogonal (TauCeti.realCliffordForm n 0)

The projection in the compact real Spin double cover is the Spin action.

theorem CliffordAlgebra.card_fiber_realCliffordSpinDoubleCoverZero_rightHom (n : ℕ) [NeZero n] (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup (TauCeti.realCliffordForm n 0))) : Nat.card ↑(⇑(realCliffordSpinDoubleCoverZero n).rightHom ⁻¹' {g}) = 2

Every fiber of the compact real Spin double cover has exactly two elements.

instance CliffordAlgebra.finite_realCliffordSpinGroupZero_one : Finite ↥(realCliffordSpinGroupZero 1)

The compact Spin group Spin(1) = {1, -1} is finite.