Rational transvections accumulate in the finite adeles

For any compatible compact-open reference family, the factorial powers of a rational Eichler transvection tend to the identity in the finite adelic special orthogonal group. Uniform integrality is essential: all powers belong to the reference subgroups wherever the original transvection does. The sequence therefore lies in one principal restricted-product stage, where coordinatewise convergence implies convergence in the restricted-product topology.

If the transvection parameter is nonzero modulo the isotropic line and that line is not in the radical, none of these factorial powers is the identity. Consequently the rational diagonal in finite adelic SO is not discrete. Its image under the continuous injective inclusion SO → O shows that the rational orthogonal diagonal is also not discrete. This contrasts with the full adeles, where the real component prevents this sequence from converging to the identity.

References

• O. T. O'Meara, Introduction to Quadratic Forms (1963), §101.
• M. Eichler, Quadratische Formen und orthogonale Gruppen (1952).

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.tendsto_finiteAdelicSpecialOrthogonalDiagonal_transvection_factorial {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {u w : V} (hu : Q u = 0) (huw : QuadraticMap.polar (⇑Q) u w = 0) : Filter.Tendsto (fun (n : ℕ) => U.finiteAdelicSpecialOrthogonalDiagonal (⟨QuadraticMap.transvection Q hu huw, ⋯⟩ ^ n.factorial)) Filter.atTop (nhds 1)

Factorial powers of a rational Eichler transvection tend to the identity in finite adelic SO, for every compatible compact-open reference family.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal_of_transvection {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) {u w : V} (hu : Q u = 0) (huw : QuadraticMap.polar (⇑Q) u w = 0) (hu₀ : (QuadraticMap.polarBilin Q) u ≠ 0) (hw : w ∉ ℚ ∙ u) : ¬DiscreteTopology ↥U.finiteAdelicSpecialOrthogonalDiagonal.range

A nontrivial rational Eichler root subgroup prevents the rational diagonal in finite adelic SO from being discrete. The hypotheses ensure that the parameter is nonzero modulo ℚ ∙ u.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicSpecialOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (hdim : 3 ≤ Module.finrank ℚ V) (hiso : ∃ (u : V), u ≠ 0 ∧ Q u = 0) : ¬DiscreteTopology ↥U.finiteAdelicSpecialOrthogonalDiagonal.range

For a nondegenerate isotropic rational quadratic space of dimension at least three, the rational diagonal is not discrete in finite adelic SO. In dimension two the transvection parameter quotient is zero, so the dimension hypothesis is essential to this argument.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicOrthogonalDiagonal_of_specialOrthogonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hSO : ¬DiscreteTopology ↥U.finiteAdelicSpecialOrthogonalDiagonal.range) : ¬DiscreteTopology ↥U.finiteAdelicOrthogonalDiagonal.range

Non-discreteness of the rational diagonal in finite adelic SO implies non-discreteness of the rational diagonal in finite adelic O.

theorem TauCeti.QuadraticMap.OrthogonalCompactOpens.not_discreteTopology_range_finiteAdelicOrthogonalDiagonal {V : Type u_1} [AddCommGroup V] [Module ℚ V] [FiniteDimensional ℚ V] {Q : QuadraticForm ℚ V} (U : OrthogonalCompactOpens Q) (hQ : QuadraticMap.Nondegenerate) (hdim : 3 ≤ Module.finrank ℚ V) (hiso : ∃ (u : V), u ≠ 0 ∧ Q u = 0) : ¬DiscreteTopology ↥U.finiteAdelicOrthogonalDiagonal.range

For a nondegenerate isotropic rational quadratic space of dimension at least three, the rational diagonal is not discrete in finite adelic O.