Compact orthogonal subgroups containing coordinate reflections

At an odd prime, a compact orthogonal subgroup containing the reflections in an orthogonal basis of unit quadratic values is integral in that basis. Compactness bounds the orbits of the basis vectors. Coordinate reflections extract each coordinate without enlarging these bounds; applying the same estimate to the inverse and using the weighted transpose identity forces every matrix entry to have norm at most one.

This criterion permits integrality of compact reference subgroups to be deduced from membership of finitely many reflections, rather than imposed as an additional hypothesis.

References

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

theorem QuadraticMap.le_integralOrthogonalSubgroup_of_isCompact_of_reflection_mem {p : ℕ} [Fact (Nat.Prime p)] {V : Type u_1} {ι : Type u_2} [AddCommGroup V] [Module ℚ_[p] V] [Fintype ι] [DecidableEq ι] (Q : QuadraticForm ℚ_[p] V) (b : Module.Basis ι ℚ_[p] V) (hp : p ≠ 2) (hb : ∀ (i j : ι), i ≠ j → IsOrtho Q (b i) (b j)) (hunit : ∀ (i : ι), ‖Q (b i)‖ = 1) (H : Subgroup ↥(TauCeti.QuadraticMap.orthogonalGroup Q)) (hH : IsCompact ↑H) (hrefl : ∀ (i : ι) (hi : Invertible (Q (b i))), TauCeti.QuadraticMap.reflectionOrthogonal Q (b i) ∈ H) : H ≤ TauCeti.QuadraticMap.integralOrthogonalSubgroup Q b

At an odd prime, a compact orthogonal subgroup containing all coordinate reflections of an orthogonal basis of unit quadratic values is contained in its integral orthogonal subgroup.