The spinor norm

The Clifford norm of a Lipschitz element is a square on the kernel of its orthogonal action. It therefore descends to the orthogonal group modulo square classes. Restricting this homomorphism to the special orthogonal group gives the spinor norm, whose kernel is exactly the image of the Spin group.

Open TauCeti for the reflection-pair and surjectivity helpers below, and CliffordAlgebra for the spinor-norm homomorphisms they describe.

Main results

• CliffordAlgebra.orthogonalSpinorNorm: the square-class-valued spinor norm on O(Q).
• CliffordAlgebra.spinorNorm: its restriction to SO(Q).
• CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_isSquare_apply: when every invertible value of the form is a square, the orthogonal spinor norm is trivial.
• CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_isSquare_apply: the same square-value hypothesis makes the Spin action surjective.
• CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_square_eq_top: the Spin action is surjective when every unit of the field is a square.
• CliffordAlgebra.range_spinToSpecialOrthogonal_eq_ker_spinorNorm: the Spin image is the kernel of the spinor norm.
• CliffordAlgebra.spinToSpinorNormKernel: the Spin action corestricted to that kernel.
• CliffordAlgebra.spinToSpinorNormKernel_surjective: the corestricted action is surjective.
• TauCeti.QuadraticMap.spinorNorm_reflectionPairSpecialOrthogonal: the spinor norm of a reflection pair.
• TauCeti.QuadraticMap.orthogonalSpinorNorm_surjective_of_spinorNorm_surjective: surjectivity on SO(Q) implies surjectivity on O(Q).

References

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

theorem CliffordAlgebra.isSquare_cliffordNorm_of_mem_ker {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) (x : ↥(lipschitzGroup Q)) (hx : x ∈ (lipschitzToOrthogonal Q).ker) : IsSquare ((cliffordNorm Q) x)

The Clifford norm of an element acting trivially on the quadratic space is a square.

noncomputable def CliffordAlgebra.orthogonalSpinorNorm {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) : ↥(TauCeti.QuadraticMap.orthogonalGroup Q) →* Multiplicative (TauCeti.SquareClassGroup K)

The Clifford norm modulo squares, descended through the Lipschitz action to O(Q).

Equations

• CliffordAlgebra.orthogonalSpinorNorm Q hQ = ((CliffordAlgebra.lipschitzToOrthogonal Q).liftOfSurjective ⋯) (CliffordAlgebra.spinorNormDescentData✝ Q hQ)

@[simp]

theorem CliffordAlgebra.orthogonalSpinorNorm_lipschitzToOrthogonal {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) (x : ↥(lipschitzGroup Q)) : (orthogonalSpinorNorm Q hQ) ((lipschitzToOrthogonal Q) x) = TauCeti.squareClassHom ((cliffordNorm Q) x)

The descended spinor norm evaluates on a Lipschitz action through its Clifford norm.

@[simp]

theorem CliffordAlgebra.orthogonalSpinorNorm_reflectionOrthogonal {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) (TauCeti.QuadraticMap.reflectionOrthogonal Q v) = TauCeti.squareClassHom (unitOfInvertible (Q v))

The spinor norm of an orthogonal reflection is the square class of the norm of its defining vector.

theorem CliffordAlgebra.orthogonalSpinorNorm_eq_one_of_isSquare_apply {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) (hsq : ∀ (v : V) [Invertible (Q v)], IsSquare (Q v)) : orthogonalSpinorNorm Q hQ = 1

If every invertible value of a finite-dimensional nondegenerate quadratic form is a square, its orthogonal spinor norm is trivial.

noncomputable def CliffordAlgebra.spinorNorm {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) : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q) →* Multiplicative (TauCeti.SquareClassGroup K)

The spinor norm on SO(Q), obtained by restricting the orthogonal spinor norm.

Equations

• CliffordAlgebra.spinorNorm Q hQ = (CliffordAlgebra.orthogonalSpinorNorm Q hQ).comp (QuadraticMap.specialOrthogonalToOrthogonal Q)

@[simp]

theorem CliffordAlgebra.spinorNorm_apply {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) (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) : (spinorNorm Q hQ) g = (orthogonalSpinorNorm Q hQ) ((QuadraticMap.specialOrthogonalToOrthogonal Q) g)

