Compactness of compact real Spin groups

Every element of a positive-dimensional compact real Spin group is a product of uniformly many normalized reflection-pair lifts. The normalized vectors range over a Euclidean unit sphere, so a fixed finite product of pairs of spheres maps continuously and surjectively onto the Spin group. In dimension zero the group is trivial, and therefore compact.

The uniform bound comes from the bounded Cartan--Dieudonne factorization. Its reflection word has even length over the special orthogonal group, hence can be grouped into pairs. One additional pair accounts for the possible scalar -1 in the kernel of the Spin projection. Repeated equal vectors pad the product without changing it.

Main result

• CliffordAlgebra.instCompactSpaceRealCliffordSpinGroupZero proves that Spin(n) is compact in every dimension.

References

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

instance CliffordAlgebra.instCompactSpaceRealCliffordSpinGroupZero (n : ℕ) : CompactSpace ↥(realCliffordSpinGroupZero n)

The compact real Spin group is compact in every dimension.