Spinor-norm images of compact-open subgroups

For compatible compact-open reference subgroups of the local orthogonal and Spin groups, the reference subgroup in the square-class group is the image of the derived special orthogonal subgroup under the local spinor norm. This file packages that restricted homomorphism and its range, and proves that the range is open. The latter follows from the local-field theorem that the squares form an open subgroup of the units, hence the square-class quotient is discrete.

In dimension at most one the local special orthogonal spinor norm is trivial, so every reference image is trivial. Thus openness alone does not identify the reference image with any particular nontrivial subgroup of local square classes.

Isometric transport of a local special orthogonal reference subgroup preserves its spinor-norm image, allowing these reference families to be compared across quadratic coordinates.

Main definitions

• TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNorm: the spinor norm restricted to the derived local special orthogonal reference subgroup.
• TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNormImage: its range in the local square-class group.

References

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

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNorm {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (p : Nat.Primes) : ↥(U.specialOrthogonal p) →* ℚ_[↑p]ˣ ⧸ Subgroup.square ℚ_[↑p]ˣ

The local spinor norm restricted to the derived special orthogonal reference subgroup.

@[simp]

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

The restricted local spinor norm agrees with the ambient spinor norm.

noncomputable def TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNormImage {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (p : Nat.Primes) : Subgroup (ℚ_[↑p]ˣ ⧸ Subgroup.square ℚ_[↑p]ˣ)

The reference subgroup in the local square-class group is the image of the derived special orthogonal reference subgroup under the spinor norm.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.mem_localSpinorNormImage_iff {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (p : Nat.Primes) (x : ℚ_[↑p]ˣ ⧸ Subgroup.square ℚ_[↑p]ˣ) : x ∈ U.localSpinorNormImage hQ p ↔ ∃ (g : ↥(U.specialOrthogonal p)), (CliffordAlgebra.spinorNorm (QuadraticForm.baseChange ℚ_[↑p] Q) ⋯) ↑g = x

Membership in the local spinor-norm image is witnessed by a point of the derived special orthogonal reference subgroup.

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

The local spinor-norm reference image is open in the square-class group.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNormImage_eq_bot_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) (p : Nat.Primes) : U.localSpinorNormImage hQ p = ⊥

In dimension at most one every local spinor-norm reference image is trivial.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.localSpinorNormImage_eq_of_isometry {V : Type u_1} {W : Type u_2} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] [AddCommGroup W] [Module ℚ W] [FiniteDimensional ℚ W] {Q : QuadraticForm ℚ V} {Q' : QuadraticForm ℚ W} (U : OrthogonalCompactOpens Q) (U' : OrthogonalCompactOpens Q') (hQ : QuadraticMap.Nondegenerate) (p : Nat.Primes) (e : QuadraticMap.IsometryEquiv (QuadraticForm.baseChange ℚ_[↑p] Q) (QuadraticForm.baseChange ℚ_[↑p] Q')) (he : Set.BijOn ⇑e.specialOrthogonalGroupCongr ↑(U.specialOrthogonal p) ↑(U'.specialOrthogonal p)) : U.localSpinorNormImage hQ p = U'.localSpinorNormImage ⋯ p

Isometric transport of a local special orthogonal reference subgroup preserves its spinor-norm image.