The spinor norm is the restriction of the orthogonal spinor norm to SO(Q).

@[simp]

theorem CliffordAlgebra.spinorNorm_spinToSpecialOrthogonal {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) (x : ↥(spinGroup Q)) : (spinorNorm Q hQ) ((spinToSpecialOrthogonal Q) x) = 1

The Spin action has trivial spinor norm.

theorem CliffordAlgebra.range_spinToSpecialOrthogonal_eq_ker_spinorNorm {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) : (spinToSpecialOrthogonal Q).range = (spinorNorm Q hQ).ker

The image of the Spin action on SO(Q) is exactly the kernel of the spinor norm.

noncomputable def CliffordAlgebra.spinToSpinorNormKernel {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) : ↥(spinGroup Q) →* ↥(spinorNorm Q hQ).ker

The Spin action with codomain restricted to the kernel of the spinor norm.

Equations

• CliffordAlgebra.spinToSpinorNormKernel Q hQ = (CliffordAlgebra.spinToSpecialOrthogonal Q).codRestrict (CliffordAlgebra.spinorNorm Q hQ).ker ⋯

@[simp]

theorem CliffordAlgebra.coe_spinToSpinorNormKernel_apply {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) (x : ↥(spinGroup Q)) : ↑((spinToSpinorNormKernel Q hQ) x) = (spinToSpecialOrthogonal Q) x

After inclusion into the special orthogonal group, spinToSpinorNormKernel is the usual Spin action.

@[simp]

theorem CliffordAlgebra.ker_spinToSpinorNormKernel {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) : (spinToSpinorNormKernel Q hQ).ker = (spinToSpecialOrthogonal Q).ker

Corestricting the Spin action to the spinor-norm kernel does not change its kernel.

theorem CliffordAlgebra.spinToSpinorNormKernel_surjective {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) : Function.Surjective ⇑(spinToSpinorNormKernel Q hQ)

The Spin action is surjective onto the kernel of the spinor norm.

theorem CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_isSquare_apply {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) (hsq : ∀ (v : V) [Invertible (Q v)], IsSquare (Q v)) : Function.Surjective ⇑(spinToSpecialOrthogonal Q)

If every invertible value of a finite-dimensional nondegenerate quadratic form is a square, the Spin action on its special orthogonal group is surjective. This differs from spinToSpecialOrthogonal_surjective_of_isSquare, which assumes that -⅟(Q v) is a square.

theorem CliffordAlgebra.spinToSpecialOrthogonal_surjective_of_square_eq_top {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) (hsquare : Subgroup.square Kˣ = ⊤) : Function.Surjective ⇑(spinToSpecialOrthogonal Q)

If every unit of the field is a square, the Spin action on the special orthogonal group of a finite-dimensional nondegenerate quadratic space is surjective.

theorem TauCeti.QuadraticMap.spinorNorm_reflectionPairSpecialOrthogonal {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 w : V) [Invertible (Q v)] [Invertible (Q w)] : (CliffordAlgebra.spinorNorm Q hQ) (QuadraticMap.reflectionPairSpecialOrthogonal Q v w) = squareClassHom (unitOfInvertible (Q v) * unitOfInvertible (Q w))

The spinor norm of a pair of reflections is the square class of the product of the quadratic values of its defining vectors.

After open TauCeti, use Q.spinorNorm_reflectionPairSpecialOrthogonal hQ v w to evaluate the pair defined by v and w.

theorem TauCeti.QuadraticMap.orthogonalSpinorNorm_surjective_of_spinorNorm_surjective {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) (hsurj : Function.Surjective ⇑(CliffordAlgebra.spinorNorm Q hQ)) : Function.Surjective ⇑(CliffordAlgebra.orthogonalSpinorNorm Q hQ)

Surjectivity of the spinor norm on the special orthogonal group implies its surjectivity on the full orthogonal group.

After open TauCeti, apply Q.orthogonalSpinorNorm_surjective_of_spinorNorm_surjective hQ hsurj to a surjectivity proof hsurj for the spinor norm on SO(Q).