Closed Spin carriers

For a nondegenerate quadratic form on a finite-dimensional space over a Hausdorff topological field in which 2 is invertible, Mathlib's Spin group is closed in the Clifford algebra with its module topology. In positive dimension the Spin group is the set of even unitary elements whose twisted conjugation preserves the vectors, each of which is a closed condition: the unitary group is closed, the even part and the space of vectors are finite-dimensional subspaces, and twisted conjugation is continuous. On the zero space the Spin group is trivial. Over a locally compact field the Spin group is therefore a locally compact Hausdorff topological group, the Spin point group over ℝ and ℚ_p.

This module also proves that every nondegenerate Spin carrier is closed in the units of its Clifford algebra, providing the closed-subgroup input for Lie-group structures. The corresponding real special-orthogonal carrier is provided separately in RealSpecialOrthogonal.lean.

References

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

Main results

• CliffordAlgebra.isClosed_spinGroup: the Spin group of a nondegenerate form is closed in the Clifford algebra.
• CliffordAlgebra.locallyCompactSpace_spinGroup: over a locally compact field it is locally compact.
• CliffordAlgebra.isClosed_range_spinGroup_toUnits: the range of the Spin group in the Clifford-algebra units is closed.

theorem CliffordAlgebra.isClosed_spinGroup {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : IsClosed ↑(spinGroup Q)

The Spin group of a nondegenerate quadratic form on a finite-dimensional space over a Hausdorff topological field in which 2 is invertible is closed in the Clifford algebra with its module topology.

theorem CliffordAlgebra.locallyCompactSpace_spinGroup {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) [LocallyCompactSpace K] (hQ : QuadraticMap.Nondegenerate) : LocallyCompactSpace ↥(spinGroup Q)

The Spin group of a nondegenerate quadratic form on a finite-dimensional space over a Hausdorff locally compact topological field in which 2 is invertible is locally compact, being closed in the locally compact Clifford algebra.

theorem CliffordAlgebra.isClosed_range_spinGroup_toUnits {K : Type u_1} {V : Type u_2} [Field K] [TopologicalSpace K] [IsTopologicalRing K] [T2Space K] [Invertible 2] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : IsClosed (Set.range ⇑spinGroup.toUnits)

The range of the Spin group of a nondegenerate quadratic form in the units of its Clifford algebra is closed.