Spinor norms under extension of scalars

Let L / K be a field extension and Q a nondegenerate quadratic form on a finite-dimensional K-vector space V. Extending scalars carries an orthogonal automorphism g of Q to an orthogonal automorphism g_L of Q.baseChange L. This file proves that the spinor norm of g_L is the image of the spinor norm of g under the pushforward of square classes Kˣ/(Kˣ)² → Lˣ/(Lˣ)².

Extending scalars carries the reflection in v to the reflection in 1 ⊗ₜ v, whose norm is the image of Q v. Since reflections generate the orthogonal group, the two homomorphisms agree everywhere. Restricting to determinant one gives the same compatibility for the spinor norm on the special orthogonal group. Applied to the completions of a number field, this compares a global spinor norm with its local ones.

Main results

• CliffordAlgebra.orthogonalSpinorNorm_comp_orthogonalGroupBaseChange: the spinor norm after extension of scalars is the pushforward of the spinor norm, as an equality of homomorphisms.
• CliffordAlgebra.orthogonalSpinorNorm_orthogonalGroupBaseChange: its pointwise form.
• CliffordAlgebra.spinorNorm_specialOrthogonalGroupBaseChange: the same on SO(Q).
• CliffordAlgebra.spinorNormKernelBaseChange: scalar extension restricted to the kernel of the spinor norm.
• CliffordAlgebra.spinorNormKernelBaseChange_spinToSpinorNormKernel: scalar extension commutes with the Spin map to the spinor-norm kernel.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §55.

theorem CliffordAlgebra.orthogonalSpinorNorm_comp_orthogonalGroupBaseChange {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : (orthogonalSpinorNorm (QuadraticForm.baseChange L Q) ⋯).comp (TauCeti.QuadraticMap.orthogonalGroupBaseChange Q) = (algebraMap K L).multiplicativeSquareClassMap.comp (orthogonalSpinorNorm Q hQ)

Extending scalars from K to L intertwines the spinor norms of Q and of Q.baseChange L with the pushforward of square classes along K → L.

@[simp]

theorem CliffordAlgebra.orthogonalSpinorNorm_orthogonalGroupBaseChange {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (g : ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) : (orthogonalSpinorNorm (QuadraticForm.baseChange L Q) ⋯) ((TauCeti.QuadraticMap.orthogonalGroupBaseChange Q) g) = (algebraMap K L).multiplicativeSquareClassMap ((orthogonalSpinorNorm Q hQ) g)

The spinor norm of an orthogonal automorphism after extending scalars from K to L is the image of its spinor norm under the pushforward of square classes.

theorem CliffordAlgebra.spinorNorm_specialOrthogonalGroupBaseChange {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (g : ↥(TauCeti.QuadraticMap.specialOrthogonalGroup Q)) : (spinorNorm (QuadraticForm.baseChange L Q) ⋯) ((TauCeti.QuadraticMap.specialOrthogonalGroupBaseChange Q) g) = (algebraMap K L).multiplicativeSquareClassMap ((spinorNorm Q hQ) g)

The spinor norm of a special orthogonal automorphism after extending scalars from K to L is the image of its spinor norm under the pushforward of square classes.

The spinor-norm kernel

noncomputable def CliffordAlgebra.spinorNormKernelBaseChange {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : ↥(spinorNorm Q hQ).ker →* ↥(spinorNorm (QuadraticForm.baseChange L Q) ⋯).ker

Scalar extension carries the spinor-norm kernel into the spinor-norm kernel of the extended quadratic form.

@[simp]

theorem CliffordAlgebra.coe_spinorNormKernelBaseChange_apply {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (g : ↥(spinorNorm Q hQ).ker) : ↑((spinorNormKernelBaseChange Q hQ) g) = (TauCeti.QuadraticMap.specialOrthogonalGroupBaseChange Q) ↑g

The underlying special-orthogonal element of a base-changed spinor-kernel element is obtained by the usual special-orthogonal base-change map.

theorem CliffordAlgebra.spinorNormKernelBaseChange_injective {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) : Function.Injective ⇑(spinorNormKernelBaseChange Q hQ)

Scalar extension is injective on the spinor-norm kernel.

@[simp]

theorem CliffordAlgebra.spinorNormKernelBaseChange_spinToSpinorNormKernel {K : Type u} {L : Type w} {V : Type v} [Field K] [Field L] [Algebra K L] [AddCommGroup V] [Module K V] [FiniteDimensional K V] [Invertible 2] (Q : QuadraticForm K V) (hQ : QuadraticMap.Nondegenerate) (x : ↥(spinGroup Q)) : (spinorNormKernelBaseChange Q hQ) ((spinToSpinorNormKernel Q hQ) x) = (spinToSpinorNormKernel (QuadraticForm.baseChange L Q) ⋯) ((spinGroupBaseChange Q) x)

Scalar extension commutes with the canonical Spin homomorphism to the spinor-norm kernel.