Rational orthogonal and Spin points are discrete in the full adeles

Let Q be a nondegenerate quadratic form on a finite-dimensional rational vector space V, and let U be any compatible compact-open reference data. Compactness and eventual membership of rational reflections imply that the reference subgroups are eventually integral in any rational basis. This file proves that the rational points O(V)(ℚ), SO(V)(ℚ) and Spin(V)(ℚ) form discrete subgroups of the full adelic groups O(V)(𝔸), SO(V)(𝔸) and Spin(V)(𝔸) built from U.

For O the argument is the classical one. In the neighbourhood of the identity consisting of the adelic isometries whose real component has matrix entries of absolute value less than 2 in b, and whose p-adic components are integral in b at every prime, a rational isometry has a matrix whose entries are p-adic integers at every prime, hence integers, and of absolute value less than 2. Only finitely many rational isometries qualify, so the identity is isolated in the diagonal image. The real factor is what bounds the size of these integer entries.

For SO the neighbourhood is pulled back along the injective inclusion SO → O, and for Spin along Spin → SO, whose rational fibres have at most two points for a nondegenerate form.

The same argument applies to degenerate forms for O and SO whenever eventual containment in an integral family is supplied explicitly.

In rank at most one, SO(V)(ℚ) is trivial even for a degenerate form, so its full adelic diagonal is discrete without either nondegeneracy or an eventual-integrality hypothesis. The corresponding O and Spin results below retain their nondegeneracy hypothesis.

Main results

• OrthogonalCompactOpens.discreteTopology_range_fullAdelicOrthogonalDiagonal, OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpecialOrthogonalDiagonal, OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal: the rational points are discrete in the full adelic groups.
• The O and SO criteria with suffix _of_eventually_integral also apply to degenerate forms.
• discreteTopology_range_fullAdelicSpecialOrthogonalDiagonal_of_finrank_le_one removes the nondegeneracy hypothesis for SO in rank at most one.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §101.
• V. Platonov, A. Rapinchuk, Algebraic Groups and Number Theory (1994), §5.1.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicOrthogonalDiagonal_of_eventually_integral {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {ι : Type u_2} [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℚ V} (hU : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[↑p] Q) (Module.Basis.baseChange ℚ_[↑p] b)) : DiscreteTopology ↥U.fullAdelicOrthogonalDiagonal.range

Rational isometries are discrete in the full adeles. If the orthogonal reference subgroups of U are, at almost every prime, integral in a rational basis b, then the diagonal image of O(V)(ℚ) is a discrete subgroup of O(V)(𝔸).

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpecialOrthogonalDiagonal_of_eventually_integral {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {ι : Type u_2} [Fintype ι] [DecidableEq ι] {b : Module.Basis ι ℚ V} (hU : ∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[↑p] Q) (Module.Basis.baseChange ℚ_[↑p] b)) : DiscreteTopology ↥U.fullAdelicSpecialOrthogonalDiagonal.range

Rational proper isometries are discrete in the full adeles. If the orthogonal reference subgroups of U are, at almost every prime, integral in a rational basis b, then the diagonal image of SO(V)(ℚ) is a discrete subgroup of SO(V)(𝔸).

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpecialOrthogonalDiagonal_of_finrank_le_one {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hV : Module.finrank ℚ V ≤ 1) : DiscreteTopology ↥U.fullAdelicSpecialOrthogonalDiagonal.range

Low-rank rational proper isometries are discrete in the full adeles. In rank at most one, the rational special orthogonal group is trivial, so neither nondegeneracy nor an integrality hypothesis on the compatible compact-open tuple is needed.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : DiscreteTopology ↥U.fullAdelicOrthogonalDiagonal.range

Rational isometries of a nondegenerate rational quadratic space form a discrete subgroup of the full adelic orthogonal group for every compatible compact-open reference family.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : DiscreteTopology ↥U.fullAdelicSpecialOrthogonalDiagonal.range

Rational proper isometries of a nondegenerate rational quadratic space form a discrete subgroup of the full adelic special orthogonal group for every compatible reference family.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.discreteTopology_range_fullAdelicSpinDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) : DiscreteTopology ↥U.fullAdelicSpinDiagonal.range

Rational Spin points of a nondegenerate rational quadratic space form a discrete subgroup of the full adelic Spin group for every compatible compact-open reference family.