Eventual integrality of compatible orthogonal reference families #
For a nondegenerate rational quadratic space, any compatible compact-open reference family is contained in the integral family of a rational basis at almost every prime. The family contains the finitely many coordinate reflections of a rational orthogonal basis at almost every prime. Outside the prime two and the primes at which a basis value is not a unit, compactness then forces integrality. Changing rational basis changes the integral subgroup at only finitely many primes.
This supplies the integrality bound used to isolate rational diagonal points in the full adeles.
References #
- O. T. O'Meara, Introduction to Quadratic Forms (1963), §43 and §101.
theorem
TauCeti.QuadraticMap.OrthogonalCompactOpens.eventually_orthogonal_le_integralOrthogonalSubgroup
{V : Type u_1}
[AddCommGroup V]
[Module ℚ V]
[FiniteDimensional ℚ V]
{Q : QuadraticForm ℚ V}
(U : OrthogonalCompactOpens Q)
(hQ : QuadraticMap.Nondegenerate)
{ι : Type u_2}
[Fintype ι]
[DecidableEq ι]
(b : Module.Basis ι ℚ V)
:
∀ᶠ (p : Nat.Primes) in Filter.cofinite, U.orthogonal p ≤ integralOrthogonalSubgroup (QuadraticForm.baseChange ℚ_[↑p] Q) (Module.Basis.baseChange ℚ_[↑p] b)
Every compatible compact-open orthogonal reference family for a nondegenerate rational form is eventually contained in the integral orthogonal family of any rational basis.