Compactness of the orthogonal group over a local field

Let Q be a quadratic form on a finite-dimensional space V over a locally compact nontrivially normed field K, such as ℝ or ℚ_p. The orthogonal group O(Q), with the canonical topology of the linear automorphism group V ≃ₗ[K] V, is compact exactly when Q is anisotropic. No nondegeneracy assumption is needed.

For an isotropic form, O(Q) is not compact over any nontrivially normed field, without local compactness or finite-dimensionality. More generally, any set of automorphisms containing the split torus of a hyperbolic pair at every square parameter is not compact; this also applies to the image of the Spin group. None of these results requires a condition on 2.

Main results

• TauCeti.QuadraticMap.not_isCompact_of_hyperbolicPairTorus_sq_mem: a set of automorphisms containing the split torus at every square parameter is not compact.
• TauCeti.QuadraticMap.isCompact_orthogonalGroup: the orthogonal group of an anisotropic form is compact.
• TauCeti.QuadraticMap.not_isCompact_orthogonalGroup: the orthogonal group of an isotropic form is not compact.
• TauCeti.QuadraticMap.isCompact_orthogonalGroup_iff: the orthogonal group is compact exactly when the form is anisotropic.

theorem TauCeti.QuadraticMap.not_isCompact_of_hyperbolicPairTorus_sq_mem {K : Type u_1} {V : Type u_2} [NontriviallyNormedField K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) {u v : V} (hu : Q u = 0) (hv : Q v = 0) (huv : QuadraticMap.polar (⇑Q) u v = 1) {S : Set (V ≃ₗ[K] V)} (hS : ∀ (t : Kˣ), ↑((hyperbolicPairTorus Q hu hv huv) (t ^ 2)) ∈ S) : ¬IsCompact S

A set of linear automorphisms containing the split torus of a hyperbolic pair at every square parameter is not compact. The square parameters suffice for applications to the image of the Spin group. No local compactness or finite-dimensionality is required.

theorem TauCeti.QuadraticMap.not_isCompact_orthogonalGroup {K : Type u_1} {V : Type u_2} [NontriviallyNormedField K] [AddCommGroup V] [Module K V] (Q : QuadraticForm K V) (hiso : ¬QuadraticMap.Anisotropic Q) : ¬IsCompact ↑(orthogonalGroup Q)

The orthogonal group of an isotropic quadratic form over a nontrivially normed field is not compact. No nondegeneracy or finite-dimensionality is required.

theorem TauCeti.QuadraticMap.isCompact_orthogonalGroup {K : Type u_1} {V : Type u_2} [NontriviallyNormedField K] [WeaklyLocallyCompactSpace K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) (hQ : QuadraticMap.Anisotropic Q) : IsCompact ↑(orthogonalGroup Q)

The orthogonal group of an anisotropic form is compact. For an anisotropic quadratic form on a finite-dimensional space over a locally compact nontrivially normed field, the orthogonal group is a compact subset of the linear automorphism group.

theorem TauCeti.QuadraticMap.isCompact_orthogonalGroup_iff {K : Type u_1} {V : Type u_2} [NontriviallyNormedField K] [WeaklyLocallyCompactSpace K] [AddCommGroup V] [Module K V] [FiniteDimensional K V] (Q : QuadraticForm K V) : IsCompact ↑(orthogonalGroup Q) ↔ QuadraticMap.Anisotropic Q

The orthogonal group of a quadratic form on a finite-dimensional space over a locally compact nontrivially normed field is compact exactly when the form is anisotropic.