The vector representation of the Lipschitz group is open

For a nondegenerate quadratic form on a finite-dimensional space over a Hausdorff topological field in which 2 is invertible, Mathlib's Lipschitz group is closed in the units of the Clifford algebra. When V is nontrivial it is the classical Clifford group of units whose twisted conjugation preserves the vectors, and each of these conditions is closed; when V is trivial it is the trivial subgroup (although then every unit preserves the zero vector space), which is closed as a point. Over a locally compact σ-compact field, such as ℝ or ℚ_p, the Lipschitz group is therefore σ-compact, while the orthogonal group is locally compact and Hausdorff. The open mapping theorem for topological groups then shows that the surjective continuous vector representation lipschitzToOrthogonal is an open map.

Openness is what lets a property of Lipschitz elements that is open in the Clifford algebra descend to an open subset of the orthogonal group; the spinor kernel is the main example.

Main results

• CliffordAlgebra.isClosed_lipschitzGroup: the Lipschitz group is closed in the units of the Clifford algebra.
• CliffordAlgebra.sigmaCompactSpace_lipschitzGroup: over a σ-compact field it is σ-compact.
• CliffordAlgebra.isOpenMap_lipschitzToOrthogonal: over a locally compact σ-compact field the vector representation onto the orthogonal group is an open map.

References

• C. Chevalley, The Algebraic Theory of Spinors, Chapter II.

theorem CliffordAlgebra.isClosed_lipschitzGroup {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 ↑(lipschitzGroup Q)

The Lipschitz 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 units of the Clifford algebra with its module topology.

theorem CliffordAlgebra.sigmaCompactSpace_lipschitzGroup {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) [SigmaCompactSpace K] (hQ : QuadraticMap.Nondegenerate) : SigmaCompactSpace ↥(lipschitzGroup Q)

Over a Hausdorff σ-compact topological field in which 2 is invertible, the Lipschitz group of a nondegenerate quadratic form on a finite-dimensional space is σ-compact, being closed in the units of the σ-compact Clifford algebra.

theorem CliffordAlgebra.isOpenMap_lipschitzToOrthogonal {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] [SigmaCompactSpace K] (hQ : QuadraticMap.Nondegenerate) : IsOpenMap ⇑(lipschitzToOrthogonal Q)

The vector representation is open. For a nondegenerate quadratic form on a finite-dimensional space over a Hausdorff, locally compact and σ-compact topological field in which 2 is invertible, the twisted-conjugation homomorphism from the Lipschitz group onto the orthogonal group is an open map for the canonical subgroup topologies.