Spinor norms in dimension one

For a nondegenerate one-dimensional quadratic space, the special orthogonal group has trivial spinor norm. The image on the full orthogonal group is generated by the square class of any nonzero value of the form. In particular, for the form a * x ^ 2 with a ≠ 0, that image is generated by [a]; it is trivial exactly when a is a square.

The orthogonal group of such a space is {1, -1}, and -1 is the reflection in every nonzero vector, so the spinor norm of -1 is that same class: [a] for Q x = a x² (CliffordAlgebra.orthogonalSpinorNorm_negOrthogonal_smul_sq). The scalar a matters: for Q x = x² the class is trivial, while for a a nonsquare the spinor norm of -1 is nontrivial (CliffordAlgebra.orthogonalSpinorNorm_negOrthogonal_smul_sq_eq_one_iff).

References

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

@[simp]

theorem CliffordAlgebra.spinorNorm_eq_one_of_finrank_le_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V ≤ 1) : spinorNorm Q hQ = 1

In dimension at most one, the spinor norm on the special orthogonal group is trivial.

theorem CliffordAlgebra.orthogonalSpinorNorm_range_eq_zpowers_of_finrank_eq_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) (v : V) [Invertible (Q v)] : (orthogonalSpinorNorm Q hQ).range = Subgroup.zpowers (TauCeti.squareClassHom (unitOfInvertible (Q v)))

In dimension one, the orthogonal spinor-norm image is the cyclic subgroup generated by any invertible value of the form.

theorem CliffordAlgebra.orthogonalSpinorNorm_eq_one_iff_isSquare_apply_of_finrank_eq_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) (v : V) [Invertible (Q v)] : orthogonalSpinorNorm Q hQ = 1 ↔ IsSquare (Q v)

The orthogonal spinor norm in dimension one is trivial exactly when any chosen nonzero value of the quadratic form is a square.

theorem CliffordAlgebra.orthogonalSpinorNorm_negOrthogonal_of_finrank_eq_one {K : Type u_1} {V : Type u_2} [Field K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank K V = 1) (v : V) [Invertible (Q v)] : (orthogonalSpinorNorm Q hQ) (QuadraticMap.negOrthogonal Q) = TauCeti.squareClassHom (unitOfInvertible (Q v))

In dimension one, -1 is the reflection in any anisotropic vector v, so its spinor norm is the square class of Q v.

theorem CliffordAlgebra.orthogonalSpinorNorm_negOrthogonal_smul_sq {K : Type u_1} [Field K] [Invertible 2] (a : Kˣ) : (orthogonalSpinorNorm (↑a • QuadraticMap.sq) ⋯) (QuadraticMap.negOrthogonal (↑a • QuadraticMap.sq)) = TauCeti.squareClassHom a

For the form Q x = a x² on K, the spinor norm of -1 is the square class of a.

theorem CliffordAlgebra.orthogonalSpinorNorm_negOrthogonal_smul_sq_eq_one_iff {K : Type u_1} [Field K] [Invertible 2] (a : Kˣ) : (orthogonalSpinorNorm (↑a • QuadraticMap.sq) ⋯) (QuadraticMap.negOrthogonal (↑a • QuadraticMap.sq)) = 1 ↔ IsSquare ↑a

For the form Q x = a x² on K, the spinor norm of -1 is trivial exactly when a is a square. With a a nonsquare, this is the dimension-one check that the spinor norm detects -1.