The finite adelic spinor norm

For a nondegenerate rational quadratic space and compatible compact-open data U, the local spinor norms assemble into a continuous homomorphism on the finite adelic special orthogonal group. Its codomain is the restricted product of local square-class groups relative to the images of U.specialOrthogonal p under the local spinor norms. These reference subgroups are derived from U, rather than independently chosen: this ensures that every reference point maps into the reference subgroup at every prime.

The adelic spinor kernel consists exactly of the adelic proper isometries with trivial spinor norm at every prime. The finite adelic Spin projection lands in this kernel. In dimension at most one the spinor norm is trivial on the entire finite adelic special orthogonal group.

The construction uses restrictedProductMapOfForall and its continuity theorem, the local reference images from SpinorNormImage, and CliffordAlgebra.continuous_spinorNorm.

Main definitions and results

• OrthogonalCompactOpens.finiteAdelicSquareClasses: the square-class restricted product with the spinor-norm reference images.
• OrthogonalCompactOpens.adelicSpinorNorm and OrthogonalCompactOpens.adelicSpinorNorm_apply: the adelic spinor norm and its coordinate evaluation rule.
• OrthogonalCompactOpens.adelicSpinorKernel and OrthogonalCompactOpens.mem_adelicSpinorKernel_iff: the kernel and its local characterization.
• OrthogonalCompactOpens.finiteAdelicSpinToSpinorKernel: the adelic Spin projection with codomain restricted to the adelic spinor kernel.

References

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

@[reducible, inline]

abbrev TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSquareClasses {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : Type

The restricted product of local square-class groups relative to the spinor-norm images of the special orthogonal reference subgroups.

instance TauCeti.QuadraticMap.OrthogonalCompactOpens.factIsOpenLocalSpinorNormImage {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : Fact (∀ (p : Nat.Primes), IsOpen ↑(U.localSpinorNormImage hQ p))

The spinor-norm reference images are open, so their restricted product is a topological group for the restricted-product topology.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorNorm {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : U.finiteAdelicSpecialOrthogonal →* U.finiteAdelicSquareClasses hQ

The finite adelic spinor norm on the special orthogonal group, formed componentwise from the local spinor norms.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorNorm_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (g : U.finiteAdelicSpecialOrthogonal) (p : Nat.Primes) : ((U.adelicSpinorNorm hQ) g) p = (CliffordAlgebra.spinorNorm (QuadraticForm.baseChange ℚ_[↑p] Q) ⋯) (g p)

Each component of the adelic spinor norm is the corresponding local spinor norm.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_adelicSpinorNorm {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : Continuous ⇑(U.adelicSpinorNorm hQ)

The finite adelic spinor norm is continuous for the restricted-product topologies.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : Subgroup U.finiteAdelicSpecialOrthogonal

The kernel of the finite adelic spinor norm in the finite adelic special orthogonal group.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorKernel_def {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : U.adelicSpinorKernel hQ = (U.adelicSpinorNorm hQ).ker

The adelic spinor kernel is the kernel of the adelic spinor-norm homomorphism.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_adelicSpinorKernel_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (g : U.finiteAdelicSpecialOrthogonal) : g ∈ U.adelicSpinorKernel hQ ↔ ∀ (p : Nat.Primes), (CliffordAlgebra.spinorNorm (QuadraticForm.baseChange ℚ_[↑p] Q) ⋯) (g p) = 1

Membership in the adelic spinor kernel means that the spinor norm is trivial at every finite prime.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorNorm_finiteAdelicSpinToSpecialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (x : U.finiteAdelicSpin) : (U.adelicSpinorNorm hQ) (U.finiteAdelicSpinToSpecialOrthogonal x) = 1

The adelic Spin projection has trivial adelic spinor norm.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.finiteAdelicSpinToSpinorKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : U.finiteAdelicSpin →* ↥(U.adelicSpinorKernel hQ)

The finite adelic Spin projection with codomain restricted to the adelic spinor kernel.

@[simp]

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.coe_finiteAdelicSpinToSpinorKernel_apply {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (x : U.finiteAdelicSpin) : ↑((U.finiteAdelicSpinToSpinorKernel hQ) x) = U.finiteAdelicSpinToSpecialOrthogonal x

The corestricted adelic Spin projection agrees with the projection into adelic SO.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.continuous_finiteAdelicSpinToSpinorKernel {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : Continuous ⇑(U.finiteAdelicSpinToSpinorKernel hQ)

The adelic Spin projection remains continuous after restricting its codomain to the kernel.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.adelicSpinorNorm_eq_one_of_finrank_le_one {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (hV : Module.finrank ℚ V ≤ 1) : U.adelicSpinorNorm hQ = 1

In dimension zero or one the finite adelic special orthogonal spinor norm is trivial.