The range of the spinor norm

On a finite-dimensional nondegenerate quadratic space in characteristic different from two, the special orthogonal group is generated by products of two reflections, and the reflection pair τ_v τ_w has spinor norm [Q v · Q w]. Hence the image of the spinor norm on SO(Q) is the subgroup of square classes generated by the products of two nonzero values of Q. This reduces the special orthogonal column of a spinor-norm calculation to the value set of the form.

On a nonzero space the special orthogonal group has index two in the orthogonal group. Consequently the orthogonal spinor-norm image is generated by the special orthogonal image and the class of any anisotropic reflection. This reduces the orthogonal column of a local spinor-norm calculation to the special orthogonal column and one value of the quadratic form.

Main results

• CliffordAlgebra.range_spinorNorm_eq_closure: the image of the spinor norm on SO(Q) is generated by the square classes of products of two represented units.
• CliffordAlgebra.spinorNorm_range_orthogonal_eq_sup: the image on O(Q) is the image on SO(Q) joined with the class of one anisotropic value.

References

O. T. O'Meara, Introduction to Quadratic Forms, §55.

theorem CliffordAlgebra.range_spinorNorm_eq_closure {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : (spinorNorm Q hQ).range = Subgroup.closure (⇑TauCeti.squareClassHom '' (QuadraticMap.unitValueSet Q * QuadraticMap.unitValueSet Q))

The image of the spinor norm on SO(Q) is generated by the square classes of the products Q v · Q w of two represented units.

theorem CliffordAlgebra.spinorNorm_range_orthogonal_eq_sup {K : Type u} {V : Type v} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (v : V) [Invertible (Q v)] : (orthogonalSpinorNorm Q hQ).range = (spinorNorm Q hQ).range ⊔ Subgroup.zpowers (TauCeti.squareClassHom (unitOfInvertible (Q v)))

The image of the spinor norm on O(Q) is generated by its image on SO(Q) and the square class of the norm of any anisotropic vector.